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/primes-dimacs-cnf/normalized-ii32d1.opb
MD5SUM151e246868267296e134c3c76a3cb289
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 286
Optimality of the best value was proved NO
Number of terms in the objective function 664
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 664
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 664
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.06
Number of variables664
Total number of constraints3035
Number of constraints which are clauses3035
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint32

Trace number 2191

Launcher Data

LAUNCH ON wulflinc12 THE 2005-09-18 18:04:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2566 boxname=wulflinc12 idbench=222 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  151e246868267296e134c3c76a3cb289  /oldhome/oroussel/tmp/wulflinc12/normalized-ii32d1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-ii32d1.opb
IDLAUNCH: 2566
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        898476 kB
Buffers:         38612 kB
Cached:          57336 kB
SwapCached:        544 kB
Active:          66752 kB
Inactive:        41412 kB
HighTotal:      131008 kB
HighFree:        73640 kB
LowTotal:       903652 kB
LowFree:        824836 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            22412 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:25:02 (client local time) WITH STATUS 10 IN 1209.65 SECONDS
stats: 2566 7 1209.65 10

Solver Data

c Parsing PB file...
c Converting 3035 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 |    3035     9828 |    1011       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 319
c ---[   0]---> Sorter-cost:30182     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        22 |   39401    94869 |   13133      22      879    40.0 |  0.000 % |
c ==============================================================================
c Found solution: 304
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        78 |   39566    95345 |   13188      77     5158    67.0 |  0.000 % |
c ==============================================================================
c Found solution: 294
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        82 |   39693    95707 |   13231      81     5475    67.6 |  0.000 % |
c |       182 |   39693    95707 |   14554     181    15088    83.4 |  0.172 % |
c |       334 |   39693    95707 |   16009     333    24915    74.8 |  0.172 % |
c |       559 |   39693    95707 |   17610     558    43774    78.4 |  0.172 % |
c |       897 |   39610    95534 |   19371     893    84437    94.6 |  0.353 % |
c |      1403 |   39610    95534 |   21308    1399   139614    99.8 |  0.353 % |
c |      2164 |   39439    95178 |   23439    2155   228675   106.1 |  0.718 % |
c |      3305 |   39396    95089 |   25783    3295   356671   108.2 |  0.806 % |
c |      5014 |   39147    94550 |   28361    4996   564213   112.9 |  1.379 % |
c ==============================================================================
c Found solution: 293
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6786 |   39147    94597 |   13049    6766   805584   119.1 |  1.379 % |
c |      6886 |   38248    92654 |   14353    6843   807275   118.0 |  3.544 % |
c |      7036 |   38101    92333 |   15789    6978   810806   116.2 |  3.889 % |
c |      7261 |   38101    92333 |   17368    7203   835914   116.1 |  3.889 % |
c |      7598 |   38101    92333 |   19105    7540   859380   114.0 |  3.889 % |
c |      8107 |   38058    92242 |   21015    8048   902377   112.1 |  3.985 % |
c |      8867 |   37957    92027 |   23117    8806   985841   112.0 |  4.209 % |
c |     10007 |   37816    91714 |   25428    9942  1069396   107.6 |  4.550 % |
c |     11717 |   37684    91426 |   27971   11649  1217804   104.5 |  4.858 % |
c |     14279 |   37684    91426 |   30768   14211  1480329   104.2 |  4.858 % |
c |     18124 |   35697    87013 |   33845   17979  1810517   100.7 |  9.636 % |
c |     23891 |   35469    86509 |   37230   23742  2607070   109.8 | 10.169 % |
c |     32540 |   35409    86375 |   40953   32384  3450033   106.5 | 10.317 % |
c |     45515 |   35296    86126 |   45048   15064  1255595    83.4 | 10.585 % |
c ==============================================================================
c Found solution: 292
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51755 |   35264    86031 |   11754   21218  1737423    81.9 | 10.585 % |
c |     51858 |   35264    86031 |   12929   10712   660163    61.6 | 10.688 % |
c |     52010 |   35264    86031 |   14222   10864   673235    62.0 | 10.688 % |
c |     52238 |   35264    86031 |   15644   11092   680554    61.4 | 10.688 % |
c |     52575 |   35264    86031 |   17209   11429   710291    62.1 | 10.688 % |
c |     53081 |   35264    86031 |   18929   11935   753857    63.2 | 10.688 % |
c |     53840 |   35264    86031 |   20822   12694   821047    64.7 | 10.688 % |
c |     54983 |   35264    86031 |   22905   13837   917888    66.3 | 10.688 % |
c |     56691 |   35264    86031 |   25195   15545  1062283    68.3 | 10.688 % |
c |     59253 |   35264    86031 |   27715   18107  1325662    73.2 | 10.688 % |
c |     63098 |   35264    86031 |   30486   21952  1774222    80.8 | 10.688 % |
c |     68864 |   35212    85914 |   33535   27717  2220091    80.1 | 10.817 % |
c |     77513 |   35212    85914 |   36889   36366  2981361    82.0 | 10.817 % |
c |     90487 |   35212    85914 |   40577   23247  1770661    76.2 | 10.817 % |
c |    109948 |   35153    85787 |   44635   42707  3210142    75.2 | 10.953 % |
c |    139140 |   35153    85787 |   49099   40523  2721836    67.2 | 10.953 % |
c ==============================================================================
c Found solution: 291
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    148770 |   35121    85732 |   11707   50152  3413506    68.1 | 10.953 % |
c |    148871 |   35121    85732 |   12877    9760   464349    47.6 | 11.093 % |
c |    149026 |   35121    85732 |   14165    9915   478892    48.3 | 11.093 % |
c |    149251 |   35121    85732 |   15582   10140   496222    48.9 | 11.093 % |
c |    149591 |   35121    85732 |   17140   10480   520952    49.7 | 11.093 % |
c |    150097 |   35121    85732 |   18854   10986   558194    50.8 | 11.093 % |
c |    150858 |   35121    85732 |   20739   11747   618457    52.6 | 11.093 % |
c |    151998 |   35121    85732 |   22813   12887   693350    53.8 | 11.093 % |
c |    153707 |   35121    85732 |   25094   14596   828225    56.7 | 11.093 % |
c |    156271 |   34396    84085 |   27604   17133   993365    58.0 | 12.902 % |
c |    160118 |   34396    84085 |   30364   20980  1393378    66.4 | 12.902 % |
c |    165886 |   34396    84085 |   33401   26748  2021075    75.6 | 12.902 % |
c |    174535 |   34396    84085 |   36741   35397  2864710    80.9 | 12.902 % |
c |    187509 |   34396    84085 |   40415   23543  1656176    70.3 | 12.902 % |
c ==============================================================================
c Found solution: 290
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    205542 |   34380    84019 |   11460   41576  3086386    74.2 | 12.902 % |
c |    205642 |   34380    84019 |   12606    8593   377408    43.9 | 12.961 % |
c |    205794 |   34380    84019 |   13866    8745   388045    44.4 | 12.961 % |
c |    206019 |   34380    84019 |   15253    8970   404742    45.1 | 12.961 % |
c |    206356 |   34380    84019 |   16778    9307   431358    46.3 | 12.961 % |
c |    206863 |   34380    84019 |   18456    9814   473568    48.3 | 12.961 % |
c |    207622 |   34380    84019 |   20302   10573   515082    48.7 | 12.961 % |
c |    208764 |   34380    84019 |   22332   11715   574466    49.0 | 12.961 % |
c |    210472 |   34380    84019 |   24565   13423   669115    49.8 | 12.961 % |
c |    213034 |   34380    84019 |   27022   15985   795872    49.8 | 12.961 % |
c |    216881 |   34380    84019 |   29724   19832   998091    50.3 | 12.961 % |
c |    222647 |   34380    84019 |   32696   25598  1341738    52.4 | 12.961 % |
c |    231296 |   34380    84019 |   35966   34247  2022239    59.0 | 12.961 % |
c |    244270 |   34380    84019 |   39563   21209  1538693    72.5 | 12.961 % |

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/24967/stat): 24967 (minisat+_script) R 24966 24967 8263 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785035488 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24967/statm): 174 3 169 147 0 27 0
[pid=24967] 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=24968
New process pid=24969
New process pid=24970
execve syscall for /bin/sed executable
One traced child (pid=24969) 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=24970) exited with status: 0
One traced child (pid=24968) exited with status: 0
New process pid=24971
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-ii32d1.opb

