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

Namemps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare2_1.opb
MD5SUM375b355299c9fbf8170e172bcbc73eb2
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 9786
Optimality of the best value was proved NO
Number of terms in the objective function 140
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 7340025
Number of bits of the sum of numbers in the objective function 23
Biggest number in a constraint 524288
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 7340025
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.36
Number of variables242
Total number of constraints67
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)54
Number of constraints which are nor clauses,nor cardinality constraints13
Minimum length of a constraint1
Maximum length of a constraint122

Trace number 6288

Launcher Data

LAUNCH ON wulflinc1 THE 2005-09-20 05:11:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3444 boxname=wulflinc1 idbench=1100 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  375b355299c9fbf8170e172bcbc73eb2  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-markshare2_1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-markshare2_1.opb
IDLAUNCH: 3444
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        867244 kB
Buffers:         14296 kB
Cached:         123808 kB
SwapCached:       1160 kB
Active:          40288 kB
Inactive:       100448 kB
HighTotal:      131008 kB
HighFree:        23884 kB
LowTotal:       903652 kB
LowFree:        843360 kB
SwapTotal:     2097136 kB
SwapFree:      2095268 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            20760 kB
Committed_AS:    92624 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:31:54 (client local time) WITH STATUS 10 IN 1209.4 SECONDS
stats: 3444 7 1209.4 10

Solver Data

c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  12]---> Adder-cost: 590   maxlim: 469334   bits: 20/19
c ---[  10]---> Adder-cost: 648   maxlim: 507792   bits: 20/19
c ---[   8]---> Adder-cost: 604   maxlim: 482140   bits: 20/19
c ---[   6]---> Adder-cost: 572   maxlim: 518845   bits: 20/19
c ---[   4]---> Adder-cost: 688   maxlim: 476350   bits: 20/19
c ---[   2]---> Adder-cost: 646   maxlim: 516106   bits: 20/19
c ---[   0]---> Adder-cost: 598   maxlim: 472356   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29589   105189 |    9863       0        0     nan |  0.000 % |
c |       100 |   29589   105189 |   10849     100      294     2.9 |  6.191 % |
c |       250 |   29589   105189 |   11934     250     1546     6.2 |  6.191 % |
c ==============================================================================
c Found solution: 895884
c ---[   0]---> Sorter-cost: 1831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       420 |   34259   116094 |   11419     420     3527     8.4 |  6.191 % |
c ==============================================================================
c Found solution: 277009
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       442 |   34312   116266 |   11437     442     3696     8.4 |  6.191 % |
c |       542 |   34312   116266 |   12580     542    19307    35.6 |  4.622 % |
c |       692 |   34312   116266 |   13838     692    20278    29.3 |  4.622 % |
c |       919 |   34304   116240 |   15222     918    23363    25.4 |  4.638 % |
c |      1256 |   34296   116214 |   16744    1254    26303    21.0 |  4.654 % |
c |      1762 |   34282   116183 |   18419    1758    31387    17.9 |  4.716 % |
c |      2523 |   34274   116157 |   20261    2518    52135    20.7 |  4.732 % |
c |      3663 |   34266   116131 |   22287    3657    86430    23.6 |  4.748 % |
c |      5371 |   34258   116105 |   24516    5364   157198    29.3 |  4.763 % |
c |      7933 |   34250   116079 |   26967    7925   283775    35.8 |  4.779 % |
c |     11777 |   34232   116039 |   29664   11766   467502    39.7 |  4.857 % |
c |     17545 |   34232   116039 |   32631   17534   744678    42.5 |  4.857 % |
c |     26194 |   34232   116039 |   35894   26183  1229982    47.0 |  4.857 % |
c |     39168 |   34232   116039 |   39483   16577   675473    40.7 |  4.857 % |
c |     58629 |   34224   116013 |   43431   36037  1748106    48.5 |  4.873 % |
c |     87821 |   34216   115987 |   47775   35097  1973601    56.2 |  4.889 % |
c |    131610 |   34216   115987 |   52552   44264  2632869    59.5 |  4.889 % |
c |    197294 |   34208   115965 |   57807   34890  2157751    61.8 |  4.920 % |
c |    295820 |   34194   115921 |   63588   47108  2866807    60.9 |  4.951 % |
c |    443610 |   34185   115894 |   69947   48453  3071079    63.4 |  4.983 % |

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/21747/stat): 21747 (minisat+_script) R 21746 21747 10120 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 1740834517 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/21747/statm): 174 3 169 147 0 27 0
[pid=21747] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libdl.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libdl.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/lib/locale/locale-archive
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
open syscall for file /usr/lib/gconv/gconv-modules.cache
New process pid=21748
New process pid=21749
New process pid=21750
execve syscall for /bin/sed executable
One traced child (pid=21749) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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
open syscall for file /usr/lib/locale/locale-archive
open syscall for file /usr/lib/gconv/gconv-modules.cache
One traced child (pid=21750) exited with status: 0
One traced child (pid=21748) exited with status: 0
New process pid=21751
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-markshare2_1.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 1512 0 0 0 977 8 0 0 25 0 1 0 1740834524 6512640 1463 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 1590 1463 145 145 0 1445 0
[pid=21751] vsize: 6360
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 10556

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 2149 0 0 0 1964 13 0 0 25 0 1 0 1740834524 9142272 2100 4294967295 134512640 135094434 3221221600 3221220256 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 2232 2100 145 145 0 2087 0
[pid=21751] vsize: 8928
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 13124

