Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namesubmitted/aloul/FPGA_SAT05/normalized-fpga45_44_sat_pb.cnf.cr.opb
MD5SUMc501a04dd091dbe678ec2743021adc30
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 46
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark14.2518
Number of variables2970
Total number of constraints2113
Number of constraints which are clauses2024
Number of constraints which are cardinality constraints (but not clauses)89
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint22
Maximum length of a constraint45

Trace number 898

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        942808 kB
Buffers:         33412 kB
Cached:          31060 kB
SwapCached:        536 kB
Active:          53784 kB
Inactive:        13252 kB
HighTotal:      131008 kB
HighFree:        97860 kB
LowTotal:       903652 kB
LowFree:        844948 kB
SwapTotal:     2097892 kB
SwapFree:      2096832 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5856 kB
Slab:            19216 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:57:11 (client local time) WITH STATUS 0 IN 1208.42 SECONDS
stats: 2395 7 1208.42 0

Solver Data

c Parsing PB file...
c Converting 2113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  88]---> BDD-cost:   85
c ---[  87]---> BDD-cost:   85
c ---[  86]---> BDD-cost:   85
c ---[  85]---> BDD-cost:   85
c ---[  84]---> BDD-cost:   85
c ---[  83]---> BDD-cost:   85
c ---[  82]---> BDD-cost:   85
c ---[  81]---> BDD-cost:   85
c ---[  80]---> BDD-cost:   85
c ---[  79]---> BDD-cost:   85
c ---[  78]---> BDD-cost:   85
c ---[  77]---> BDD-cost:   85
c ---[  76]---> BDD-cost:   85
c ---[  75]---> BDD-cost:   85
c ---[  74]---> BDD-cost:   85
c ---[  73]---> BDD-cost:   85
c ---[  72]---> BDD-cost:   85
c ---[  71]---> BDD-cost:   85
c ---[  70]---> BDD-cost:   85
c ---[  69]---> BDD-cost:   85
c ---[  68]---> BDD-cost:   85
c ---[  67]---> BDD-cost:   85
c ---[  66]---> BDD-cost:   85
c ---[  65]---> BDD-cost:   85
c ---[  64]---> BDD-cost:   85
c ---[  63]---> BDD-cost:   85
c ---[  62]---> BDD-cost:   85
c ---[  61]---> BDD-cost:   85
c ---[  60]---> BDD-cost:   85
c ---[  59]---> BDD-cost:   85
c ---[  58]---> BDD-cost:   85
c ---[  57]---> BDD-cost:   85
c ---[  56]---> BDD-cost:   85
c ---[  55]---> BDD-cost:   85
c ---[  54]---> BDD-cost:   85
c ---[  53]---> BDD-cost:   85
c ---[  52]---> BDD-cost:   85
c ---[  51]---> BDD-cost:   85
c ---[  50]---> BDD-cost:   85
c ---[  49]---> BDD-cost:   85
c ---[  48]---> BDD-cost:   85
c ---[  47]---> BDD-cost:   85
c ---[  46]---> BDD-cost:   85
c ---[  45]---> BDD-cost:   85
c ---[  44]---> BDD-cost:   85
c ---[  43]---> BDD-cost:   41
c ---[  42]---> BDD-cost:   41
c ---[  41]---> BDD-cost:   41
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   41
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:   41
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:   41
c ---[  33]---> BDD-cost:   41
c ---[  32]---> BDD-cost:   41
c ---[  31]---> BDD-cost:   41
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:   41
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:   41
c ---[  24]---> BDD-cost:   41
c ---[  23]---> BDD-cost:   41
c ---[  22]---> BDD-cost:   41
c ---[  21]---> BDD-cost:   43
c ---[  20]---> BDD-cost:   43
c ---[  19]---> BDD-cost:   43
c ---[  18]---> BDD-cost:   43
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:   43
c ---[  15]---> BDD-cost:   43
c ---[  14]---> BDD-cost:   43
c ---[  13]---> BDD-cost:   43
c ---[  12]---> BDD-cost:   43
c ---[  11]---> BDD-cost:   43
c ---[  10]---> BDD-cost:   43
c ---[   9]---> BDD-cost:   43
c ---[   8]---> BDD-cost:   43
c ---[   7]---> BDD-cost:   43
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   43
c ---[   3]---> BDD-cost:   43
c ---[   2]---> BDD-cost:   43
c ---[   1]---> BDD-cost:   43
c ---[   0]---> BDD-cost:   43
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   16073    84083 |    5357       0        0     nan |  0.000 % |
c |       101 |   16073    84083 |    5892     101    25615   253.6 |  1.030 % |
c |       252 |   16073    84083 |    6481     252    61496   244.0 |  1.030 % |
c |       477 |   16073    84083 |    7130     477   112639   236.1 |  1.030 % |
c |       816 |   16073    84083 |    7843     816   210746   258.3 |  1.030 % |
c |      1323 |   16073    84083 |    8627    1323   346348   261.8 |  1.030 % |
c |      2083 |   16073    84083 |    9490    2083   564649   271.1 |  1.030 % |
c |      3223 |   16073    84083 |   10439    3223   718568   223.0 |  1.030 % |
c |      4931 |   16073    84083 |   11483    4931  1368853   277.6 |  1.030 % |
c |      7493 |   16073    84083 |   12631    7493  2490469   332.4 |  1.030 % |
c |     11338 |   16073    84083 |   13894   11338  3675913   324.2 |  1.030 % |
c |     17111 |   16073    84083 |   15284   17111  5830865   340.8 |  1.030 % |
c |     25761 |   16073    84083 |   16812   17206  6458966   375.4 |  1.030 % |
c |     38737 |   16073    84083 |   18493   11018  2215373   201.1 |  1.030 % |
c |     58201 |   16073    84083 |   20343   17865  7499448   419.8 |  1.030 % |
c |     87396 |   16073    84083 |   22377   17045  3155458   185.1 |  1.030 % |
c |    131187 |   16073    84083 |   24615   16857  8064521   478.4 |  1.030 % |
c |    196875 |   16073    84083 |   27076   16816  7876802   468.4 |  1.030 % |

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/24000/stat): 24000 (minisat+_script) R 23999 24000 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841308164 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24000/statm): 174 3 169 147 0 27 0
[pid=24000] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=24001
New process pid=24002
New process pid=24003
execve syscall for /bin/sed executable
One traced child (pid=24002) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=24003) exited with status: 0
One traced child (pid=24001) exited with status: 0
New process pid=24004
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-fpga45_44_sat_pb.cnf.cr.opb