[startup+10.0041 s]
Raw data (loadavg): 0.47 0.69 0.86 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 2514 0 0 0 974 11 0 0 25 0 1 0 1785035493 10997760 2446 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 2685 2446 145 145 0 2540 0
[pid=24971] vsize: 10740
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 12864

[startup+20.0049 s]
Raw data (loadavg): 0.56 0.70 0.86 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) T 24967 24967 8263 0 -1 0 2838 0 0 0 1968 14 0 0 25 0 1 0 1785035493 12328960 2770 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24971/statm): 3010 2770 145 145 0 2865 0
[pid=24971] vsize: 12040
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 14164

[startup+30.0067 s]
Raw data (loadavg): 0.62 0.71 0.86 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 3210 0 0 0 2962 17 0 0 25 0 1 0 1785035493 13873152 3142 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 3387 3142 145 145 0 3242 0
[pid=24971] vsize: 13548
Current children cumulated CPU time (s) 29.79
Current children cumulated vsize (Kb) 15672

[startup+40.0075 s]
Raw data (loadavg): 0.68 0.72 0.86 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 3610 0 0 0 3954 20 0 0 25 0 1 0 1785035493 15499264 3542 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 3784 3542 145 145 0 3639 0
[pid=24971] vsize: 15136
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 17260

