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-chnl15_25_pb.cnf.cr.opb
MD5SUM808390b13d2d87ec4e78f628ed3af9ba
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 26
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.024995
Number of variables750
Total number of constraints80
Number of constraints which are clauses50
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint25

Trace number 809

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        947156 kB
Buffers:         34296 kB
Cached:          28952 kB
SwapCached:        740 kB
Active:          54860 kB
Inactive:        10948 kB
HighTotal:      131008 kB
HighFree:        99988 kB
LowTotal:       903652 kB
LowFree:        847168 kB
SwapTotal:     2097136 kB
SwapFree:      2095892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            16012 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:44:04 (client local time) WITH STATUS 0 IN 1209.92 SECONDS
stats: 2349 7 1209.92 0

Solver Data

c Parsing PB file...
c Converting 80 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3530     9810 |    1176       0        0     nan |  0.000 % |
c |       103 |    3530     9810 |    1293     103     5007    48.6 |  1.389 % |
c |       253 |    3530     9810 |    1422     253    13026    51.5 |  1.389 % |
c |       478 |    3530     9810 |    1565     478    27883    58.3 |  1.390 % |
c |       818 |    3530     9810 |    1721     818    54244    66.3 |  1.389 % |
c |      1324 |    3530     9810 |    1893    1324    89008    67.2 |  1.389 % |
c |      2084 |    3530     9810 |    2083    2084   154915    74.3 |  1.389 % |
c |      3224 |    3530     9810 |    2291    1835   146216    79.7 |  1.389 % |
c |      4932 |    3530     9810 |    2520    2209   220568    99.8 |  1.389 % |
c |      7494 |    3530     9810 |    2772    1902   214616   112.8 |  1.389 % |
c |     11338 |    3530     9810 |    3050    2643   352193   133.3 |  1.389 % |
c |     17107 |    3530     9810 |    3355    3014   336789   111.7 |  1.389 % |
c |     25756 |    3530     9810 |    3690    2249   281918   125.4 |  1.389 % |
c |     38731 |    3530     9810 |    4059    2796   359962   128.7 |  1.389 % |
c |     58192 |    3530     9810 |    4465    2453   289039   117.8 |  1.389 % |
c |     87386 |    3530     9810 |    4912    2518   277999   110.4 |  1.389 % |
c |    131177 |    3530     9810 |    5403    3570   478640   134.1 |  1.389 % |
c |    196861 |    3530     9810 |    5944    4748   630300   132.8 |  1.389 % |
c |    295392 |    3530     9810 |    6538    4647   519495   111.8 |  1.389 % |
c |    443181 |    3530     9810 |    7192    6344   768707   121.2 |  1.389 % |
c |    664866 |    3530     9810 |    7911    7564   930517   123.0 |  1.389 % |
c |    997394 |    3530     9810 |    8702    5038   677958   134.6 |  1.389 % |

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/17851/stat): 17851 (minisat+_script) R 17850 17851 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783025155 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/17851/statm): 174 3 169 147 0 27 0
[pid=17851] 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=17852
New process pid=17853
New process pid=17854
execve syscall for /bin/sed executable
One traced child (pid=17853) 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=17854) exited with status: 0
One traced child (pid=17852) exited with status: 0
New process pid=17855
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-chnl15_25_pb.cnf.cr.opb

[startup+10.0049 s]
Raw data (loadavg): 0.82 0.95 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 869 0 2 0 978 4 0 0 25 0 1 0 1783025160 3878912 858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17855/statm): 947 858 145 145 0 802 0
[pid=17855] vsize: 3788
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 5912

[startup+20.0065 s]
Raw data (loadavg): 0.85 0.95 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1037 0 2 0 1975 6 0 0 25 0 1 0 1783025160 4579328 1026 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1118 1026 145 145 0 973 0
[pid=17855] vsize: 4472
Current children cumulated CPU time (s) 19.83
Current children cumulated vsize (Kb) 6596

[startup+30.0071 s]
Raw data (loadavg): 0.87 0.95 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1181 0 2 0 2972 7 0 0 25 0 1 0 1783025160 5177344 1170 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17855/statm): 1264 1170 145 145 0 1119 0
[pid=17855] vsize: 5056
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 7180

[startup+40.0088 s]
Raw data (loadavg): 0.89 0.95 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1201 0 2 0 3971 7 0 0 25 0 1 0 1783025160 5259264 1190 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17855/statm): 1284 1190 145 145 0 1139 0
[pid=17855] vsize: 5136
Current children cumulated CPU time (s) 39.8
Current children cumulated vsize (Kb) 7260

