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/manquinho/logic-synthesis/normalized-f51m.b.opb
MD5SUM4fc22abde8250807abd95442a25fac44
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 18
Optimality of the best value was proved YES
Number of terms in the objective function 407
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 407
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 407
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark99.3649
Number of variables406
Total number of constraints538
Number of constraints which are clauses520
Number of constraints which are cardinality constraints (but not clauses)18
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint123

Trace number 912

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        946448 kB
Buffers:         33752 kB
Cached:          29784 kB
SwapCached:        792 kB
Active:          53964 kB
Inactive:        12276 kB
HighTotal:      131008 kB
HighFree:        97412 kB
LowTotal:       903652 kB
LowFree:        849036 kB
SwapTotal:     2097136 kB
SwapFree:      2095876 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5752 kB
Slab:            16380 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 13:04:58 (client local time) WITH STATUS 10 IN 1209.94 SECONDS
stats: 2411 7 1209.94 10

Solver Data

c Parsing PB file...
c Converting 498 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     498    13351 |     166       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 26
c ---[   0]---> Sorter-cost:14920     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   16604    50904 |    5534       1       18    18.0 |  0.000 % |
c |       101 |   16604    50904 |    6087     101     2898    28.7 |  0.055 % |
c ==============================================================================
c Found solution: 21
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       208 |   16615    50935 |    5538     187    12825    68.6 |  0.055 % |
c |       309 |   16615    50935 |    6091     288    21975    76.3 |  0.192 % |
c |       459 |   16615    50935 |    6700     438    33909    77.4 |  0.192 % |
c |       686 |   16615    50935 |    7371     665    58415    87.8 |  0.192 % |
c |      1029 |   16615    50935 |    8108    1008    95310    94.6 |  0.192 % |
c |      1536 |   16615    50935 |    8919    1515   138105    91.2 |  0.192 % |
c ==============================================================================
c Found solution: 19
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1913 |   16410    50460 |    5470    1862   174770    93.9 |  0.192 % |
c |      2013 |   16410    50460 |    6017    1962   183811    93.7 |  1.618 % |
c |      2163 |   16402    50444 |    6618    2111   189584    89.8 |  1.655 % |
c |      2388 |   16402    50444 |    7280    2336   201318    86.2 |  1.655 % |
c |      2726 |   16402    50444 |    8008    2674   217793    81.4 |  1.655 % |
c |      3232 |   16402    50444 |    8809    3180   247166    77.7 |  1.655 % |
c |      3992 |   16402    50444 |    9690    3940   279064    70.8 |  1.655 % |
c |      5131 |   16402    50444 |   10659    5079   327949    64.6 |  1.655 % |
c |      6839 |   16402    50444 |   11725    6787   409251    60.3 |  1.655 % |
c |      9401 |   16402    50444 |   12897    9349   513437    54.9 |  1.655 % |
c |     13245 |   16402    50444 |   14187   13193   698978    53.0 |  1.655 % |
c |     19011 |   16402    50444 |   15606   11519   497107    43.2 |  1.655 % |
c |     27660 |   16402    50444 |   17167   12053   609989    50.6 |  1.655 % |
c ==============================================================================
c Found solution: 18
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33376 |   16414    50475 |    5471   17769   928999    52.3 |  1.655 % |
c |     33478 |   16414    50475 |    6018    4545   221744    48.8 |  1.663 % |
c |     33628 |   16414    50475 |    6619    4695   229759    48.9 |  1.663 % |
c |     33855 |   16414    50475 |    7281    4922   240660    48.9 |  1.663 % |
c |     34192 |   16414    50475 |    8010    5259   254469    48.4 |  1.663 % |
c |     34700 |   16414    50475 |    8811    5767   274708    47.6 |  1.663 % |
c |     35461 |   16414    50475 |    9692    6528   308203    47.2 |  1.663 % |
c |     36601 |   16414    50475 |   10661    7668   361716    47.2 |  1.663 % |
c |     38309 |   16414    50475 |   11727    9376   425326    45.4 |  1.663 % |
c |     40871 |   16414    50475 |   12900   11938   539786    45.2 |  1.663 % |
c |     44717 |   16414    50475 |   14190    9168   330073    36.0 |  1.663 % |
c |     50487 |   16414    50475 |   15609    7682   245410    31.9 |  1.663 % |
c |     59136 |   16414    50475 |   17170    8283   287557    34.7 |  1.663 % |
c |     72111 |   16414    50475 |   18887   12406   433973    35.0 |  1.663 % |
c |     91574 |   16414    50475 |   20776   12488   450296    36.1 |  1.663 % |
c |    120768 |   16414    50475 |   22853   20303   750005    36.9 |  1.663 % |
c |    164558 |   16414    50475 |   25139   17290   577512    33.4 |  1.663 % |
c |    230246 |   16414    50475 |   27653   18531   543896    29.4 |  1.663 % |
c |    328772 |   16414    50475 |   30418   14118   592755    42.0 |  1.663 % |
c |    476561 |   16414    50475 |   33460   30736  1029565    33.5 |  1.663 % |

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/29832/stat): 29832 (minisat+_script) R 29831 29832 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1769561544 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/29832/statm): 174 3 169 147 0 27 0
[pid=29832] 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=29833
New process pid=29834
New process pid=29835
execve syscall for /bin/sed executable
One traced child (pid=29834) 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=29835) exited with status: 0
One traced child (pid=29833) exited with status: 0
New process pid=29836
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-f51m.b.opb