[startup+50.0094 s]
Raw data (loadavg): 0.73 0.73 0.86 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 3931 0 0 0 4949 22 0 0 25 0 1 0 1785035493 16801792 3863 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 4102 3863 145 145 0 3957 0
[pid=24971] vsize: 16408
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 18532

[startup+60.0102 s]
Raw data (loadavg): 0.77 0.74 0.86 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 4143 0 0 0 5945 24 0 0 25 0 1 0 1785035493 17727488 4075 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 4328 4075 145 145 0 4183 0
[pid=24971] vsize: 17312
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 19436

[startup+70.011 s]
Raw data (loadavg): 0.80 0.74 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 4399 0 0 0 6939 26 0 0 25 0 1 0 1785035493 18767872 4331 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24971/statm): 4582 4331 145 145 0 4437 0
[pid=24971] vsize: 18328
Current children cumulated CPU time (s) 69.65
Current children cumulated vsize (Kb) 20452

[startup+80.0128 s]
Raw data (loadavg): 0.83 0.75 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 4675 0 0 0 7935 28 0 0 25 0 1 0 1785035493 19894272 4607 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 4857 4607 145 145 0 4712 0
[pid=24971] vsize: 19428
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 21552

[startup+90.0137 s]
Raw data (loadavg): 0.86 0.76 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 5001 0 0 0 8929 31 0 0 25 0 1 0 1785035493 21225472 4933 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 5182 4933 145 145 0 5037 0
[pid=24971] vsize: 20728
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 22852

[startup+100.014 s]
Raw data (loadavg): 0.88 0.77 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 5242 0 0 0 9925 33 0 0 25 0 1 0 1785035493 22204416 5174 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 5421 5174 145 145 0 5276 0
[pid=24971] vsize: 21684
Current children cumulated CPU time (s) 99.58
Current children cumulated vsize (Kb) 23808

