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-cc.opb
MD5SUM0493ba9e257fafbb54efa7af2eeb7bf2
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1567
Optimality of the best value was proved YES
Number of terms in the objective function 133
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 5699
Number of bits of the sum of numbers in the objective function 13
Biggest number in a constraint 60
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 5699
Number of bits of the biggest sum of numbers13
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark15.8786
Number of variables133
Total number of constraints229
Number of constraints which are clauses229
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 constraint1
Maximum length of a constraint31

Trace number 2202

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        923400 kB
Buffers:         34744 kB
Cached:          52832 kB
SwapCached:        960 kB
Active:          64376 kB
Inactive:        25872 kB
HighTotal:      131008 kB
HighFree:        75796 kB
LowTotal:       903652 kB
LowFree:        847604 kB
SwapTotal:     2097136 kB
SwapFree:      2095628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            15412 kB
Committed_AS:    72332 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:30:45 (client local time) WITH STATUS 10 IN 1209.78 SECONDS
stats: 2594 7 1209.78 10

Solver Data

c Parsing PB file...
c Converting 199 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 |     197      772 |      65       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 1846
c ---[   0]---> Sorter-cost:10637     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23652    55574 |    7884       0        0     nan |  0.000 % |
c |       101 |   23607    55480 |    8672     100      739     7.4 |  0.303 % |
c |       253 |   23607    55480 |    9539     252     1980     7.9 |  0.304 % |
c |       479 |   23461    55153 |   10493     470     4112     8.7 |  0.715 % |
c |       817 |   23461    55153 |   11542     808    23124    28.6 |  0.715 % |
c |      1324 |   23390    54993 |   12697    1309    32152    24.6 |  0.954 % |
c ==============================================================================
c Found solution: 1819
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1541 |   23584    55524 |    7861    1525    35890    23.5 |  0.954 % |
c |      1641 |   23584    55524 |    8647    1625    37279    22.9 |  0.975 % |
c |      1791 |   23584    55524 |    9511    1775    48320    27.2 |  0.975 % |
c ==============================================================================
c Found solution: 1816
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1928 |   23589    55542 |    7863    1912    52144    27.3 |  0.975 % |
c ==============================================================================
c Found solution: 1760
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2000 |   23541    55436 |    7847    1977    53026    26.8 |  0.975 % |
c |      2102 |   23541    55436 |    8631    2079    56552    27.2 |  1.220 % |
c |      2252 |   23541    55436 |    9494    2229    66629    29.9 |  1.220 % |
c |      2478 |   23541    55436 |   10444    2455    80579    32.8 |  1.220 % |
c |      2815 |   23541    55436 |   11488    2792    90211    32.3 |  1.220 % |
c |      3321 |   23541    55436 |   12637    3298   122096    37.0 |  1.220 % |
c |      4081 |   23541    55436 |   13901    4058   134982    33.3 |  1.220 % |
c |      5221 |   23541    55436 |   15291    5198   172493    33.2 |  1.220 % |
c |      6930 |   23541    55436 |   16820    6907   288316    41.7 |  1.220 % |
c |      9492 |   23541    55436 |   18502    9469   347250    36.7 |  1.220 % |
c |     13337 |   23541    55436 |   20353   13314   653004    49.0 |  1.220 % |
c |     19103 |   23541    55436 |   22388   19080  1024357    53.7 |  1.220 % |
c ==============================================================================
c Found solution: 1731
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19218 |   23678    55796 |    7892   19195  1027813    53.5 |  1.220 % |
c ==============================================================================
c Found solution: 1693
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19301 |   23689    55852 |    7896    4882   258270    52.9 |  1.220 % |
c |     19401 |   23689    55852 |    8685    4982   263869    53.0 |  1.251 % |
c |     19551 |   23689    55852 |    9554    5132   267144    52.1 |  1.251 % |
c |     19776 |   23689    55852 |   10509    5357   285175    53.2 |  1.251 % |
c |     20116 |   23689    55852 |   11560    5697   295627    51.9 |  1.251 % |
c |     20624 |   23689    55852 |   12716    6205   316292    51.0 |  1.251 % |
c |     21385 |   23689    55852 |   13988    6966   351890    50.5 |  1.251 % |
c |     22524 |   23689    55852 |   15387    8105   406290    50.1 |  1.251 % |
c |     24239 |   23689    55852 |   16925    9820   481842    49.1 |  1.251 % |
c |     26802 |   23689    55852 |   18618   12383   610593    49.3 |  1.251 % |
c |     30646 |   23689    55852 |   20480   16227   886767    54.6 |  1.251 % |
c |     36413 |   23665    55799 |   22528   11355   488645    43.0 |  1.335 % |
c ==============================================================================
c Found solution: 1688
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40664 |   23674    55865 |    7891   15606   741288    47.5 |  1.335 % |
c ==============================================================================
c Found solution: 1679
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40687 |   23679    55878 |    7893    7826   331922    42.4 |  1.335 % |
c |     40787 |   23679    55878 |    8682    7926   333913    42.1 |  1.355 % |
c |     40938 |   23679    55878 |    9550    8077   342378    42.4 |  1.355 % |
c |     41163 |   23679    55878 |   10505    8302   357891    43.1 |  1.355 % |
c |     41501 |   23679    55878 |   11556    8640   379272    43.9 |  1.355 % |
c |     42008 |   23679    55878 |   12711    9147   416772    45.6 |  1.355 % |
c |     42767 |   23675    55869 |   13982    9901   445961    45.0 |  1.366 % |
c |     43906 |   23675    55869 |   15381   11040   512916    46.5 |  1.366 % |
c |     45616 |   23667    55853 |   16919   12746   598834    47.0 |  1.408 % |
c |     48178 |   23667    55853 |   18611   15308   693981    45.3 |  1.408 % |
c |     52022 |   23667    55853 |   20472   19152   959983    50.1 |  1.408 % |
c |     57789 |   23667    55853 |   22519   13640   627202    46.0 |  1.408 % |
c |     66438 |   23667    55853 |   24771   22289  1218970    54.7 |  1.408 % |
c |     79412 |   23667    55853 |   27248   22217  1222636    55.0 |  1.408 % |
c ==============================================================================
c Found solution: 1633
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89499 |   23688    55912 |    7896   17467   750810    43.0 |  1.408 % |
c |     89600 |   23688    55912 |    8685    4470   131522    29.4 |  1.417 % |
c |     89750 |   23688    55912 |    9554    4620   139225    30.1 |  1.417 % |
c |     89975 |   23682    55900 |   10509    4844   153049    31.6 |  1.448 % |
c |     90312 |   23682    55900 |   11560    5181   171167    33.0 |  1.448 % |
c |     90818 |   23660    55850 |   12716    5685   187037    32.9 |  1.544 % |
c |     91579 |   23660    55850 |   13988    6446   206247    32.0 |  1.544 % |
c |     92720 |   23660    55850 |   15387    7587   293552    38.7 |  1.544 % |
c |     94430 |   23660    55850 |   16925    9297   336282    36.2 |  1.544 % |
c |     96993 |   23660    55850 |   18618   11860   427336    36.0 |  1.544 % |
c |    100837 |   23646    55818 |   20480   15691   582488    37.1 |  1.586 % |
c |    106605 |   23646    55818 |   22528   21459   805228    37.5 |  1.586 % |
c |    115255 |   23646    55818 |   24781   17976   609237    33.9 |  1.586 % |
c |    128230 |   23646    55818 |   27259   17813   628007    35.3 |  1.586 % |
c |    147691 |   23646    55818 |   29985   23003   702842    30.6 |  1.586 % |
c |    176885 |   23646    55818 |   32983   18811   650416    34.6 |  1.586 % |
c |    220674 |   23646    55818 |   36281   22829  1310770    57.4 |  1.586 % |
c |    286359 |   23646    55818 |   39910   19503   943184    48.4 |  1.586 % |
c |    384885 |   23646    55818 |   43901   34851  1504695    43.2 |  1.586 % |

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/15197/stat): 15197 (minisat+_script) R 15196 15197 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785067555 712704 3 4294967295 134512640 135087896 3221224528 3221224528 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/15197/statm): 174 3 169 147 0 27 0
[pid=15197] 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=15198
New process pid=15199
New process pid=15200
execve syscall for /bin/sed executable
One traced child (pid=15199) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=15200) exited with status: 0
One traced child (pid=15198) exited with status: 0
New process pid=15201
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-cc.opb