[startup+10.0042 s]
Raw data (loadavg): 0.94 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 1440 0 0 0 980 7 0 0 25 0 1 0 1769561549 6647808 1423 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 1623 1423 145 145 0 1478 0
[pid=29836] vsize: 6492
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 8616

[startup+20.005 s]
Raw data (loadavg): 0.95 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) T 29832 29832 27660 0 -1 0 1708 0 0 0 1975 9 0 0 25 0 1 0 1769561549 7766016 1691 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29836/statm): 1896 1691 145 145 0 1751 0
[pid=29836] vsize: 7584
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 9708

[startup+30.0068 s]
Raw data (loadavg): 0.95 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 1979 0 0 0 2969 11 0 0 25 0 1 0 1769561549 8867840 1962 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2165 1962 145 145 0 2020 0
[pid=29836] vsize: 8660
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 10784

[startup+40.0076 s]
Raw data (loadavg): 0.96 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 1990 0 0 0 3969 11 0 0 25 0 1 0 1769561549 8937472 1973 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2182 1973 145 145 0 2037 0
[pid=29836] vsize: 8728
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 10852

[startup+50.0094 s]
Raw data (loadavg): 0.97 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2009 0 0 0 4969 11 0 0 25 0 1 0 1769561549 9031680 1992 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2205 1992 145 145 0 2060 0
[pid=29836] vsize: 8820
Current children cumulated CPU time (s) 49.82
Current children cumulated vsize (Kb) 10944

[startup+60.0102 s]
Raw data (loadavg): 0.97 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2042 0 0 0 5969 12 0 0 25 0 1 0 1769561549 9162752 2025 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2237 2025 145 145 0 2092 0
[pid=29836] vsize: 8948
Current children cumulated CPU time (s) 59.83
Current children cumulated vsize (Kb) 11072

[startup+70.0109 s]
Raw data (loadavg): 0.97 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2169 0 0 0 6967 13 0 0 25 0 1 0 1769561549 9682944 2152 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2364 2152 145 145 0 2219 0
[pid=29836] vsize: 9456
Current children cumulated CPU time (s) 69.82
Current children cumulated vsize (Kb) 11580

[startup+80.0117 s]
Raw data (loadavg): 0.98 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2289 0 0 0 7965 14 0 0 25 0 1 0 1769561549 10235904 2272 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2499 2272 145 145 0 2354 0
[pid=29836] vsize: 9996
Current children cumulated CPU time (s) 79.81
Current children cumulated vsize (Kb) 12120

[startup+90.0125 s]
Raw data (loadavg): 0.98 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2289 0 0 0 8965 14 0 0 25 0 1 0 1769561549 10235904 2272 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2499 2272 145 145 0 2354 0
[pid=29836] vsize: 9996
Current children cumulated CPU time (s) 89.81
Current children cumulated vsize (Kb) 12120

[startup+100.013 s]
Raw data (loadavg): 0.98 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2289 0 0 0 9965 14 0 0 25 0 1 0 1769561549 10235904 2272 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2499 2272 145 145 0 2354 0
[pid=29836] vsize: 9996
Current children cumulated CPU time (s) 99.81
Current children cumulated vsize (Kb) 12120