[startup+10.005 s]
Raw data (loadavg): 0.94 0.98 0.95 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 2860 0 3 0 949 13 0 0 25 0 1 0 1841308170 12001280 2849 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24004/statm): 2930 2849 145 145 0 2785 0
[pid=24004] vsize: 11720
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 13844

[startup+20.0058 s]
Raw data (loadavg): 0.95 0.98 0.95 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 4529 0 3 0 1928 24 0 0 25 0 1 0 1841308170 18853888 4518 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24004/statm): 4603 4518 145 145 0 4458 0
[pid=24004] vsize: 18412
Current children cumulated CPU time (s) 19.54
Current children cumulated vsize (Kb) 20536

[startup+30.0074 s]
Raw data (loadavg): 0.95 0.98 0.95 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 5924 0 3 0 2906 32 0 0 25 0 1 0 1841308170 24559616 5913 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 5996 5913 145 145 0 5851 0
[pid=24004] vsize: 23984
Current children cumulated CPU time (s) 29.4
Current children cumulated vsize (Kb) 26108

[startup+40.0082 s]
Raw data (loadavg): 1.03 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7035 0 3 0 3890 39 0 0 25 0 1 0 1841308170 29188096 7024 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 7126 7024 145 145 0 6981 0
[pid=24004] vsize: 28504
Current children cumulated CPU time (s) 39.31
Current children cumulated vsize (Kb) 30628