[startup+30.0062 s]
Raw data (loadavg): 0.95 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 2668 0 0 0 2953 18 0 0 25 0 1 0 1740834524 11235328 2619 4294967295 134512640 135094434 3221221600 3221220256 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 2743 2619 145 145 0 2598 0
[pid=21751] vsize: 10972
Current children cumulated CPU time (s) 29.73
Current children cumulated vsize (Kb) 15168

[startup+40.007 s]
Raw data (loadavg): 0.95 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3017 0 0 0 3947 21 0 0 25 0 1 0 1740834524 12775424 2968 4294967295 134512640 135094434 3221221600 3221220272 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 3119 2968 145 145 0 2974 0
[pid=21751] vsize: 12476
Current children cumulated CPU time (s) 39.7
Current children cumulated vsize (Kb) 16672

[startup+50.0078 s]
Raw data (loadavg): 0.96 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3017 0 0 0 4947 21 0 0 25 0 1 0 1740834524 12775424 2968 4294967295 134512640 135094434 3221221600 3221220236 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 3119 2968 145 145 0 2974 0
[pid=21751] vsize: 12476
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 16672

[startup+60.0086 s]
Raw data (loadavg): 0.97 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3017 0 0 0 5946 21 0 0 25 0 1 0 1740834524 12775424 2968 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 3119 2968 145 145 0 2974 0
[pid=21751] vsize: 12476
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 16672

[startup+70.0094 s]
Raw data (loadavg): 0.97 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3295 0 0 0 6941 24 0 0 25 0 1 0 1740834524 13901824 3246 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 3394 3246 145 145 0 3249 0
[pid=21751] vsize: 13576
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 17772

[startup+80.0101 s]
Raw data (loadavg): 0.98 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3721 0 0 0 7933 27 0 0 25 0 1 0 1740834524 15626240 3672 4294967295 134512640 135094434 3221221600 3221220240 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 3815 3672 145 145 0 3670 0
[pid=21751] vsize: 15260
Current children cumulated CPU time (s) 79.62
Current children cumulated vsize (Kb) 19456

[startup+90.0109 s]
Raw data (loadavg): 0.98 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3721 0 0 0 8933 27 0 0 25 0 1 0 1740834524 15626240 3672 4294967295 134512640 135094434 3221221600 3221220192 134557488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 3815 3672 145 145 0 3670 0
[pid=21751] vsize: 15260
Current children cumulated CPU time (s) 89.62
Current children cumulated vsize (Kb) 19456

[startup+100.011 s]
Raw data (loadavg): 0.98 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3721 0 0 0 9933 27 0 0 25 0 1 0 1740834524 15626240 3672 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 3815 3672 145 145 0 3670 0
[pid=21751] vsize: 15260
Current children cumulated CPU time (s) 99.62
Current children cumulated vsize (Kb) 19456