[startup+110.014 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2289 0 0 0 10966 14 0 0 25 0 1 0 1769561549 10235904 2272 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2499 2272 145 145 0 2354 0
[pid=29836] vsize: 9996
Current children cumulated CPU time (s) 109.82
Current children cumulated vsize (Kb) 12120

[startup+120.015 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2293 0 0 0 11966 14 0 0 25 0 1 0 1769561549 10252288 2276 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2503 2276 145 145 0 2358 0
[pid=29836] vsize: 10012
Current children cumulated CPU time (s) 119.82
Current children cumulated vsize (Kb) 12136

[startup+130.016 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2297 0 0 0 12966 14 0 0 25 0 1 0 1769561549 10268672 2280 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2507 2280 145 145 0 2362 0
[pid=29836] vsize: 10028
Current children cumulated CPU time (s) 129.82
Current children cumulated vsize (Kb) 12152

[startup+140.016 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2304 0 0 0 13966 14 0 0 25 0 1 0 1769561549 10301440 2287 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2515 2287 145 145 0 2370 0
[pid=29836] vsize: 10060
Current children cumulated CPU time (s) 139.82
Current children cumulated vsize (Kb) 12184

[startup+150.018 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2304 0 0 0 14967 14 0 0 25 0 1 0 1769561549 10301440 2287 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2515 2287 145 145 0 2370 0
[pid=29836] vsize: 10060
Current children cumulated CPU time (s) 149.83
Current children cumulated vsize (Kb) 12184

[startup+160.019 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2343 0 0 0 15966 14 0 0 25 0 1 0 1769561549 10547200 2326 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2575 2326 145 145 0 2430 0
[pid=29836] vsize: 10300
Current children cumulated CPU time (s) 159.82
Current children cumulated vsize (Kb) 12424

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2344 0 0 0 16966 14 0 0 25 0 1 0 1769561549 10547200 2327 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2575 2327 145 145 0 2430 0
[pid=29836] vsize: 10300
Current children cumulated CPU time (s) 169.82
Current children cumulated vsize (Kb) 12424

[startup+180.02 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2344 0 0 0 17966 15 0 0 25 0 1 0 1769561549 10547200 2327 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 2575 2327 145 145 0 2430 0
[pid=29836] vsize: 10300
Current children cumulated CPU time (s) 179.83
Current children cumulated vsize (Kb) 12424

[startup+190.021 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2349 0 0 0 18965 16 0 0 25 0 1 0 1769561549 10563584 2332 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 2579 2332 145 145 0 2434 0
[pid=29836] vsize: 10316
Current children cumulated CPU time (s) 189.83
Current children cumulated vsize (Kb) 12440

[startup+200.021 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2359 0 0 0 19964 16 0 0 25 0 1 0 1769561549 10612736 2342 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 2591 2342 145 145 0 2446 0
[pid=29836] vsize: 10364
Current children cumulated CPU time (s) 199.82
Current children cumulated vsize (Kb) 12488

[startup+210.022 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2391 0 0 0 20963 17 0 0 25 0 1 0 1769561549 10752000 2374 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 2625 2374 145 145 0 2480 0
[pid=29836] vsize: 10500
Current children cumulated CPU time (s) 209.82
Current children cumulated vsize (Kb) 12624

[startup+220.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2439 0 0 0 21962 18 0 0 25 0 1 0 1769561549 10956800 2422 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 2675 2422 145 145 0 2530 0
[pid=29836] vsize: 10700
Current children cumulated CPU time (s) 219.82
Current children cumulated vsize (Kb) 12824

[startup+230.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2451 0 0 0 22962 18 0 0 25 0 1 0 1769561549 11005952 2434 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 2687 2434 145 145 0 2542 0
[pid=29836] vsize: 10748
Current children cumulated CPU time (s) 229.82
Current children cumulated vsize (Kb) 12872

[startup+240.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2456 0 0 0 23962 18 0 0 25 0 1 0 1769561549 11071488 2439 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2703 2439 145 145 0 2558 0
[pid=29836] vsize: 10812
Current children cumulated CPU time (s) 239.82
Current children cumulated vsize (Kb) 12936

[startup+250.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2474 0 0 0 24962 19 0 0 25 0 1 0 1769561549 11120640 2457 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2715 2457 145 145 0 2570 0
[pid=29836] vsize: 10860
Current children cumulated CPU time (s) 249.83
Current children cumulated vsize (Kb) 12984

[startup+260.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2476 0 0 0 25962 19 0 0 25 0 1 0 1769561549 11120640 2459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2715 2459 145 145 0 2570 0
[pid=29836] vsize: 10860
Current children cumulated CPU time (s) 259.83
Current children cumulated vsize (Kb) 12984

[startup+270.026 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2484 0 0 0 26962 19 0 0 25 0 1 0 1769561549 11153408 2467 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2723 2467 145 145 0 2578 0
[pid=29836] vsize: 10892
Current children cumulated CPU time (s) 269.83
Current children cumulated vsize (Kb) 13016

[startup+280.026 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2484 0 0 0 27963 19 0 0 25 0 1 0 1769561549 11153408 2467 4294967295 134512640 135094434 3221224448 3221223104 134558292 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2723 2467 145 145 0 2578 0
[pid=29836] vsize: 10892
Current children cumulated CPU time (s) 279.84
Current children cumulated vsize (Kb) 13016

[startup+290.027 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2484 0 0 0 28963 19 0 0 25 0 1 0 1769561549 11153408 2467 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2723 2467 145 145 0 2578 0
[pid=29836] vsize: 10892
Current children cumulated CPU time (s) 289.84
Current children cumulated vsize (Kb) 13016

[startup+300.027 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2503 0 0 0 29963 19 0 0 25 0 1 0 1769561549 11235328 2486 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2743 2486 145 145 0 2598 0
[pid=29836] vsize: 10972
Current children cumulated CPU time (s) 299.84
Current children cumulated vsize (Kb) 13096

[startup+310.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2569 0 0 0 30961 20 0 0 25 0 1 0 1769561549 11493376 2552 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2806 2552 145 145 0 2661 0
[pid=29836] vsize: 11224
Current children cumulated CPU time (s) 309.83
Current children cumulated vsize (Kb) 13348

[startup+320.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2587 0 0 0 31961 20 0 0 25 0 1 0 1769561549 11591680 2570 4294967295 134512640 135094434 3221224448 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2830 2570 145 145 0 2685 0
[pid=29836] vsize: 11320
Current children cumulated CPU time (s) 319.83
Current children cumulated vsize (Kb) 13444

[startup+330.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2601 0 0 0 32961 20 0 0 25 0 1 0 1769561549 11689984 2584 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2854 2584 145 145 0 2709 0
[pid=29836] vsize: 11416
Current children cumulated CPU time (s) 329.83
Current children cumulated vsize (Kb) 13540

[startup+340.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2614 0 0 0 33961 20 0 0 25 0 1 0 1769561549 11722752 2597 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2862 2597 145 145 0 2717 0
[pid=29836] vsize: 11448
Current children cumulated CPU time (s) 339.83
Current children cumulated vsize (Kb) 13572

[startup+350.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2614 0 0 0 34962 20 0 0 25 0 1 0 1769561549 11722752 2597 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2862 2597 145 145 0 2717 0
[pid=29836] vsize: 11448
Current children cumulated CPU time (s) 349.84
Current children cumulated vsize (Kb) 13572

[startup+360.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2620 0 0 0 35962 20 0 0 25 0 1 0 1769561549 11755520 2603 4294967295 134512640 135094434 3221224448 3221223136 134554676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2870 2603 145 145 0 2725 0
[pid=29836] vsize: 11480
Current children cumulated CPU time (s) 359.84
Current children cumulated vsize (Kb) 13604

[startup+370.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2620 0 0 0 36962 20 0 0 25 0 1 0 1769561549 11755520 2603 4294967295 134512640 135094434 3221224448 3221223060 134563134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2870 2603 145 145 0 2725 0
[pid=29836] vsize: 11480
Current children cumulated CPU time (s) 369.84
Current children cumulated vsize (Kb) 13604

[startup+380.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2620 0 0 0 37962 20 0 0 25 0 1 0 1769561549 11755520 2603 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2870 2603 145 145 0 2725 0
[pid=29836] vsize: 11480
Current children cumulated CPU time (s) 379.84
Current children cumulated vsize (Kb) 13604

[startup+390.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2641 0 0 0 38962 20 0 0 25 0 1 0 1769561549 11886592 2624 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2902 2624 145 145 0 2757 0
[pid=29836] vsize: 11608
Current children cumulated CPU time (s) 389.84
Current children cumulated vsize (Kb) 13732

[startup+400.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2651 0 0 0 39962 21 0 0 25 0 1 0 1769561549 11948032 2634 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2917 2634 145 145 0 2772 0
[pid=29836] vsize: 11668
Current children cumulated CPU time (s) 399.85
Current children cumulated vsize (Kb) 13792

[startup+410.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2658 0 0 0 40963 21 0 0 25 0 1 0 1769561549 11964416 2641 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2921 2641 145 145 0 2776 0
[pid=29836] vsize: 11684
Current children cumulated CPU time (s) 409.86
Current children cumulated vsize (Kb) 13808

[startup+420.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2661 0 0 0 41963 21 0 0 25 0 1 0 1769561549 12029952 2644 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2937 2644 145 145 0 2792 0
[pid=29836] vsize: 11748
Current children cumulated CPU time (s) 419.86
Current children cumulated vsize (Kb) 13872

[startup+430.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2698 0 0 0 42963 21 0 0 25 0 1 0 1769561549 12165120 2681 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2970 2681 145 145 0 2825 0
[pid=29836] vsize: 11880
Current children cumulated CPU time (s) 429.86
Current children cumulated vsize (Kb) 14004

[startup+440.039 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2698 0 0 0 43963 21 0 0 25 0 1 0 1769561549 12165120 2681 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2970 2681 145 145 0 2825 0
[pid=29836] vsize: 11880
Current children cumulated CPU time (s) 439.86
Current children cumulated vsize (Kb) 14004

[startup+450.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2709 0 0 0 44963 21 0 0 25 0 1 0 1769561549 12214272 2692 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2982 2692 145 145 0 2837 0
[pid=29836] vsize: 11928
Current children cumulated CPU time (s) 449.86
Current children cumulated vsize (Kb) 14052

[startup+460.041 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2710 0 0 0 45964 21 0 0 25 0 1 0 1769561549 12214272 2693 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 2982 2693 145 145 0 2837 0
[pid=29836] vsize: 11928
Current children cumulated CPU time (s) 459.87
Current children cumulated vsize (Kb) 14052

[startup+470.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2747 0 0 0 46963 21 0 0 25 0 1 0 1769561549 12378112 2730 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3022 2730 145 145 0 2877 0
[pid=29836] vsize: 12088
Current children cumulated CPU time (s) 469.86
Current children cumulated vsize (Kb) 14212

[startup+480.042 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2747 0 0 0 47963 21 0 0 25 0 1 0 1769561549 12378112 2730 4294967295 134512640 135094434 3221224448 3221223072 134557722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3022 2730 145 145 0 2877 0
[pid=29836] vsize: 12088
Current children cumulated CPU time (s) 479.86
Current children cumulated vsize (Kb) 14212

[startup+490.043 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2755 0 0 0 48964 21 0 0 25 0 1 0 1769561549 12410880 2738 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3030 2738 145 145 0 2885 0
[pid=29836] vsize: 12120
Current children cumulated CPU time (s) 489.87
Current children cumulated vsize (Kb) 14244

[startup+500.044 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2762 0 0 0 49964 21 0 0 25 0 1 0 1769561549 12443648 2745 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3038 2745 145 145 0 2893 0
[pid=29836] vsize: 12152
Current children cumulated CPU time (s) 499.87
Current children cumulated vsize (Kb) 14276

[startup+510.044 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2762 0 0 0 50964 21 0 0 25 0 1 0 1769561549 12443648 2745 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3038 2745 145 145 0 2893 0
[pid=29836] vsize: 12152
Current children cumulated CPU time (s) 509.87
Current children cumulated vsize (Kb) 14276

[startup+520.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2767 0 0 0 51964 21 0 0 25 0 1 0 1769561549 12476416 2750 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3046 2750 145 145 0 2901 0
[pid=29836] vsize: 12184
Current children cumulated CPU time (s) 519.87
Current children cumulated vsize (Kb) 14308

[startup+530.046 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2778 0 0 0 52964 22 0 0 25 0 1 0 1769561549 12525568 2761 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3058 2761 145 145 0 2913 0
[pid=29836] vsize: 12232
Current children cumulated CPU time (s) 529.88
Current children cumulated vsize (Kb) 14356

[startup+540.047 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2778 0 0 0 53964 22 0 0 25 0 1 0 1769561549 12525568 2761 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3058 2761 145 145 0 2913 0
[pid=29836] vsize: 12232
Current children cumulated CPU time (s) 539.88
Current children cumulated vsize (Kb) 14356

[startup+550.048 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2784 0 0 0 54965 22 0 0 25 0 1 0 1769561549 12558336 2767 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3066 2767 145 145 0 2921 0
[pid=29836] vsize: 12264
Current children cumulated CPU time (s) 549.89
Current children cumulated vsize (Kb) 14388

[startup+560.048 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2792 0 0 0 55965 22 0 0 25 0 1 0 1769561549 12591104 2775 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3074 2775 145 145 0 2929 0
[pid=29836] vsize: 12296
Current children cumulated CPU time (s) 559.89
Current children cumulated vsize (Kb) 14420

[startup+570.049 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2793 0 0 0 56965 22 0 0 25 0 1 0 1769561549 12591104 2776 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3074 2776 145 145 0 2929 0
[pid=29836] vsize: 12296
Current children cumulated CPU time (s) 569.89
Current children cumulated vsize (Kb) 14420

[startup+580.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2807 0 0 0 57964 22 0 0 25 0 1 0 1769561549 12656640 2790 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 3090 2790 145 145 0 2945 0
[pid=29836] vsize: 12360
Current children cumulated CPU time (s) 579.88
Current children cumulated vsize (Kb) 14484

[startup+590.051 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2809 0 0 0 58964 22 0 0 25 0 1 0 1769561549 12656640 2792 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3090 2792 145 145 0 2945 0
[pid=29836] vsize: 12360
Current children cumulated CPU time (s) 589.88
Current children cumulated vsize (Kb) 14484

[startup+600.052 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2828 0 0 0 59964 22 0 0 25 0 1 0 1769561549 12754944 2811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3114 2811 145 145 0 2969 0
[pid=29836] vsize: 12456
Current children cumulated CPU time (s) 599.88
Current children cumulated vsize (Kb) 14580

[startup+610.052 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2829 0 0 0 60963 22 0 0 25 0 1 0 1769561549 12754944 2812 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3114 2812 145 145 0 2969 0
[pid=29836] vsize: 12456
Current children cumulated CPU time (s) 609.87
Current children cumulated vsize (Kb) 14580

[startup+620.052 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2850 0 0 0 61964 22 0 0 25 0 1 0 1769561549 12886016 2833 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3146 2833 145 145 0 3001 0
[pid=29836] vsize: 12584
Current children cumulated CPU time (s) 619.88
Current children cumulated vsize (Kb) 14708

[startup+630.053 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2864 0 0 0 62964 23 0 0 25 0 1 0 1769561549 12951552 2847 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3162 2847 145 145 0 3017 0
[pid=29836] vsize: 12648
Current children cumulated CPU time (s) 629.89
Current children cumulated vsize (Kb) 14772

[startup+640.054 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2865 0 0 0 63964 23 0 0 25 0 1 0 1769561549 12951552 2848 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3162 2848 145 145 0 3017 0
[pid=29836] vsize: 12648
Current children cumulated CPU time (s) 639.89
Current children cumulated vsize (Kb) 14772

[startup+650.053 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2865 0 0 0 64964 23 0 0 25 0 1 0 1769561549 12951552 2848 4294967295 134512640 135094434 3221224448 3221223136 134554763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3162 2848 145 145 0 3017 0
[pid=29836] vsize: 12648
Current children cumulated CPU time (s) 649.89
Current children cumulated vsize (Kb) 14772

[startup+660.054 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2874 0 0 0 65964 23 0 0 25 0 1 0 1769561549 13017088 2857 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2857 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 659.89
Current children cumulated vsize (Kb) 14836

[startup+670.055 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2877 0 0 0 66964 23 0 0 25 0 1 0 1769561549 13017088 2860 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2860 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 669.89
Current children cumulated vsize (Kb) 14836

[startup+680.056 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2879 0 0 0 67965 23 0 0 25 0 1 0 1769561549 13017088 2862 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2862 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 679.9
Current children cumulated vsize (Kb) 14836

[startup+690.057 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2880 0 0 0 68965 23 0 0 25 0 1 0 1769561549 13017088 2863 4294967295 134512640 135094434 3221224448 3221223100 134562036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2863 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 689.9
Current children cumulated vsize (Kb) 14836

[startup+700.057 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 69965 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 699.9
Current children cumulated vsize (Kb) 14836

[startup+710.058 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 70965 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 709.9
Current children cumulated vsize (Kb) 14836

[startup+720.059 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 71966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 719.91
Current children cumulated vsize (Kb) 14836

[startup+730.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 72966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 729.91
Current children cumulated vsize (Kb) 14836

[startup+740.061 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 73966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 739.91
Current children cumulated vsize (Kb) 14836

[startup+750.061 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 74966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 749.91
Current children cumulated vsize (Kb) 14836

[startup+760.062 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 75966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 759.91
Current children cumulated vsize (Kb) 14836

[startup+770.062 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 76966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0
[pid=29836] vsize: 12712
Current children cumulated CPU time (s) 769.91
Current children cumulated vsize (Kb) 14836

[startup+780.064 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2898 0 0 0 77967 23 0 0 25 0 1 0 1769561549 13082624 2881 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3194 2881 145 145 0 3049 0
[pid=29836] vsize: 12776
Current children cumulated CPU time (s) 779.92
Current children cumulated vsize (Kb) 14900

[startup+790.064 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2985 0 0 0 78964 25 0 0 25 0 1 0 1769561549 13438976 2968 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3281 2968 145 145 0 3136 0
[pid=29836] vsize: 13124
Current children cumulated CPU time (s) 789.91
Current children cumulated vsize (Kb) 15248

[startup+800.064 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2998 0 0 0 79964 25 0 0 25 0 1 0 1769561549 13504512 2981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3297 2981 145 145 0 3152 0
[pid=29836] vsize: 13188
Current children cumulated CPU time (s) 799.91
Current children cumulated vsize (Kb) 15312

[startup+810.065 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2998 0 0 0 80964 25 0 0 25 0 1 0 1769561549 13504512 2981 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3297 2981 145 145 0 3152 0
[pid=29836] vsize: 13188
Current children cumulated CPU time (s) 809.91
Current children cumulated vsize (Kb) 15312

[startup+820.066 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3062 0 0 0 81963 26 0 0 25 0 1 0 1769561549 13774848 3045 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3363 3045 145 145 0 3218 0
[pid=29836] vsize: 13452
Current children cumulated CPU time (s) 819.91
Current children cumulated vsize (Kb) 15576

[startup+830.067 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3062 0 0 0 82962 26 0 0 25 0 1 0 1769561549 13774848 3045 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3363 3045 145 145 0 3218 0
[pid=29836] vsize: 13452
Current children cumulated CPU time (s) 829.9
Current children cumulated vsize (Kb) 15576

[startup+840.067 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3071 0 0 0 83963 26 0 0 25 0 1 0 1769561549 13824000 3054 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3375 3054 145 145 0 3230 0
[pid=29836] vsize: 13500
Current children cumulated CPU time (s) 839.91
Current children cumulated vsize (Kb) 15624

[startup+850.068 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3117 0 0 0 84962 27 0 0 25 0 1 0 1769561549 14012416 3100 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3421 3100 145 145 0 3276 0
[pid=29836] vsize: 13684
Current children cumulated CPU time (s) 849.91
Current children cumulated vsize (Kb) 15808

[startup+860.069 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3249 0 0 0 85960 28 0 0 25 0 1 0 1769561549 14548992 3232 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3552 3232 145 145 0 3407 0
[pid=29836] vsize: 14208
Current children cumulated CPU time (s) 859.9
Current children cumulated vsize (Kb) 16332

[startup+870.07 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3369 0 0 0 86958 28 0 0 25 0 1 0 1769561549 15048704 3352 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3674 3352 145 145 0 3529 0
[pid=29836] vsize: 14696
Current children cumulated CPU time (s) 869.88
Current children cumulated vsize (Kb) 16820

[startup+880.072 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3381 0 0 0 87958 29 0 0 25 0 1 0 1769561549 15114240 3364 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3690 3364 145 145 0 3545 0
[pid=29836] vsize: 14760
Current children cumulated CPU time (s) 879.89
Current children cumulated vsize (Kb) 16884

[startup+890.072 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3382 0 0 0 88958 29 0 0 25 0 1 0 1769561549 15114240 3365 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3690 3365 145 145 0 3545 0
[pid=29836] vsize: 14760
Current children cumulated CPU time (s) 889.89
Current children cumulated vsize (Kb) 16884

[startup+900.073 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3396 0 0 0 89958 29 0 0 25 0 1 0 1769561549 15179776 3379 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3706 3379 145 145 0 3561 0
[pid=29836] vsize: 14824
Current children cumulated CPU time (s) 899.89
Current children cumulated vsize (Kb) 16948

[startup+910.074 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3399 0 0 0 90958 29 0 0 25 0 1 0 1769561549 15179776 3382 4294967295 134512640 135094434 3221224448 3221223072 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3706 3382 145 145 0 3561 0
[pid=29836] vsize: 14824
Current children cumulated CPU time (s) 909.89
Current children cumulated vsize (Kb) 16948

[startup+920.075 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3399 0 0 0 91959 29 0 0 25 0 1 0 1769561549 15179776 3382 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3706 3382 145 145 0 3561 0
[pid=29836] vsize: 14824
Current children cumulated CPU time (s) 919.9
Current children cumulated vsize (Kb) 16948

[startup+930.075 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3402 0 0 0 92959 29 0 0 25 0 1 0 1769561549 15179776 3385 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3706 3385 145 145 0 3561 0
[pid=29836] vsize: 14824
Current children cumulated CPU time (s) 929.9
Current children cumulated vsize (Kb) 16948

[startup+940.076 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3406 0 0 0 93959 29 0 0 25 0 1 0 1769561549 15179776 3389 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3706 3389 145 145 0 3561 0
[pid=29836] vsize: 14824
Current children cumulated CPU time (s) 939.9
Current children cumulated vsize (Kb) 16948

[startup+950.077 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3415 0 0 0 94959 29 0 0 25 0 1 0 1769561549 15212544 3398 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3714 3398 145 145 0 3569 0
[pid=29836] vsize: 14856
Current children cumulated CPU time (s) 949.9
Current children cumulated vsize (Kb) 16980

[startup+960.078 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3415 0 0 0 95959 29 0 0 25 0 1 0 1769561549 15212544 3398 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3714 3398 145 145 0 3569 0
[pid=29836] vsize: 14856
Current children cumulated CPU time (s) 959.9
Current children cumulated vsize (Kb) 16980

[startup+970.079 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3415 0 0 0 96959 29 0 0 25 0 1 0 1769561549 15212544 3398 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3714 3398 145 145 0 3569 0
[pid=29836] vsize: 14856
Current children cumulated CPU time (s) 969.9
Current children cumulated vsize (Kb) 16980

[startup+980.079 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3416 0 0 0 97960 29 0 0 25 0 1 0 1769561549 15212544 3399 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3714 3399 145 145 0 3569 0
[pid=29836] vsize: 14856
Current children cumulated CPU time (s) 979.91
Current children cumulated vsize (Kb) 16980

[startup+990.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3429 0 0 0 98960 30 0 0 25 0 1 0 1769561549 15310848 3412 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3738 3412 145 145 0 3593 0
[pid=29836] vsize: 14952
Current children cumulated CPU time (s) 989.92
Current children cumulated vsize (Kb) 17076

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3441 0 0 0 99960 30 0 0 25 0 1 0 1769561549 15343616 3424 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3746 3424 145 145 0 3601 0
[pid=29836] vsize: 14984
Current children cumulated CPU time (s) 999.92
Current children cumulated vsize (Kb) 17108

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3446 0 0 0 100960 30 0 0 25 0 1 0 1769561549 15360000 3429 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3750 3429 145 145 0 3605 0
[pid=29836] vsize: 15000
Current children cumulated CPU time (s) 1009.92
Current children cumulated vsize (Kb) 17124

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3449 0 0 0 101960 30 0 0 25 0 1 0 1769561549 15360000 3432 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3750 3432 145 145 0 3605 0
[pid=29836] vsize: 15000
Current children cumulated CPU time (s) 1019.92
Current children cumulated vsize (Kb) 17124

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3451 0 0 0 102960 30 0 0 25 0 1 0 1769561549 15360000 3434 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3750 3434 145 145 0 3605 0
[pid=29836] vsize: 15000
Current children cumulated CPU time (s) 1029.92
Current children cumulated vsize (Kb) 17124

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3451 0 0 0 103961 30 0 0 25 0 1 0 1769561549 15360000 3434 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3750 3434 145 145 0 3605 0
[pid=29836] vsize: 15000
Current children cumulated CPU time (s) 1039.93
Current children cumulated vsize (Kb) 17124

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3451 0 0 0 104961 30 0 0 25 0 1 0 1769561549 15360000 3434 4294967295 134512640 135094434 3221224448 3221223104 134558184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3750 3434 145 145 0 3605 0
[pid=29836] vsize: 15000
Current children cumulated CPU time (s) 1049.93
Current children cumulated vsize (Kb) 17124

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3476 0 0 0 105961 30 0 0 25 0 1 0 1769561549 15491072 3459 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3782 3459 145 145 0 3637 0
[pid=29836] vsize: 15128
Current children cumulated CPU time (s) 1059.93
Current children cumulated vsize (Kb) 17252

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3493 0 0 0 106961 30 0 0 25 0 1 0 1769561549 15556608 3476 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3798 3476 145 145 0 3653 0
[pid=29836] vsize: 15192
Current children cumulated CPU time (s) 1069.93
Current children cumulated vsize (Kb) 17316

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3493 0 0 0 107961 30 0 0 25 0 1 0 1769561549 15556608 3476 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3798 3476 145 145 0 3653 0
[pid=29836] vsize: 15192
Current children cumulated CPU time (s) 1079.93
Current children cumulated vsize (Kb) 17316

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3493 0 0 0 108961 30 0 0 25 0 1 0 1769561549 15556608 3476 4294967295 134512640 135094434 3221224448 3221223120 134555570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3798 3476 145 145 0 3653 0
[pid=29836] vsize: 15192
Current children cumulated CPU time (s) 1089.93
Current children cumulated vsize (Kb) 17316

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3493 0 0 0 109962 30 0 0 25 0 1 0 1769561549 15556608 3476 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3798 3476 145 145 0 3653 0
[pid=29836] vsize: 15192
Current children cumulated CPU time (s) 1099.94
Current children cumulated vsize (Kb) 17316

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3498 0 0 0 110962 30 0 0 25 0 1 0 1769561549 15589376 3481 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3806 3481 145 145 0 3661 0
[pid=29836] vsize: 15224
Current children cumulated CPU time (s) 1109.94
Current children cumulated vsize (Kb) 17348

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3507 0 0 0 111962 30 0 0 25 0 1 0 1769561549 15654912 3490 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3822 3490 145 145 0 3677 0
[pid=29836] vsize: 15288
Current children cumulated CPU time (s) 1119.94
Current children cumulated vsize (Kb) 17412

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3508 0 0 0 112962 30 0 0 25 0 1 0 1769561549 15654912 3491 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3822 3491 145 145 0 3677 0
[pid=29836] vsize: 15288
Current children cumulated CPU time (s) 1129.94
Current children cumulated vsize (Kb) 17412

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3508 0 0 0 113962 30 0 0 25 0 1 0 1769561549 15654912 3491 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3822 3491 145 145 0 3677 0
[pid=29836] vsize: 15288
Current children cumulated CPU time (s) 1139.94
Current children cumulated vsize (Kb) 17412

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3521 0 0 0 114962 30 0 0 25 0 1 0 1769561549 15720448 3504 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3838 3504 145 145 0 3693 0
[pid=29836] vsize: 15352
Current children cumulated CPU time (s) 1149.94
Current children cumulated vsize (Kb) 17476

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3522 0 0 0 115963 30 0 0 25 0 1 0 1769561549 15720448 3505 4294967295 134512640 135094434 3221224448 3221223072 134557583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3838 3505 145 145 0 3693 0
[pid=29836] vsize: 15352
Current children cumulated CPU time (s) 1159.95
Current children cumulated vsize (Kb) 17476

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3523 0 0 0 116963 30 0 0 25 0 1 0 1769561549 15720448 3506 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3838 3506 145 145 0 3693 0
[pid=29836] vsize: 15352
Current children cumulated CPU time (s) 1169.95
Current children cumulated vsize (Kb) 17476

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3524 0 0 0 117963 30 0 0 25 0 1 0 1769561549 15720448 3507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3838 3507 145 145 0 3693 0
[pid=29836] vsize: 15352
Current children cumulated CPU time (s) 1179.95
Current children cumulated vsize (Kb) 17476

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3524 0 0 0 118964 30 0 0 25 0 1 0 1769561549 15720448 3507 4294967295 134512640 135094434 3221224448 3221223040 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29836/statm): 3838 3507 145 145 0 3693 0
[pid=29836] vsize: 15352
Current children cumulated CPU time (s) 1189.96
Current children cumulated vsize (Kb) 17476

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3557 0 0 0 119963 31 0 0 25 0 1 0 1769561549 15982592 3540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 3902 3540 145 145 0 3757 0
[pid=29836] vsize: 15608
Current children cumulated CPU time (s) 1199.96
Current children cumulated vsize (Kb) 17732

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3558 0 0 0 120961 31 0 0 25 0 1 0 1769561549 15982592 3541 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 3902 3541 145 145 0 3757 0
[pid=29836] vsize: 15608
Current children cumulated CPU time (s) 1209.94
Current children cumulated vsize (Kb) 17732



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 29836
Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29832/statm): 531 226 485 147 0 384 0
[pid=29832] vsize: 2124
Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3558 0 0 0 120961 31 0 0 25 0 1 0 1769561549 15982592 3541 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29836/statm): 3902 3541 145 145 0 3757 0
[pid=29836] vsize: 15608
Current children cumulated CPU time (s) 1209.94
Current children cumulated vsize (Kb) 17732

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.94
CPU user time (s): 1209.62
CPU system time (s): 0.32595
CPU usage (%): 99.9862
Max. virtual memory (cumulated for all children) (Kb): 17732

Verifier Data

ERROR: no interpretation found !