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-chnl20_30_pb.cnf.cr.opb
MD5SUMafcc4289aafaea265ed2d465965a3342
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 31
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.040993
Number of variables1200
Total number of constraints100
Number of constraints which are clauses60
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint30

Trace number 812

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        717104 kB
Buffers:         35348 kB
Cached:         251616 kB
SwapCached:       1016 kB
Active:          92492 kB
Inactive:       197192 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        716852 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5768 kB
Slab:            22164 kB
Committed_AS:    64340 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:44:15 (client local time) WITH STATUS 0 IN 1209.58 SECONDS
stats: 2352 7 1209.58 0

Solver Data

c Parsing PB file...
c Converting 100 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................
c ---[  39]---> BDD-cost:   57
c ---[  38]---> BDD-cost:   57
c ---[  37]---> BDD-cost:   57
c ---[  36]---> BDD-cost:   57
c ---[  35]---> BDD-cost:   57
c ---[  34]---> BDD-cost:   57
c ---[  33]---> BDD-cost:   57
c ---[  32]---> BDD-cost:   57
c ---[  31]---> BDD-cost:   57
c ---[  30]---> BDD-cost:   57
c ---[  29]---> BDD-cost:   57
c ---[  28]---> BDD-cost:   57
c ---[  27]---> BDD-cost:   57
c ---[  26]---> BDD-cost:   57
c ---[  25]---> BDD-cost:   57
c ---[  24]---> BDD-cost:   57
c ---[  23]---> BDD-cost:   57
c ---[  22]---> BDD-cost:   57
c ---[  21]---> BDD-cost:   57
c ---[  20]---> BDD-cost:   57
c ---[  19]---> BDD-cost:   57
c ---[  18]---> BDD-cost:   57
c ---[  17]---> BDD-cost:   57
c ---[  16]---> BDD-cost:   57
c ---[  15]---> BDD-cost:   57
c ---[  14]---> BDD-cost:   57
c ---[  13]---> BDD-cost:   57
c ---[  12]---> BDD-cost:   57
c ---[  11]---> BDD-cost:   57
c ---[  10]---> BDD-cost:   57
c ---[   9]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   57
c ---[   7]---> BDD-cost:   57
c ---[   6]---> BDD-cost:   57
c ---[   5]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   57
c ---[   3]---> BDD-cost:   57
c ---[   2]---> BDD-cost:   57
c ---[   1]---> BDD-cost:   57
c ---[   0]---> BDD-cost:   57
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5700    15880 |    1900       0        0     nan |  0.000 % |
c |       100 |    5700    15880 |    2090     100     8350    83.5 |  1.149 % |
c |       254 |    5700    15880 |    2299     254    20183    79.5 |  1.149 % |
c |       483 |    5700    15880 |    2528     483    43595    90.3 |  1.150 % |
c |       820 |    5700    15880 |    2781     820    74636    91.0 |  1.149 % |
c |      1326 |    5700    15880 |    3059    1326   152844   115.3 |  1.149 % |
c |      2085 |    5700    15880 |    3365    2085   236742   113.5 |  1.149 % |
c |      3224 |    5700    15880 |    3702    3224   390616   121.2 |  1.149 % |
c |      4934 |    5700    15880 |    4072    2499   282510   113.0 |  1.149 % |
c |      7497 |    5700    15880 |    4480    5062   635699   125.6 |  1.149 % |
c |     11341 |    5700    15880 |    4928    3602   393130   109.1 |  1.149 % |
c |     17107 |    5700    15880 |    5420    3198   429474   134.3 |  1.149 % |
c |     25758 |    5700    15880 |    5963    5184   809083   156.1 |  1.149 % |
c |     38734 |    5700    15880 |    6559    4258   595019   139.7 |  1.149 % |
c |     58195 |    5700    15880 |    7215    4350   474363   109.0 |  1.149 % |
c |     87389 |    5700    15880 |    7936    5401   906885   167.9 |  1.149 % |
c |    131180 |    5700    15880 |    8730    8927  1807067   202.4 |  1.150 % |
c |    196867 |    5700    15880 |    9603    7833  1793666   229.0 |  1.149 % |
c |    295396 |    5700    15880 |   10563    5671   840337   148.2 |  1.149 % |
c |    443189 |    5700    15880 |   11620    8324  1522755   182.9 |  1.149 % |
c |    664881 |    5700    15880 |   12782    7923  1541577   194.6 |  1.149 % |

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/11836/stat): 11836 (minisat+_script) R 11835 11836 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841190087 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/11836/statm): 174 3 169 147 0 27 0
[pid=11836] 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=11837
New process pid=11838
New process pid=11839
execve syscall for /bin/sed executable
One traced child (pid=11838) 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=11839) exited with status: 0
One traced child (pid=11837) exited with status: 0
New process pid=11840
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-chnl20_30_pb.cnf.cr.opb