[startup+110.011 s]
Raw data (loadavg): 0.98 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3762 0 0 0 10932 27 0 0 25 0 1 0 1740834524 15798272 3713 4294967295 134512640 135094434 3221221600 3221220256 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 3857 3713 145 145 0 3712 0
[pid=21751] vsize: 15428
Current children cumulated CPU time (s) 109.61
Current children cumulated vsize (Kb) 19624

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4157 0 0 0 11923 31 0 0 25 0 1 0 1740834524 17408000 4108 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 4250 4108 145 145 0 4105 0
[pid=21751] vsize: 17000
Current children cumulated CPU time (s) 119.56
Current children cumulated vsize (Kb) 21196

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 12921 33 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0
[pid=21751] vsize: 17616
Current children cumulated CPU time (s) 129.56
Current children cumulated vsize (Kb) 21812

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 13921 33 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220256 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0
[pid=21751] vsize: 17616
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 21812

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 14921 33 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0
[pid=21751] vsize: 17616
Current children cumulated CPU time (s) 149.56
Current children cumulated vsize (Kb) 21812

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 15921 34 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220264 134556595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0
[pid=21751] vsize: 17616
Current children cumulated CPU time (s) 159.57
Current children cumulated vsize (Kb) 21812

[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 16921 34 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220272 134555957 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0
[pid=21751] vsize: 17616
Current children cumulated CPU time (s) 169.57
Current children cumulated vsize (Kb) 21812

[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4573 0 0 0 17916 36 0 0 25 0 1 0 1740834524 19103744 4524 4294967295 134512640 135094434 3221221600 3221220192 134557352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 4664 4524 145 145 0 4519 0
[pid=21751] vsize: 18656
Current children cumulated CPU time (s) 179.54
Current children cumulated vsize (Kb) 22852

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 18908 39 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0
[pid=21751] vsize: 20020
Current children cumulated CPU time (s) 189.49
Current children cumulated vsize (Kb) 24216

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 19908 40 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0
[pid=21751] vsize: 20020
Current children cumulated CPU time (s) 199.5
Current children cumulated vsize (Kb) 24216

[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 20908 40 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0
[pid=21751] vsize: 20020
Current children cumulated CPU time (s) 209.5
Current children cumulated vsize (Kb) 24216

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 21909 40 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0
[pid=21751] vsize: 20020
Current children cumulated CPU time (s) 219.51
Current children cumulated vsize (Kb) 24216

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 22908 40 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0
[pid=21751] vsize: 20020
Current children cumulated CPU time (s) 229.5
Current children cumulated vsize (Kb) 24216

[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4933 0 0 0 23909 40 0 0 25 0 1 0 1740834524 20582400 4884 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5025 4884 145 145 0 4880 0
[pid=21751] vsize: 20100
Current children cumulated CPU time (s) 239.51
Current children cumulated vsize (Kb) 24296

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4996 0 0 0 24908 40 0 0 25 0 1 0 1740834524 20840448 4947 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5088 4947 145 145 0 4943 0
[pid=21751] vsize: 20352
Current children cumulated CPU time (s) 249.5
Current children cumulated vsize (Kb) 24548

[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4996 0 0 0 25908 40 0 0 25 0 1 0 1740834524 20840448 4947 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5088 4947 145 145 0 4943 0
[pid=21751] vsize: 20352
Current children cumulated CPU time (s) 259.5
Current children cumulated vsize (Kb) 24548

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4996 0 0 0 26908 40 0 0 25 0 1 0 1740834524 20840448 4947 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5088 4947 145 145 0 4943 0
[pid=21751] vsize: 20352
Current children cumulated CPU time (s) 269.5
Current children cumulated vsize (Kb) 24548

[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4996 0 0 0 27908 40 0 0 25 0 1 0 1740834524 20840448 4947 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5088 4947 145 145 0 4943 0
[pid=21751] vsize: 20352
Current children cumulated CPU time (s) 279.5
Current children cumulated vsize (Kb) 24548

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5021 0 0 0 28908 40 0 0 25 0 1 0 1740834524 20946944 4972 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5114 4972 145 145 0 4969 0
[pid=21751] vsize: 20456
Current children cumulated CPU time (s) 289.5
Current children cumulated vsize (Kb) 24652

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5384 0 0 0 29901 44 0 0 25 0 1 0 1740834524 22425600 5335 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5475 5335 145 145 0 5330 0
[pid=21751] vsize: 21900
Current children cumulated CPU time (s) 299.47
Current children cumulated vsize (Kb) 26096

[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 30899 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0
[pid=21751] vsize: 22608
Current children cumulated CPU time (s) 309.46
Current children cumulated vsize (Kb) 26804

[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 31899 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0
[pid=21751] vsize: 22608
Current children cumulated CPU time (s) 319.46
Current children cumulated vsize (Kb) 26804

[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 32899 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220272 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0
[pid=21751] vsize: 22608
Current children cumulated CPU time (s) 329.46
Current children cumulated vsize (Kb) 26804

[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 33900 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0
[pid=21751] vsize: 22608
Current children cumulated CPU time (s) 339.47
Current children cumulated vsize (Kb) 26804

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 34900 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0
[pid=21751] vsize: 22608
Current children cumulated CPU time (s) 349.47
Current children cumulated vsize (Kb) 26804

[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 35900 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0
[pid=21751] vsize: 22608
Current children cumulated CPU time (s) 359.47
Current children cumulated vsize (Kb) 26804

[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5739 0 0 0 36897 46 0 0 25 0 1 0 1740834524 23871488 5690 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 5828 5690 145 145 0 5683 0
[pid=21751] vsize: 23312
Current children cumulated CPU time (s) 369.45
Current children cumulated vsize (Kb) 27508

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6064 0 0 0 37891 49 0 0 25 0 1 0 1740834524 25214976 6015 4294967295 134512640 135094434 3221221600 3221220192 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6156 6015 145 145 0 6011 0
[pid=21751] vsize: 24624
Current children cumulated CPU time (s) 379.42
Current children cumulated vsize (Kb) 28820

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 38890 49 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0
[pid=21751] vsize: 24736
Current children cumulated CPU time (s) 389.41
Current children cumulated vsize (Kb) 28932

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 39890 49 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0
[pid=21751] vsize: 24736
Current children cumulated CPU time (s) 399.41
Current children cumulated vsize (Kb) 28932

[startup+410.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 40890 49 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0
[pid=21751] vsize: 24736
Current children cumulated CPU time (s) 409.41
Current children cumulated vsize (Kb) 28932

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 41890 49 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0
[pid=21751] vsize: 24736
Current children cumulated CPU time (s) 419.41
Current children cumulated vsize (Kb) 28932

[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 42890 50 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0
[pid=21751] vsize: 24736
Current children cumulated CPU time (s) 429.42
Current children cumulated vsize (Kb) 28932

[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 43889 50 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134558035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0
[pid=21751] vsize: 24736
Current children cumulated CPU time (s) 439.41
Current children cumulated vsize (Kb) 28932

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6097 0 0 0 44889 50 0 0 25 0 1 0 1740834524 25329664 6048 4294967295 134512640 135094434 3221221600 3221220264 134556595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6184 6048 145 145 0 6039 0
[pid=21751] vsize: 24736
Current children cumulated CPU time (s) 449.41
Current children cumulated vsize (Kb) 28932

[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 45887 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220192 134557191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 459.4
Current children cumulated vsize (Kb) 29356

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 46887 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 469.4
Current children cumulated vsize (Kb) 29356

[startup+480.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 47887 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 479.4
Current children cumulated vsize (Kb) 29356

[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 48887 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 489.4
Current children cumulated vsize (Kb) 29356

[startup+500.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 49888 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 499.41
Current children cumulated vsize (Kb) 29356

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 50888 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 509.41
Current children cumulated vsize (Kb) 29356

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 51888 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 519.41
Current children cumulated vsize (Kb) 29356

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 52888 52 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 529.42
Current children cumulated vsize (Kb) 29356

[startup+540.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 53888 52 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 539.42
Current children cumulated vsize (Kb) 29356

[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 54889 52 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 549.43
Current children cumulated vsize (Kb) 29356

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 55889 52 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0
[pid=21751] vsize: 25160
Current children cumulated CPU time (s) 559.43
Current children cumulated vsize (Kb) 29356

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6275 0 0 0 56888 52 0 0 25 0 1 0 1740834524 26050560 6226 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6360 6226 145 145 0 6215 0
[pid=21751] vsize: 25440
Current children cumulated CPU time (s) 569.42
Current children cumulated vsize (Kb) 29636

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6435 0 0 0 57886 53 0 0 25 0 1 0 1740834524 26734592 6386 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6527 6386 145 145 0 6382 0
[pid=21751] vsize: 26108
Current children cumulated CPU time (s) 579.41
Current children cumulated vsize (Kb) 30304

[startup+590.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6435 0 0 0 58886 53 0 0 25 0 1 0 1740834524 26734592 6386 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6527 6386 145 145 0 6382 0
[pid=21751] vsize: 26108
Current children cumulated CPU time (s) 589.41
Current children cumulated vsize (Kb) 30304

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6445 0 0 0 59886 53 0 0 25 0 1 0 1740834524 26832896 6396 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6551 6396 145 145 0 6406 0
[pid=21751] vsize: 26204
Current children cumulated CPU time (s) 599.41
Current children cumulated vsize (Kb) 30400

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6456 0 0 0 60886 53 0 0 25 0 1 0 1740834524 26865664 6407 4294967295 134512640 135094434 3221221600 3221220256 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6559 6407 145 145 0 6414 0
[pid=21751] vsize: 26236
Current children cumulated CPU time (s) 609.41
Current children cumulated vsize (Kb) 30432

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6457 0 0 0 61886 53 0 0 25 0 1 0 1740834524 26865664 6408 4294967295 134512640 135094434 3221221600 3221220256 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6559 6408 145 145 0 6414 0
[pid=21751] vsize: 26236
Current children cumulated CPU time (s) 619.41
Current children cumulated vsize (Kb) 30432

[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6473 0 0 0 62887 53 0 0 25 0 1 0 1740834524 26963968 6424 4294967295 134512640 135094434 3221221600 3221220256 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6583 6424 145 145 0 6438 0
[pid=21751] vsize: 26332
Current children cumulated CPU time (s) 629.42
Current children cumulated vsize (Kb) 30528

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6473 0 0 0 63887 53 0 0 25 0 1 0 1740834524 26963968 6424 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6583 6424 145 145 0 6438 0
[pid=21751] vsize: 26332
Current children cumulated CPU time (s) 639.42
Current children cumulated vsize (Kb) 30528

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6480 0 0 0 64887 53 0 0 25 0 1 0 1740834524 26996736 6431 4294967295 134512640 135094434 3221221600 3221220272 134556610 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6591 6431 145 145 0 6446 0
[pid=21751] vsize: 26364
Current children cumulated CPU time (s) 649.42
Current children cumulated vsize (Kb) 30560

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6486 0 0 0 65887 53 0 0 25 0 1 0 1740834524 27029504 6437 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6599 6437 145 145 0 6454 0
[pid=21751] vsize: 26396
Current children cumulated CPU time (s) 659.42
Current children cumulated vsize (Kb) 30592

[startup+670.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6486 0 0 0 66887 53 0 0 25 0 1 0 1740834524 27029504 6437 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6599 6437 145 145 0 6454 0
[pid=21751] vsize: 26396
Current children cumulated CPU time (s) 669.42
Current children cumulated vsize (Kb) 30592

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6487 0 0 0 67888 53 0 0 25 0 1 0 1740834524 27029504 6438 4294967295 134512640 135094434 3221221600 3221220256 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6599 6438 145 145 0 6454 0
[pid=21751] vsize: 26396
Current children cumulated CPU time (s) 679.43
Current children cumulated vsize (Kb) 30592

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6527 0 0 0 68888 54 0 0 25 0 1 0 1740834524 27291648 6478 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6663 6478 145 145 0 6518 0
[pid=21751] vsize: 26652
Current children cumulated CPU time (s) 689.44
Current children cumulated vsize (Kb) 30848

[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6589 0 0 0 69887 54 0 0 25 0 1 0 1740834524 27594752 6540 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6737 6540 145 145 0 6592 0
[pid=21751] vsize: 26948
Current children cumulated CPU time (s) 699.43
Current children cumulated vsize (Kb) 31144

[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6787 0 0 0 70883 56 0 0 25 0 1 0 1740834524 28397568 6738 4294967295 134512640 135094434 3221221600 3221220256 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6933 6738 145 145 0 6788 0
[pid=21751] vsize: 27732
Current children cumulated CPU time (s) 709.41
Current children cumulated vsize (Kb) 31928

[startup+720.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6826 0 0 0 71881 57 0 0 25 0 1 0 1740834524 28553216 6777 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6971 6777 145 145 0 6826 0
[pid=21751] vsize: 27884
Current children cumulated CPU time (s) 719.4
Current children cumulated vsize (Kb) 32080

[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6826 0 0 0 72881 58 0 0 25 0 1 0 1740834524 28553216 6777 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6971 6777 145 145 0 6826 0
[pid=21751] vsize: 27884
Current children cumulated CPU time (s) 729.41
Current children cumulated vsize (Kb) 32080

[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6826 0 0 0 73881 58 0 0 25 0 1 0 1740834524 28553216 6777 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6971 6777 145 145 0 6826 0
[pid=21751] vsize: 27884
Current children cumulated CPU time (s) 739.41
Current children cumulated vsize (Kb) 32080

[startup+750.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6826 0 0 0 74881 58 0 0 25 0 1 0 1740834524 28553216 6777 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6971 6777 145 145 0 6826 0
[pid=21751] vsize: 27884
Current children cumulated CPU time (s) 749.41
Current children cumulated vsize (Kb) 32080

[startup+760.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6832 0 0 0 75881 59 0 0 25 0 1 0 1740834524 28581888 6783 4294967295 134512640 135094434 3221221600 3221220256 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6978 6783 145 145 0 6833 0
[pid=21751] vsize: 27912
Current children cumulated CPU time (s) 759.42
Current children cumulated vsize (Kb) 32108

[startup+770.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6833 0 0 0 76881 59 0 0 25 0 1 0 1740834524 28581888 6784 4294967295 134512640 135094434 3221221600 3221220256 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6978 6784 145 145 0 6833 0
[pid=21751] vsize: 27912
Current children cumulated CPU time (s) 769.42
Current children cumulated vsize (Kb) 32108

[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6839 0 0 0 77881 59 0 0 25 0 1 0 1740834524 28614656 6790 4294967295 134512640 135094434 3221221600 3221220288 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6986 6790 145 145 0 6841 0
[pid=21751] vsize: 27944
Current children cumulated CPU time (s) 779.42
Current children cumulated vsize (Kb) 32140

[startup+790.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6846 0 0 0 78882 59 0 0 25 0 1 0 1740834524 28647424 6797 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 6994 6797 145 145 0 6849 0
[pid=21751] vsize: 27976
Current children cumulated CPU time (s) 789.43
Current children cumulated vsize (Kb) 32172

[startup+800.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6858 0 0 0 79881 59 0 0 25 0 1 0 1740834524 28712960 6809 4294967295 134512640 135094434 3221221600 3221220256 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7010 6809 145 145 0 6865 0
[pid=21751] vsize: 28040
Current children cumulated CPU time (s) 799.42
Current children cumulated vsize (Kb) 32236

[startup+810.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6868 0 0 0 80881 59 0 0 25 0 1 0 1740834524 28778496 6819 4294967295 134512640 135094434 3221221600 3221220256 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7026 6819 145 145 0 6881 0
[pid=21751] vsize: 28104
Current children cumulated CPU time (s) 809.42
Current children cumulated vsize (Kb) 32300

[startup+820.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6868 0 0 0 81881 59 0 0 25 0 1 0 1740834524 28778496 6819 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7026 6819 145 145 0 6881 0
[pid=21751] vsize: 28104
Current children cumulated CPU time (s) 819.42
Current children cumulated vsize (Kb) 32300

[startup+830.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6936 0 0 0 82880 60 0 0 25 0 1 0 1740834524 29057024 6887 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7094 6887 145 145 0 6949 0
[pid=21751] vsize: 28376
Current children cumulated CPU time (s) 829.42
Current children cumulated vsize (Kb) 32572

[startup+840.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7186 0 0 0 83875 62 0 0 25 0 1 0 1740834524 30351360 7137 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7410 7137 145 145 0 7265 0
[pid=21751] vsize: 29640
Current children cumulated CPU time (s) 839.39
Current children cumulated vsize (Kb) 33836

[startup+850.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7360 0 0 0 84871 63 0 0 25 0 1 0 1740834524 31072256 7311 4294967295 134512640 135094434 3221221600 3221220256 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7586 7311 145 145 0 7441 0
[pid=21751] vsize: 30344
Current children cumulated CPU time (s) 849.36
Current children cumulated vsize (Kb) 34540

[startup+860.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7360 0 0 0 85871 64 0 0 25 0 1 0 1740834524 31072256 7311 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7586 7311 145 145 0 7441 0
[pid=21751] vsize: 30344
Current children cumulated CPU time (s) 859.37
Current children cumulated vsize (Kb) 34540

[startup+870.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7362 0 0 0 86871 64 0 0 25 0 1 0 1740834524 31072256 7313 4294967295 134512640 135094434 3221221600 3221220256 134557934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7586 7313 145 145 0 7441 0
[pid=21751] vsize: 30344
Current children cumulated CPU time (s) 869.37
Current children cumulated vsize (Kb) 34540

[startup+880.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7364 0 0 0 87872 64 0 0 25 0 1 0 1740834524 31072256 7315 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7586 7315 145 145 0 7441 0
[pid=21751] vsize: 30344
Current children cumulated CPU time (s) 879.38
Current children cumulated vsize (Kb) 34540

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7367 0 0 0 88872 64 0 0 25 0 1 0 1740834524 31072256 7318 4294967295 134512640 135094434 3221221600 3221220192 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7586 7318 145 145 0 7441 0
[pid=21751] vsize: 30344
Current children cumulated CPU time (s) 889.38
Current children cumulated vsize (Kb) 34540

[startup+900.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7367 0 0 0 89872 64 0 0 25 0 1 0 1740834524 31072256 7318 4294967295 134512640 135094434 3221221600 3221220256 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7586 7318 145 145 0 7441 0
[pid=21751] vsize: 30344
Current children cumulated CPU time (s) 899.38
Current children cumulated vsize (Kb) 34540

[startup+910.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7367 0 0 0 90872 64 0 0 25 0 1 0 1740834524 31072256 7318 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7586 7318 145 145 0 7441 0
[pid=21751] vsize: 30344
Current children cumulated CPU time (s) 909.38
Current children cumulated vsize (Kb) 34540

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7372 0 0 0 91872 64 0 0 25 0 1 0 1740834524 31105024 7323 4294967295 134512640 135094434 3221221600 3221220256 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7594 7323 145 145 0 7449 0
[pid=21751] vsize: 30376
Current children cumulated CPU time (s) 919.38
Current children cumulated vsize (Kb) 34572

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7387 0 0 0 92873 64 0 0 25 0 1 0 1740834524 31203328 7338 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7618 7338 145 145 0 7473 0
[pid=21751] vsize: 30472
Current children cumulated CPU time (s) 929.39
Current children cumulated vsize (Kb) 34668

[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7389 0 0 0 93872 64 0 0 25 0 1 0 1740834524 31203328 7340 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7618 7340 145 145 0 7473 0
[pid=21751] vsize: 30472
Current children cumulated CPU time (s) 939.38
Current children cumulated vsize (Kb) 34668

[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7422 0 0 0 94873 64 0 0 25 0 1 0 1740834524 31363072 7373 4294967295 134512640 135094434 3221221600 3221220288 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7657 7373 145 145 0 7512 0
[pid=21751] vsize: 30628
Current children cumulated CPU time (s) 949.39
Current children cumulated vsize (Kb) 34824

[startup+960.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7467 0 0 0 95872 65 0 0 25 0 1 0 1740834524 31539200 7418 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7700 7418 145 145 0 7555 0
[pid=21751] vsize: 30800
Current children cumulated CPU time (s) 959.39
Current children cumulated vsize (Kb) 34996

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7736 0 0 0 96867 67 0 0 25 0 1 0 1740834524 32636928 7687 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 7968 7687 145 145 0 7823 0
[pid=21751] vsize: 31872
Current children cumulated CPU time (s) 969.36
Current children cumulated vsize (Kb) 36068

[startup+980.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 97864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220192 134551428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 979.35
Current children cumulated vsize (Kb) 36952

[startup+990.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 98864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 989.35
Current children cumulated vsize (Kb) 36952

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 99864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 999.35
Current children cumulated vsize (Kb) 36952

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 100864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220272 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 1009.35
Current children cumulated vsize (Kb) 36952

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 101864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220212 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 1019.35
Current children cumulated vsize (Kb) 36952

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 102864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 1029.35
Current children cumulated vsize (Kb) 36952

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 103865 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 1039.36
Current children cumulated vsize (Kb) 36952

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 104865 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 1049.36
Current children cumulated vsize (Kb) 36952

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 105865 70 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134557987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 1059.37
Current children cumulated vsize (Kb) 36952

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 106865 70 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0
[pid=21751] vsize: 32756
Current children cumulated CPU time (s) 1069.37
Current children cumulated vsize (Kb) 36952

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7951 0 0 0 107865 70 0 0 25 0 1 0 1740834524 33607680 7902 4294967295 134512640 135094434 3221221600 3221220256 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 8205 7902 145 145 0 8060 0
[pid=21751] vsize: 32820
Current children cumulated CPU time (s) 1079.37
Current children cumulated vsize (Kb) 37016

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7951 0 0 0 108865 70 0 0 25 0 1 0 1740834524 33607680 7902 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21751/statm): 8205 7902 145 145 0 8060 0
[pid=21751] vsize: 32820
Current children cumulated CPU time (s) 1089.37
Current children cumulated vsize (Kb) 37016

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7951 0 0 0 109864 70 0 0 25 0 1 0 1740834524 33607680 7902 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8205 7902 145 145 0 8060 0
[pid=21751] vsize: 32820
Current children cumulated CPU time (s) 1099.36
Current children cumulated vsize (Kb) 37016

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7956 0 0 0 110865 70 0 0 25 0 1 0 1740834524 33640448 7907 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8213 7907 145 145 0 8068 0
[pid=21751] vsize: 32852
Current children cumulated CPU time (s) 1109.37
Current children cumulated vsize (Kb) 37048

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7966 0 0 0 111865 70 0 0 25 0 1 0 1740834524 33640448 7917 4294967295 134512640 135094434 3221221600 3221220240 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8213 7917 145 145 0 8068 0
[pid=21751] vsize: 32852
Current children cumulated CPU time (s) 1119.37
Current children cumulated vsize (Kb) 37048

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 112865 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0
[pid=21751] vsize: 32884
Current children cumulated CPU time (s) 1129.37
Current children cumulated vsize (Kb) 37080

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 113865 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0
[pid=21751] vsize: 32884
Current children cumulated CPU time (s) 1139.37
Current children cumulated vsize (Kb) 37080

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 114865 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0
[pid=21751] vsize: 32884
Current children cumulated CPU time (s) 1149.37
Current children cumulated vsize (Kb) 37080

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 115865 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0
[pid=21751] vsize: 32884
Current children cumulated CPU time (s) 1159.37
Current children cumulated vsize (Kb) 37080

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 116866 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134557978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0
[pid=21751] vsize: 32884
Current children cumulated CPU time (s) 1169.38
Current children cumulated vsize (Kb) 37080

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 117866 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0
[pid=21751] vsize: 32884
Current children cumulated CPU time (s) 1179.38
Current children cumulated vsize (Kb) 37080

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7972 0 0 0 118866 70 0 0 25 0 1 0 1740834524 33673216 7923 4294967295 134512640 135094434 3221221600 3221220256 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8221 7923 145 145 0 8076 0
[pid=21751] vsize: 32884
Current children cumulated CPU time (s) 1189.38
Current children cumulated vsize (Kb) 37080

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7973 0 0 0 119866 71 0 0 25 0 1 0 1740834524 33673216 7924 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8221 7924 145 145 0 8076 0
[pid=21751] vsize: 32884
Current children cumulated CPU time (s) 1199.39
Current children cumulated vsize (Kb) 37080

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7982 0 0 0 120866 71 0 0 25 0 1 0 1740834524 33738752 7933 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8237 7933 145 145 0 8092 0
[pid=21751] vsize: 32948
Current children cumulated CPU time (s) 1209.39
Current children cumulated vsize (Kb) 37144



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/56 21751
Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0
[pid=21747] vsize: 4196
Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7982 0 0 0 120866 71 0 0 25 0 1 0 1740834524 33738752 7933 4294967295 134512640 135094434 3221221600 3221220064 134780585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21751/statm): 8237 7933 145 145 0 8092 0
[pid=21751] vsize: 32948
Current children cumulated CPU time (s) 1209.39
Current children cumulated vsize (Kb) 37144

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.4
CPU user time (s): 1208.67
CPU system time (s): 0.727889
CPU usage (%): 99.9413
Max. virtual memory (cumulated for all children) (Kb): 37144

Verifier Data

ERROR: no interpretation found !