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/synthesis-ptl-cmos-circuits/normalized-cm42a.opb
MD5SUM62b75258091a8b1382fa8b1c633d9511
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 694
Optimality of the best value was proved YES
Number of terms in the objective function 99
Biggest coefficient in the objective function 60
Number of bits for the biggest coefficient in the objective function 6
Sum of the numbers in the objective function 4087
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 60
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 4087
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark13.371
Number of variables99
Total number of constraints185
Number of constraints which are clauses185
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 constraint20

Trace number 2203

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        935888 kB
Buffers:         26072 kB
Cached:          45900 kB
SwapCached:        516 kB
Active:          26108 kB
Inactive:        48300 kB
HighTotal:      131008 kB
HighFree:        81144 kB
LowTotal:       903652 kB
LowFree:        854744 kB
SwapTotal:     2097892 kB
SwapFree:      2096672 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            18652 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:30:46 (client local time) WITH STATUS 10 IN 1209.84 SECONDS
stats: 2595 7 1209.84 10

Solver Data

c Parsing PB file...
c Converting 185 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 |     185      626 |      61       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 939
c ---[   0]---> Sorter-cost: 8480     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21020    49263 |    7006       0        0     nan |  0.000 % |
c |       100 |   20519    48138 |    7706      89     1028    11.6 |  1.713 % |
c |       250 |   20519    48138 |    8477     239     3004    12.6 |  1.713 % |
c |       475 |   20519    48138 |    9324     464     6184    13.3 |  1.713 % |
c |       812 |   20519    48138 |   10257     801    13852    17.3 |  1.713 % |
c |      1318 |   20519    48138 |   11283    1307    26131    20.0 |  1.713 % |
c |      2077 |   20519    48138 |   12411    2066    36951    17.9 |  1.713 % |
c |      3218 |   20519    48138 |   13652    3207    50232    15.7 |  1.713 % |
c ==============================================================================
c Found solution: 930
c ---[   0]---> Sorter-cost: 6779     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4515 |   36935    86465 |   12311    4239   125935    29.7 |  1.713 % |
c |      4615 |   36935    86465 |   13542    4339   127931    29.5 |  1.049 % |
c ==============================================================================
c Found solution: 871
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4625 |   37031    86764 |   12343    4349   128034    29.4 |  1.049 % |
c ==============================================================================
c Found solution: 868
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4628 |   37041    86807 |   12347    4352   128611    29.6 |  1.049 % |
c ==============================================================================
c Found solution: 848
c ---[   0]---> Sorter-cost:    2     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4714 |   37044    86814 |   12348    4438   131852    29.7 |  1.049 % |
c |      4815 |   37044    86814 |   13582    4539   137459    30.3 |  1.066 % |
c |      4965 |   37044    86814 |   14941    4689   139947    29.8 |  1.066 % |
c ==============================================================================
c Found solution: 843
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4995 |   37052    86848 |   12350    4719   141269    29.9 |  1.066 % |
c |      5095 |   37052    86848 |   13585    4819   146504    30.4 |  1.073 % |
c |      5245 |   37052    86848 |   14943    4969   148441    29.9 |  1.073 % |
c ==============================================================================
c Found solution: 760
c ---[   0]---> Sorter-cost:    4     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5423 |   37074    86904 |   12358    5147   151537    29.4 |  1.073 % |
c |      5525 |   36992    86727 |   13593    5248   152666    29.1 |  1.269 % |
c |      5677 |   36992    86727 |   14953    5400   154353    28.6 |  1.269 % |
c |      5902 |   36845    86396 |   16448    5570   159179    28.6 |  1.560 % |
c |      6239 |   36845    86396 |   18093    5907   171397    29.0 |  1.560 % |
c |      6747 |   36845    86396 |   19902    6415   186197    29.0 |  1.560 % |
c ==============================================================================
c Found solution: 750
c ---[   0]---> Sorter-cost:    4     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6801 |   36853    86417 |   12284    6469   186718    28.9 |  1.560 % |
c |      6903 |   36853    86417 |   13512    6571   189822    28.9 |  1.567 % |
c |      7053 |   36853    86417 |   14863    6721   194339    28.9 |  1.567 % |
c ==============================================================================
c Found solution: 727
c ---[   0]---> Sorter-cost:    2     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7081 |   36859    86432 |   12286    6749   194737    28.9 |  1.567 % |
c |      7185 |   36859    86432 |   13514    6853   196190    28.6 |  1.574 % |
c ==============================================================================
c Found solution: 725
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7267 |   36863    86444 |   12287    6935   197305    28.5 |  1.574 % |
c |      7368 |   36863    86444 |   13515    7036   199384    28.3 |  1.581 % |
c |      7519 |   36863    86444 |   14867    7187   204956    28.5 |  1.581 % |
c |      7745 |   36863    86444 |   16353    7413   209249    28.2 |  1.581 % |
c |      8082 |   36863    86444 |   17989    7750   217404    28.1 |  1.581 % |
c |      8588 |   36863    86444 |   19788    8256   232248    28.1 |  1.581 % |
c |      9350 |   36863    86444 |   21767    9018   254804    28.3 |  1.581 % |
c |     10490 |   36863    86444 |   23943   10158   295961    29.1 |  1.581 % |
c |     12198 |   36863    86444 |   26338   11866   348800    29.4 |  1.581 % |
c |     14760 |   36863    86444 |   28972   14428   430582    29.8 |  1.581 % |
c |     18605 |   36863    86444 |   31869   18273   554507    30.3 |  1.581 % |
c |     24371 |   36863    86444 |   35056   24039   742719    30.9 |  1.581 % |
c ==============================================================================
c Found solution: 721
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32325 |   36870    86462 |   12290   31993  1001266    31.3 |  1.581 % |
c |     32425 |   36870    86462 |   13519    7193   181885    25.3 |  1.587 % |
c |     32575 |   36870    86462 |   14870    7343   187243    25.5 |  1.587 % |
c |     32800 |   36870    86462 |   16357    7568   193785    25.6 |  1.587 % |
c |     33137 |   36870    86462 |   17993    7905   204955    25.9 |  1.587 % |
c |     33643 |   36870    86462 |   19793    8411   222819    26.5 |  1.587 % |
c |     34402 |   36870    86462 |   21772    9170   247919    27.0 |  1.587 % |
c |     35541 |   36870    86462 |   23949   10309   281263    27.3 |  1.587 % |
c |     37251 |   36673    86016 |   26344   11354   308391    27.2 |  2.010 % |
c |     39814 |   36673    86016 |   28979   13917   414447    29.8 |  2.010 % |
c |     43658 |   36673    86016 |   31877   17761   606961    34.2 |  2.010 % |
c |     49424 |   36673    86016 |   35064   23527   847619    36.0 |  2.010 % |
c ==============================================================================
c Found solution: 696
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54796 |   36681    86035 |   12227   28899  1065079    36.9 |  2.010 % |
c |     54897 |   36681    86035 |   13449    7326   204774    28.0 |  2.016 % |
c |     55050 |   36681    86035 |   14794    7479   209137    28.0 |  2.016 % |
c |     55279 |   36681    86035 |   16274    7708   217316    28.2 |  2.016 % |
c |     55616 |   36681    86035 |   17901    8045   227927    28.3 |  2.016 % |
c |     56123 |   36681    86035 |   19691    8552   242511    28.4 |  2.016 % |
c |     56882 |   36681    86035 |   21660    9311   267475    28.7 |  2.016 % |
c |     58021 |   36681    86035 |   23826   10450   303809    29.1 |  2.016 % |
c |     59730 |   36681    86035 |   26209   12159   371468    30.6 |  2.016 % |
c |     62293 |   36681    86035 |   28830   14722   458406    31.1 |  2.016 % |
c |     66138 |   36596    85839 |   31713   18566   616592    33.2 |  2.220 % |
c |     71905 |   36596    85839 |   34885   24333   831643    34.2 |  2.220 % |
c |     80554 |   36596    85839 |   38373   32982  1166482    35.4 |  2.220 % |
c |     93528 |   36596    85839 |   42210   22811   854263    37.4 |  2.220 % |
c |    112990 |   36596    85839 |   46432   42273  1684549    39.8 |  2.220 % |
c |    142185 |   36596    85839 |   51075   42418  1729647    40.8 |  2.220 % |
c |    185974 |   36596    85839 |   56182   51791  2490585    48.1 |  2.220 % |
c ==============================================================================
c Found solution: 694
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225026 |   36603    85855 |   12201   53073  2198951    41.4 |  2.220 % |
c |    225126 |   36603    85855 |   13421    9803   290594    29.6 |  2.227 % |
c |    225276 |   36603    85855 |   14763    9953   297699    29.9 |  2.227 % |
c |    225504 |   36603    85855 |   16239   10181   308736    30.3 |  2.227 % |
c |    225843 |   36603    85855 |   17863   10520   324699    30.9 |  2.227 % |
c |    226349 |   36603    85855 |   19649   11026   350759    31.8 |  2.227 % |
c |    227109 |   36603    85855 |   21614   11786   380901    32.3 |  2.227 % |
c |    228248 |   36603    85855 |   23776   12925   435314    33.7 |  2.227 % |
c |    229958 |   36603    85855 |   26153   14635   527195    36.0 |  2.227 % |
c |    232522 |   36603    85855 |   28769   17199   660247    38.4 |  2.227 % |
c |    236366 |   36603    85855 |   31646   21043   843540    40.1 |  2.227 % |
c |    242132 |   36603    85855 |   34810   26809  1110921    41.4 |  2.227 % |
c |    250782 |   36603    85855 |   38291   35459  1600907    45.1 |  2.227 % |
c |    263756 |   36603    85855 |   42121   26184  1173309    44.8 |  2.227 % |
c |    283217 |   36603    85855 |   46333   18155   718766    39.6 |  2.227 % |

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/25857/stat): 25857 (minisat+_script) R 25856 25857 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843334155 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/25857/statm): 174 3 169 147 0 27 0
[pid=25857] 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=25858
New process pid=25859
New process pid=25860
One traced child (pid=25859) exited with status: 0
execve syscall for /bin/sed executable
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=25860) exited with status: 0
One traced child (pid=25858) exited with status: 0
New process pid=25861
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-cm42a.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 1461 0 0 0 982 6 0 0 25 0 1 0 1843334160 6553600 1447 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 1600 1447 145 145 0 1455 0
[pid=25861] vsize: 6400
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 8524