[startup+10.006 s]
Raw data (loadavg): 0.93 0.98 0.96 2/58 11840
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1258 0 3 0 966 7 0 0 25 0 1 0 1841190092 5480448 1248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 1338 1248 145 145 0 1193 0
[pid=11840] vsize: 5352
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 7476

[startup+20.0069 s]
Raw data (loadavg): 0.94 0.98 0.96 2/58 11840
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1617 0 3 0 1962 9 0 0 25 0 1 0 1841190092 6971392 1607 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 1702 1607 145 145 0 1557 0
[pid=11840] vsize: 6808
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 8932

[startup+30.0078 s]
Raw data (loadavg): 0.95 0.98 0.96 2/58 11842
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1747 0 3 0 2959 10 0 0 25 0 1 0 1841190092 7516160 1737 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 1835 1737 145 145 0 1690 0
[pid=11840] vsize: 7340
Current children cumulated CPU time (s) 29.71
Current children cumulated vsize (Kb) 9464

[startup+40.0087 s]
Raw data (loadavg): 0.96 0.98 0.96 2/58 11842
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1881 0 3 0 3958 11 0 0 25 0 1 0 1841190092 8085504 1871 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 1974 1871 145 145 0 1829 0
[pid=11840] vsize: 7896
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 10020

[startup+50.0097 s]
Raw data (loadavg): 0.96 0.98 0.96 2/58 11842
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1913 0 3 0 4958 11 0 0 25 0 1 0 1841190092 8241152 1903 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2012 1903 145 145 0 1867 0
[pid=11840] vsize: 8048
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 10172

[startup+60.0106 s]
Raw data (loadavg): 0.97 0.98 0.96 2/58 11842
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1939 0 3 0 5958 12 0 0 25 0 1 0 1841190092 8372224 1929 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2044 1929 145 145 0 1899 0
[pid=11840] vsize: 8176
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 10300

[startup+70.0115 s]
Raw data (loadavg): 0.97 0.98 0.96 2/58 11842
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2138 0 3 0 6956 12 0 0 25 0 1 0 1841190092 9224192 2128 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2252 2128 145 145 0 2107 0
[pid=11840] vsize: 9008
Current children cumulated CPU time (s) 69.7
Current children cumulated vsize (Kb) 11132

[startup+80.0125 s]
Raw data (loadavg): 0.98 0.98 0.96 2/58 11842
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2325 0 3 0 7953 13 0 0 25 0 1 0 1841190092 9998336 2315 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2441 2315 145 145 0 2296 0
[pid=11840] vsize: 9764
Current children cumulated CPU time (s) 79.68
Current children cumulated vsize (Kb) 11888

[startup+90.0134 s]
Raw data (loadavg): 0.98 0.98 0.96 2/58 11844
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2361 0 3 0 8953 14 0 0 25 0 1 0 1841190092 10162176 2351 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2481 2351 145 145 0 2336 0
[pid=11840] vsize: 9924
Current children cumulated CPU time (s) 89.69
Current children cumulated vsize (Kb) 12048

[startup+100.014 s]
Raw data (loadavg): 0.98 0.98 0.96 2/58 11844
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2741 0 3 0 9948 16 0 0 25 0 1 0 1841190092 11722752 2731 4294967295 134512640 135094434 3221224432 3221223088 134558129 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2862 2731 145 145 0 2717 0
[pid=11840] vsize: 11448
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 13572

[startup+110.016 s]
Raw data (loadavg): 0.98 0.98 0.96 2/58 11844
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2781 0 3 0 10948 16 0 0 25 0 1 0 1841190092 11902976 2771 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2906 2771 145 145 0 2761 0
[pid=11840] vsize: 11624
Current children cumulated CPU time (s) 109.66
Current children cumulated vsize (Kb) 13748