[startup+50.0104 s]
Raw data (loadavg): 0.91 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1251 0 2 0 4970 8 0 0 25 0 1 0 1783025160 5472256 1240 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1336 1240 145 145 0 1191 0
[pid=17855] vsize: 5344
Current children cumulated CPU time (s) 49.8
Current children cumulated vsize (Kb) 7468

[startup+60.011 s]
Raw data (loadavg): 0.92 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1284 0 2 0 5970 9 0 0 25 0 1 0 1783025160 5615616 1273 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1371 1273 145 145 0 1226 0
[pid=17855] vsize: 5484
Current children cumulated CPU time (s) 59.81
Current children cumulated vsize (Kb) 7608

[startup+70.0126 s]
Raw data (loadavg): 0.93 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1382 0 2 0 6969 9 0 0 25 0 1 0 1783025160 6033408 1371 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1473 1371 145 145 0 1328 0
[pid=17855] vsize: 5892
Current children cumulated CPU time (s) 69.8
Current children cumulated vsize (Kb) 8016

[startup+80.0133 s]
Raw data (loadavg): 0.94 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1468 0 2 0 7968 9 0 0 25 0 1 0 1783025160 6385664 1457 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1559 1457 145 145 0 1414 0
[pid=17855] vsize: 6236
Current children cumulated CPU time (s) 79.79
Current children cumulated vsize (Kb) 8360

[startup+90.0139 s]
Raw data (loadavg): 0.95 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1500 0 2 0 8967 10 0 0 25 0 1 0 1783025160 6516736 1489 4294967295 134512640 135094434 3221224432 3221223024 134556980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1591 1489 145 145 0 1446 0
[pid=17855] vsize: 6364
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 8488

[startup+100.015 s]
Raw data (loadavg): 0.96 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1508 0 2 0 9967 10 0 0 25 0 1 0 1783025160 6549504 1497 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1599 1497 145 145 0 1454 0
[pid=17855] vsize: 6396
Current children cumulated CPU time (s) 99.79
Current children cumulated vsize (Kb) 8520

[startup+110.015 s]
Raw data (loadavg): 0.96 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1587 0 2 0 10967 11 0 0 25 0 1 0 1783025160 6868992 1576 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1677 1576 145 145 0 1532 0
[pid=17855] vsize: 6708
Current children cumulated CPU time (s) 109.8
Current children cumulated vsize (Kb) 8832

[startup+120.017 s]
Raw data (loadavg): 0.97 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1590 0 2 0 11967 11 0 0 25 0 1 0 1783025160 6881280 1579 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1680 1579 145 145 0 1535 0
[pid=17855] vsize: 6720
Current children cumulated CPU time (s) 119.8
Current children cumulated vsize (Kb) 8844

[startup+130.017 s]
Raw data (loadavg): 0.97 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1590 0 2 0 12967 11 0 0 25 0 1 0 1783025160 6881280 1579 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1680 1579 145 145 0 1535 0
[pid=17855] vsize: 6720
Current children cumulated CPU time (s) 129.8
Current children cumulated vsize (Kb) 8844

