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_50_pb.cnf.cr.opb
MD5SUM2cb05b3a6451c60276a625949666f14e
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 51
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.133979
Number of variables4000
Total number of constraints180
Number of constraints which are clauses100
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 constraint50

Trace number 823

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        940816 kB
Buffers:         34528 kB
Cached:          24808 kB
SwapCached:        844 kB
Active:          53544 kB
Inactive:         8372 kB
HighTotal:      131008 kB
HighFree:       103292 kB
LowTotal:       903652 kB
LowFree:        837524 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            26328 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:48:22 (client local time) WITH STATUS 0 IN 1208.37 SECONDS
stats: 2360 7 1208.37 0

Solver Data

c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................
c ---[  79]---> BDD-cost:   97
c ---[  78]---> BDD-cost:   97
c ---[  77]---> BDD-cost:   97
c ---[  76]---> BDD-cost:   97
c ---[  75]---> BDD-cost:   97
c ---[  74]---> BDD-cost:   97
c ---[  73]---> BDD-cost:   97
c ---[  72]---> BDD-cost:   97
c ---[  71]---> BDD-cost:   97
c ---[  70]---> BDD-cost:   97
c ---[  69]---> BDD-cost:   97
c ---[  68]---> BDD-cost:   97
c ---[  67]---> BDD-cost:   97
c ---[  66]---> BDD-cost:   97
c ---[  65]---> BDD-cost:   97
c ---[  64]---> BDD-cost:   97
c ---[  63]---> BDD-cost:   97
c ---[  62]---> BDD-cost:   97
c ---[  61]---> BDD-cost:   97
c ---[  60]---> BDD-cost:   97
c ---[  59]---> BDD-cost:   97
c ---[  58]---> BDD-cost:   97
c ---[  57]---> BDD-cost:   97
c ---[  56]---> BDD-cost:   97
c ---[  55]---> BDD-cost:   97
c ---[  54]---> BDD-cost:   97
c ---[  53]---> BDD-cost:   97
c ---[  52]---> BDD-cost:   97
c ---[  51]---> BDD-cost:   97
c ---[  50]---> BDD-cost:   97
c ---[  49]---> BDD-cost:   97
c ---[  48]---> BDD-cost:   97
c ---[  47]---> BDD-cost:   97
c ---[  46]---> BDD-cost:   97
c ---[  45]---> BDD-cost:   97
c ---[  44]---> BDD-cost:   97
c ---[  43]---> BDD-cost:   97
c ---[  42]---> BDD-cost:   97
c ---[  41]---> BDD-cost:   97
c ---[  40]---> BDD-cost:   97
c ---[  39]---> BDD-cost:   97
c ---[  38]---> BDD-cost:   97
c ---[  37]---> BDD-cost:   97
c ---[  36]---> BDD-cost:   97
c ---[  35]---> BDD-cost:   97
c ---[  34]---> BDD-cost:   97
c ---[  33]---> BDD-cost:   97
c ---[  32]---> BDD-cost:   97
c ---[  31]---> BDD-cost:   97
c ---[  30]---> BDD-cost:   97
c ---[  29]---> BDD-cost:   97
c ---[  28]---> BDD-cost:   97
c ---[  27]---> BDD-cost:   97
c ---[  26]---> BDD-cost:   97
c ---[  25]---> BDD-cost:   97
c ---[  24]---> BDD-cost:   97
c ---[  23]---> BDD-cost:   97
c ---[  22]---> BDD-cost:   97
c ---[  21]---> BDD-cost:   97
c ---[  20]---> BDD-cost:   97
c ---[  19]---> BDD-cost:   97
c ---[  18]---> BDD-cost:   97
c ---[  17]---> BDD-cost:   97
c ---[  16]---> BDD-cost:   97
c ---[  15]---> BDD-cost:   97
c ---[  14]---> BDD-cost:   97
c ---[  13]---> BDD-cost:   97
c ---[  12]---> BDD-cost:   97
c ---[  11]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   9]---> BDD-cost:   97
c ---[   8]---> BDD-cost:   97
c ---[   7]---> BDD-cost:   97
c ---[   6]---> BDD-cost:   97
c ---[   5]---> BDD-cost:   97
c ---[   4]---> BDD-cost:   97
c ---[   3]---> BDD-cost:   97
c ---[   2]---> BDD-cost:   97
c ---[   1]---> BDD-cost:   97
c ---[   0]---> BDD-cost:   97
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   19380    54160 |    6460       0        0     nan |  0.000 % |
c |       103 |   19380    54160 |    7106     103    15224   147.8 |  0.680 % |
c |       264 |   19380    54160 |    7816     264    48573   184.0 |  0.680 % |
c |       491 |   19380    54160 |    8598     491    85624   174.4 |  0.680 % |
c |       828 |   19380    54160 |    9458     828   154823   187.0 |  0.680 % |
c |      1334 |   19380    54160 |   10403    1334   306589   229.8 |  0.680 % |
c |      2093 |   19380    54160 |   11444    2093   485053   231.8 |  0.680 % |
c |      3234 |   19380    54160 |   12588    3234   825279   255.2 |  0.680 % |
c |      4943 |   19380    54160 |   13847    4943  1417289   286.7 |  0.680 % |
c |      7505 |   19380    54160 |   15232    7505  2438701   324.9 |  0.680 % |
c |     11349 |   19380    54160 |   16755   11349  3669460   323.3 |  0.680 % |
c |     17115 |   19380    54160 |   18431   17115  6183322   361.3 |  0.680 % |
c |     25765 |   19380    54160 |   20274   14106  6524975   462.6 |  0.680 % |
c |     38745 |   19380    54160 |   22301   13797  6591558   477.8 |  0.680 % |
c |     58212 |   19380    54160 |   24531   17990  8193323   455.4 |  0.680 % |
c |     87406 |   19380    54160 |   26985   14543  4843174   333.0 |  0.680 % |
c |    131196 |   19380    54160 |   29683   19996 12157179   608.0 |  0.680 % |
c |    196881 |   19380    54160 |   32651   14613  5410723   370.3 |  0.680 % |

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/825/stat): 825 (minisat+_script) R 824 825 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841220947 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/825/statm): 174 3 169 147 0 27 0
[pid=825] 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=826
New process pid=827
New process pid=828
execve syscall for /bin/sed executable
One traced child (pid=827) 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=828) exited with status: 0
One traced child (pid=826) exited with status: 0
New process pid=829
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-chnl40_50_pb.cnf.cr.opb