[startup+20.0056 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 1613 0 0 0 1979 8 0 0 25 0 1 0 1843334160 7196672 1599 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 1757 1599 145 145 0 1612 0
[pid=25861] vsize: 7028
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 9152

[startup+30.0072 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 1758 0 0 0 2977 10 0 0 25 0 1 0 1843334160 7782400 1744 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 1900 1744 145 145 0 1755 0
[pid=25861] vsize: 7600
Current children cumulated CPU time (s) 29.87
Current children cumulated vsize (Kb) 9724

[startup+40.0078 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 1894 0 0 0 3973 12 0 0 25 0 1 0 1843334160 8331264 1880 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2034 1880 145 145 0 1889 0
[pid=25861] vsize: 8136
Current children cumulated CPU time (s) 39.85
Current children cumulated vsize (Kb) 10260

[startup+50.0094 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2024 0 0 0 4970 13 0 0 25 0 1 0 1843334160 8929280 2010 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2180 2010 145 145 0 2035 0
[pid=25861] vsize: 8720
Current children cumulated CPU time (s) 49.83
Current children cumulated vsize (Kb) 10844

[startup+60.01 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2136 0 0 0 5968 14 0 0 25 0 1 0 1843334160 9379840 2122 4294967295 134512640 135094434 3221224448 3221223120 134555802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2290 2122 145 145 0 2145 0
[pid=25861] vsize: 9160
Current children cumulated CPU time (s) 59.82
Current children cumulated vsize (Kb) 11284

[startup+70.0116 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2272 0 0 0 6966 15 0 0 25 0 1 0 1843334160 9928704 2258 4294967295 134512640 135094434 3221224448 3221223040 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2424 2258 145 145 0 2279 0
[pid=25861] vsize: 9696
Current children cumulated CPU time (s) 69.81
Current children cumulated vsize (Kb) 11820

[startup+80.0132 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2394 0 0 0 7964 16 0 0 25 0 1 0 1843334160 10428416 2380 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2546 2380 145 145 0 2401 0
[pid=25861] vsize: 10184
Current children cumulated CPU time (s) 79.8
Current children cumulated vsize (Kb) 12308

[startup+90.0138 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2524 0 0 0 8961 18 0 0 25 0 1 0 1843334160 10944512 2510 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2672 2510 145 145 0 2527 0
[pid=25861] vsize: 10688
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 12812

[startup+100.015 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2588 0 0 0 9959 20 0 0 25 0 1 0 1843334160 11206656 2574 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2736 2574 145 145 0 2591 0
[pid=25861] vsize: 10944
Current children cumulated CPU time (s) 99.79
Current children cumulated vsize (Kb) 13068

[startup+110.016 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2590 0 0 0 10958 20 0 0 25 0 1 0 1843334160 11218944 2576 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2739 2576 145 145 0 2594 0
[pid=25861] vsize: 10956
Current children cumulated CPU time (s) 109.78
Current children cumulated vsize (Kb) 13080

[startup+120.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2600 0 0 0 11957 21 0 0 25 0 1 0 1843334160 11268096 2586 4294967295 134512640 135094434 3221224448 3221223120 134555566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2751 2586 145 145 0 2606 0
[pid=25861] vsize: 11004
Current children cumulated CPU time (s) 119.78
Current children cumulated vsize (Kb) 13128

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2603 0 0 0 12957 21 0 0 25 0 1 0 1843334160 11280384 2589 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2754 2589 145 145 0 2609 0
[pid=25861] vsize: 11016
Current children cumulated CPU time (s) 129.78
Current children cumulated vsize (Kb) 13140

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2614 0 0 0 13956 22 0 0 25 0 1 0 1843334160 11329536 2600 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2766 2600 145 145 0 2621 0
[pid=25861] vsize: 11064
Current children cumulated CPU time (s) 139.78
Current children cumulated vsize (Kb) 13188

[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2628 0 0 0 14956 23 0 0 25 0 1 0 1843334160 11395072 2614 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2782 2614 145 145 0 2637 0
[pid=25861] vsize: 11128
Current children cumulated CPU time (s) 149.79
Current children cumulated vsize (Kb) 13252

[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2638 0 0 0 15955 23 0 0 25 0 1 0 1843334160 11427840 2624 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2790 2624 145 145 0 2645 0
[pid=25861] vsize: 11160
Current children cumulated CPU time (s) 159.78
Current children cumulated vsize (Kb) 13284

[startup+170.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2687 0 0 0 16954 24 0 0 25 0 1 0 1843334160 11624448 2673 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2838 2673 145 145 0 2693 0
[pid=25861] vsize: 11352
Current children cumulated CPU time (s) 169.78
Current children cumulated vsize (Kb) 13476

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2769 0 0 0 17952 25 0 0 25 0 1 0 1843334160 11976704 2755 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2924 2755 145 145 0 2779 0
[pid=25861] vsize: 11696
Current children cumulated CPU time (s) 179.77
Current children cumulated vsize (Kb) 13820

[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2769 0 0 0 18952 25 0 0 25 0 1 0 1843334160 11976704 2755 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2924 2755 145 145 0 2779 0
[pid=25861] vsize: 11696
Current children cumulated CPU time (s) 189.77
Current children cumulated vsize (Kb) 13820

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2771 0 0 0 19952 26 0 0 25 0 1 0 1843334160 11988992 2757 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2927 2757 145 145 0 2782 0
[pid=25861] vsize: 11708
Current children cumulated CPU time (s) 199.78
Current children cumulated vsize (Kb) 13832

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2792 0 0 0 20951 26 0 0 25 0 1 0 1843334160 12083200 2778 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2950 2778 145 145 0 2805 0
[pid=25861] vsize: 11800
Current children cumulated CPU time (s) 209.77
Current children cumulated vsize (Kb) 13924

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2794 0 0 0 21951 27 0 0 25 0 1 0 1843334160 12083200 2780 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2950 2780 145 145 0 2805 0
[pid=25861] vsize: 11800
Current children cumulated CPU time (s) 219.78
Current children cumulated vsize (Kb) 13924

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2814 0 0 0 22951 27 0 0 25 0 1 0 1843334160 12214272 2800 4294967295 134512640 135094434 3221224448 3221223072 134562078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 2982 2800 145 145 0 2837 0
[pid=25861] vsize: 11928
Current children cumulated CPU time (s) 229.78
Current children cumulated vsize (Kb) 14052

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2830 0 0 0 23950 27 0 0 25 0 1 0 1843334160 12312576 2816 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 3006 2816 145 145 0 2861 0
[pid=25861] vsize: 12024
Current children cumulated CPU time (s) 239.77
Current children cumulated vsize (Kb) 14148

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2830 0 0 0 24950 28 0 0 25 0 1 0 1843334160 12312576 2816 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 3006 2816 145 145 0 2861 0
[pid=25861] vsize: 12024
Current children cumulated CPU time (s) 249.78
Current children cumulated vsize (Kb) 14148

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2852 0 0 0 25949 29 0 0 25 0 1 0 1843334160 12398592 2838 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 3027 2838 145 145 0 2882 0
[pid=25861] vsize: 12108
Current children cumulated CPU time (s) 259.78
Current children cumulated vsize (Kb) 14232

[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 2951 0 0 0 26948 29 0 0 25 0 1 0 1843334160 12795904 2937 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3124 2937 145 145 0 2979 0
[pid=25861] vsize: 12496
Current children cumulated CPU time (s) 269.77
Current children cumulated vsize (Kb) 14620

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3067 0 0 0 27947 30 0 0 25 0 1 0 1843334160 13447168 3053 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3283 3053 145 145 0 3138 0
[pid=25861] vsize: 13132
Current children cumulated CPU time (s) 279.77
Current children cumulated vsize (Kb) 15256

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3185 0 0 0 28945 32 0 0 25 0 1 0 1843334160 13914112 3171 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3397 3171 145 145 0 3252 0
[pid=25861] vsize: 13588
Current children cumulated CPU time (s) 289.77
Current children cumulated vsize (Kb) 15712

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3300 0 0 0 29943 33 0 0 25 0 1 0 1843334160 14434304 3286 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3524 3286 145 145 0 3379 0
[pid=25861] vsize: 14096
Current children cumulated CPU time (s) 299.76
Current children cumulated vsize (Kb) 16220

[startup+310.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3300 0 0 0 30944 33 0 0 25 0 1 0 1843334160 14434304 3286 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3524 3286 145 145 0 3379 0
[pid=25861] vsize: 14096
Current children cumulated CPU time (s) 309.77
Current children cumulated vsize (Kb) 16220

[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3303 0 0 0 31944 33 0 0 25 0 1 0 1843334160 14450688 3289 4294967295 134512640 135094434 3221224448 3221223072 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3528 3289 145 145 0 3383 0
[pid=25861] vsize: 14112
Current children cumulated CPU time (s) 319.77
Current children cumulated vsize (Kb) 16236

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3306 0 0 0 32944 33 0 0 25 0 1 0 1843334160 14450688 3292 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3528 3292 145 145 0 3383 0
[pid=25861] vsize: 14112
Current children cumulated CPU time (s) 329.77
Current children cumulated vsize (Kb) 16236

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3315 0 0 0 33944 33 0 0 25 0 1 0 1843334160 14512128 3301 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3543 3301 145 145 0 3398 0
[pid=25861] vsize: 14172
Current children cumulated CPU time (s) 339.77
Current children cumulated vsize (Kb) 16296

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3316 0 0 0 34943 34 0 0 25 0 1 0 1843334160 14512128 3302 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3543 3302 145 145 0 3398 0
[pid=25861] vsize: 14172
Current children cumulated CPU time (s) 349.77
Current children cumulated vsize (Kb) 16296

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3326 0 0 0 35943 35 0 0 25 0 1 0 1843334160 14544896 3312 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3551 3312 145 145 0 3406 0
[pid=25861] vsize: 14204
Current children cumulated CPU time (s) 359.78
Current children cumulated vsize (Kb) 16328

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3326 0 0 0 36943 35 0 0 25 0 1 0 1843334160 14544896 3312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3551 3312 145 145 0 3406 0
[pid=25861] vsize: 14204
Current children cumulated CPU time (s) 369.78
Current children cumulated vsize (Kb) 16328

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3400 0 0 0 37941 36 0 0 25 0 1 0 1843334160 14876672 3386 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3632 3386 145 145 0 3487 0
[pid=25861] vsize: 14528
Current children cumulated CPU time (s) 379.77
Current children cumulated vsize (Kb) 16652

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3505 0 0 0 38940 37 0 0 25 0 1 0 1843334160 15314944 3491 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3739 3491 145 145 0 3594 0
[pid=25861] vsize: 14956
Current children cumulated CPU time (s) 389.77
Current children cumulated vsize (Kb) 17080

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3591 0 0 0 39939 37 0 0 25 0 1 0 1843334160 15675392 3577 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3827 3577 145 145 0 3682 0
[pid=25861] vsize: 15308
Current children cumulated CPU time (s) 399.76
Current children cumulated vsize (Kb) 17432

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3677 0 0 0 40937 38 0 0 25 0 1 0 1843334160 15994880 3663 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 3905 3663 145 145 0 3760 0
[pid=25861] vsize: 15620
Current children cumulated CPU time (s) 409.75
Current children cumulated vsize (Kb) 17744

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3781 0 0 0 41936 39 0 0 25 0 1 0 1843334160 16470016 3767 4294967295 134512640 135094434 3221224448 3221223152 134555118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4021 3767 145 145 0 3876 0
[pid=25861] vsize: 16084
Current children cumulated CPU time (s) 419.75
Current children cumulated vsize (Kb) 18208

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3895 0 0 0 42934 40 0 0 25 0 1 0 1843334160 16957440 3881 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4140 3881 145 145 0 3995 0
[pid=25861] vsize: 16560
Current children cumulated CPU time (s) 429.74
Current children cumulated vsize (Kb) 18684

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3946 0 0 0 43933 41 0 0 25 0 1 0 1843334160 17154048 3932 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4188 3932 145 145 0 4043 0
[pid=25861] vsize: 16752
Current children cumulated CPU time (s) 439.74
Current children cumulated vsize (Kb) 18876

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3946 0 0 0 44934 41 0 0 25 0 1 0 1843334160 17154048 3932 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4188 3932 145 145 0 4043 0
[pid=25861] vsize: 16752
Current children cumulated CPU time (s) 449.75
Current children cumulated vsize (Kb) 18876

[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3946 0 0 0 45934 41 0 0 25 0 1 0 1843334160 17154048 3932 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4188 3932 145 145 0 4043 0
[pid=25861] vsize: 16752
Current children cumulated CPU time (s) 459.75
Current children cumulated vsize (Kb) 18876

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3946 0 0 0 46934 41 0 0 25 0 1 0 1843334160 17154048 3932 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4188 3932 145 145 0 4043 0
[pid=25861] vsize: 16752
Current children cumulated CPU time (s) 469.75
Current children cumulated vsize (Kb) 18876

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3946 0 0 0 47934 41 0 0 25 0 1 0 1843334160 17154048 3932 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4188 3932 145 145 0 4043 0
[pid=25861] vsize: 16752
Current children cumulated CPU time (s) 479.75
Current children cumulated vsize (Kb) 18876

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3946 0 0 0 48934 41 0 0 25 0 1 0 1843334160 17154048 3932 4294967295 134512640 135094434 3221224448 3221223072 134562122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4188 3932 145 145 0 4043 0
[pid=25861] vsize: 16752
Current children cumulated CPU time (s) 489.75
Current children cumulated vsize (Kb) 18876

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3963 0 0 0 49934 41 0 0 25 0 1 0 1843334160 17252352 3949 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4212 3949 145 145 0 4067 0
[pid=25861] vsize: 16848
Current children cumulated CPU time (s) 499.75
Current children cumulated vsize (Kb) 18972

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3966 0 0 0 50934 41 0 0 25 0 1 0 1843334160 17350656 3952 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4236 3952 145 145 0 4091 0
[pid=25861] vsize: 16944
Current children cumulated CPU time (s) 509.75
Current children cumulated vsize (Kb) 19068

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3966 0 0 0 51935 41 0 0 25 0 1 0 1843334160 17350656 3952 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4236 3952 145 145 0 4091 0
[pid=25861] vsize: 16944
Current children cumulated CPU time (s) 519.76
Current children cumulated vsize (Kb) 19068

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3966 0 0 0 52935 42 0 0 25 0 1 0 1843334160 17350656 3952 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4236 3952 145 145 0 4091 0
[pid=25861] vsize: 16944
Current children cumulated CPU time (s) 529.77
Current children cumulated vsize (Kb) 19068

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 3997 0 0 0 53934 42 0 0 25 0 1 0 1843334160 17432576 3983 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4256 3983 145 145 0 4111 0
[pid=25861] vsize: 17024
Current children cumulated CPU time (s) 539.76
Current children cumulated vsize (Kb) 19148

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4014 0 0 0 54935 42 0 0 25 0 1 0 1843334160 17498112 4000 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4272 4000 145 145 0 4127 0
[pid=25861] vsize: 17088
Current children cumulated CPU time (s) 549.77
Current children cumulated vsize (Kb) 19212

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4014 0 0 0 55935 42 0 0 25 0 1 0 1843334160 17498112 4000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4272 4000 145 145 0 4127 0
[pid=25861] vsize: 17088
Current children cumulated CPU time (s) 559.77
Current children cumulated vsize (Kb) 19212

[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4124 0 0 0 56933 43 0 0 25 0 1 0 1843334160 17952768 4110 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4383 4110 145 145 0 4238 0
[pid=25861] vsize: 17532
Current children cumulated CPU time (s) 569.76
Current children cumulated vsize (Kb) 19656

[startup+580.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4254 0 0 0 57930 44 0 0 25 0 1 0 1843334160 18477056 4240 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4511 4240 145 145 0 4366 0
[pid=25861] vsize: 18044
Current children cumulated CPU time (s) 579.74
Current children cumulated vsize (Kb) 20168

[startup+590.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4350 0 0 0 58928 46 0 0 25 0 1 0 1843334160 18857984 4336 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4604 4336 145 145 0 4459 0
[pid=25861] vsize: 18416
Current children cumulated CPU time (s) 589.74
Current children cumulated vsize (Kb) 20540

[startup+600.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4350 0 0 0 59929 46 0 0 25 0 1 0 1843334160 18857984 4336 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4604 4336 145 145 0 4459 0
[pid=25861] vsize: 18416
Current children cumulated CPU time (s) 599.75
Current children cumulated vsize (Kb) 20540

[startup+610.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4350 0 0 0 60929 46 0 0 25 0 1 0 1843334160 18857984 4336 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4604 4336 145 145 0 4459 0
[pid=25861] vsize: 18416
Current children cumulated CPU time (s) 609.75
Current children cumulated vsize (Kb) 20540

[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4350 0 0 0 61929 46 0 0 25 0 1 0 1843334160 18857984 4336 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4604 4336 145 145 0 4459 0
[pid=25861] vsize: 18416
Current children cumulated CPU time (s) 619.75
Current children cumulated vsize (Kb) 20540

[startup+630.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4350 0 0 0 62929 46 0 0 25 0 1 0 1843334160 18857984 4336 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4604 4336 145 145 0 4459 0
[pid=25861] vsize: 18416
Current children cumulated CPU time (s) 629.75
Current children cumulated vsize (Kb) 20540

[startup+640.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4350 0 0 0 63929 46 0 0 25 0 1 0 1843334160 18857984 4336 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4604 4336 145 145 0 4459 0
[pid=25861] vsize: 18416
Current children cumulated CPU time (s) 639.75
Current children cumulated vsize (Kb) 20540

[startup+650.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4350 0 0 0 64930 46 0 0 25 0 1 0 1843334160 18857984 4336 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4604 4336 145 145 0 4459 0
[pid=25861] vsize: 18416
Current children cumulated CPU time (s) 649.76
Current children cumulated vsize (Kb) 20540

[startup+660.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4350 0 0 0 65930 46 0 0 25 0 1 0 1843334160 18857984 4336 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4604 4336 145 145 0 4459 0
[pid=25861] vsize: 18416
Current children cumulated CPU time (s) 659.76
Current children cumulated vsize (Kb) 20540

[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4361 0 0 0 66930 46 0 0 25 0 1 0 1843334160 18923520 4347 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4620 4347 145 145 0 4475 0
[pid=25861] vsize: 18480
Current children cumulated CPU time (s) 669.76
Current children cumulated vsize (Kb) 20604

[startup+680.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4379 0 0 0 67930 46 0 0 25 0 1 0 1843334160 19005440 4365 4294967295 134512640 135094434 3221224448 3221223040 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4640 4365 145 145 0 4495 0
[pid=25861] vsize: 18560
Current children cumulated CPU time (s) 679.76
Current children cumulated vsize (Kb) 20684

[startup+690.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4380 0 0 0 68930 46 0 0 25 0 1 0 1843334160 19005440 4366 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4640 4366 145 145 0 4495 0
[pid=25861] vsize: 18560
Current children cumulated CPU time (s) 689.76
Current children cumulated vsize (Kb) 20684

[startup+700.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4391 0 0 0 69930 47 0 0 25 0 1 0 1843334160 19070976 4377 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4656 4377 145 145 0 4511 0
[pid=25861] vsize: 18624
Current children cumulated CPU time (s) 699.77
Current children cumulated vsize (Kb) 20748

[startup+710.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4403 0 0 0 70931 47 0 0 25 0 1 0 1843334160 19136512 4389 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4672 4389 145 145 0 4527 0
[pid=25861] vsize: 18688
Current children cumulated CPU time (s) 709.78
Current children cumulated vsize (Kb) 20812

[startup+720.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4492 0 0 0 71929 47 0 0 25 0 1 0 1843334160 19529728 4478 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4768 4478 145 145 0 4623 0
[pid=25861] vsize: 19072
Current children cumulated CPU time (s) 719.76
Current children cumulated vsize (Kb) 21196

[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4641 0 0 0 72927 49 0 0 25 0 1 0 1843334160 20135936 4627 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 4916 4627 145 145 0 4771 0
[pid=25861] vsize: 19664
Current children cumulated CPU time (s) 729.76
Current children cumulated vsize (Kb) 21788

[startup+740.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4750 0 0 0 73924 50 0 0 25 0 1 0 1843334160 20570112 4736 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 5022 4736 145 145 0 4877 0
[pid=25861] vsize: 20088
Current children cumulated CPU time (s) 739.74
Current children cumulated vsize (Kb) 22212

[startup+750.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4814 0 0 0 74922 51 0 0 25 0 1 0 1843334160 20824064 4800 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 5084 4800 145 145 0 4939 0
[pid=25861] vsize: 20336
Current children cumulated CPU time (s) 749.73
Current children cumulated vsize (Kb) 22460

[startup+760.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4904 0 0 0 75920 52 0 0 25 0 1 0 1843334160 21209088 4890 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5178 4890 145 145 0 5033 0
[pid=25861] vsize: 20712
Current children cumulated CPU time (s) 759.72
Current children cumulated vsize (Kb) 22836

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4995 0 0 0 76919 53 0 0 25 0 1 0 1843334160 21569536 4981 4294967295 134512640 135094434 3221224448 3221223040 134784939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5266 4981 145 145 0 5121 0
[pid=25861] vsize: 21064
Current children cumulated CPU time (s) 769.72
Current children cumulated vsize (Kb) 23188

[startup+780.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 4996 0 0 0 77919 53 0 0 25 0 1 0 1843334160 21569536 4982 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5266 4982 145 145 0 5121 0
[pid=25861] vsize: 21064
Current children cumulated CPU time (s) 779.72
Current children cumulated vsize (Kb) 23188

[startup+790.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5005 0 0 0 78919 53 0 0 25 0 1 0 1843334160 21635072 4991 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5282 4991 145 145 0 5137 0
[pid=25861] vsize: 21128
Current children cumulated CPU time (s) 789.72
Current children cumulated vsize (Kb) 23252

[startup+800.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5005 0 0 0 79919 53 0 0 25 0 1 0 1843334160 21635072 4991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5282 4991 145 145 0 5137 0
[pid=25861] vsize: 21128
Current children cumulated CPU time (s) 799.72
Current children cumulated vsize (Kb) 23252

[startup+810.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5017 0 0 0 80919 53 0 0 25 0 1 0 1843334160 21700608 5003 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5298 5003 145 145 0 5153 0
[pid=25861] vsize: 21192
Current children cumulated CPU time (s) 809.72
Current children cumulated vsize (Kb) 23316

[startup+820.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5017 0 0 0 81920 53 0 0 25 0 1 0 1843334160 21700608 5003 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5298 5003 145 145 0 5153 0
[pid=25861] vsize: 21192
Current children cumulated CPU time (s) 819.73
Current children cumulated vsize (Kb) 23316

[startup+830.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5018 0 0 0 82920 53 0 0 25 0 1 0 1843334160 21700608 5004 4294967295 134512640 135094434 3221224448 3221223072 134557616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5298 5004 145 145 0 5153 0
[pid=25861] vsize: 21192
Current children cumulated CPU time (s) 829.73
Current children cumulated vsize (Kb) 23316

[startup+840.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5018 0 0 0 83920 53 0 0 25 0 1 0 1843334160 21700608 5004 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5298 5004 145 145 0 5153 0
[pid=25861] vsize: 21192
Current children cumulated CPU time (s) 839.73
Current children cumulated vsize (Kb) 23316

[startup+850.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5018 0 0 0 84920 53 0 0 25 0 1 0 1843334160 21700608 5004 4294967295 134512640 135094434 3221224448 3221223040 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5298 5004 145 145 0 5153 0
[pid=25861] vsize: 21192
Current children cumulated CPU time (s) 849.73
Current children cumulated vsize (Kb) 23316

[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5018 0 0 0 85920 53 0 0 25 0 1 0 1843334160 21700608 5004 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5298 5004 145 145 0 5153 0
[pid=25861] vsize: 21192
Current children cumulated CPU time (s) 859.73
Current children cumulated vsize (Kb) 23316

[startup+870.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5018 0 0 0 86921 53 0 0 25 0 1 0 1843334160 21700608 5004 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5298 5004 145 145 0 5153 0
[pid=25861] vsize: 21192
Current children cumulated CPU time (s) 869.74
Current children cumulated vsize (Kb) 23316

[startup+880.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5019 0 0 0 87921 53 0 0 25 0 1 0 1843334160 21700608 5005 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5298 5005 145 145 0 5153 0
[pid=25861] vsize: 21192
Current children cumulated CPU time (s) 879.74
Current children cumulated vsize (Kb) 23316

[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5037 0 0 0 88921 53 0 0 25 0 1 0 1843334160 21831680 5023 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5023 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 889.74
Current children cumulated vsize (Kb) 23444

[startup+900.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 89921 53 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 899.74
Current children cumulated vsize (Kb) 23444

[startup+910.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 90921 53 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 909.74
Current children cumulated vsize (Kb) 23444

[startup+920.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 91921 54 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 919.75
Current children cumulated vsize (Kb) 23444

[startup+930.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 92921 54 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 929.75
Current children cumulated vsize (Kb) 23444

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 93921 54 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 939.75
Current children cumulated vsize (Kb) 23444

[startup+950.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 94920 55 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 949.75
Current children cumulated vsize (Kb) 23444

[startup+960.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 95920 56 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 959.76
Current children cumulated vsize (Kb) 23444

[startup+970.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 96920 56 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 969.76
Current children cumulated vsize (Kb) 23444

[startup+980.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 97920 56 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 979.76
Current children cumulated vsize (Kb) 23444

[startup+990.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 98919 57 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 989.76
Current children cumulated vsize (Kb) 23444

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 99920 57 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223040 134556894 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 999.77
Current children cumulated vsize (Kb) 23444

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 100920 57 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1009.77
Current children cumulated vsize (Kb) 23444

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 101920 57 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1019.77
Current children cumulated vsize (Kb) 23444

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 102920 57 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1029.77
Current children cumulated vsize (Kb) 23444

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 103920 57 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1039.77
Current children cumulated vsize (Kb) 23444

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 104920 57 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1049.77
Current children cumulated vsize (Kb) 23444

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 105920 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1059.78
Current children cumulated vsize (Kb) 23444

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 106921 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1069.79
Current children cumulated vsize (Kb) 23444

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 107921 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1079.79
Current children cumulated vsize (Kb) 23444

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 108921 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1089.79
Current children cumulated vsize (Kb) 23444

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 109921 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1099.79
Current children cumulated vsize (Kb) 23444

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 110921 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223088 134538541 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1109.79
Current children cumulated vsize (Kb) 23444

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 111922 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1119.8
Current children cumulated vsize (Kb) 23444

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 112922 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1129.8
Current children cumulated vsize (Kb) 23444

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 113922 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1139.8
Current children cumulated vsize (Kb) 23444

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 114922 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1149.8
Current children cumulated vsize (Kb) 23444

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 115922 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1159.8
Current children cumulated vsize (Kb) 23444

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 116923 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1169.81
Current children cumulated vsize (Kb) 23444

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 117923 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1179.81
Current children cumulated vsize (Kb) 23444

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 118923 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1189.81
Current children cumulated vsize (Kb) 23444

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5038 0 0 0 119923 58 0 0 25 0 1 0 1843334160 21831680 5024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5024 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1199.81
Current children cumulated vsize (Kb) 23444

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5039 0 0 0 120923 59 0 0 25 0 1 0 1843334160 21831680 5025 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5025 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1209.82
Current children cumulated vsize (Kb) 23444



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 25861
Raw data (/proc/25857/stat): 25857 (minisat+_script) S 25856 25857 19316 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843334155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25857/statm): 531 226 485 147 0 384 0
[pid=25857] vsize: 2124
Raw data (/proc/25861/stat): 25861 (minisat+_64-bit) R 25857 25857 19316 0 -1 0 5039 0 0 0 120924 59 0 0 25 0 1 0 1843334160 21831680 5025 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25861/statm): 5330 5025 145 145 0 5185 0
[pid=25861] vsize: 21320
Current children cumulated CPU time (s) 1209.83
Current children cumulated vsize (Kb) 23444

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.84
CPU user time (s): 1209.24
CPU system time (s): 0.600908
CPU usage (%): 99.9775
Max. virtual memory (cumulated for all children) (Kb): 23444

Verifier Data

ERROR: no interpretation found !