[startup+140.018 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1609 0 2 0 13967 11 0 0 25 0 1 0 1783025160 6963200 1598 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1700 1598 145 145 0 1555 0
[pid=17855] vsize: 6800
Current children cumulated CPU time (s) 139.8
Current children cumulated vsize (Kb) 8924

[startup+150.019 s]
Raw data (loadavg): 0.98 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1723 0 2 0 14966 12 0 0 25 0 1 0 1783025160 7442432 1712 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1817 1712 145 145 0 1672 0
[pid=17855] vsize: 7268
Current children cumulated CPU time (s) 149.8
Current children cumulated vsize (Kb) 9392

[startup+160.019 s]
Raw data (loadavg): 0.98 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1767 0 2 0 15966 12 0 0 25 0 1 0 1783025160 7643136 1756 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1866 1756 145 145 0 1721 0
[pid=17855] vsize: 7464
Current children cumulated CPU time (s) 159.8
Current children cumulated vsize (Kb) 9588

[startup+170.02 s]
Raw data (loadavg): 0.98 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1860 0 2 0 16964 13 0 0 25 0 1 0 1783025160 8036352 1849 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17855/statm): 1962 1849 145 145 0 1817 0
[pid=17855] vsize: 7848
Current children cumulated CPU time (s) 169.79
Current children cumulated vsize (Kb) 9972

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1860 0 2 0 17963 13 0 0 25 0 1 0 1783025160 8036352 1849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1962 1849 145 145 0 1817 0
[pid=17855] vsize: 7848
Current children cumulated CPU time (s) 179.78
Current children cumulated vsize (Kb) 9972

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1860 0 2 0 18964 13 0 0 25 0 1 0 1783025160 8036352 1849 4294967295 134512640 135094434 3221224432 3221223088 134558113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1962 1849 145 145 0 1817 0
[pid=17855] vsize: 7848
Current children cumulated CPU time (s) 189.79
Current children cumulated vsize (Kb) 9972

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1863 0 2 0 19964 13 0 0 25 0 1 0 1783025160 8048640 1852 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1965 1852 145 145 0 1820 0
[pid=17855] vsize: 7860
Current children cumulated CPU time (s) 199.79
Current children cumulated vsize (Kb) 9984

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1867 0 2 0 20964 13 0 0 25 0 1 0 1783025160 8065024 1856 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 1969 1856 145 145 0 1824 0
[pid=17855] vsize: 7876
Current children cumulated CPU time (s) 209.79
Current children cumulated vsize (Kb) 10000

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1924 0 2 0 21964 14 0 0 25 0 1 0 1783025160 8314880 1913 4294967295 134512640 135094434 3221224432 3221223024 134557419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2030 1913 145 145 0 1885 0
[pid=17855] vsize: 8120
Current children cumulated CPU time (s) 219.8
Current children cumulated vsize (Kb) 10244

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1956 0 2 0 22964 14 0 0 25 0 1 0 1783025160 8437760 1945 4294967295 134512640 135094434 3221224432 3221223024 134557488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2060 1945 145 145 0 1915 0
[pid=17855] vsize: 8240
Current children cumulated CPU time (s) 229.8
Current children cumulated vsize (Kb) 10364

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1956 0 2 0 23964 14 0 0 25 0 1 0 1783025160 8437760 1945 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2060 1945 145 145 0 1915 0
[pid=17855] vsize: 8240
Current children cumulated CPU time (s) 239.8
Current children cumulated vsize (Kb) 10364

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2032 0 2 0 24963 15 0 0 25 0 1 0 1783025160 8749056 2021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2136 2021 145 145 0 1991 0
[pid=17855] vsize: 8544
Current children cumulated CPU time (s) 249.8
Current children cumulated vsize (Kb) 10668

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2075 0 2 0 25963 15 0 0 25 0 1 0 1783025160 8925184 2064 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2179 2064 145 145 0 2034 0
[pid=17855] vsize: 8716
Current children cumulated CPU time (s) 259.8
Current children cumulated vsize (Kb) 10840

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2075 0 2 0 26963 15 0 0 25 0 1 0 1783025160 8925184 2064 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2179 2064 145 145 0 2034 0
[pid=17855] vsize: 8716
Current children cumulated CPU time (s) 269.8
Current children cumulated vsize (Kb) 10840

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2102 0 2 0 27963 15 0 0 25 0 1 0 1783025160 9027584 2091 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2204 2091 145 145 0 2059 0
[pid=17855] vsize: 8816
Current children cumulated CPU time (s) 279.8
Current children cumulated vsize (Kb) 10940

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2130 0 2 0 28963 15 0 0 25 0 1 0 1783025160 9158656 2119 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2236 2119 145 145 0 2091 0
[pid=17855] vsize: 8944
Current children cumulated CPU time (s) 289.8
Current children cumulated vsize (Kb) 11068

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2135 0 2 0 29963 15 0 0 25 0 1 0 1783025160 9191424 2124 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2244 2124 145 145 0 2099 0
[pid=17855] vsize: 8976
Current children cumulated CPU time (s) 299.8
Current children cumulated vsize (Kb) 11100

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2154 0 2 0 30963 15 0 0 25 0 1 0 1783025160 9269248 2143 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2263 2143 145 145 0 2118 0
[pid=17855] vsize: 9052
Current children cumulated CPU time (s) 309.8
Current children cumulated vsize (Kb) 11176

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2159 0 2 0 31963 15 0 0 25 0 1 0 1783025160 9302016 2148 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2271 2148 145 145 0 2126 0
[pid=17855] vsize: 9084
Current children cumulated CPU time (s) 319.8
Current children cumulated vsize (Kb) 11208

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2159 0 2 0 32964 15 0 0 25 0 1 0 1783025160 9302016 2148 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2271 2148 145 145 0 2126 0
[pid=17855] vsize: 9084
Current children cumulated CPU time (s) 329.81
Current children cumulated vsize (Kb) 11208

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2219 0 2 0 33963 16 0 0 25 0 1 0 1783025160 9568256 2208 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2336 2208 145 145 0 2191 0
[pid=17855] vsize: 9344
Current children cumulated CPU time (s) 339.81
Current children cumulated vsize (Kb) 11468

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2223 0 2 0 34963 16 0 0 25 0 1 0 1783025160 9584640 2212 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2340 2212 145 145 0 2195 0
[pid=17855] vsize: 9360
Current children cumulated CPU time (s) 349.81
Current children cumulated vsize (Kb) 11484

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2249 0 2 0 35963 16 0 0 25 0 1 0 1783025160 9728000 2238 4294967295 134512640 135094434 3221224432 3221223104 134555890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2375 2238 145 145 0 2230 0
[pid=17855] vsize: 9500
Current children cumulated CPU time (s) 359.81
Current children cumulated vsize (Kb) 11624

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.95 3/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2255 0 2 0 36964 16 0 0 25 0 1 0 1783025160 9740288 2244 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2378 2244 145 145 0 2233 0
[pid=17855] vsize: 9512
Current children cumulated CPU time (s) 369.82
Current children cumulated vsize (Kb) 11636

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2279 0 2 0 37963 16 0 0 25 0 1 0 1783025160 9850880 2268 4294967295 134512640 135094434 3221224432 3221223104 134556549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2405 2268 145 145 0 2260 0
[pid=17855] vsize: 9620
Current children cumulated CPU time (s) 379.81
Current children cumulated vsize (Kb) 11744