[startup+50.0089 s]
Raw data (loadavg): 1.03 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7104 0 3 0 4889 40 0 0 25 0 1 0 1841308170 29470720 7093 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 7195 7093 145 145 0 7050 0
[pid=24004] vsize: 28780
Current children cumulated CPU time (s) 49.31
Current children cumulated vsize (Kb) 30904

[startup+60.0096 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7104 0 3 0 5890 40 0 0 25 0 1 0 1841308170 29470720 7093 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 7195 7093 145 145 0 7050 0
[pid=24004] vsize: 28780
Current children cumulated CPU time (s) 59.32
Current children cumulated vsize (Kb) 30904

[startup+70.0103 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7890 0 3 0 6878 44 0 0 25 0 1 0 1841308170 32702464 7879 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24004/statm): 7984 7879 145 145 0 7839 0
[pid=24004] vsize: 31936
Current children cumulated CPU time (s) 69.24
Current children cumulated vsize (Kb) 34060

[startup+80.012 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7893 0 3 0 7878 44 0 0 25 0 1 0 1841308170 32702464 7882 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 7984 7882 145 145 0 7839 0
[pid=24004] vsize: 31936
Current children cumulated CPU time (s) 79.24
Current children cumulated vsize (Kb) 34060

[startup+90.0127 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7894 0 3 0 8878 44 0 0 25 0 1 0 1841308170 32702464 7883 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 7984 7883 145 145 0 7839 0
[pid=24004] vsize: 31936
Current children cumulated CPU time (s) 89.24
Current children cumulated vsize (Kb) 34060

[startup+100.013 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7894 0 3 0 9878 44 0 0 25 0 1 0 1841308170 32702464 7883 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 7984 7883 145 145 0 7839 0
[pid=24004] vsize: 31936
Current children cumulated CPU time (s) 99.24
Current children cumulated vsize (Kb) 34060

[startup+110.015 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7894 0 3 0 10879 44 0 0 25 0 1 0 1841308170 32702464 7883 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 7984 7883 145 145 0 7839 0
[pid=24004] vsize: 31936
Current children cumulated CPU time (s) 109.25
Current children cumulated vsize (Kb) 34060

[startup+120.016 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 8144 0 3 0 11875 46 0 0 25 0 1 0 1841308170 33726464 8133 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 8234 8133 145 145 0 8089 0
[pid=24004] vsize: 32936
Current children cumulated CPU time (s) 119.23
Current children cumulated vsize (Kb) 35060

[startup+130.018 s]
Raw data (loadavg): 1.01 1.00 0.96 1/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) T 24000 24000 21452 0 -1 0 8651 0 3 0 12868 49 0 0 25 0 1 0 1841308170 35815424 8640 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24004/statm): 8744 8640 145 145 0 8599 0
[pid=24004] vsize: 34976
Current children cumulated CPU time (s) 129.19
Current children cumulated vsize (Kb) 37100

[startup+140.018 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9267 0 3 0 13858 53 0 0 25 0 1 0 1841308170 38354944 9256 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24004/statm): 9364 9256 145 145 0 9219 0
[pid=24004] vsize: 37456
Current children cumulated CPU time (s) 139.13
Current children cumulated vsize (Kb) 39580

[startup+150.019 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9799 0 3 0 14851 56 0 0 25 0 1 0 1841308170 40542208 9788 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 9898 9788 145 145 0 9753 0
[pid=24004] vsize: 39592
Current children cumulated CPU time (s) 149.09
Current children cumulated vsize (Kb) 41716

[startup+160.021 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9800 0 3 0 15852 56 0 0 25 0 1 0 1841308170 40542208 9789 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 9898 9789 145 145 0 9753 0
[pid=24004] vsize: 39592
Current children cumulated CPU time (s) 159.1
Current children cumulated vsize (Kb) 41716

[startup+170.021 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9800 0 3 0 16852 56 0 0 25 0 1 0 1841308170 40542208 9789 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 9898 9789 145 145 0 9753 0
[pid=24004] vsize: 39592
Current children cumulated CPU time (s) 169.1
Current children cumulated vsize (Kb) 41716

[startup+180.022 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9800 0 3 0 17852 56 0 0 25 0 1 0 1841308170 40542208 9789 4294967295 134512640 135094434 3221224432 3221223104 134556540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 9898 9789 145 145 0 9753 0
[pid=24004] vsize: 39592
Current children cumulated CPU time (s) 179.1
Current children cumulated vsize (Kb) 41716

[startup+190.023 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9800 0 3 0 18853 56 0 0 25 0 1 0 1841308170 40542208 9789 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 9898 9789 145 145 0 9753 0
[pid=24004] vsize: 39592
Current children cumulated CPU time (s) 189.11
Current children cumulated vsize (Kb) 41716

[startup+200.024 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 10594 0 3 0 19839 61 0 0 25 0 1 0 1841308170 43798528 10583 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24004/statm): 10693 10583 145 145 0 10548 0
[pid=24004] vsize: 42772
Current children cumulated CPU time (s) 199.02
Current children cumulated vsize (Kb) 44896

[startup+210.024 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12082 0 3 0 20818 69 0 0 25 0 1 0 1841308170 49885184 12071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24004/statm): 12179 12071 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 208.89
Current children cumulated vsize (Kb) 50840

[startup+220.025 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12082 0 3 0 21817 70 0 0 25 0 1 0 1841308170 49885184 12071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12071 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 218.89
Current children cumulated vsize (Kb) 50840

[startup+230.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12082 0 3 0 22818 70 0 0 25 0 1 0 1841308170 49885184 12071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12071 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 228.9
Current children cumulated vsize (Kb) 50840

[startup+240.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12082 0 3 0 23818 70 0 0 25 0 1 0 1841308170 49885184 12071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12071 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 238.9
Current children cumulated vsize (Kb) 50840

[startup+250.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 24818 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 248.9
Current children cumulated vsize (Kb) 50840

[startup+260.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 25818 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 258.9
Current children cumulated vsize (Kb) 50840

[startup+270.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 26818 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 268.9
Current children cumulated vsize (Kb) 50840

[startup+280.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 27819 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 278.91
Current children cumulated vsize (Kb) 50840

[startup+290.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 28819 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223056 134562146 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 288.91
Current children cumulated vsize (Kb) 50840

[startup+300.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 29819 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 298.91
Current children cumulated vsize (Kb) 50840

[startup+310.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 30820 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 308.92
Current children cumulated vsize (Kb) 50840

[startup+320.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 31820 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 318.92
Current children cumulated vsize (Kb) 50840

[startup+330.036 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 32820 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 328.92
Current children cumulated vsize (Kb) 50840

[startup+340.036 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 33820 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 338.92
Current children cumulated vsize (Kb) 50840

[startup+350.037 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 34821 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 348.93
Current children cumulated vsize (Kb) 50840

[startup+360.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 35821 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 358.93
Current children cumulated vsize (Kb) 50840

[startup+370.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 36821 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 368.93
Current children cumulated vsize (Kb) 50840

[startup+380.041 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 37822 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 378.94
Current children cumulated vsize (Kb) 50840

[startup+390.042 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 38822 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0
[pid=24004] vsize: 48716
Current children cumulated CPU time (s) 388.94
Current children cumulated vsize (Kb) 50840

[startup+400.043 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12275 0 3 0 39819 70 0 0 25 0 1 0 1841308170 50671616 12264 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 12371 12264 145 145 0 12226 0
[pid=24004] vsize: 49484
Current children cumulated CPU time (s) 398.91
Current children cumulated vsize (Kb) 51608

[startup+410.043 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12976 0 3 0 40808 76 0 0 25 0 1 0 1841308170 53547008 12965 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 13073 12965 145 145 0 12928 0
[pid=24004] vsize: 52292
Current children cumulated CPU time (s) 408.86
Current children cumulated vsize (Kb) 54416

[startup+420.045 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 13499 0 3 0 41801 78 0 0 25 0 1 0 1841308170 55701504 13488 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 13599 13488 145 145 0 13454 0
[pid=24004] vsize: 54396
Current children cumulated CPU time (s) 418.81
Current children cumulated vsize (Kb) 56520

[startup+430.047 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 13675 0 3 0 42798 79 0 0 25 0 1 0 1841308170 56475648 13664 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 13788 13664 145 145 0 13643 0
[pid=24004] vsize: 55152
Current children cumulated CPU time (s) 428.79
Current children cumulated vsize (Kb) 57276

[startup+440.048 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 13898 0 3 0 43795 80 0 0 25 0 1 0 1841308170 57462784 13887 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14029 13887 145 145 0 13884 0
[pid=24004] vsize: 56116
Current children cumulated CPU time (s) 438.77
Current children cumulated vsize (Kb) 58240

[startup+450.048 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14387 0 3 0 44787 83 0 0 25 0 1 0 1841308170 59469824 14376 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14519 14376 145 145 0 14374 0
[pid=24004] vsize: 58076
Current children cumulated CPU time (s) 448.72
Current children cumulated vsize (Kb) 60200

[startup+460.049 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 45778 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 458.67
Current children cumulated vsize (Kb) 61872

[startup+470.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 46779 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 468.68
Current children cumulated vsize (Kb) 61872

[startup+480.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 47779 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 478.68
Current children cumulated vsize (Kb) 61872

[startup+490.051 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 48779 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 488.68
Current children cumulated vsize (Kb) 61872

[startup+500.051 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 49779 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 498.68
Current children cumulated vsize (Kb) 61872

[startup+510.052 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 50780 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 508.69
Current children cumulated vsize (Kb) 61872

[startup+520.052 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 51780 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 518.69
Current children cumulated vsize (Kb) 61872

[startup+530.052 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 52780 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 528.69
Current children cumulated vsize (Kb) 61872

[startup+540.053 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 53780 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0
[pid=24004] vsize: 59748
Current children cumulated CPU time (s) 538.69
Current children cumulated vsize (Kb) 61872

[startup+550.053 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14874 0 3 0 54780 88 0 0 25 0 1 0 1841308170 61464576 14863 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 15006 14863 145 145 0 14861 0
[pid=24004] vsize: 60024
Current children cumulated CPU time (s) 548.7
Current children cumulated vsize (Kb) 62148

[startup+560.054 s]
Raw data (loadavg): 1.07 1.02 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 15389 0 3 0 55772 90 0 0 25 0 1 0 1841308170 63586304 15378 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 15524 15378 145 145 0 15379 0
[pid=24004] vsize: 62096
Current children cumulated CPU time (s) 558.64
Current children cumulated vsize (Kb) 64220

[startup+570.055 s]
Raw data (loadavg): 1.06 1.02 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 15879 0 3 0 56765 94 0 0 25 0 1 0 1841308170 65593344 15868 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 16014 15868 145 145 0 15869 0
[pid=24004] vsize: 64056
Current children cumulated CPU time (s) 568.61
Current children cumulated vsize (Kb) 66180

[startup+580.056 s]
Raw data (loadavg): 1.05 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16220 0 3 0 57760 96 0 0 25 0 1 0 1841308170 67002368 16209 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 16358 16209 145 145 0 16213 0
[pid=24004] vsize: 65432
Current children cumulated CPU time (s) 578.58
Current children cumulated vsize (Kb) 67556

[startup+590.056 s]
Raw data (loadavg): 1.04 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 58756 97 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0
[pid=24004] vsize: 66380
Current children cumulated CPU time (s) 588.55
Current children cumulated vsize (Kb) 68504

[startup+600.057 s]
Raw data (loadavg): 1.04 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 59756 97 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0
[pid=24004] vsize: 66380
Current children cumulated CPU time (s) 598.55
Current children cumulated vsize (Kb) 68504

[startup+610.058 s]
Raw data (loadavg): 1.03 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 60756 97 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0
[pid=24004] vsize: 66380
Current children cumulated CPU time (s) 608.55
Current children cumulated vsize (Kb) 68504

[startup+620.058 s]
Raw data (loadavg): 1.02 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 61756 98 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0
[pid=24004] vsize: 66380
Current children cumulated CPU time (s) 618.56
Current children cumulated vsize (Kb) 68504

[startup+630.059 s]
Raw data (loadavg): 1.02 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 62756 98 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0
[pid=24004] vsize: 66380
Current children cumulated CPU time (s) 628.56
Current children cumulated vsize (Kb) 68504

[startup+640.06 s]
Raw data (loadavg): 1.02 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 63756 98 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0
[pid=24004] vsize: 66380
Current children cumulated CPU time (s) 638.56
Current children cumulated vsize (Kb) 68504

[startup+650.059 s]
Raw data (loadavg): 1.01 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16642 0 3 0 64754 99 0 0 25 0 1 0 1841308170 68734976 16631 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 16781 16631 145 145 0 16636 0
[pid=24004] vsize: 67124
Current children cumulated CPU time (s) 648.55
Current children cumulated vsize (Kb) 69248

[startup+660.061 s]
Raw data (loadavg): 1.01 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17491 0 3 0 65742 104 0 0 25 0 1 0 1841308170 72228864 17480 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 17634 17480 145 145 0 17489 0
[pid=24004] vsize: 70536
Current children cumulated CPU time (s) 658.48
Current children cumulated vsize (Kb) 72660

[startup+670.062 s]
Raw data (loadavg): 1.01 1.01 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17883 0 3 0 66737 106 0 0 25 0 1 0 1841308170 73842688 17872 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17872 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 668.45
Current children cumulated vsize (Kb) 74236

[startup+680.062 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17885 0 3 0 67737 106 0 0 25 0 1 0 1841308170 73842688 17874 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17874 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 678.45
Current children cumulated vsize (Kb) 74236

[startup+690.062 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17885 0 3 0 68737 106 0 0 25 0 1 0 1841308170 73842688 17874 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17874 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 688.45
Current children cumulated vsize (Kb) 74236

[startup+700.063 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 69738 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 698.46
Current children cumulated vsize (Kb) 74236

[startup+710.064 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 70738 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 708.46
Current children cumulated vsize (Kb) 74236

[startup+720.064 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 71738 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 718.46
Current children cumulated vsize (Kb) 74236

[startup+730.065 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 72738 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 728.46
Current children cumulated vsize (Kb) 74236

[startup+740.066 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 73739 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 738.47
Current children cumulated vsize (Kb) 74236

[startup+750.067 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 74739 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 748.47
Current children cumulated vsize (Kb) 74236

[startup+760.068 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 75739 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 758.47
Current children cumulated vsize (Kb) 74236

[startup+770.069 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 76740 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 768.48
Current children cumulated vsize (Kb) 74236

[startup+780.07 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 77740 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 778.48
Current children cumulated vsize (Kb) 74236

[startup+790.071 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 78740 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 788.48
Current children cumulated vsize (Kb) 74236

[startup+800.07 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 79740 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0
[pid=24004] vsize: 72112
Current children cumulated CPU time (s) 798.48
Current children cumulated vsize (Kb) 74236

[startup+810.071 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) T 24000 24000 21452 0 -1 0 18221 0 3 0 80735 108 0 0 25 0 1 0 1841308170 75264000 18210 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18375 18210 145 145 0 18230 0
[pid=24004] vsize: 73500
Current children cumulated CPU time (s) 808.45
Current children cumulated vsize (Kb) 75624

[startup+820.072 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 18819 0 3 0 81725 112 0 0 25 0 1 0 1841308170 77721600 18808 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 18975 18808 145 145 0 18830 0
[pid=24004] vsize: 75900
Current children cumulated CPU time (s) 818.39
Current children cumulated vsize (Kb) 78024

[startup+830.071 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19206 0 3 0 82720 114 0 0 25 0 1 0 1841308170 79388672 19195 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19382 19195 145 145 0 19237 0
[pid=24004] vsize: 77528
Current children cumulated CPU time (s) 828.36
Current children cumulated vsize (Kb) 79652

[startup+840.072 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 83716 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 838.34
Current children cumulated vsize (Kb) 80800

[startup+850.073 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 84716 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 848.34
Current children cumulated vsize (Kb) 80800

[startup+860.073 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 85716 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 858.34
Current children cumulated vsize (Kb) 80800

[startup+870.074 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 86717 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 868.35
Current children cumulated vsize (Kb) 80800

[startup+880.075 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 87717 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 878.35
Current children cumulated vsize (Kb) 80800

[startup+890.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 88717 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 888.35
Current children cumulated vsize (Kb) 80800

[startup+900.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 89717 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 898.35
Current children cumulated vsize (Kb) 80800

[startup+910.077 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 90718 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 908.36
Current children cumulated vsize (Kb) 80800

[startup+920.078 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 91718 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 918.36
Current children cumulated vsize (Kb) 80800

[startup+930.078 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 92718 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134555980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 928.36
Current children cumulated vsize (Kb) 80800

[startup+940.079 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 93718 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 938.36
Current children cumulated vsize (Kb) 80800

[startup+950.08 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 94719 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 948.37
Current children cumulated vsize (Kb) 80800

[startup+960.082 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 95719 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 958.37
Current children cumulated vsize (Kb) 80800

[startup+970.082 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 96719 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 968.37
Current children cumulated vsize (Kb) 80800

[startup+980.083 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 97719 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 978.37
Current children cumulated vsize (Kb) 80800

[startup+990.084 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 98720 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 988.38
Current children cumulated vsize (Kb) 80800

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 99720 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 998.38
Current children cumulated vsize (Kb) 80800

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 100720 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1008.38
Current children cumulated vsize (Kb) 80800

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 101720 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1018.38
Current children cumulated vsize (Kb) 80800

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 102721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1028.39
Current children cumulated vsize (Kb) 80800

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 103721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1038.39
Current children cumulated vsize (Kb) 80800

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 104721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1048.39
Current children cumulated vsize (Kb) 80800

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 105721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1058.39
Current children cumulated vsize (Kb) 80800

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 106721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1068.39
Current children cumulated vsize (Kb) 80800

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 107722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1078.4
Current children cumulated vsize (Kb) 80800

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 108722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1088.4
Current children cumulated vsize (Kb) 80800

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 109721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1098.39
Current children cumulated vsize (Kb) 80800

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 110722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1108.4
Current children cumulated vsize (Kb) 80800

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 111722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1118.4
Current children cumulated vsize (Kb) 80800

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 112722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1128.4
Current children cumulated vsize (Kb) 80800

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 113722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1138.4
Current children cumulated vsize (Kb) 80800

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19498 0 3 0 114723 116 0 0 25 0 1 0 1841308170 80564224 19487 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19487 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1148.41
Current children cumulated vsize (Kb) 80800

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19499 0 3 0 115723 116 0 0 25 0 1 0 1841308170 80564224 19488 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 19669 19488 145 145 0 19524 0
[pid=24004] vsize: 78676
Current children cumulated CPU time (s) 1158.41
Current children cumulated vsize (Kb) 80800

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 116717 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0
[pid=24004] vsize: 80064
Current children cumulated CPU time (s) 1168.38
Current children cumulated vsize (Kb) 82188

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 117717 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0
[pid=24004] vsize: 80064
Current children cumulated CPU time (s) 1178.38
Current children cumulated vsize (Kb) 82188

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 118718 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0
[pid=24004] vsize: 80064
Current children cumulated CPU time (s) 1188.39
Current children cumulated vsize (Kb) 82188

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 119718 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0
[pid=24004] vsize: 80064
Current children cumulated CPU time (s) 1198.39
Current children cumulated vsize (Kb) 82188

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 120718 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0
[pid=24004] vsize: 80064
Current children cumulated CPU time (s) 1208.39
Current children cumulated vsize (Kb) 82188



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 24004
Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24000/statm): 531 226 485 147 0 384 0
[pid=24000] vsize: 2124
Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 120718 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0
[pid=24004] vsize: 80064
Current children cumulated CPU time (s) 1208.39
Current children cumulated vsize (Kb) 82188

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1208.42
CPU user time (s): 1207.19
CPU system time (s): 1.22981
CPU usage (%): 99.8576
Max. virtual memory (cumulated for all children) (Kb): 82188

Verifier Data

ERROR: no interpretation found !