[startup+10.005 s]
Raw data (loadavg): 0.97 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 1302 0 0 0 981 7 0 0 25 0 1 0 1785067560 5853184 1236 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 1429 1236 145 145 0 1284 0
[pid=15201] vsize: 5716
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 7840

[startup+20.0058 s]
Raw data (loadavg): 0.98 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 1624 0 0 0 1976 10 0 0 25 0 1 0 1785067560 7180288 1558 4294967295 134512640 135094434 3221224448 3221223040 134557377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 1753 1558 145 145 0 1608 0
[pid=15201] vsize: 7012
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 9136

[startup+30.0077 s]
Raw data (loadavg): 0.98 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2035 0 0 0 2968 13 0 0 25 0 1 0 1785067560 8916992 1969 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2177 1969 145 145 0 2032 0
[pid=15201] vsize: 8708
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 10832

[startup+40.0086 s]
Raw data (loadavg): 0.98 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2205 0 0 0 3965 14 0 0 25 0 1 0 1785067560 9601024 2139 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2344 2139 145 145 0 2199 0
[pid=15201] vsize: 9376
Current children cumulated CPU time (s) 39.79
Current children cumulated vsize (Kb) 11500

[startup+50.0094 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2205 0 0 0 4964 14 0 0 25 0 1 0 1785067560 9601024 2139 4294967295 134512640 135094434 3221224448 3221223072 134557724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2344 2139 145 145 0 2199 0
[pid=15201] vsize: 9376
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 11500

[startup+60.0113 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2205 0 0 0 5964 15 0 0 25 0 1 0 1785067560 9601024 2139 4294967295 134512640 135094434 3221224448 3221223040 134556793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2344 2139 145 145 0 2199 0
[pid=15201] vsize: 9376
Current children cumulated CPU time (s) 59.79
Current children cumulated vsize (Kb) 11500

[startup+70.0121 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2293 0 0 0 6962 16 0 0 25 0 1 0 1785067560 9953280 2227 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2430 2227 145 145 0 2285 0
[pid=15201] vsize: 9720
Current children cumulated CPU time (s) 69.78
Current children cumulated vsize (Kb) 11844

[startup+80.014 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2308 0 0 0 7961 17 0 0 25 0 1 0 1785067560 10014720 2242 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2445 2242 145 145 0 2300 0
[pid=15201] vsize: 9780
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 11904

[startup+90.0148 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2308 0 0 0 8961 17 0 0 25 0 1 0 1785067560 10014720 2242 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2445 2242 145 145 0 2300 0
[pid=15201] vsize: 9780
Current children cumulated CPU time (s) 89.78
Current children cumulated vsize (Kb) 11904

[startup+100.016 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2308 0 0 0 9960 18 0 0 25 0 1 0 1785067560 10014720 2242 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2445 2242 145 145 0 2300 0
[pid=15201] vsize: 9780
Current children cumulated CPU time (s) 99.78
Current children cumulated vsize (Kb) 11904

[startup+110.018 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2416 0 0 0 10957 19 0 0 25 0 1 0 1785067560 10452992 2350 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2552 2350 145 145 0 2407 0
[pid=15201] vsize: 10208
Current children cumulated CPU time (s) 109.76
Current children cumulated vsize (Kb) 12332

[startup+120.019 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2416 0 0 0 11957 20 0 0 25 0 1 0 1785067560 10452992 2350 4294967295 134512640 135094434 3221224448 3221223040 134557044 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2552 2350 145 145 0 2407 0
[pid=15201] vsize: 10208
Current children cumulated CPU time (s) 119.77
Current children cumulated vsize (Kb) 12332

[startup+130.02 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2630 0 0 0 12952 22 0 0 25 0 1 0 1785067560 11325440 2564 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 2765 2564 145 145 0 2620 0
[pid=15201] vsize: 11060
Current children cumulated CPU time (s) 129.74
Current children cumulated vsize (Kb) 13184

[startup+140.021 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2867 0 0 0 13947 25 0 0 25 0 1 0 1785067560 12288000 2801 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3000 2801 145 145 0 2855 0
[pid=15201] vsize: 12000
Current children cumulated CPU time (s) 139.72
Current children cumulated vsize (Kb) 14124

[startup+150.022 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2867 0 0 0 14947 25 0 0 25 0 1 0 1785067560 12288000 2801 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3000 2801 145 145 0 2855 0
[pid=15201] vsize: 12000
Current children cumulated CPU time (s) 149.72
Current children cumulated vsize (Kb) 14124

[startup+160.023 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2867 0 0 0 15946 26 0 0 25 0 1 0 1785067560 12288000 2801 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3000 2801 145 145 0 2855 0
[pid=15201] vsize: 12000
Current children cumulated CPU time (s) 159.72
Current children cumulated vsize (Kb) 14124

[startup+170.024 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2872 0 0 0 16946 27 0 0 25 0 1 0 1785067560 12304384 2806 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3004 2806 145 145 0 2859 0
[pid=15201] vsize: 12016
Current children cumulated CPU time (s) 169.73
Current children cumulated vsize (Kb) 14140

[startup+180.025 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2927 0 0 0 17944 27 0 0 25 0 1 0 1785067560 12529664 2861 4294967295 134512640 135094434 3221224448 3221223072 134562152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3059 2861 145 145 0 2914 0
[pid=15201] vsize: 12236
Current children cumulated CPU time (s) 179.71
Current children cumulated vsize (Kb) 14360

[startup+190.026 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 18944 28 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 189.72
Current children cumulated vsize (Kb) 14400

[startup+200.027 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 19944 28 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 199.72
Current children cumulated vsize (Kb) 14400

[startup+210.029 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 20944 28 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 209.72
Current children cumulated vsize (Kb) 14400

[startup+220.03 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 21943 29 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 219.72
Current children cumulated vsize (Kb) 14400

[startup+230.032 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 22943 29 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 229.72
Current children cumulated vsize (Kb) 14400

[startup+240.033 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 23943 30 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 239.73
Current children cumulated vsize (Kb) 14400

[startup+250.033 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 24943 30 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 249.73
Current children cumulated vsize (Kb) 14400

[startup+260.035 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 25942 30 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 259.72
Current children cumulated vsize (Kb) 14400

[startup+270.036 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 26942 30 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 269.72
Current children cumulated vsize (Kb) 14400

[startup+280.037 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 27942 31 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 279.73
Current children cumulated vsize (Kb) 14400

[startup+290.039 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2937 0 0 0 28942 31 0 0 25 0 1 0 1785067560 12570624 2871 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2871 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 289.73
Current children cumulated vsize (Kb) 14400

[startup+300.04 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2938 0 0 0 29942 31 0 0 25 0 1 0 1785067560 12570624 2872 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2872 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 299.73
Current children cumulated vsize (Kb) 14400

[startup+310.041 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2938 0 0 0 30942 32 0 0 25 0 1 0 1785067560 12570624 2872 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2872 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 309.74
Current children cumulated vsize (Kb) 14400

[startup+320.041 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2938 0 0 0 31941 32 0 0 25 0 1 0 1785067560 12570624 2872 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2872 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 319.73
Current children cumulated vsize (Kb) 14400

[startup+330.043 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2938 0 0 0 32941 33 0 0 25 0 1 0 1785067560 12570624 2872 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2872 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 329.74
Current children cumulated vsize (Kb) 14400

[startup+340.044 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2939 0 0 0 33941 33 0 0 25 0 1 0 1785067560 12570624 2873 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2873 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 339.74
Current children cumulated vsize (Kb) 14400

[startup+350.045 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2941 0 0 0 34941 33 0 0 25 0 1 0 1785067560 12570624 2875 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2875 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 349.74
Current children cumulated vsize (Kb) 14400

[startup+360.047 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2941 0 0 0 35940 34 0 0 25 0 1 0 1785067560 12570624 2875 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2875 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 359.74
Current children cumulated vsize (Kb) 14400

[startup+370.048 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2941 0 0 0 36940 34 0 0 25 0 1 0 1785067560 12570624 2875 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2875 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 369.74
Current children cumulated vsize (Kb) 14400

[startup+380.05 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2941 0 0 0 37940 34 0 0 25 0 1 0 1785067560 12570624 2875 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3069 2875 145 145 0 2924 0
[pid=15201] vsize: 12276
Current children cumulated CPU time (s) 379.74
Current children cumulated vsize (Kb) 14400

[startup+390.05 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2943 0 0 0 38940 35 0 0 25 0 1 0 1785067560 12623872 2877 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3082 2877 145 145 0 2937 0
[pid=15201] vsize: 12328
Current children cumulated CPU time (s) 389.75
Current children cumulated vsize (Kb) 14452

[startup+400.051 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2943 0 0 0 39940 35 0 0 25 0 1 0 1785067560 12623872 2877 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3082 2877 145 145 0 2937 0
[pid=15201] vsize: 12328
Current children cumulated CPU time (s) 399.75
Current children cumulated vsize (Kb) 14452

[startup+410.053 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2947 0 0 0 40939 36 0 0 25 0 1 0 1785067560 12623872 2881 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3082 2881 145 145 0 2937 0
[pid=15201] vsize: 12328
Current children cumulated CPU time (s) 409.75
Current children cumulated vsize (Kb) 14452

[startup+420.054 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 2952 0 0 0 41939 36 0 0 25 0 1 0 1785067560 12640256 2886 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3086 2886 145 145 0 2941 0
[pid=15201] vsize: 12344
Current children cumulated CPU time (s) 419.75
Current children cumulated vsize (Kb) 14468

[startup+430.056 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 3133 0 0 0 42934 38 0 0 25 0 1 0 1785067560 13381632 3067 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3267 3067 145 145 0 3122 0
[pid=15201] vsize: 13068
Current children cumulated CPU time (s) 429.72
Current children cumulated vsize (Kb) 15192

[startup+440.058 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 3407 0 0 0 43930 41 0 0 25 0 1 0 1785067560 14630912 3341 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3572 3341 145 145 0 3427 0
[pid=15201] vsize: 14288
Current children cumulated CPU time (s) 439.71
Current children cumulated vsize (Kb) 16412

[startup+450.059 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 3443 0 0 0 44929 41 0 0 25 0 1 0 1785067560 14774272 3377 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3607 3377 145 145 0 3462 0
[pid=15201] vsize: 14428
Current children cumulated CPU time (s) 449.7
Current children cumulated vsize (Kb) 16552

[startup+460.059 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 3467 0 0 0 45929 42 0 0 25 0 1 0 1785067560 14880768 3401 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3633 3401 145 145 0 3488 0
[pid=15201] vsize: 14532
Current children cumulated CPU time (s) 459.71
Current children cumulated vsize (Kb) 16656

[startup+470.061 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 3468 0 0 0 46929 42 0 0 25 0 1 0 1785067560 14880768 3402 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3633 3402 145 145 0 3488 0
[pid=15201] vsize: 14532
Current children cumulated CPU time (s) 469.71
Current children cumulated vsize (Kb) 16656

[startup+480.063 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 3548 0 0 0 47928 42 0 0 25 0 1 0 1785067560 15208448 3482 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3713 3482 145 145 0 3568 0
[pid=15201] vsize: 14852
Current children cumulated CPU time (s) 479.7
Current children cumulated vsize (Kb) 16976

[startup+490.064 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 3807 0 0 0 48924 44 0 0 25 0 1 0 1785067560 16265216 3741 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 3971 3741 145 145 0 3826 0
[pid=15201] vsize: 15884
Current children cumulated CPU time (s) 489.68
Current children cumulated vsize (Kb) 18008

[startup+500.065 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4000 0 0 0 49921 46 0 0 25 0 1 0 1785067560 17100800 3934 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4175 3934 145 145 0 4030 0
[pid=15201] vsize: 16700
Current children cumulated CPU time (s) 499.67
Current children cumulated vsize (Kb) 18824

[startup+510.067 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4164 0 0 0 50918 47 0 0 25 0 1 0 1785067560 17797120 4098 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4345 4098 145 145 0 4200 0
[pid=15201] vsize: 17380
Current children cumulated CPU time (s) 509.65
Current children cumulated vsize (Kb) 19504

[startup+520.067 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4167 0 0 0 51917 48 0 0 25 0 1 0 1785067560 17813504 4101 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4349 4101 145 145 0 4204 0
[pid=15201] vsize: 17396
Current children cumulated CPU time (s) 519.65
Current children cumulated vsize (Kb) 19520

[startup+530.069 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4173 0 0 0 52917 48 0 0 25 0 1 0 1785067560 17846272 4107 4294967295 134512640 135094434 3221224448 3221223040 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4357 4107 145 145 0 4212 0
[pid=15201] vsize: 17428
Current children cumulated CPU time (s) 529.65
Current children cumulated vsize (Kb) 19552

[startup+540.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4178 0 0 0 53916 49 0 0 25 0 1 0 1785067560 17879040 4112 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4365 4112 145 145 0 4220 0
[pid=15201] vsize: 17460
Current children cumulated CPU time (s) 539.65
Current children cumulated vsize (Kb) 19584

[startup+550.071 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4178 0 0 0 54916 50 0 0 25 0 1 0 1785067560 17879040 4112 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4365 4112 145 145 0 4220 0
[pid=15201] vsize: 17460
Current children cumulated CPU time (s) 549.66
Current children cumulated vsize (Kb) 19584

[startup+560.073 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4178 0 0 0 55915 50 0 0 25 0 1 0 1785067560 17879040 4112 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4365 4112 145 145 0 4220 0
[pid=15201] vsize: 17460
Current children cumulated CPU time (s) 559.65
Current children cumulated vsize (Kb) 19584

[startup+570.075 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4204 0 0 0 56914 51 0 0 25 0 1 0 1785067560 17973248 4138 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4388 4138 145 145 0 4243 0
[pid=15201] vsize: 17552
Current children cumulated CPU time (s) 569.65
Current children cumulated vsize (Kb) 19676

[startup+580.076 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4210 0 0 0 57914 51 0 0 25 0 1 0 1785067560 17997824 4144 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4394 4144 145 145 0 4249 0
[pid=15201] vsize: 17576
Current children cumulated CPU time (s) 579.65
Current children cumulated vsize (Kb) 19700

[startup+590.076 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4210 0 0 0 58914 52 0 0 25 0 1 0 1785067560 17997824 4144 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4394 4144 145 145 0 4249 0
[pid=15201] vsize: 17576
Current children cumulated CPU time (s) 589.66
Current children cumulated vsize (Kb) 19700

[startup+600.077 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4210 0 0 0 59913 52 0 0 25 0 1 0 1785067560 17997824 4144 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4394 4144 145 145 0 4249 0
[pid=15201] vsize: 17576
Current children cumulated CPU time (s) 599.65
Current children cumulated vsize (Kb) 19700

[startup+610.079 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4222 0 0 0 60913 52 0 0 25 0 1 0 1785067560 18063360 4156 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4410 4156 145 145 0 4265 0
[pid=15201] vsize: 17640
Current children cumulated CPU time (s) 609.65
Current children cumulated vsize (Kb) 19764

[startup+620.08 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4230 0 0 0 61913 52 0 0 25 0 1 0 1785067560 18096128 4164 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4418 4164 145 145 0 4273 0
[pid=15201] vsize: 17672
Current children cumulated CPU time (s) 619.65
Current children cumulated vsize (Kb) 19796

[startup+630.082 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4246 0 0 0 62914 52 0 0 25 0 1 0 1785067560 18161664 4180 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4434 4180 145 145 0 4289 0
[pid=15201] vsize: 17736
Current children cumulated CPU time (s) 629.66
Current children cumulated vsize (Kb) 19860

[startup+640.083 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4247 0 0 0 63914 52 0 0 25 0 1 0 1785067560 18161664 4181 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4434 4181 145 145 0 4289 0
[pid=15201] vsize: 17736
Current children cumulated CPU time (s) 639.66
Current children cumulated vsize (Kb) 19860

[startup+650.084 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4248 0 0 0 64914 52 0 0 25 0 1 0 1785067560 18161664 4182 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4434 4182 145 145 0 4289 0
[pid=15201] vsize: 17736
Current children cumulated CPU time (s) 649.66
Current children cumulated vsize (Kb) 19860

[startup+660.084 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4248 0 0 0 65914 52 0 0 25 0 1 0 1785067560 18161664 4182 4294967295 134512640 135094434 3221224448 3221223120 134556401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4434 4182 145 145 0 4289 0
[pid=15201] vsize: 17736
Current children cumulated CPU time (s) 659.66
Current children cumulated vsize (Kb) 19860

[startup+670.085 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4248 0 0 0 66915 52 0 0 25 0 1 0 1785067560 18161664 4182 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4434 4182 145 145 0 4289 0
[pid=15201] vsize: 17736
Current children cumulated CPU time (s) 669.67
Current children cumulated vsize (Kb) 19860

[startup+680.086 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4252 0 0 0 67915 52 0 0 25 0 1 0 1785067560 18178048 4186 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4438 4186 145 145 0 4293 0
[pid=15201] vsize: 17752
Current children cumulated CPU time (s) 679.67
Current children cumulated vsize (Kb) 19876

[startup+690.087 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4257 0 0 0 68915 52 0 0 25 0 1 0 1785067560 18210816 4191 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4446 4191 145 145 0 4301 0
[pid=15201] vsize: 17784
Current children cumulated CPU time (s) 689.67
Current children cumulated vsize (Kb) 19908

[startup+700.087 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4260 0 0 0 69915 52 0 0 25 0 1 0 1785067560 18227200 4194 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4450 4194 145 145 0 4305 0
[pid=15201] vsize: 17800
Current children cumulated CPU time (s) 699.67
Current children cumulated vsize (Kb) 19924

[startup+710.088 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4261 0 0 0 70915 52 0 0 25 0 1 0 1785067560 18227200 4195 4294967295 134512640 135094434 3221224448 3221223040 134556993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4450 4195 145 145 0 4305 0
[pid=15201] vsize: 17800
Current children cumulated CPU time (s) 709.67
Current children cumulated vsize (Kb) 19924

[startup+720.088 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4277 0 0 0 71916 52 0 0 25 0 1 0 1785067560 18325504 4211 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4474 4211 145 145 0 4329 0
[pid=15201] vsize: 17896
Current children cumulated CPU time (s) 719.68
Current children cumulated vsize (Kb) 20020

[startup+730.089 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4278 0 0 0 72915 52 0 0 25 0 1 0 1785067560 18325504 4212 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4474 4212 145 145 0 4329 0
[pid=15201] vsize: 17896
Current children cumulated CPU time (s) 729.67
Current children cumulated vsize (Kb) 20020

[startup+740.09 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4278 0 0 0 73915 52 0 0 25 0 1 0 1785067560 18325504 4212 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4474 4212 145 145 0 4329 0
[pid=15201] vsize: 17896
Current children cumulated CPU time (s) 739.67
Current children cumulated vsize (Kb) 20020

[startup+750.091 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4292 0 0 0 74915 52 0 0 25 0 1 0 1785067560 18423808 4226 4294967295 134512640 135094434 3221224448 3221223040 134556914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4498 4226 145 145 0 4353 0
[pid=15201] vsize: 17992
Current children cumulated CPU time (s) 749.67
Current children cumulated vsize (Kb) 20116

[startup+760.092 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4293 0 0 0 75916 52 0 0 25 0 1 0 1785067560 18423808 4227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4498 4227 145 145 0 4353 0
[pid=15201] vsize: 17992
Current children cumulated CPU time (s) 759.68
Current children cumulated vsize (Kb) 20116

[startup+770.093 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4293 0 0 0 76916 52 0 0 25 0 1 0 1785067560 18423808 4227 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4498 4227 145 145 0 4353 0
[pid=15201] vsize: 17992
Current children cumulated CPU time (s) 769.68
Current children cumulated vsize (Kb) 20116

[startup+780.094 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4295 0 0 0 77916 52 0 0 25 0 1 0 1785067560 18423808 4229 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4498 4229 145 145 0 4353 0
[pid=15201] vsize: 17992
Current children cumulated CPU time (s) 779.68
Current children cumulated vsize (Kb) 20116

[startup+790.095 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4308 0 0 0 78916 52 0 0 25 0 1 0 1785067560 18489344 4242 4294967295 134512640 135094434 3221224448 3221223040 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4514 4242 145 145 0 4369 0
[pid=15201] vsize: 18056
Current children cumulated CPU time (s) 789.68
Current children cumulated vsize (Kb) 20180

[startup+800.094 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4319 0 0 0 79916 53 0 0 25 0 1 0 1785067560 18522112 4253 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4522 4253 145 145 0 4377 0
[pid=15201] vsize: 18088
Current children cumulated CPU time (s) 799.69
Current children cumulated vsize (Kb) 20212

[startup+810.096 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4337 0 0 0 80916 53 0 0 25 0 1 0 1785067560 18583552 4271 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4537 4271 145 145 0 4392 0
[pid=15201] vsize: 18148
Current children cumulated CPU time (s) 809.69
Current children cumulated vsize (Kb) 20272

[startup+820.097 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4337 0 0 0 81917 53 0 0 25 0 1 0 1785067560 18583552 4271 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4537 4271 145 145 0 4392 0
[pid=15201] vsize: 18148
Current children cumulated CPU time (s) 819.7
Current children cumulated vsize (Kb) 20272

[startup+830.098 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4342 0 0 0 82917 53 0 0 25 0 1 0 1785067560 18616320 4276 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4545 4276 145 145 0 4400 0
[pid=15201] vsize: 18180
Current children cumulated CPU time (s) 829.7
Current children cumulated vsize (Kb) 20304

[startup+840.099 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4342 0 0 0 83917 53 0 0 25 0 1 0 1785067560 18616320 4276 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4545 4276 145 145 0 4400 0
[pid=15201] vsize: 18180
Current children cumulated CPU time (s) 839.7
Current children cumulated vsize (Kb) 20304

[startup+850.1 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4346 0 0 0 84917 53 0 0 25 0 1 0 1785067560 18632704 4280 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4549 4280 145 145 0 4404 0
[pid=15201] vsize: 18196
Current children cumulated CPU time (s) 849.7
Current children cumulated vsize (Kb) 20320

[startup+860.101 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4353 0 0 0 85917 53 0 0 25 0 1 0 1785067560 18665472 4287 4294967295 134512640 135094434 3221224448 3221223104 134558238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4557 4287 145 145 0 4412 0
[pid=15201] vsize: 18228
Current children cumulated CPU time (s) 859.7
Current children cumulated vsize (Kb) 20352

[startup+870.101 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4356 0 0 0 86917 53 0 0 25 0 1 0 1785067560 18698240 4290 4294967295 134512640 135094434 3221224448 3221223120 134556552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4565 4290 145 145 0 4420 0
[pid=15201] vsize: 18260
Current children cumulated CPU time (s) 869.7
Current children cumulated vsize (Kb) 20384

[startup+880.103 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4360 0 0 0 87918 53 0 0 25 0 1 0 1785067560 18698240 4294 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4565 4294 145 145 0 4420 0
[pid=15201] vsize: 18260
Current children cumulated CPU time (s) 879.71
Current children cumulated vsize (Kb) 20384

[startup+890.104 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4373 0 0 0 88918 53 0 0 25 0 1 0 1785067560 18780160 4307 4294967295 134512640 135094434 3221224448 3221223104 134558172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4585 4307 145 145 0 4440 0
[pid=15201] vsize: 18340
Current children cumulated CPU time (s) 889.71
Current children cumulated vsize (Kb) 20464

[startup+900.105 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4391 0 0 0 89918 53 0 0 25 0 1 0 1785067560 18878464 4325 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4609 4325 145 145 0 4464 0
[pid=15201] vsize: 18436
Current children cumulated CPU time (s) 899.71
Current children cumulated vsize (Kb) 20560

[startup+910.107 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4391 0 0 0 90918 53 0 0 25 0 1 0 1785067560 18878464 4325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4609 4325 145 145 0 4464 0
[pid=15201] vsize: 18436
Current children cumulated CPU time (s) 909.71
Current children cumulated vsize (Kb) 20560

[startup+920.108 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4391 0 0 0 91918 53 0 0 25 0 1 0 1785067560 18878464 4325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4609 4325 145 145 0 4464 0
[pid=15201] vsize: 18436
Current children cumulated CPU time (s) 919.71
Current children cumulated vsize (Kb) 20560

[startup+930.109 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4398 0 0 0 92917 54 0 0 25 0 1 0 1785067560 18911232 4332 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4617 4332 145 145 0 4472 0
[pid=15201] vsize: 18468
Current children cumulated CPU time (s) 929.71
Current children cumulated vsize (Kb) 20592

[startup+940.11 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4411 0 0 0 93917 54 0 0 25 0 1 0 1785067560 18993152 4345 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4637 4345 145 145 0 4492 0
[pid=15201] vsize: 18548
Current children cumulated CPU time (s) 939.71
Current children cumulated vsize (Kb) 20672

[startup+950.111 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4411 0 0 0 94917 54 0 0 25 0 1 0 1785067560 18993152 4345 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4637 4345 145 145 0 4492 0
[pid=15201] vsize: 18548
Current children cumulated CPU time (s) 949.71
Current children cumulated vsize (Kb) 20672

[startup+960.112 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4411 0 0 0 95918 54 0 0 25 0 1 0 1785067560 18993152 4345 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4637 4345 145 145 0 4492 0
[pid=15201] vsize: 18548
Current children cumulated CPU time (s) 959.72
Current children cumulated vsize (Kb) 20672

[startup+970.113 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4411 0 0 0 96918 54 0 0 25 0 1 0 1785067560 18993152 4345 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4637 4345 145 145 0 4492 0
[pid=15201] vsize: 18548
Current children cumulated CPU time (s) 969.72
Current children cumulated vsize (Kb) 20672

[startup+980.115 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4411 0 0 0 97918 54 0 0 25 0 1 0 1785067560 18993152 4345 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15201/statm): 4637 4345 145 145 0 4492 0
[pid=15201] vsize: 18548
Current children cumulated CPU time (s) 979.72
Current children cumulated vsize (Kb) 20672

[startup+990.116 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4417 0 0 0 98917 54 0 0 25 0 1 0 1785067560 19025920 4351 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4645 4351 145 145 0 4500 0
[pid=15201] vsize: 18580
Current children cumulated CPU time (s) 989.71
Current children cumulated vsize (Kb) 20704

[startup+1000.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4417 0 0 0 99917 54 0 0 25 0 1 0 1785067560 19025920 4351 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4645 4351 145 145 0 4500 0
[pid=15201] vsize: 18580
Current children cumulated CPU time (s) 999.71
Current children cumulated vsize (Kb) 20704

[startup+1010.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4417 0 0 0 100918 54 0 0 25 0 1 0 1785067560 19025920 4351 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4645 4351 145 145 0 4500 0
[pid=15201] vsize: 18580
Current children cumulated CPU time (s) 1009.72
Current children cumulated vsize (Kb) 20704

[startup+1020.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4417 0 0 0 101917 54 0 0 25 0 1 0 1785067560 19025920 4351 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4645 4351 145 145 0 4500 0
[pid=15201] vsize: 18580
Current children cumulated CPU time (s) 1019.71
Current children cumulated vsize (Kb) 20704

[startup+1030.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4423 0 0 0 102918 54 0 0 25 0 1 0 1785067560 19058688 4357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4653 4357 145 145 0 4508 0
[pid=15201] vsize: 18612
Current children cumulated CPU time (s) 1029.72
Current children cumulated vsize (Kb) 20736

[startup+1040.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4426 0 0 0 103918 54 0 0 25 0 1 0 1785067560 19058688 4360 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4653 4360 145 145 0 4508 0
[pid=15201] vsize: 18612
Current children cumulated CPU time (s) 1039.72
Current children cumulated vsize (Kb) 20736

[startup+1050.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4426 0 0 0 104918 54 0 0 25 0 1 0 1785067560 19058688 4360 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4653 4360 145 145 0 4508 0
[pid=15201] vsize: 18612
Current children cumulated CPU time (s) 1049.72
Current children cumulated vsize (Kb) 20736

[startup+1060.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4426 0 0 0 105918 54 0 0 25 0 1 0 1785067560 19058688 4360 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4653 4360 145 145 0 4508 0
[pid=15201] vsize: 18612
Current children cumulated CPU time (s) 1059.72
Current children cumulated vsize (Kb) 20736

[startup+1070.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4431 0 0 0 106919 54 0 0 25 0 1 0 1785067560 19091456 4365 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4661 4365 145 145 0 4516 0
[pid=15201] vsize: 18644
Current children cumulated CPU time (s) 1069.73
Current children cumulated vsize (Kb) 20768

[startup+1080.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4438 0 0 0 107919 55 0 0 25 0 1 0 1785067560 19124224 4372 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4669 4372 145 145 0 4524 0
[pid=15201] vsize: 18676
Current children cumulated CPU time (s) 1079.74
Current children cumulated vsize (Kb) 20800

[startup+1090.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4443 0 0 0 108919 55 0 0 25 0 1 0 1785067560 19156992 4377 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4677 4377 145 145 0 4532 0
[pid=15201] vsize: 18708
Current children cumulated CPU time (s) 1089.74
Current children cumulated vsize (Kb) 20832

[startup+1100.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4444 0 0 0 109919 55 0 0 25 0 1 0 1785067560 19156992 4378 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4677 4378 145 145 0 4532 0
[pid=15201] vsize: 18708
Current children cumulated CPU time (s) 1099.74
Current children cumulated vsize (Kb) 20832

[startup+1110.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4444 0 0 0 110919 55 0 0 25 0 1 0 1785067560 19156992 4378 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4677 4378 145 145 0 4532 0
[pid=15201] vsize: 18708
Current children cumulated CPU time (s) 1109.74
Current children cumulated vsize (Kb) 20832

[startup+1120.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4466 0 0 0 111919 55 0 0 25 0 1 0 1785067560 19320832 4400 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4717 4400 145 145 0 4572 0
[pid=15201] vsize: 18868
Current children cumulated CPU time (s) 1119.74
Current children cumulated vsize (Kb) 20992

[startup+1130.12 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4469 0 0 0 112920 55 0 0 25 0 1 0 1785067560 19320832 4403 4294967295 134512640 135094434 3221224448 3221223040 134557375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4717 4403 145 145 0 4572 0
[pid=15201] vsize: 18868
Current children cumulated CPU time (s) 1129.75
Current children cumulated vsize (Kb) 20992

[startup+1140.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4480 0 0 0 113920 55 0 0 25 0 1 0 1785067560 19353600 4414 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4725 4414 145 145 0 4580 0
[pid=15201] vsize: 18900
Current children cumulated CPU time (s) 1139.75
Current children cumulated vsize (Kb) 21024

[startup+1150.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4481 0 0 0 114920 55 0 0 25 0 1 0 1785067560 19353600 4415 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4725 4415 145 145 0 4580 0
[pid=15201] vsize: 18900
Current children cumulated CPU time (s) 1149.75
Current children cumulated vsize (Kb) 21024

[startup+1160.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4481 0 0 0 115920 55 0 0 25 0 1 0 1785067560 19353600 4415 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4725 4415 145 145 0 4580 0
[pid=15201] vsize: 18900
Current children cumulated CPU time (s) 1159.75
Current children cumulated vsize (Kb) 21024

[startup+1170.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4495 0 0 0 116920 55 0 0 25 0 1 0 1785067560 19419136 4429 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4741 4429 145 145 0 4596 0
[pid=15201] vsize: 18964
Current children cumulated CPU time (s) 1169.75
Current children cumulated vsize (Kb) 21088

[startup+1180.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4496 0 0 0 117921 55 0 0 25 0 1 0 1785067560 19419136 4430 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4741 4430 145 145 0 4596 0
[pid=15201] vsize: 18964
Current children cumulated CPU time (s) 1179.76
Current children cumulated vsize (Kb) 21088

[startup+1190.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4497 0 0 0 118921 55 0 0 25 0 1 0 1785067560 19419136 4431 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4741 4431 145 145 0 4596 0
[pid=15201] vsize: 18964
Current children cumulated CPU time (s) 1189.76
Current children cumulated vsize (Kb) 21088

[startup+1200.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4498 0 0 0 119921 55 0 0 25 0 1 0 1785067560 19419136 4432 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4741 4432 145 145 0 4596 0
[pid=15201] vsize: 18964
Current children cumulated CPU time (s) 1199.76
Current children cumulated vsize (Kb) 21088

[startup+1210.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4503 0 0 0 120921 55 0 0 25 0 1 0 1785067560 19451904 4437 4294967295 134512640 135094434 3221224448 3221223040 134557319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4749 4437 145 145 0 4604 0
[pid=15201] vsize: 18996
Current children cumulated CPU time (s) 1209.76
Current children cumulated vsize (Kb) 21120



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 15201
Raw data (/proc/15197/stat): 15197 (minisat+_script) S 15196 15197 6847 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785067555 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15197/statm): 531 226 485 147 0 384 0
[pid=15197] vsize: 2124
Raw data (/proc/15201/stat): 15201 (minisat+_64-bit) R 15197 15197 6847 0 -1 0 4503 0 0 0 120921 55 0 0 25 0 1 0 1785067560 19451904 4437 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15201/statm): 4749 4437 145 145 0 4604 0
[pid=15201] vsize: 18996
Current children cumulated CPU time (s) 1209.76
Current children cumulated vsize (Kb) 21120

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1209.78
CPU user time (s): 1209.22
CPU system time (s): 0.562914
CPU usage (%): 99.9701
Max. virtual memory (cumulated for all children) (Kb): 21120

Verifier Data

ERROR: no interpretation found !