[startup+10.0061 s]
Raw data (loadavg): 0.96 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 2935 0 3 0 949 15 0 0 25 0 1 0 1841220952 12627968 2924 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 3083 2924 145 145 0 2938 0
[pid=829] vsize: 12332
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 14456

[startup+20.0081 s]
Raw data (loadavg): 0.96 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 4691 0 3 0 1924 25 0 0 25 0 1 0 1841220952 19841024 4680 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 4844 4680 145 145 0 4699 0
[pid=829] vsize: 19376
Current children cumulated CPU time (s) 19.49
Current children cumulated vsize (Kb) 21500

[startup+30.009 s]
Raw data (loadavg): 0.97 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 6160 0 3 0 2904 34 0 0 25 0 1 0 1841220952 25849856 6149 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 6311 6149 145 145 0 6166 0
[pid=829] vsize: 25244
Current children cumulated CPU time (s) 29.38
Current children cumulated vsize (Kb) 27368

[startup+40.0099 s]
Raw data (loadavg): 0.97 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 7110 0 3 0 3890 38 0 0 25 0 1 0 1841220952 29798400 7099 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 7275 7099 145 145 0 7130 0
[pid=829] vsize: 29100
Current children cumulated CPU time (s) 39.28
Current children cumulated vsize (Kb) 31224