[startup+120.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11844
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2863 0 3 0 11947 17 0 0 25 0 1 0 1841190092 12251136 2853 4294967295 134512640 135094434 3221224432 3221223104 134555291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2991 2853 145 145 0 2846 0
[pid=11840] vsize: 11964
Current children cumulated CPU time (s) 119.66
Current children cumulated vsize (Kb) 14088

[startup+130.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11844
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2863 0 3 0 12947 17 0 0 25 0 1 0 1841190092 12251136 2853 4294967295 134512640 135094434 3221224432 3221223104 134556426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 2991 2853 145 145 0 2846 0
[pid=11840] vsize: 11964
Current children cumulated CPU time (s) 129.66
Current children cumulated vsize (Kb) 14088

[startup+140.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11844
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2918 0 3 0 13947 18 0 0 25 0 1 0 1841190092 12480512 2908 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 3047 2908 145 145 0 2902 0
[pid=11840] vsize: 12188
Current children cumulated CPU time (s) 139.67
Current children cumulated vsize (Kb) 14312

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11846
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3251 0 3 0 14943 19 0 0 25 0 1 0 1841190092 13856768 3241 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 3383 3241 145 145 0 3238 0
[pid=11840] vsize: 13532
Current children cumulated CPU time (s) 149.64
Current children cumulated vsize (Kb) 15656

[startup+160.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11846
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3486 0 3 0 15940 21 0 0 25 0 1 0 1841190092 14839808 3476 4294967295 134512640 135094434 3221224432 3221223024 134785070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 3623 3476 145 145 0 3478 0
[pid=11840] vsize: 14492
Current children cumulated CPU time (s) 159.63
Current children cumulated vsize (Kb) 16616

[startup+170.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11846
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3707 0 3 0 16934 23 0 0 25 0 1 0 1841190092 15749120 3697 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 3845 3697 145 145 0 3700 0
[pid=11840] vsize: 15380
Current children cumulated CPU time (s) 169.59
Current children cumulated vsize (Kb) 17504

[startup+180.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11846
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3840 0 3 0 17932 24 0 0 25 0 1 0 1841190092 16322560 3830 4294967295 134512640 135094434 3221224432 3221223024 134557336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 3985 3830 145 145 0 3840 0
[pid=11840] vsize: 15940
Current children cumulated CPU time (s) 179.58
Current children cumulated vsize (Kb) 18064

[startup+190.024 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11846
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3867 0 3 0 18931 25 0 0 25 0 1 0 1841190092 16433152 3857 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4012 3857 145 145 0 3867 0
[pid=11840] vsize: 16048
Current children cumulated CPU time (s) 189.58
Current children cumulated vsize (Kb) 18172

[startup+200.025 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11846
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3868 0 3 0 19931 25 0 0 25 0 1 0 1841190092 16433152 3858 4294967295 134512640 135094434 3221224432 3221223024 134551885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4012 3858 145 145 0 3867 0
[pid=11840] vsize: 16048
Current children cumulated CPU time (s) 199.58
Current children cumulated vsize (Kb) 18172

[startup+210.026 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11848
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3886 0 3 0 20930 26 0 0 25 0 1 0 1841190092 16531456 3876 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4036 3876 145 145 0 3891 0
[pid=11840] vsize: 16144
Current children cumulated CPU time (s) 209.58
Current children cumulated vsize (Kb) 18268

[startup+220.027 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11848
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3892 0 3 0 21930 26 0 0 25 0 1 0 1841190092 16564224 3882 4294967295 134512640 135094434 3221224432 3221222976 134779266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4044 3882 145 145 0 3899 0
[pid=11840] vsize: 16176
Current children cumulated CPU time (s) 219.58
Current children cumulated vsize (Kb) 18300

[startup+230.027 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11848
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3892 0 3 0 22929 27 0 0 25 0 1 0 1841190092 16564224 3882 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4044 3882 145 145 0 3899 0
[pid=11840] vsize: 16176
Current children cumulated CPU time (s) 229.58
Current children cumulated vsize (Kb) 18300

[startup+240.028 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11848
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4045 0 3 0 23927 28 0 0 25 0 1 0 1841190092 17203200 4035 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4200 4035 145 145 0 4055 0
[pid=11840] vsize: 16800
Current children cumulated CPU time (s) 239.57
Current children cumulated vsize (Kb) 18924

[startup+250.029 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11848
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4075 0 3 0 24927 28 0 0 25 0 1 0 1841190092 17342464 4065 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4234 4065 145 145 0 4089 0
[pid=11840] vsize: 16936
Current children cumulated CPU time (s) 249.57
Current children cumulated vsize (Kb) 19060

[startup+260.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11848
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4222 0 3 0 25925 29 0 0 25 0 1 0 1841190092 17960960 4212 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4212 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 259.56
Current children cumulated vsize (Kb) 19664

[startup+270.032 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11850
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4223 0 3 0 26924 30 0 0 25 0 1 0 1841190092 17960960 4213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4213 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 269.56
Current children cumulated vsize (Kb) 19664

[startup+280.033 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11850
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4223 0 3 0 27923 30 0 0 25 0 1 0 1841190092 17960960 4213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4213 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 279.55
Current children cumulated vsize (Kb) 19664

[startup+290.035 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11850
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4224 0 3 0 28923 31 0 0 25 0 1 0 1841190092 17960960 4214 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4214 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 289.56
Current children cumulated vsize (Kb) 19664

[startup+300.036 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11850
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4224 0 3 0 29922 32 0 0 25 0 1 0 1841190092 17960960 4214 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4214 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 299.56
Current children cumulated vsize (Kb) 19664

[startup+310.037 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11850
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4226 0 3 0 30922 32 0 0 25 0 1 0 1841190092 17960960 4216 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4216 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 309.56
Current children cumulated vsize (Kb) 19664

[startup+320.038 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11850
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 31922 32 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 319.56
Current children cumulated vsize (Kb) 19664

[startup+330.039 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11852
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 32921 33 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 329.56
Current children cumulated vsize (Kb) 19664

[startup+340.04 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11852
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 33921 33 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 339.56
Current children cumulated vsize (Kb) 19664

[startup+350.041 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11852
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 34920 34 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 19664

[startup+360.043 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11852
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 35920 34 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 19664

[startup+370.044 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11852
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 36920 35 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 369.57
Current children cumulated vsize (Kb) 19664

[startup+380.044 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11852
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 37919 35 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 379.56
Current children cumulated vsize (Kb) 19664

[startup+390.045 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11854
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 38918 36 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 389.56
Current children cumulated vsize (Kb) 19664

[startup+400.046 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11854
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 39918 36 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 399.56
Current children cumulated vsize (Kb) 19664

[startup+410.048 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11854
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 40917 37 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 409.56
Current children cumulated vsize (Kb) 19664

[startup+420.049 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11854
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 41917 37 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 419.56
Current children cumulated vsize (Kb) 19664

[startup+430.05 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11854
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 42916 38 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 429.56
Current children cumulated vsize (Kb) 19664

[startup+440.052 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11854
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 43916 38 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 439.56
Current children cumulated vsize (Kb) 19664

[startup+450.053 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11856
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 44915 39 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 449.56
Current children cumulated vsize (Kb) 19664

[startup+460.055 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11856
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 45915 39 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 459.56
Current children cumulated vsize (Kb) 19664

[startup+470.056 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11856
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 46915 40 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 469.57
Current children cumulated vsize (Kb) 19664

[startup+480.057 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11856
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 47915 40 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 479.57
Current children cumulated vsize (Kb) 19664

[startup+490.059 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11856
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 48914 40 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 489.56
Current children cumulated vsize (Kb) 19664

[startup+500.06 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11856
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 49914 40 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0
[pid=11840] vsize: 17540
Current children cumulated CPU time (s) 499.56
Current children cumulated vsize (Kb) 19664

[startup+510.06 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11858
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4229 0 3 0 50915 40 0 0 25 0 1 0 1841190092 17965056 4219 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4386 4219 145 145 0 4241 0
[pid=11840] vsize: 17544
Current children cumulated CPU time (s) 509.57
Current children cumulated vsize (Kb) 19668

[startup+520.061 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11858
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4290 0 3 0 51914 41 0 0 25 0 1 0 1841190092 18214912 4280 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4447 4280 145 145 0 4302 0
[pid=11840] vsize: 17788
Current children cumulated CPU time (s) 519.57
Current children cumulated vsize (Kb) 19912

[startup+530.062 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11858
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4291 0 3 0 52913 41 0 0 25 0 1 0 1841190092 18214912 4281 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4447 4281 145 145 0 4302 0
[pid=11840] vsize: 17788
Current children cumulated CPU time (s) 529.56
Current children cumulated vsize (Kb) 19912

[startup+540.063 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11858
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4291 0 3 0 53913 42 0 0 25 0 1 0 1841190092 18214912 4281 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4447 4281 145 145 0 4302 0
[pid=11840] vsize: 17788
Current children cumulated CPU time (s) 539.57
Current children cumulated vsize (Kb) 19912

[startup+550.064 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11858
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4291 0 3 0 54912 42 0 0 25 0 1 0 1841190092 18214912 4281 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4447 4281 145 145 0 4302 0
[pid=11840] vsize: 17788
Current children cumulated CPU time (s) 549.56
Current children cumulated vsize (Kb) 19912

[startup+560.066 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11858
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4291 0 3 0 55912 42 0 0 25 0 1 0 1841190092 18214912 4281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4447 4281 145 145 0 4302 0
[pid=11840] vsize: 17788
Current children cumulated CPU time (s) 559.56
Current children cumulated vsize (Kb) 19912

[startup+570.067 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11862
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4295 0 3 0 56913 42 0 0 25 0 1 0 1841190092 18239488 4285 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4453 4285 145 145 0 4308 0
[pid=11840] vsize: 17812
Current children cumulated CPU time (s) 569.57
Current children cumulated vsize (Kb) 19936

[startup+580.068 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11862
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4295 0 3 0 57913 42 0 0 25 0 1 0 1841190092 18239488 4285 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4453 4285 145 145 0 4308 0
[pid=11840] vsize: 17812
Current children cumulated CPU time (s) 579.57
Current children cumulated vsize (Kb) 19936

[startup+590.069 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11862
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4306 0 3 0 58913 42 0 0 25 0 1 0 1841190092 18305024 4296 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4469 4296 145 145 0 4324 0
[pid=11840] vsize: 17876
Current children cumulated CPU time (s) 589.57
Current children cumulated vsize (Kb) 20000

[startup+600.07 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11862
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4313 0 3 0 59913 42 0 0 25 0 1 0 1841190092 18337792 4303 4294967295 134512640 135094434 3221224432 3221223024 134551876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4477 4303 145 145 0 4332 0
[pid=11840] vsize: 17908
Current children cumulated CPU time (s) 599.57
Current children cumulated vsize (Kb) 20032

[startup+610.071 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11862
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4313 0 3 0 60914 42 0 0 25 0 1 0 1841190092 18337792 4303 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4477 4303 145 145 0 4332 0
[pid=11840] vsize: 17908
Current children cumulated CPU time (s) 609.58
Current children cumulated vsize (Kb) 20032

[startup+620.072 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11862
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4350 0 3 0 61913 43 0 0 25 0 1 0 1841190092 18509824 4340 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4519 4340 145 145 0 4374 0
[pid=11840] vsize: 18076
Current children cumulated CPU time (s) 619.58
Current children cumulated vsize (Kb) 20200

[startup+630.073 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11866
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4414 0 3 0 62912 44 0 0 25 0 1 0 1841190092 18796544 4404 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4589 4404 145 145 0 4444 0
[pid=11840] vsize: 18356
Current children cumulated CPU time (s) 629.58
Current children cumulated vsize (Kb) 20480

[startup+640.074 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11866
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4425 0 3 0 63912 44 0 0 25 0 1 0 1841190092 18862080 4415 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4605 4415 145 145 0 4460 0
[pid=11840] vsize: 18420
Current children cumulated CPU time (s) 639.58
Current children cumulated vsize (Kb) 20544

[startup+650.074 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11866
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4425 0 3 0 64912 44 0 0 25 0 1 0 1841190092 18862080 4415 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4605 4415 145 145 0 4460 0
[pid=11840] vsize: 18420
Current children cumulated CPU time (s) 649.58
Current children cumulated vsize (Kb) 20544

[startup+660.076 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11866
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4431 0 3 0 65912 44 0 0 25 0 1 0 1841190092 18894848 4421 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4613 4421 145 145 0 4468 0
[pid=11840] vsize: 18452
Current children cumulated CPU time (s) 659.58
Current children cumulated vsize (Kb) 20576

[startup+670.076 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11866
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4437 0 3 0 66913 44 0 0 25 0 1 0 1841190092 18927616 4427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4621 4427 145 145 0 4476 0
[pid=11840] vsize: 18484
Current children cumulated CPU time (s) 669.59
Current children cumulated vsize (Kb) 20608

[startup+680.077 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11866
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4531 0 3 0 67911 44 0 0 25 0 1 0 1841190092 19324928 4521 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4718 4521 145 145 0 4573 0
[pid=11840] vsize: 18872
Current children cumulated CPU time (s) 679.57
Current children cumulated vsize (Kb) 20996

[startup+690.078 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11868
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4544 0 3 0 68911 44 0 0 25 0 1 0 1841190092 19390464 4534 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4734 4534 145 145 0 4589 0
[pid=11840] vsize: 18936
Current children cumulated CPU time (s) 689.57
Current children cumulated vsize (Kb) 21060

[startup+700.079 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11868
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4544 0 3 0 69911 45 0 0 25 0 1 0 1841190092 19390464 4534 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4734 4534 145 145 0 4589 0
[pid=11840] vsize: 18936
Current children cumulated CPU time (s) 699.58
Current children cumulated vsize (Kb) 21060

[startup+710.08 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11868
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4651 0 3 0 70910 45 0 0 25 0 1 0 1841190092 19832832 4641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4842 4641 145 145 0 4697 0
[pid=11840] vsize: 19368
Current children cumulated CPU time (s) 709.57
Current children cumulated vsize (Kb) 21492

[startup+720.081 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11868
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4653 0 3 0 71910 45 0 0 25 0 1 0 1841190092 19832832 4643 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4842 4643 145 145 0 4697 0
[pid=11840] vsize: 19368
Current children cumulated CPU time (s) 719.57
Current children cumulated vsize (Kb) 21492

[startup+730.082 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11868
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4653 0 3 0 72910 45 0 0 25 0 1 0 1841190092 19832832 4643 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 4842 4643 145 145 0 4697 0
[pid=11840] vsize: 19368
Current children cumulated CPU time (s) 729.57
Current children cumulated vsize (Kb) 21492

[startup+740.084 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11868
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4655 0 3 0 73909 45 0 0 25 0 1 0 1841190092 19845120 4645 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4845 4645 145 145 0 4700 0
[pid=11840] vsize: 19380
Current children cumulated CPU time (s) 739.56
Current children cumulated vsize (Kb) 21504

[startup+750.085 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11870
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4668 0 3 0 74909 45 0 0 25 0 1 0 1841190092 19910656 4658 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4861 4658 145 145 0 4716 0
[pid=11840] vsize: 19444
Current children cumulated CPU time (s) 749.56
Current children cumulated vsize (Kb) 21568

[startup+760.086 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11870
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4690 0 3 0 75909 46 0 0 25 0 1 0 1841190092 20008960 4680 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4885 4680 145 145 0 4740 0
[pid=11840] vsize: 19540
Current children cumulated CPU time (s) 759.57
Current children cumulated vsize (Kb) 21664

[startup+770.087 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11870
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4707 0 3 0 76909 46 0 0 25 0 1 0 1841190092 20107264 4697 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4909 4697 145 145 0 4764 0
[pid=11840] vsize: 19636
Current children cumulated CPU time (s) 769.57
Current children cumulated vsize (Kb) 21760

[startup+780.087 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11870
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4712 0 3 0 77909 46 0 0 25 0 1 0 1841190092 20140032 4702 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4917 4702 145 145 0 4772 0
[pid=11840] vsize: 19668
Current children cumulated CPU time (s) 779.57
Current children cumulated vsize (Kb) 21792

[startup+790.088 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11870
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4714 0 3 0 78910 46 0 0 25 0 1 0 1841190092 20140032 4704 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4917 4704 145 145 0 4772 0
[pid=11840] vsize: 19668
Current children cumulated CPU time (s) 789.58
Current children cumulated vsize (Kb) 21792

[startup+800.088 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11870
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4714 0 3 0 79910 46 0 0 25 0 1 0 1841190092 20140032 4704 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4917 4704 145 145 0 4772 0
[pid=11840] vsize: 19668
Current children cumulated CPU time (s) 799.58
Current children cumulated vsize (Kb) 21792

[startup+810.089 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11872
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4715 0 3 0 80909 47 0 0 25 0 1 0 1841190092 20140032 4705 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4917 4705 145 145 0 4772 0
[pid=11840] vsize: 19668
Current children cumulated CPU time (s) 809.58
Current children cumulated vsize (Kb) 21792

[startup+820.09 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11872
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4715 0 3 0 81909 47 0 0 25 0 1 0 1841190092 20140032 4705 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4917 4705 145 145 0 4772 0
[pid=11840] vsize: 19668
Current children cumulated CPU time (s) 819.58
Current children cumulated vsize (Kb) 21792

[startup+830.091 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11872
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4723 0 3 0 82909 48 0 0 25 0 1 0 1841190092 20172800 4713 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4925 4713 145 145 0 4780 0
[pid=11840] vsize: 19700
Current children cumulated CPU time (s) 829.59
Current children cumulated vsize (Kb) 21824

[startup+840.092 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11872
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4723 0 3 0 83909 48 0 0 25 0 1 0 1841190092 20172800 4713 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4925 4713 145 145 0 4780 0
[pid=11840] vsize: 19700
Current children cumulated CPU time (s) 839.59
Current children cumulated vsize (Kb) 21824

[startup+850.093 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11872
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4741 0 3 0 84908 48 0 0 25 0 1 0 1841190092 20303872 4731 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4957 4731 145 145 0 4812 0
[pid=11840] vsize: 19828
Current children cumulated CPU time (s) 849.58
Current children cumulated vsize (Kb) 21952

[startup+860.095 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11872
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4742 0 3 0 85909 48 0 0 25 0 1 0 1841190092 20303872 4732 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4957 4732 145 145 0 4812 0
[pid=11840] vsize: 19828
Current children cumulated CPU time (s) 859.59
Current children cumulated vsize (Kb) 21952

[startup+870.096 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11874
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4752 0 3 0 86908 49 0 0 25 0 1 0 1841190092 20336640 4742 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4965 4742 145 145 0 4820 0
[pid=11840] vsize: 19860
Current children cumulated CPU time (s) 869.59
Current children cumulated vsize (Kb) 21984

[startup+880.097 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11874
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4776 0 3 0 87908 49 0 0 25 0 1 0 1841190092 20443136 4766 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 4991 4766 145 145 0 4846 0
[pid=11840] vsize: 19964
Current children cumulated CPU time (s) 879.59
Current children cumulated vsize (Kb) 22088

[startup+890.098 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11874
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4853 0 3 0 88907 50 0 0 25 0 1 0 1841190092 20787200 4843 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5075 4843 145 145 0 4930 0
[pid=11840] vsize: 20300
Current children cumulated CPU time (s) 889.59
Current children cumulated vsize (Kb) 22424

[startup+900.099 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11874
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4880 0 3 0 89907 50 0 0 25 0 1 0 1841190092 20955136 4870 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5116 4870 145 145 0 4971 0
[pid=11840] vsize: 20464
Current children cumulated CPU time (s) 899.59
Current children cumulated vsize (Kb) 22588

[startup+910.101 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11874
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4895 0 3 0 90907 50 0 0 25 0 1 0 1841190092 21053440 4885 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5140 4885 145 145 0 4995 0
[pid=11840] vsize: 20560
Current children cumulated CPU time (s) 909.59
Current children cumulated vsize (Kb) 22684

[startup+920.102 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11874
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4922 0 3 0 91907 50 0 0 25 0 1 0 1841190092 21184512 4912 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5172 4912 145 145 0 5027 0
[pid=11840] vsize: 20688
Current children cumulated CPU time (s) 919.59
Current children cumulated vsize (Kb) 22812

[startup+930.102 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11876
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4935 0 3 0 92907 50 0 0 25 0 1 0 1841190092 21250048 4925 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5188 4925 145 145 0 5043 0
[pid=11840] vsize: 20752
Current children cumulated CPU time (s) 929.59
Current children cumulated vsize (Kb) 22876

[startup+940.103 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11876
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4935 0 3 0 93907 50 0 0 25 0 1 0 1841190092 21250048 4925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5188 4925 145 145 0 5043 0
[pid=11840] vsize: 20752
Current children cumulated CPU time (s) 939.59
Current children cumulated vsize (Kb) 22876

[startup+950.104 s]
Raw data (loadavg): 0.99 0.98 0.96 3/58 11876
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4936 0 3 0 94907 51 0 0 25 0 1 0 1841190092 21250048 4926 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5188 4926 145 145 0 5043 0
[pid=11840] vsize: 20752
Current children cumulated CPU time (s) 949.6
Current children cumulated vsize (Kb) 22876

[startup+960.104 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11876
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4955 0 3 0 95908 51 0 0 25 0 1 0 1841190092 21348352 4945 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5212 4945 145 145 0 5067 0
[pid=11840] vsize: 20848
Current children cumulated CPU time (s) 959.61
Current children cumulated vsize (Kb) 22972

[startup+970.105 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11876
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5037 0 3 0 96906 52 0 0 25 0 1 0 1841190092 21680128 5027 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5293 5027 145 145 0 5148 0
[pid=11840] vsize: 21172
Current children cumulated CPU time (s) 969.6
Current children cumulated vsize (Kb) 23296

[startup+980.106 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11876
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5171 0 3 0 97904 53 0 0 25 0 1 0 1841190092 22224896 5161 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5426 5161 145 145 0 5281 0
[pid=11840] vsize: 21704
Current children cumulated CPU time (s) 979.59
Current children cumulated vsize (Kb) 23828

[startup+990.107 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11878
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5171 0 3 0 98904 53 0 0 25 0 1 0 1841190092 22224896 5161 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5426 5161 145 145 0 5281 0
[pid=11840] vsize: 21704
Current children cumulated CPU time (s) 989.59
Current children cumulated vsize (Kb) 23828

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11878
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5172 0 3 0 99904 53 0 0 25 0 1 0 1841190092 22224896 5162 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5426 5162 145 145 0 5281 0
[pid=11840] vsize: 21704
Current children cumulated CPU time (s) 999.59
Current children cumulated vsize (Kb) 23828

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11878
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5256 0 3 0 100903 54 0 0 25 0 1 0 1841190092 22568960 5246 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5510 5246 145 145 0 5365 0
[pid=11840] vsize: 22040
Current children cumulated CPU time (s) 1009.59
Current children cumulated vsize (Kb) 24164

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11878
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5272 0 3 0 101903 54 0 0 25 0 1 0 1841190092 22638592 5262 4294967295 134512640 135094434 3221224432 3221223088 134558298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5527 5262 145 145 0 5382 0
[pid=11840] vsize: 22108
Current children cumulated CPU time (s) 1019.59
Current children cumulated vsize (Kb) 24232

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11878
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5566 0 3 0 102898 56 0 0 25 0 1 0 1841190092 23855104 5556 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 5824 5556 145 145 0 5679 0
[pid=11840] vsize: 23296
Current children cumulated CPU time (s) 1029.56
Current children cumulated vsize (Kb) 25420

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11878
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5854 0 3 0 103893 59 0 0 25 0 1 0 1841190092 25047040 5844 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5844 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1039.54
Current children cumulated vsize (Kb) 26584

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11880
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5854 0 3 0 104893 59 0 0 25 0 1 0 1841190092 25047040 5844 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5844 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1049.54
Current children cumulated vsize (Kb) 26584

[startup+1060.12 s]
Raw data (loadavg): 0.99 0.98 0.96 2/58 11880
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5854 0 3 0 105893 59 0 0 25 0 1 0 1841190092 25047040 5844 4294967295 134512640 135094434 3221224432 3221223024 134551918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5844 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1059.54
Current children cumulated vsize (Kb) 26584

[startup+1070.12 s]
Raw data (loadavg): 1.14 1.02 0.97 2/58 11880
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5854 0 3 0 106893 59 0 0 25 0 1 0 1841190092 25047040 5844 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5844 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1069.54
Current children cumulated vsize (Kb) 26584

[startup+1080.12 s]
Raw data (loadavg): 1.12 1.02 0.97 2/58 11880
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5855 0 3 0 107894 59 0 0 25 0 1 0 1841190092 25047040 5845 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5845 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1079.55
Current children cumulated vsize (Kb) 26584

[startup+1090.12 s]
Raw data (loadavg): 1.10 1.01 0.97 2/58 11880
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5855 0 3 0 108894 60 0 0 25 0 1 0 1841190092 25047040 5845 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5845 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1089.56
Current children cumulated vsize (Kb) 26584

[startup+1100.12 s]
Raw data (loadavg): 1.08 1.01 0.97 2/58 11880
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5857 0 3 0 109894 60 0 0 25 0 1 0 1841190092 25047040 5847 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11840/statm): 6115 5847 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1099.56
Current children cumulated vsize (Kb) 26584

[startup+1110.12 s]
Raw data (loadavg): 1.07 1.01 0.97 2/58 11882
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 110893 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1109.55
Current children cumulated vsize (Kb) 26584

[startup+1120.12 s]
Raw data (loadavg): 1.06 1.01 0.97 2/58 11882
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 111893 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1119.55
Current children cumulated vsize (Kb) 26584

[startup+1130.12 s]
Raw data (loadavg): 1.05 1.01 0.97 2/58 11882
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 112894 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1129.56
Current children cumulated vsize (Kb) 26584

[startup+1140.12 s]
Raw data (loadavg): 1.04 1.01 0.97 2/58 11882
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 113894 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1139.56
Current children cumulated vsize (Kb) 26584

[startup+1150.13 s]
Raw data (loadavg): 1.04 1.01 0.97 2/58 11882
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 114894 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1149.56
Current children cumulated vsize (Kb) 26584

[startup+1160.13 s]
Raw data (loadavg): 1.03 1.01 0.97 2/58 11882
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 115894 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1159.56
Current children cumulated vsize (Kb) 26584

[startup+1170.13 s]
Raw data (loadavg): 1.02 1.01 0.97 2/58 11884
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5862 0 3 0 116894 60 0 0 25 0 1 0 1841190092 25047040 5852 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6115 5852 145 145 0 5970 0
[pid=11840] vsize: 24460
Current children cumulated CPU time (s) 1169.56
Current children cumulated vsize (Kb) 26584

[startup+1180.13 s]
Raw data (loadavg): 1.02 1.01 0.97 2/58 11884
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 117894 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0
[pid=11840] vsize: 24520
Current children cumulated CPU time (s) 1179.56
Current children cumulated vsize (Kb) 26644

[startup+1190.13 s]
Raw data (loadavg): 1.02 1.00 0.97 2/58 11884
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 118895 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0
[pid=11840] vsize: 24520
Current children cumulated CPU time (s) 1189.57
Current children cumulated vsize (Kb) 26644

[startup+1200.13 s]
Raw data (loadavg): 1.01 1.00 0.97 2/58 11884
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 119895 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0
[pid=11840] vsize: 24520
Current children cumulated CPU time (s) 1199.57
Current children cumulated vsize (Kb) 26644

[startup+1210.13 s]
Raw data (loadavg): 1.01 1.00 0.97 2/58 11884
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 120895 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0
[pid=11840] vsize: 24520
Current children cumulated CPU time (s) 1209.57
Current children cumulated vsize (Kb) 26644



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 1.01 1.00 0.97 2/58 11884
Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11836/statm): 531 226 485 147 0 384 0
[pid=11836] vsize: 2124
Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 120895 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0
[pid=11840] vsize: 24520
Current children cumulated CPU time (s) 1209.57
Current children cumulated vsize (Kb) 26644

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1209.58
CPU user time (s): 1208.96
CPU system time (s): 0.618905
CPU usage (%): 99.9529
Max. virtual memory (cumulated for all children) (Kb): 26644

Verifier Data

ERROR: no interpretation found !