[startup+110.015 s]
Raw data (loadavg): 0.90 0.77 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 5437 0 0 0 10922 35 0 0 25 0 1 0 1785035493 22999040 5369 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 5615 5369 145 145 0 5470 0
[pid=24971] vsize: 22460
Current children cumulated CPU time (s) 109.57
Current children cumulated vsize (Kb) 24584

[startup+120.016 s]
Raw data (loadavg): 0.91 0.78 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 5626 0 0 0 11919 35 0 0 25 0 1 0 1785035493 23760896 5558 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 5801 5558 145 145 0 5656 0
[pid=24971] vsize: 23204
Current children cumulated CPU time (s) 119.54
Current children cumulated vsize (Kb) 25328

[startup+130.017 s]
Raw data (loadavg): 0.93 0.79 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 5810 0 0 0 12916 37 0 0 25 0 1 0 1785035493 24510464 5742 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 5984 5742 145 145 0 5839 0
[pid=24971] vsize: 23936
Current children cumulated CPU time (s) 129.53
Current children cumulated vsize (Kb) 26060

[startup+140.018 s]
Raw data (loadavg): 0.94 0.80 0.87 1/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) T 24967 24967 8263 0 -1 0 6007 0 0 0 13913 38 0 0 25 0 1 0 1785035493 25317376 5939 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24971/statm): 6181 5939 145 145 0 6036 0
[pid=24971] vsize: 24724
Current children cumulated CPU time (s) 139.51
Current children cumulated vsize (Kb) 26848

[startup+150.02 s]
Raw data (loadavg): 0.95 0.80 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 6191 0 0 0 14910 39 0 0 25 0 1 0 1785035493 26193920 6123 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 6395 6123 145 145 0 6250 0
[pid=24971] vsize: 25580
Current children cumulated CPU time (s) 149.49
Current children cumulated vsize (Kb) 27704

[startup+160.02 s]
Raw data (loadavg): 0.95 0.81 0.87 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 6398 0 0 0 15907 41 0 0 25 0 1 0 1785035493 27041792 6330 4294967295 134512640 135094434 3221224448 3221223040 134556847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 6602 6330 145 145 0 6457 0
[pid=24971] vsize: 26408
Current children cumulated CPU time (s) 159.48
Current children cumulated vsize (Kb) 28532

[startup+170.021 s]
Raw data (loadavg): 0.96 0.81 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 6595 0 0 0 16903 43 0 0 25 0 1 0 1785035493 27840512 6527 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 6797 6527 145 145 0 6652 0
[pid=24971] vsize: 27188
Current children cumulated CPU time (s) 169.46
Current children cumulated vsize (Kb) 29312

[startup+180.022 s]
Raw data (loadavg): 0.97 0.82 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 6792 0 0 0 17900 45 0 0 25 0 1 0 1785035493 28655616 6724 4294967295 134512640 135094434 3221224448 3221223072 134562146 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 6996 6724 145 145 0 6851 0
[pid=24971] vsize: 27984
Current children cumulated CPU time (s) 179.45
Current children cumulated vsize (Kb) 30108

[startup+190.023 s]
Raw data (loadavg): 0.97 0.82 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7039 0 0 0 18896 46 0 0 25 0 1 0 1785035493 29655040 6971 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7240 6971 145 145 0 7095 0
[pid=24971] vsize: 28960
Current children cumulated CPU time (s) 189.42
Current children cumulated vsize (Kb) 31084

[startup+200.025 s]
Raw data (loadavg): 0.98 0.83 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7237 0 0 0 19893 48 0 0 25 0 1 0 1785035493 30470144 7169 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7439 7169 145 145 0 7294 0
[pid=24971] vsize: 29756
Current children cumulated CPU time (s) 199.41
Current children cumulated vsize (Kb) 31880