[startup+50.0108 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 8603 0 3 0 4869 47 0 0 25 0 1 0 1841220952 35909632 8592 4294967295 134512640 135094434 3221224432 3221223104 134555795 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 8767 8592 145 145 0 8622 0
[pid=829] vsize: 35068
Current children cumulated CPU time (s) 49.16
Current children cumulated vsize (Kb) 37192

[startup+60.0118 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 9850 0 3 0 5852 54 0 0 25 0 1 0 1841220952 41009152 9839 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 10012 9839 145 145 0 9867 0
[pid=829] vsize: 40048
Current children cumulated CPU time (s) 59.06
Current children cumulated vsize (Kb) 42172

[startup+70.0127 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 10507 0 3 0 6841 58 0 0 25 0 1 0 1841220952 43692032 10496 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 10667 10496 145 145 0 10522 0
[pid=829] vsize: 42668
Current children cumulated CPU time (s) 68.99
Current children cumulated vsize (Kb) 44792

[startup+80.0136 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 10507 0 3 0 7841 58 0 0 25 0 1 0 1841220952 43692032 10496 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 10667 10496 145 145 0 10522 0
[pid=829] vsize: 42668
Current children cumulated CPU time (s) 78.99
Current children cumulated vsize (Kb) 44792

[startup+90.0145 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 10507 0 3 0 8841 58 0 0 25 0 1 0 1841220952 43692032 10496 4294967295 134512640 135094434 3221224432 3221223024 134557348 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 10667 10496 145 145 0 10522 0
[pid=829] vsize: 42668
Current children cumulated CPU time (s) 88.99
Current children cumulated vsize (Kb) 44792

[startup+100.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 11340 0 3 0 9830 64 0 0 25 0 1 0 1841220952 47104000 11329 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 11500 11329 145 145 0 11355 0
[pid=829] vsize: 46000
Current children cumulated CPU time (s) 98.94
Current children cumulated vsize (Kb) 48124

[startup+110.016 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 12792 0 3 0 10812 72 0 0 25 0 1 0 1841220952 53047296 12781 4294967295 134512640 135094434 3221224432 3221223104 134556270 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 12951 12781 145 145 0 12806 0
[pid=829] vsize: 51804
Current children cumulated CPU time (s) 108.84
Current children cumulated vsize (Kb) 53928

[startup+120.017 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 12792 0 3 0 11813 72 0 0 25 0 1 0 1841220952 53047296 12781 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 12951 12781 145 145 0 12806 0
[pid=829] vsize: 51804
Current children cumulated CPU time (s) 118.85
Current children cumulated vsize (Kb) 53928

[startup+130.018 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 12792 0 3 0 12812 72 0 0 25 0 1 0 1841220952 53047296 12781 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 12951 12781 145 145 0 12806 0
[pid=829] vsize: 51804
Current children cumulated CPU time (s) 128.84
Current children cumulated vsize (Kb) 53928

[startup+140.019 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 12792 0 3 0 13812 72 0 0 25 0 1 0 1841220952 53047296 12781 4294967295 134512640 135094434 3221224432 3221223024 134557253 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 12951 12781 145 145 0 12806 0
[pid=829] vsize: 51804
Current children cumulated CPU time (s) 138.84
Current children cumulated vsize (Kb) 53928

[startup+150.02 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 12792 0 3 0 14813 72 0 0 25 0 1 0 1841220952 53047296 12781 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 12951 12781 145 145 0 12806 0
[pid=829] vsize: 51804
Current children cumulated CPU time (s) 148.85
Current children cumulated vsize (Kb) 53928

[startup+160.021 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 12792 0 3 0 15813 72 0 0 25 0 1 0 1841220952 53047296 12781 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 12951 12781 145 145 0 12806 0
[pid=829] vsize: 51804
Current children cumulated CPU time (s) 158.85
Current children cumulated vsize (Kb) 53928

[startup+170.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 13520 0 3 0 16801 77 0 0 25 0 1 0 1841220952 56053760 13509 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 13685 13509 145 145 0 13540 0
[pid=829] vsize: 54740
Current children cumulated CPU time (s) 168.78
Current children cumulated vsize (Kb) 56864

[startup+180.023 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14376 0 3 0 17788 83 0 0 25 0 1 0 1841220952 59551744 14365 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14539 14365 145 145 0 14394 0
[pid=829] vsize: 58156
Current children cumulated CPU time (s) 178.71
Current children cumulated vsize (Kb) 60280

[startup+190.024 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14586 0 3 0 18784 85 0 0 25 0 1 0 1841220952 60407808 14575 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14575 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 188.69
Current children cumulated vsize (Kb) 61116

[startup+200.025 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14586 0 3 0 19784 85 0 0 25 0 1 0 1841220952 60407808 14575 4294967295 134512640 135094434 3221224432 3221223104 134555340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14575 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 198.69
Current children cumulated vsize (Kb) 61116

[startup+210.026 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14586 0 3 0 20784 85 0 0 25 0 1 0 1841220952 60407808 14575 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14575 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 208.69
Current children cumulated vsize (Kb) 61116

[startup+220.027 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14586 0 3 0 21784 85 0 0 25 0 1 0 1841220952 60407808 14575 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14575 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 218.69
Current children cumulated vsize (Kb) 61116

[startup+230.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14586 0 3 0 22784 85 0 0 25 0 1 0 1841220952 60407808 14575 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14575 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 228.69
Current children cumulated vsize (Kb) 61116

[startup+240.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14587 0 3 0 23784 85 0 0 25 0 1 0 1841220952 60407808 14576 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14576 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 238.69
Current children cumulated vsize (Kb) 61116

[startup+250.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14588 0 3 0 24785 85 0 0 25 0 1 0 1841220952 60407808 14577 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14577 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 248.7
Current children cumulated vsize (Kb) 61116

[startup+260.03 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 25785 85 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 258.7
Current children cumulated vsize (Kb) 61116

[startup+270.031 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 26785 85 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 268.7
Current children cumulated vsize (Kb) 61116

[startup+280.032 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 27785 85 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 278.7
Current children cumulated vsize (Kb) 61116

[startup+290.033 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 28785 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223024 134557287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 288.71
Current children cumulated vsize (Kb) 61116

[startup+300.034 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 29785 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 298.71
Current children cumulated vsize (Kb) 61116

[startup+310.035 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 30786 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 308.72
Current children cumulated vsize (Kb) 61116

[startup+320.036 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 31786 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 318.72
Current children cumulated vsize (Kb) 61116

[startup+330.036 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 32786 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 328.72
Current children cumulated vsize (Kb) 61116

[startup+340.037 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 33786 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 338.72
Current children cumulated vsize (Kb) 61116

[startup+350.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 34787 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 348.73
Current children cumulated vsize (Kb) 61116

[startup+360.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 35787 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 358.73
Current children cumulated vsize (Kb) 61116

[startup+370.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 36787 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 368.73
Current children cumulated vsize (Kb) 61116

[startup+380.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 37787 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 378.73
Current children cumulated vsize (Kb) 61116

[startup+390.042 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 38787 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 388.73
Current children cumulated vsize (Kb) 61116

[startup+400.043 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 39787 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 398.73
Current children cumulated vsize (Kb) 61116

[startup+410.044 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 40788 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 408.74
Current children cumulated vsize (Kb) 61116

[startup+420.045 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 41788 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 418.74
Current children cumulated vsize (Kb) 61116

[startup+430.046 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 42788 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 428.74
Current children cumulated vsize (Kb) 61116

[startup+440.047 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 43787 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 438.73
Current children cumulated vsize (Kb) 61116

[startup+450.048 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 44787 86 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 448.73
Current children cumulated vsize (Kb) 61116

[startup+460.05 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 45787 87 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 458.74
Current children cumulated vsize (Kb) 61116

[startup+470.051 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14589 0 3 0 46787 87 0 0 25 0 1 0 1841220952 60407808 14578 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14748 14578 145 145 0 14603 0
[pid=829] vsize: 58992
Current children cumulated CPU time (s) 468.74
Current children cumulated vsize (Kb) 61116

[startup+480.051 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 14631 0 3 0 47786 88 0 0 25 0 1 0 1841220952 60579840 14620 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 14790 14620 145 145 0 14645 0
[pid=829] vsize: 59160
Current children cumulated CPU time (s) 478.74
Current children cumulated vsize (Kb) 61284

[startup+490.052 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15418 0 3 0 48772 94 0 0 25 0 1 0 1841220952 63815680 15407 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15407 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 488.66
Current children cumulated vsize (Kb) 64444

[startup+500.053 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15418 0 3 0 49772 95 0 0 25 0 1 0 1841220952 63815680 15407 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15407 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 498.67
Current children cumulated vsize (Kb) 64444

[startup+510.052 s]
Raw data (loadavg): 1.07 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15418 0 3 0 50772 95 0 0 25 0 1 0 1841220952 63815680 15407 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15407 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 508.67
Current children cumulated vsize (Kb) 64444

[startup+520.053 s]
Raw data (loadavg): 1.06 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15418 0 3 0 51772 95 0 0 25 0 1 0 1841220952 63815680 15407 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15407 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 518.67
Current children cumulated vsize (Kb) 64444

[startup+530.054 s]
Raw data (loadavg): 1.05 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15418 0 3 0 52772 96 0 0 25 0 1 0 1841220952 63815680 15407 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15407 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 528.68
Current children cumulated vsize (Kb) 64444

[startup+540.055 s]
Raw data (loadavg): 1.04 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15420 0 3 0 53772 96 0 0 25 0 1 0 1841220952 63815680 15409 4294967295 134512640 135094434 3221224432 3221223104 134555821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15409 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 538.68
Current children cumulated vsize (Kb) 64444

[startup+550.056 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15420 0 3 0 54772 96 0 0 25 0 1 0 1841220952 63815680 15409 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15409 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 548.68
Current children cumulated vsize (Kb) 64444

[startup+560.057 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15420 0 3 0 55772 96 0 0 25 0 1 0 1841220952 63815680 15409 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15409 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 558.68
Current children cumulated vsize (Kb) 64444

[startup+570.058 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15420 0 3 0 56772 96 0 0 25 0 1 0 1841220952 63815680 15409 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15409 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 568.68
Current children cumulated vsize (Kb) 64444

[startup+580.059 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 15421 0 3 0 57772 96 0 0 25 0 1 0 1841220952 63815680 15410 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 15580 15410 145 145 0 15435 0
[pid=829] vsize: 62320
Current children cumulated CPU time (s) 578.68
Current children cumulated vsize (Kb) 64444

[startup+590.06 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 16094 0 3 0 58764 100 0 0 25 0 1 0 1841220952 66613248 16083 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 16263 16083 145 145 0 16118 0
[pid=829] vsize: 65052
Current children cumulated CPU time (s) 588.64
Current children cumulated vsize (Kb) 67176

[startup+600.061 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 16744 0 3 0 59755 104 0 0 25 0 1 0 1841220952 69292032 16733 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 16917 16733 145 145 0 16772 0
[pid=829] vsize: 67668
Current children cumulated CPU time (s) 598.59
Current children cumulated vsize (Kb) 69792

[startup+610.062 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 17378 0 3 0 60745 109 0 0 25 0 1 0 1841220952 71901184 17367 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 17554 17367 145 145 0 17409 0
[pid=829] vsize: 70216
Current children cumulated CPU time (s) 608.54
Current children cumulated vsize (Kb) 72340

[startup+620.063 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 18203 0 3 0 61735 113 0 0 25 0 1 0 1841220952 75280384 18192 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 18379 18192 145 145 0 18234 0
[pid=829] vsize: 73516
Current children cumulated CPU time (s) 618.48
Current children cumulated vsize (Kb) 75640

[startup+630.063 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 19038 0 3 0 62722 119 0 0 25 0 1 0 1841220952 78782464 19027 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 19234 19027 145 145 0 19089 0
[pid=829] vsize: 76936
Current children cumulated CPU time (s) 628.41
Current children cumulated vsize (Kb) 79060

[startup+640.064 s]
Raw data (loadavg): 1.00 1.00 0.97 1/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) T 825 825 31027 0 -1 0 19448 0 3 0 63717 121 0 0 25 0 1 0 1841220952 80482304 19437 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/829/statm): 19649 19437 145 145 0 19504 0
[pid=829] vsize: 78596
Current children cumulated CPU time (s) 638.38
Current children cumulated vsize (Kb) 80720

[startup+650.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 19933 0 3 0 64710 124 0 0 25 0 1 0 1841220952 82464768 19922 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 20133 19922 145 145 0 19988 0
[pid=829] vsize: 80532
Current children cumulated CPU time (s) 648.34
Current children cumulated vsize (Kb) 82656

[startup+660.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 20403 0 3 0 65703 127 0 0 25 0 1 0 1841220952 84443136 20392 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 20616 20392 145 145 0 20471 0
[pid=829] vsize: 82464
Current children cumulated CPU time (s) 658.3
Current children cumulated vsize (Kb) 84588

[startup+670.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 20958 0 3 0 66694 131 0 0 25 0 1 0 1841220952 86732800 20947 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21175 20947 145 145 0 21030 0
[pid=829] vsize: 84700
Current children cumulated CPU time (s) 668.25
Current children cumulated vsize (Kb) 86824

[startup+680.067 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21064 0 3 0 67692 132 0 0 25 0 1 0 1841220952 87191552 21053 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21053 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 678.24
Current children cumulated vsize (Kb) 87272

[startup+690.068 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21064 0 3 0 68693 132 0 0 25 0 1 0 1841220952 87191552 21053 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21053 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 688.25
Current children cumulated vsize (Kb) 87272

[startup+700.069 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21064 0 3 0 69693 132 0 0 25 0 1 0 1841220952 87191552 21053 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21053 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 698.25
Current children cumulated vsize (Kb) 87272

[startup+710.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21064 0 3 0 70693 132 0 0 25 0 1 0 1841220952 87191552 21053 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21053 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 708.25
Current children cumulated vsize (Kb) 87272

[startup+720.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21064 0 3 0 71693 132 0 0 25 0 1 0 1841220952 87191552 21053 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21053 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 718.25
Current children cumulated vsize (Kb) 87272

[startup+730.072 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21064 0 3 0 72693 132 0 0 25 0 1 0 1841220952 87191552 21053 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21053 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 728.25
Current children cumulated vsize (Kb) 87272

[startup+740.074 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21066 0 3 0 73693 132 0 0 25 0 1 0 1841220952 87191552 21055 4294967295 134512640 135094434 3221224432 3221223072 134538540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 21287 21055 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 738.25
Current children cumulated vsize (Kb) 87272

[startup+750.075 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21066 0 3 0 74692 133 0 0 25 0 1 0 1841220952 87191552 21055 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21055 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 748.25
Current children cumulated vsize (Kb) 87272

[startup+760.075 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21066 0 3 0 75692 133 0 0 25 0 1 0 1841220952 87191552 21055 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21055 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 758.25
Current children cumulated vsize (Kb) 87272

[startup+770.076 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21066 0 3 0 76692 133 0 0 25 0 1 0 1841220952 87191552 21055 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21287 21055 145 145 0 21142 0
[pid=829] vsize: 85148
Current children cumulated CPU time (s) 768.25
Current children cumulated vsize (Kb) 87272

[startup+780.077 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21101 0 3 0 77693 133 0 0 25 0 1 0 1841220952 87453696 21090 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21351 21090 145 145 0 21206 0
[pid=829] vsize: 85404
Current children cumulated CPU time (s) 778.26
Current children cumulated vsize (Kb) 87528

[startup+790.077 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 78689 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 788.24
Current children cumulated vsize (Kb) 88672

[startup+800.078 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 79689 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 798.24
Current children cumulated vsize (Kb) 88672

[startup+810.079 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 80689 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 808.24
Current children cumulated vsize (Kb) 88672

[startup+820.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 81690 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 818.25
Current children cumulated vsize (Kb) 88672

[startup+830.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 82689 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 828.24
Current children cumulated vsize (Kb) 88672

[startup+840.081 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 83690 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 838.25
Current children cumulated vsize (Kb) 88672

[startup+850.082 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 84690 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 848.25
Current children cumulated vsize (Kb) 88672

[startup+860.083 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 85690 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 858.25
Current children cumulated vsize (Kb) 88672

[startup+870.084 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 86690 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 868.25
Current children cumulated vsize (Kb) 88672

[startup+880.085 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 87691 135 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 878.26
Current children cumulated vsize (Kb) 88672

[startup+890.086 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 88690 136 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 888.26
Current children cumulated vsize (Kb) 88672

[startup+900.087 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 89691 136 0 0 25 0 1 0 1841220952 88625152 21377 4294967295 134512640 135094434 3221224432 3221223104 134556270 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21637 21377 145 145 0 21492 0
[pid=829] vsize: 86548
Current children cumulated CPU time (s) 898.27
Current children cumulated vsize (Kb) 88672

[startup+910.087 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 90691 136 0 0 25 0 1 0 1841220952 88416256 21326 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21326 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 908.27
Current children cumulated vsize (Kb) 88468

[startup+920.088 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 91691 136 0 0 25 0 1 0 1841220952 88416256 21326 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21326 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 918.27
Current children cumulated vsize (Kb) 88468

[startup+930.088 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 92691 136 0 0 25 0 1 0 1841220952 88416256 21326 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21326 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 928.27
Current children cumulated vsize (Kb) 88468

[startup+940.089 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21388 0 3 0 93692 136 0 0 25 0 1 0 1841220952 88416256 21326 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21326 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 938.28
Current children cumulated vsize (Kb) 88468

[startup+950.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21389 0 3 0 94692 136 0 0 25 0 1 0 1841220952 88416256 21327 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21327 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 948.28
Current children cumulated vsize (Kb) 88468

[startup+960.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21389 0 3 0 95692 136 0 0 25 0 1 0 1841220952 88416256 21327 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21327 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 958.28
Current children cumulated vsize (Kb) 88468

[startup+970.091 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 96692 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 968.28
Current children cumulated vsize (Kb) 88468

[startup+980.092 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 97692 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 978.28
Current children cumulated vsize (Kb) 88468

[startup+990.093 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 98692 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 988.28
Current children cumulated vsize (Kb) 88468

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 99692 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 998.28
Current children cumulated vsize (Kb) 88468

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 100692 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1008.28
Current children cumulated vsize (Kb) 88468

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 101692 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1018.28
Current children cumulated vsize (Kb) 88468

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 102692 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1028.28
Current children cumulated vsize (Kb) 88468

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 103692 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1038.28
Current children cumulated vsize (Kb) 88468

[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 104693 136 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223024 134551885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1048.29
Current children cumulated vsize (Kb) 88468

[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 105693 137 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223104 134555676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1058.3
Current children cumulated vsize (Kb) 88468

[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 106693 137 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1068.3
Current children cumulated vsize (Kb) 88468

[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 107692 138 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1078.3
Current children cumulated vsize (Kb) 88468

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 108691 139 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1088.3
Current children cumulated vsize (Kb) 88468

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21390 0 3 0 109691 139 0 0 25 0 1 0 1841220952 88416256 21328 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21328 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1098.3
Current children cumulated vsize (Kb) 88468

[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21391 0 3 0 110691 140 0 0 25 0 1 0 1841220952 88416256 21329 4294967295 134512640 135094434 3221224432 3221223104 134556450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21586 21329 145 145 0 21441 0
[pid=829] vsize: 86344
Current children cumulated CPU time (s) 1108.31
Current children cumulated vsize (Kb) 88468

[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21509 0 3 0 111690 140 0 0 25 0 1 0 1841220952 88899584 21447 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21447 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1118.3
Current children cumulated vsize (Kb) 88940

[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21509 0 3 0 112689 141 0 0 25 0 1 0 1841220952 88899584 21447 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21447 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1128.3
Current children cumulated vsize (Kb) 88940

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21509 0 3 0 113689 141 0 0 25 0 1 0 1841220952 88899584 21447 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21447 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1138.3
Current children cumulated vsize (Kb) 88940

[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21509 0 3 0 114690 141 0 0 25 0 1 0 1841220952 88899584 21447 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21447 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1148.31
Current children cumulated vsize (Kb) 88940

[startup+1160.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21509 0 3 0 115690 141 0 0 25 0 1 0 1841220952 88899584 21447 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21447 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1158.31
Current children cumulated vsize (Kb) 88940

[startup+1170.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21509 0 3 0 116690 141 0 0 25 0 1 0 1841220952 88899584 21447 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21447 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1168.31
Current children cumulated vsize (Kb) 88940

[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21509 0 3 0 117690 141 0 0 25 0 1 0 1841220952 88899584 21447 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21447 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1178.31
Current children cumulated vsize (Kb) 88940

[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21511 0 3 0 118690 142 0 0 25 0 1 0 1841220952 88899584 21449 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21449 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1188.32
Current children cumulated vsize (Kb) 88940

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21511 0 3 0 119690 142 0 0 25 0 1 0 1841220952 88899584 21449 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21449 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1198.32
Current children cumulated vsize (Kb) 88940

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21511 0 3 0 120690 142 0 0 25 0 1 0 1841220952 88899584 21449 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21449 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1208.32
Current children cumulated vsize (Kb) 88940



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 829
Raw data (/proc/825/stat): 825 (minisat+_script) S 824 825 31027 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1841220947 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/825/statm): 531 226 485 147 0 384 0
[pid=825] vsize: 2124
Raw data (/proc/829/stat): 829 (minisat+_64-bit) R 825 825 31027 0 -1 0 21511 0 3 0 120690 142 0 0 25 0 1 0 1841220952 88899584 21449 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/829/statm): 21704 21449 145 145 0 21559 0
[pid=829] vsize: 86816
Current children cumulated CPU time (s) 1208.32
Current children cumulated vsize (Kb) 88940

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

Child status: 0
Real time (s): 1210.17
CPU time (s): 1208.37
CPU user time (s): 1206.91
CPU system time (s): 1.46278
CPU usage (%): 99.8517
Max. virtual memory (cumulated for all children) (Kb): 88940

Verifier Data

ERROR: no interpretation found !