[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2304 0 2 0 38963 16 0 0 25 0 1 0 1783025160 9981952 2293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2437 2293 145 145 0 2292 0
[pid=17855] vsize: 9748
Current children cumulated CPU time (s) 389.81
Current children cumulated vsize (Kb) 11872

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2321 0 2 0 39964 16 0 0 25 0 1 0 1783025160 10076160 2310 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2460 2310 145 145 0 2315 0
[pid=17855] vsize: 9840
Current children cumulated CPU time (s) 399.82
Current children cumulated vsize (Kb) 11964

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2438 0 2 0 40961 18 0 0 25 0 1 0 1783025160 10559488 2427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2578 2427 145 145 0 2433 0
[pid=17855] vsize: 10312
Current children cumulated CPU time (s) 409.81
Current children cumulated vsize (Kb) 12436

[startup+420.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2535 0 2 0 41960 18 0 0 25 0 1 0 1783025160 10952704 2524 4294967295 134512640 135094434 3221224432 3221222992 134550333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2674 2524 145 145 0 2529 0
[pid=17855] vsize: 10696
Current children cumulated CPU time (s) 419.8
Current children cumulated vsize (Kb) 12820

[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2574 0 2 0 42960 19 0 0 25 0 1 0 1783025160 11141120 2563 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2720 2563 145 145 0 2575 0
[pid=17855] vsize: 10880
Current children cumulated CPU time (s) 429.81
Current children cumulated vsize (Kb) 13004

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2580 0 2 0 43960 19 0 0 25 0 1 0 1783025160 11169792 2569 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2727 2569 145 145 0 2582 0
[pid=17855] vsize: 10908
Current children cumulated CPU time (s) 439.81
Current children cumulated vsize (Kb) 13032

[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2583 0 2 0 44960 19 0 0 25 0 1 0 1783025160 11169792 2572 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2727 2572 145 145 0 2582 0
[pid=17855] vsize: 10908
Current children cumulated CPU time (s) 449.81
Current children cumulated vsize (Kb) 13032

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.95 3/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2603 0 2 0 45960 19 0 0 25 0 1 0 1783025160 11272192 2592 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2752 2592 145 145 0 2607 0
[pid=17855] vsize: 11008
Current children cumulated CPU time (s) 459.81
Current children cumulated vsize (Kb) 13132

[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2608 0 2 0 46960 19 0 0 25 0 1 0 1783025160 11304960 2597 4294967295 134512640 135094434 3221224432 3221223024 134551925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2760 2597 145 145 0 2615 0
[pid=17855] vsize: 11040
Current children cumulated CPU time (s) 469.81
Current children cumulated vsize (Kb) 13164

[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2613 0 2 0 47961 19 0 0 25 0 1 0 1783025160 11337728 2602 4294967295 134512640 135094434 3221224432 3221222188 134563367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2768 2602 145 145 0 2623 0
[pid=17855] vsize: 11072
Current children cumulated CPU time (s) 479.82
Current children cumulated vsize (Kb) 13196

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2680 0 2 0 48960 19 0 0 25 0 1 0 1783025160 11644928 2669 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2843 2669 145 145 0 2698 0
[pid=17855] vsize: 11372
Current children cumulated CPU time (s) 489.81
Current children cumulated vsize (Kb) 13496

[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2680 0 2 0 49961 19 0 0 25 0 1 0 1783025160 11644928 2669 4294967295 134512640 135094434 3221224432 3221223024 134551997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2843 2669 145 145 0 2698 0
[pid=17855] vsize: 11372
Current children cumulated CPU time (s) 499.82
Current children cumulated vsize (Kb) 13496

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2680 0 2 0 50961 19 0 0 25 0 1 0 1783025160 11644928 2669 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2843 2669 145 145 0 2698 0
[pid=17855] vsize: 11372
Current children cumulated CPU time (s) 509.82
Current children cumulated vsize (Kb) 13496

[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2681 0 2 0 51961 19 0 0 25 0 1 0 1783025160 11644928 2670 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2843 2670 145 145 0 2698 0
[pid=17855] vsize: 11372
Current children cumulated CPU time (s) 519.82
Current children cumulated vsize (Kb) 13496

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 52961 19 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0
[pid=17855] vsize: 11432
Current children cumulated CPU time (s) 529.82
Current children cumulated vsize (Kb) 13556

[startup+540.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 53961 19 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0
[pid=17855] vsize: 11432
Current children cumulated CPU time (s) 539.82
Current children cumulated vsize (Kb) 13556

[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 54961 20 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0
[pid=17855] vsize: 11432
Current children cumulated CPU time (s) 549.83
Current children cumulated vsize (Kb) 13556

[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 55960 21 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0
[pid=17855] vsize: 11432
Current children cumulated CPU time (s) 559.83
Current children cumulated vsize (Kb) 13556

[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 56961 21 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0
[pid=17855] vsize: 11432
Current children cumulated CPU time (s) 569.84
Current children cumulated vsize (Kb) 13556

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 57961 21 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0
[pid=17855] vsize: 11432
Current children cumulated CPU time (s) 579.84
Current children cumulated vsize (Kb) 13556

[startup+590.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2697 0 2 0 58961 21 0 0 25 0 1 0 1783025160 11739136 2686 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2866 2686 145 145 0 2721 0
[pid=17855] vsize: 11464
Current children cumulated CPU time (s) 589.84
Current children cumulated vsize (Kb) 13588

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2709 0 2 0 59961 21 0 0 25 0 1 0 1783025160 11788288 2698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2878 2698 145 145 0 2733 0
[pid=17855] vsize: 11512
Current children cumulated CPU time (s) 599.84
Current children cumulated vsize (Kb) 13636

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2711 0 2 0 60961 21 0 0 25 0 1 0 1783025160 11808768 2700 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2883 2700 145 145 0 2738 0
[pid=17855] vsize: 11532
Current children cumulated CPU time (s) 609.84
Current children cumulated vsize (Kb) 13656

[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2711 0 2 0 61961 21 0 0 25 0 1 0 1783025160 11808768 2700 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2883 2700 145 145 0 2738 0
[pid=17855] vsize: 11532
Current children cumulated CPU time (s) 619.84
Current children cumulated vsize (Kb) 13656

[startup+630.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2721 0 2 0 62960 22 0 0 25 0 1 0 1783025160 11874304 2710 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 2899 2710 145 145 0 2754 0
[pid=17855] vsize: 11596
Current children cumulated CPU time (s) 629.84
Current children cumulated vsize (Kb) 13720

[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2917 0 2 0 63959 22 0 0 25 0 1 0 1783025160 12709888 2906 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3103 2906 145 145 0 2958 0
[pid=17855] vsize: 12412
Current children cumulated CPU time (s) 639.83
Current children cumulated vsize (Kb) 14536

[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2940 0 2 0 64959 22 0 0 25 0 1 0 1783025160 12804096 2929 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3126 2929 145 145 0 2981 0
[pid=17855] vsize: 12504
Current children cumulated CPU time (s) 649.83
Current children cumulated vsize (Kb) 14628

[startup+660.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2972 0 2 0 65958 22 0 0 25 0 1 0 1783025160 12959744 2961 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3164 2961 145 145 0 3019 0
[pid=17855] vsize: 12656
Current children cumulated CPU time (s) 659.82
Current children cumulated vsize (Kb) 14780

[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2978 0 2 0 66958 22 0 0 25 0 1 0 1783025160 12992512 2967 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3172 2967 145 145 0 3027 0
[pid=17855] vsize: 12688
Current children cumulated CPU time (s) 669.82
Current children cumulated vsize (Kb) 14812

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2986 0 2 0 67959 22 0 0 25 0 1 0 1783025160 13025280 2975 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3180 2975 145 145 0 3035 0
[pid=17855] vsize: 12720
Current children cumulated CPU time (s) 679.83
Current children cumulated vsize (Kb) 14844

[startup+690.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2991 0 2 0 68959 23 0 0 25 0 1 0 1783025160 13058048 2980 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3188 2980 145 145 0 3043 0
[pid=17855] vsize: 12752
Current children cumulated CPU time (s) 689.84
Current children cumulated vsize (Kb) 14876

[startup+700.062 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3009 0 2 0 69959 23 0 0 25 0 1 0 1783025160 13156352 2998 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3212 2998 145 145 0 3067 0
[pid=17855] vsize: 12848
Current children cumulated CPU time (s) 699.84
Current children cumulated vsize (Kb) 14972

[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3009 0 2 0 70959 23 0 0 25 0 1 0 1783025160 13156352 2998 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3212 2998 145 145 0 3067 0
[pid=17855] vsize: 12848
Current children cumulated CPU time (s) 709.84
Current children cumulated vsize (Kb) 14972

[startup+720.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3021 0 2 0 71959 23 0 0 25 0 1 0 1783025160 13221888 3010 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3228 3010 145 145 0 3083 0
[pid=17855] vsize: 12912
Current children cumulated CPU time (s) 719.84
Current children cumulated vsize (Kb) 15036

[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3029 0 2 0 72959 23 0 0 25 0 1 0 1783025160 13254656 3018 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3236 3018 145 145 0 3091 0
[pid=17855] vsize: 12944
Current children cumulated CPU time (s) 729.84
Current children cumulated vsize (Kb) 15068

[startup+740.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3068 0 2 0 73959 23 0 0 25 0 1 0 1783025160 13406208 3057 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3273 3057 145 145 0 3128 0
[pid=17855] vsize: 13092
Current children cumulated CPU time (s) 739.84
Current children cumulated vsize (Kb) 15216

[startup+750.065 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3068 0 2 0 74959 23 0 0 25 0 1 0 1783025160 13406208 3057 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3273 3057 145 145 0 3128 0
[pid=17855] vsize: 13092
Current children cumulated CPU time (s) 749.84
Current children cumulated vsize (Kb) 15216

[startup+760.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3079 0 2 0 75959 23 0 0 25 0 1 0 1783025160 13471744 3068 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3289 3068 145 145 0 3144 0
[pid=17855] vsize: 13156
Current children cumulated CPU time (s) 759.84
Current children cumulated vsize (Kb) 15280

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3079 0 2 0 76959 24 0 0 25 0 1 0 1783025160 13471744 3068 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3289 3068 145 145 0 3144 0
[pid=17855] vsize: 13156
Current children cumulated CPU time (s) 769.85
Current children cumulated vsize (Kb) 15280

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3091 0 2 0 77959 24 0 0 25 0 1 0 1783025160 13520896 3080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3301 3080 145 145 0 3156 0
[pid=17855] vsize: 13204
Current children cumulated CPU time (s) 779.85
Current children cumulated vsize (Kb) 15328

[startup+790.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3099 0 2 0 78959 24 0 0 25 0 1 0 1783025160 13570048 3088 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3313 3088 145 145 0 3168 0
[pid=17855] vsize: 13252
Current children cumulated CPU time (s) 789.85
Current children cumulated vsize (Kb) 15376

[startup+800.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3124 0 2 0 79959 24 0 0 25 0 1 0 1783025160 13684736 3113 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3341 3113 145 145 0 3196 0
[pid=17855] vsize: 13364
Current children cumulated CPU time (s) 799.85
Current children cumulated vsize (Kb) 15488

[startup+810.069 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3143 0 2 0 80960 24 0 0 25 0 1 0 1783025160 13783040 3132 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3365 3132 145 145 0 3220 0
[pid=17855] vsize: 13460
Current children cumulated CPU time (s) 809.86
Current children cumulated vsize (Kb) 15584

[startup+820.069 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3143 0 2 0 81960 24 0 0 25 0 1 0 1783025160 13783040 3132 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3365 3132 145 145 0 3220 0
[pid=17855] vsize: 13460
Current children cumulated CPU time (s) 819.86
Current children cumulated vsize (Kb) 15584

[startup+830.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3165 0 2 0 82960 24 0 0 25 0 1 0 1783025160 13881344 3154 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3389 3154 145 145 0 3244 0
[pid=17855] vsize: 13556
Current children cumulated CPU time (s) 829.86
Current children cumulated vsize (Kb) 15680

[startup+840.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3165 0 2 0 83960 24 0 0 25 0 1 0 1783025160 13881344 3154 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3389 3154 145 145 0 3244 0
[pid=17855] vsize: 13556
Current children cumulated CPU time (s) 839.86
Current children cumulated vsize (Kb) 15680

[startup+850.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3210 0 2 0 84960 24 0 0 25 0 1 0 1783025160 14082048 3199 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3438 3199 145 145 0 3293 0
[pid=17855] vsize: 13752
Current children cumulated CPU time (s) 849.86
Current children cumulated vsize (Kb) 15876

[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3266 0 2 0 85960 25 0 0 25 0 1 0 1783025160 14323712 3255 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3255 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 859.87
Current children cumulated vsize (Kb) 16112

[startup+870.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3268 0 2 0 86960 25 0 0 25 0 1 0 1783025160 14323712 3257 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3257 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 869.87
Current children cumulated vsize (Kb) 16112

[startup+880.074 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 87960 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223104 134555666 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 879.87
Current children cumulated vsize (Kb) 16112

[startup+890.075 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 88960 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 889.87
Current children cumulated vsize (Kb) 16112

[startup+900.075 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 89960 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 899.87
Current children cumulated vsize (Kb) 16112

[startup+910.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 90961 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 909.88
Current children cumulated vsize (Kb) 16112

[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 91961 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 919.88
Current children cumulated vsize (Kb) 16112

[startup+930.077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 92961 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 929.88
Current children cumulated vsize (Kb) 16112

[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 93961 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 939.88
Current children cumulated vsize (Kb) 16112

[startup+950.079 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 94962 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 949.89
Current children cumulated vsize (Kb) 16112

[startup+960.079 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 95962 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 959.89
Current children cumulated vsize (Kb) 16112

[startup+970.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 96962 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 969.89
Current children cumulated vsize (Kb) 16112

[startup+980.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 97962 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 979.89
Current children cumulated vsize (Kb) 16112

[startup+990.082 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 98963 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 989.9
Current children cumulated vsize (Kb) 16112

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 99963 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 999.9
Current children cumulated vsize (Kb) 16112

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 100963 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223104 134555300 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0
[pid=17855] vsize: 13988
Current children cumulated CPU time (s) 1009.9
Current children cumulated vsize (Kb) 16112

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3302 0 2 0 101962 26 0 0 25 0 1 0 1783025160 14446592 3291 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3527 3291 145 145 0 3382 0
[pid=17855] vsize: 14108
Current children cumulated CPU time (s) 1019.9
Current children cumulated vsize (Kb) 16232

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3364 0 2 0 102961 26 0 0 25 0 1 0 1783025160 14749696 3353 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3601 3353 145 145 0 3456 0
[pid=17855] vsize: 14404
Current children cumulated CPU time (s) 1029.89
Current children cumulated vsize (Kb) 16528

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3376 0 2 0 103961 26 0 0 25 0 1 0 1783025160 14798848 3365 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3613 3365 145 145 0 3468 0
[pid=17855] vsize: 14452
Current children cumulated CPU time (s) 1039.89
Current children cumulated vsize (Kb) 16576

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3381 0 2 0 104961 26 0 0 25 0 1 0 1783025160 14831616 3370 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3621 3370 145 145 0 3476 0
[pid=17855] vsize: 14484
Current children cumulated CPU time (s) 1049.89
Current children cumulated vsize (Kb) 16608

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3381 0 2 0 105962 26 0 0 25 0 1 0 1783025160 14831616 3370 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3621 3370 145 145 0 3476 0
[pid=17855] vsize: 14484
Current children cumulated CPU time (s) 1059.9
Current children cumulated vsize (Kb) 16608

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3381 0 2 0 106962 26 0 0 25 0 1 0 1783025160 14831616 3370 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3621 3370 145 145 0 3476 0
[pid=17855] vsize: 14484
Current children cumulated CPU time (s) 1069.9
Current children cumulated vsize (Kb) 16608

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3382 0 2 0 107962 26 0 0 25 0 1 0 1783025160 14831616 3371 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3621 3371 145 145 0 3476 0
[pid=17855] vsize: 14484
Current children cumulated CPU time (s) 1079.9
Current children cumulated vsize (Kb) 16608

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3382 0 2 0 108962 26 0 0 25 0 1 0 1783025160 14831616 3371 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3621 3371 145 145 0 3476 0
[pid=17855] vsize: 14484
Current children cumulated CPU time (s) 1089.9
Current children cumulated vsize (Kb) 16608

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3425 0 2 0 109962 26 0 0 25 0 1 0 1783025160 15011840 3414 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3665 3414 145 145 0 3520 0
[pid=17855] vsize: 14660
Current children cumulated CPU time (s) 1099.9
Current children cumulated vsize (Kb) 16784

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3462 0 2 0 110962 27 0 0 25 0 1 0 1783025160 15159296 3451 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3701 3451 145 145 0 3556 0
[pid=17855] vsize: 14804
Current children cumulated CPU time (s) 1109.91
Current children cumulated vsize (Kb) 16928

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3462 0 2 0 111962 27 0 0 25 0 1 0 1783025160 15159296 3451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3701 3451 145 145 0 3556 0
[pid=17855] vsize: 14804
Current children cumulated CPU time (s) 1119.91
Current children cumulated vsize (Kb) 16928

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3462 0 2 0 112962 27 0 0 25 0 1 0 1783025160 15159296 3451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3701 3451 145 145 0 3556 0
[pid=17855] vsize: 14804
Current children cumulated CPU time (s) 1129.91
Current children cumulated vsize (Kb) 16928

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3462 0 2 0 113963 27 0 0 25 0 1 0 1783025160 15159296 3451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3701 3451 145 145 0 3556 0
[pid=17855] vsize: 14804
Current children cumulated CPU time (s) 1139.92
Current children cumulated vsize (Kb) 16928

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3463 0 2 0 114962 28 0 0 25 0 1 0 1783025160 15163392 3452 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3702 3452 145 145 0 3557 0
[pid=17855] vsize: 14808
Current children cumulated CPU time (s) 1149.92
Current children cumulated vsize (Kb) 16932

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3521 0 2 0 115960 29 0 0 25 0 1 0 1783025160 15400960 3510 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3760 3510 145 145 0 3615 0
[pid=17855] vsize: 15040
Current children cumulated CPU time (s) 1159.91
Current children cumulated vsize (Kb) 17164

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3532 0 2 0 116960 29 0 0 25 0 1 0 1783025160 15466496 3521 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3776 3521 145 145 0 3631 0
[pid=17855] vsize: 15104
Current children cumulated CPU time (s) 1169.91
Current children cumulated vsize (Kb) 17228

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.95 3/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3533 0 2 0 117961 29 0 0 25 0 1 0 1783025160 15470592 3522 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3777 3522 145 145 0 3632 0
[pid=17855] vsize: 15108
Current children cumulated CPU time (s) 1179.92
Current children cumulated vsize (Kb) 17232

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3543 0 2 0 118961 29 0 0 25 0 1 0 1783025160 15532032 3532 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3792 3532 145 145 0 3647 0
[pid=17855] vsize: 15168
Current children cumulated CPU time (s) 1189.92
Current children cumulated vsize (Kb) 17292

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3565 0 2 0 119961 29 0 0 25 0 1 0 1783025160 15626240 3554 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3815 3554 145 145 0 3670 0
[pid=17855] vsize: 15260
Current children cumulated CPU time (s) 1199.92
Current children cumulated vsize (Kb) 17384

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3570 0 2 0 120961 30 0 0 25 0 1 0 1783025160 15659008 3559 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3823 3559 145 145 0 3678 0
[pid=17855] vsize: 15292
Current children cumulated CPU time (s) 1209.93
Current children cumulated vsize (Kb) 17416



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 17855
Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17851/statm): 531 226 485 147 0 384 0
[pid=17851] vsize: 2124
Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3570 0 2 0 120961 30 0 0 25 0 1 0 1783025160 15659008 3559 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17855/statm): 3823 3559 145 145 0 3678 0
[pid=17855] vsize: 15292
Current children cumulated CPU time (s) 1209.93
Current children cumulated vsize (Kb) 17416

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

Child status: 0
Real time (s): 1210.11
CPU time (s): 1209.92
CPU user time (s): 1209.61
CPU system time (s): 0.308953
CPU usage (%): 99.9844
Max. virtual memory (cumulated for all children) (Kb): 17416

Verifier Data

ERROR: no interpretation found !