[startup+210.026 s]
Raw data (loadavg): 0.98 0.83 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7396 0 0 0 20890 49 0 0 25 0 1 0 1785035493 31129600 7328 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7600 7328 145 145 0 7455 0
[pid=24971] vsize: 30400
Current children cumulated CPU time (s) 209.39
Current children cumulated vsize (Kb) 32524

[startup+220.026 s]
Raw data (loadavg): 0.98 0.84 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 21890 50 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 219.4
Current children cumulated vsize (Kb) 32640

[startup+230.027 s]
Raw data (loadavg): 0.98 0.84 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 22890 50 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 229.4
Current children cumulated vsize (Kb) 32640

[startup+240.028 s]
Raw data (loadavg): 0.99 0.85 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 23889 51 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 239.4
Current children cumulated vsize (Kb) 32640

[startup+250.029 s]
Raw data (loadavg): 0.99 0.85 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 24889 51 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 249.4
Current children cumulated vsize (Kb) 32640

[startup+260.031 s]
Raw data (loadavg): 0.99 0.86 0.88 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 25889 52 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134557369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 259.41
Current children cumulated vsize (Kb) 32640

[startup+270.032 s]
Raw data (loadavg): 0.99 0.86 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 26889 52 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 269.41
Current children cumulated vsize (Kb) 32640

[startup+280.032 s]
Raw data (loadavg): 0.99 0.87 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 27889 52 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 279.41
Current children cumulated vsize (Kb) 32640

[startup+290.033 s]
Raw data (loadavg): 0.99 0.87 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 28889 52 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223072 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 289.41
Current children cumulated vsize (Kb) 32640

[startup+300.034 s]
Raw data (loadavg): 0.99 0.87 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 29889 53 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 299.42
Current children cumulated vsize (Kb) 32640

[startup+310.035 s]
Raw data (loadavg): 0.99 0.88 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 30889 53 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 309.42
Current children cumulated vsize (Kb) 32640

[startup+320.036 s]
Raw data (loadavg): 0.99 0.88 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 31889 53 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 319.42
Current children cumulated vsize (Kb) 32640

[startup+330.038 s]
Raw data (loadavg): 0.99 0.88 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 32889 53 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 329.42
Current children cumulated vsize (Kb) 32640

[startup+340.038 s]
Raw data (loadavg): 0.99 0.89 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 33890 53 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 339.43
Current children cumulated vsize (Kb) 32640

[startup+350.04 s]
Raw data (loadavg): 0.99 0.89 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 34890 53 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 349.43
Current children cumulated vsize (Kb) 32640

[startup+360.041 s]
Raw data (loadavg): 0.99 0.89 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 35890 53 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 359.43
Current children cumulated vsize (Kb) 32640

[startup+370.041 s]
Raw data (loadavg): 0.99 0.90 0.89 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 36890 53 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 369.43
Current children cumulated vsize (Kb) 32640

[startup+380.043 s]
Raw data (loadavg): 0.99 0.90 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 37890 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 379.44
Current children cumulated vsize (Kb) 32640

[startup+390.043 s]
Raw data (loadavg): 0.99 0.90 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 38890 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 389.44
Current children cumulated vsize (Kb) 32640

[startup+400.045 s]
Raw data (loadavg): 0.99 0.91 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 39891 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 399.45
Current children cumulated vsize (Kb) 32640

[startup+410.046 s]
Raw data (loadavg): 0.99 0.91 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 40891 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 409.45
Current children cumulated vsize (Kb) 32640

[startup+420.047 s]
Raw data (loadavg): 0.99 0.91 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 41891 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134785070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 419.45
Current children cumulated vsize (Kb) 32640

[startup+430.048 s]
Raw data (loadavg): 0.99 0.91 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 42891 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 429.45
Current children cumulated vsize (Kb) 32640

[startup+440.049 s]
Raw data (loadavg): 0.99 0.92 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 43891 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223120 134556071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 439.45
Current children cumulated vsize (Kb) 32640

[startup+450.049 s]
Raw data (loadavg): 0.99 0.92 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 44891 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 449.45
Current children cumulated vsize (Kb) 32640

[startup+460.05 s]
Raw data (loadavg): 0.99 0.92 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 45892 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 459.46
Current children cumulated vsize (Kb) 32640

[startup+470.051 s]
Raw data (loadavg): 0.99 0.92 0.90 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 46892 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 469.46
Current children cumulated vsize (Kb) 32640

[startup+480.052 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 47892 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 479.46
Current children cumulated vsize (Kb) 32640

[startup+490.053 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 48892 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 489.46
Current children cumulated vsize (Kb) 32640

[startup+500.055 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 49893 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223040 134785070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 499.47
Current children cumulated vsize (Kb) 32640

[startup+510.055 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7423 0 0 0 50893 54 0 0 25 0 1 0 1785035493 31248384 7355 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7355 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 509.47
Current children cumulated vsize (Kb) 32640

[startup+520.055 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7425 0 0 0 51893 55 0 0 25 0 1 0 1785035493 31248384 7357 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7357 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 519.48
Current children cumulated vsize (Kb) 32640

[startup+530.056 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7425 0 0 0 52893 55 0 0 25 0 1 0 1785035493 31248384 7357 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7629 7357 145 145 0 7484 0
[pid=24971] vsize: 30516
Current children cumulated CPU time (s) 529.48
Current children cumulated vsize (Kb) 32640

[startup+540.058 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7437 0 0 0 53893 55 0 0 25 0 1 0 1785035493 31313920 7369 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7369 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 539.48
Current children cumulated vsize (Kb) 32704

[startup+550.059 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7438 0 0 0 54894 55 0 0 25 0 1 0 1785035493 31313920 7370 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7370 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 549.49
Current children cumulated vsize (Kb) 32704

[startup+560.06 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7440 0 0 0 55894 55 0 0 25 0 1 0 1785035493 31313920 7372 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7372 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 559.49
Current children cumulated vsize (Kb) 32704

[startup+570.06 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 56894 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 569.49
Current children cumulated vsize (Kb) 32704

[startup+580.061 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 57894 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221222912 134781309 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 579.49
Current children cumulated vsize (Kb) 32704

[startup+590.062 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 58894 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 589.49
Current children cumulated vsize (Kb) 32704

[startup+600.064 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 59894 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 599.49
Current children cumulated vsize (Kb) 32704

[startup+610.065 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 60895 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223120 134555953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 609.5
Current children cumulated vsize (Kb) 32704

[startup+620.066 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 61895 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223040 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 619.5
Current children cumulated vsize (Kb) 32704

[startup+630.066 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 62895 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 629.5
Current children cumulated vsize (Kb) 32704

[startup+640.067 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 63896 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 639.51
Current children cumulated vsize (Kb) 32704

[startup+650.069 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 64896 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 649.51
Current children cumulated vsize (Kb) 32704

[startup+660.07 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 65896 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 659.51
Current children cumulated vsize (Kb) 32704

[startup+670.071 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7441 0 0 0 66896 55 0 0 25 0 1 0 1785035493 31313920 7373 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7645 7373 145 145 0 7500 0
[pid=24971] vsize: 30580
Current children cumulated CPU time (s) 669.51
Current children cumulated vsize (Kb) 32704

[startup+680.072 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7462 0 0 0 67896 55 0 0 25 0 1 0 1785035493 31444992 7394 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7677 7394 145 145 0 7532 0
[pid=24971] vsize: 30708
Current children cumulated CPU time (s) 679.51
Current children cumulated vsize (Kb) 32832

[startup+690.073 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7474 0 0 0 68896 55 0 0 25 0 1 0 1785035493 31543296 7406 4294967295 134512640 135094434 3221224448 3221223104 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7701 7406 145 145 0 7556 0
[pid=24971] vsize: 30804
Current children cumulated CPU time (s) 689.51
Current children cumulated vsize (Kb) 32928

[startup+700.075 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7497 0 0 0 69896 55 0 0 25 0 1 0 1785035493 31674368 7429 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7733 7429 145 145 0 7588 0
[pid=24971] vsize: 30932
Current children cumulated CPU time (s) 699.51
Current children cumulated vsize (Kb) 33056

[startup+710.076 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7498 0 0 0 70897 55 0 0 25 0 1 0 1785035493 31674368 7430 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7733 7430 145 145 0 7588 0
[pid=24971] vsize: 30932
Current children cumulated CPU time (s) 709.52
Current children cumulated vsize (Kb) 33056

[startup+720.077 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7510 0 0 0 71897 55 0 0 25 0 1 0 1785035493 31739904 7442 4294967295 134512640 135094434 3221224448 3221223040 134556823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7749 7442 145 145 0 7604 0
[pid=24971] vsize: 30996
Current children cumulated CPU time (s) 719.52
Current children cumulated vsize (Kb) 33120

[startup+730.078 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7551 0 0 0 72897 56 0 0 25 0 1 0 1785035493 31936512 7483 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7797 7483 145 145 0 7652 0
[pid=24971] vsize: 31188
Current children cumulated CPU time (s) 729.53
Current children cumulated vsize (Kb) 33312

[startup+740.078 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7552 0 0 0 73897 56 0 0 25 0 1 0 1785035493 31936512 7484 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7797 7484 145 145 0 7652 0
[pid=24971] vsize: 31188
Current children cumulated CPU time (s) 739.53
Current children cumulated vsize (Kb) 33312

[startup+750.08 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 74897 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 749.53
Current children cumulated vsize (Kb) 33408

[startup+760.081 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 75897 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 759.53
Current children cumulated vsize (Kb) 33408

[startup+770.082 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 76898 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 769.54
Current children cumulated vsize (Kb) 33408

[startup+780.083 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 77898 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223040 134556791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 779.54
Current children cumulated vsize (Kb) 33408

[startup+790.084 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 78898 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 789.54
Current children cumulated vsize (Kb) 33408

[startup+800.085 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 79898 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 799.54
Current children cumulated vsize (Kb) 33408

[startup+810.086 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 80898 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 809.54
Current children cumulated vsize (Kb) 33408

[startup+820.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 81898 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 819.54
Current children cumulated vsize (Kb) 33408

[startup+830.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 82899 56 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 829.55
Current children cumulated vsize (Kb) 33408

[startup+840.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 83897 58 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223072 134557702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 839.55
Current children cumulated vsize (Kb) 33408

[startup+850.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 84898 58 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 849.56
Current children cumulated vsize (Kb) 33408

[startup+860.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 85898 58 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 859.56
Current children cumulated vsize (Kb) 33408

[startup+870.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 86897 59 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 869.56
Current children cumulated vsize (Kb) 33408

[startup+880.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7554 0 0 0 87897 59 0 0 25 0 1 0 1785035493 32034816 7486 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7486 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 879.56
Current children cumulated vsize (Kb) 33408

[startup+890.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7559 0 0 0 88898 59 0 0 25 0 1 0 1785035493 32034816 7491 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7821 7491 145 145 0 7676 0
[pid=24971] vsize: 31284
Current children cumulated CPU time (s) 889.57
Current children cumulated vsize (Kb) 33408

[startup+900.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 89898 59 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 899.57
Current children cumulated vsize (Kb) 33440

[startup+910.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 90898 59 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 909.57
Current children cumulated vsize (Kb) 33440

[startup+920.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 91898 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 919.58
Current children cumulated vsize (Kb) 33440

[startup+930.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 92898 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 929.58
Current children cumulated vsize (Kb) 33440

[startup+940.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 93897 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 939.57
Current children cumulated vsize (Kb) 33440

[startup+950.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 94896 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 949.56
Current children cumulated vsize (Kb) 33440

[startup+960.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 95897 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 959.57
Current children cumulated vsize (Kb) 33440

[startup+970.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 96897 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 969.57
Current children cumulated vsize (Kb) 33440

[startup+980.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 97897 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 979.57
Current children cumulated vsize (Kb) 33440

[startup+990.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 98897 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 989.57
Current children cumulated vsize (Kb) 33440

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 99897 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 999.57
Current children cumulated vsize (Kb) 33440

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7568 0 0 0 100897 60 0 0 25 0 1 0 1785035493 32067584 7500 4294967295 134512640 135094434 3221224448 3221223040 134557348 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7829 7500 145 145 0 7684 0
[pid=24971] vsize: 31316
Current children cumulated CPU time (s) 1009.57
Current children cumulated vsize (Kb) 33440

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7574 0 0 0 101897 61 0 0 25 0 1 0 1785035493 32100352 7506 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7506 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1019.58
Current children cumulated vsize (Kb) 33472

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 102897 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1029.58
Current children cumulated vsize (Kb) 33472

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 103898 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1039.59
Current children cumulated vsize (Kb) 33472

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 104898 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1049.59
Current children cumulated vsize (Kb) 33472

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 105898 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1059.59
Current children cumulated vsize (Kb) 33472

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 106898 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1069.59
Current children cumulated vsize (Kb) 33472

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 107898 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1079.59
Current children cumulated vsize (Kb) 33472

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 108899 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1089.6
Current children cumulated vsize (Kb) 33472

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 109899 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1099.6
Current children cumulated vsize (Kb) 33472

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 110899 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1109.6
Current children cumulated vsize (Kb) 33472

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 111899 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1119.6
Current children cumulated vsize (Kb) 33472

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 112899 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1129.6
Current children cumulated vsize (Kb) 33472

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 113899 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1139.6
Current children cumulated vsize (Kb) 33472

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 114900 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223088 134562165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1149.61
Current children cumulated vsize (Kb) 33472

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 115900 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1159.61
Current children cumulated vsize (Kb) 33472

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 116900 61 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1169.61
Current children cumulated vsize (Kb) 33472

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7575 0 0 0 117900 62 0 0 25 0 1 0 1785035493 32100352 7507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7507 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1179.62
Current children cumulated vsize (Kb) 33472

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7577 0 0 0 118900 62 0 0 25 0 1 0 1785035493 32100352 7509 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7509 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1189.62
Current children cumulated vsize (Kb) 33472

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7577 0 0 0 119900 62 0 0 25 0 1 0 1785035493 32100352 7509 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7509 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1199.62
Current children cumulated vsize (Kb) 33472

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7578 0 0 0 120901 62 0 0 25 0 1 0 1785035493 32100352 7510 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7510 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1209.63
Current children cumulated vsize (Kb) 33472



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24971
Raw data (/proc/24967/stat): 24967 (minisat+_script) S 24966 24967 8263 0 -1 0 288 239 0 0 0 0 0 0 21 0 1 0 1785035488 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24967/statm): 531 226 485 147 0 384 0
[pid=24967] vsize: 2124
Raw data (/proc/24971/stat): 24971 (minisat+_64-bit) R 24967 24967 8263 0 -1 0 7578 0 0 0 120901 62 0 0 25 0 1 0 1785035493 32100352 7510 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24971/statm): 7837 7510 145 145 0 7692 0
[pid=24971] vsize: 31348
Current children cumulated CPU time (s) 1209.63
Current children cumulated vsize (Kb) 33472

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1209.65
CPU user time (s): 1209.02
CPU system time (s): 0.635903
CPU usage (%): 99.9595
Max. virtual memory (cumulated for all children) (Kb): 33472

Verifier Data

ERROR: no interpretation found !