Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-khb05250.opb
MD5SUM5d4b655a5461d6a0782bca8bd105f9c2
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 303845819772
Optimality of the best value was proved NO
Number of terms in the objective function 37494
Biggest coefficient in the objective function 6251324899328
Number of bits for the biggest coefficient in the objective function 43
Sum of the numbers in the objective function 5652283493428566
Number of bits of the sum of numbers in the objective function 53
Biggest number in a constraint 6251324899328
Number of bits of the biggest number in a constraint 43
Biggest sum of numbers in a constraint 5652283493428566
Number of bits of the biggest sum of numbers53
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1233.78
Number of variables38297
Total number of constraints126
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)24
Number of constraints which are nor clauses,nor cardinality constraints102
Minimum length of a constraint1
Maximum length of a constraint1530

Trace number 4555

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        853240 kB
Buffers:         39856 kB
Cached:         114552 kB
SwapCached:       1040 kB
Active:          67232 kB
Inactive:        89880 kB
HighTotal:      131008 kB
HighFree:        23884 kB
LowTotal:       903652 kB
LowFree:        829356 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            18628 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:42:46 (client local time) WITH STATUS 0 IN 1209.4 SECONDS
stats: 3018 7 1209.4 0

Solver Data

c Parsing PB file...
c Converting 179 PB-constraints to clauses...
c   -- Unit propagations: pppppp
c   -- Detecting intervals from adjacent constraints: ############################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 178]---> BDD-cost:   22
c ---[ 174]---> Adder-cost: 843   maxlim: 149504   bits: 19/18
c ---[ 172]---> Adder-cost: 795   maxlim: 89088   bits: 18/17
c ---[ 170]---> Adder-cost: 939   maxlim: 688128   bits: 21/20
c ---[ 168]---> Adder-cost: 987   maxlim: 1369088   bits: 22/21
c ---[ 166]---> Adder-cost: 699   maxlim: 31744   bits: 16/15
c ---[ 164]---> Adder-cost: 939   maxlim: 572416   bits: 21/20
c ---[ 162]---> Adder-cost: 1035   maxlim: 2426880   bits: 23/22
c ---[ 160]---> Adder-cost: 987   maxlim: 1115136   bits: 22/21
c ---[ 158]---> Adder-cost: 747   maxlim: 33792   bits: 17/16
c ---[ 156]---> Adder-cost: 747   maxlim: 32768   bits: 17/16
c ---[ 154]---> Adder-cost: 1083   maxlim: 5626880   bits: 24/23
c ---[ 152]---> Adder-cost: 939   maxlim: 925696   bits: 21/20
c ---[ 150]---> Adder-cost: 987   maxlim: 1501184   bits: 22/21
c ---[ 148]---> Adder-cost: 843   maxlim: 146432   bits: 19/18
c ---[ 146]---> Adder-cost: 939   maxlim: 629760   bits: 21/20
c ---[ 144]---> Adder-cost: 939   maxlim: 577536   bits: 21/20
c ---[ 142]---> Adder-cost: 843   maxlim: 231424   bits: 19/18
c ---[ 140]---> Adder-cost: 1035   maxlim: 3088384   bits: 23/22
c ---[ 138]---> Adder-cost: 843   maxlim: 259072   bits: 19/18
c ---[ 136]---> Adder-cost: 843   maxlim: 199680   bits: 19/18
c ---[ 134]---> Adder-cost: 747   maxlim: 38912   bits: 17/16
c ---[ 132]---> Adder-cost: 939   maxlim: 826368   bits: 21/20
c ---[ 130]---> Adder-cost: 939   maxlim: 564224   bits: 21/20
c ---[ 128]---> Adder-cost: 891   maxlim: 311296   bits: 20/19
c ---[ 126]---> Adder-cost: 939   maxlim: 833536   bits: 21/20
c ---[ 124]---> Adder-cost: 891   maxlim: 345088   bits: 20/19
c ---[ 122]---> Adder-cost: 1083   maxlim: 4472832   bits: 24/23
c ---[ 120]---> Adder-cost: 939   maxlim: 590848   bits: 21/20
c ---[ 118]---> Adder-cost: 891   maxlim: 493568   bits: 20/19
c ---[ 116]---> Adder-cost: 891   maxlim: 506880   bits: 20/19
c ---[ 114]---> Adder-cost: 843   maxlim: 236544   bits: 19/18
c ---[ 112]---> Adder-cost: 891   maxlim: 329728   bits: 20/19
c ---[ 110]---> Adder-cost: 939   maxlim: 701440   bits: 21/20
c ---[ 108]---> Adder-cost: 1095   maxlim: 13221888   bits: 25/24
c ---[ 106]---> Adder-cost: 891   maxlim: 332800   bits: 20/19
c ---[ 104]---> Adder-cost: 891   maxlim: 374784   bits: 20/19
c ---[ 102]---> Adder-cost: 1035   maxlim: 3759104   bits: 23/22
c ---[ 100]---> Adder-cost: 1035   maxlim: 2266112   bits: 23/22
c ---[  98]---> Adder-cost: 939   maxlim: 721920   bits: 21/20
c ---[  96]---> Adder-cost: 891   maxlim: 335872   bits: 20/19
c ---[  94]---> Adder-cost: 987   maxlim: 1721344   bits: 22/21
c ---[  92]---> Adder-cost: 987   maxlim: 1143808   bits: 22/21
c ---[  90]---> Adder-cost: 891   maxlim: 281600   bits: 20/19
c ---[  88]---> Adder-cost: 891   maxlim: 512000   bits: 20/19
c ---[  86]---> Adder-cost: 1035   maxlim: 2294784   bits: 23/22
c ---[  84]---> Adder-cost: 939   maxlim: 750592   bits: 21/20
c ---[  82]---> Adder-cost: 843   maxlim: 227328   bits: 19/18
c ---[  80]---> Adder-cost: 747   maxlim: 50176   bits: 17/16
c ---[  78]---> Adder-cost: 987   maxlim: 1499136   bits: 22/21
c ---[  76]---> Adder-cost: 843   maxlim: 227328   bits: 19/18
c ---[  74]---> Adder-cost: 1104   maxlim: 150048743   bits: 28/28
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:   33
c ---[  71]---> BDD-cost:   33
c ---[  70]---> BDD-cost:   33
c ---[  69]---> BDD-cost:   33
c ---[  68]---> BDD-cost:   33
c ---[  67]---> BDD-cost:   33
c ---[  66]---> BDD-cost:   33
c ---[  65]---> BDD-cost:   33
c ---[  64]---> BDD-cost:   33
c ---[  63]---> BDD-cost:   33
c ---[  62]---> BDD-cost:   33
c ---[  61]---> BDD-cost:   33
c ---[  60]---> BDD-cost:   33
c ---[  59]---> BDD-cost:   33
c ---[  58]---> BDD-cost:   33
c ---[  57]---> BDD-cost:   33
c ---[  56]---> BDD-cost:   33
c ---[  55]---> BDD-cost:   33
c ---[  54]---> BDD-cost:   33
c ---[  53]---> BDD-cost:   33
c ---[  52]---> BDD-cost:   33
c ---[  51]---> BDD-cost:   33
c ---[  50]---> BDD-cost:   33
c ---[  48]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  46]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  44]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  42]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  40]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  38]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  36]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  34]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  32]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  30]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  28]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  26]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  24]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  22]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  20]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  18]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  16]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  14]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  12]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[  10]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[   8]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[   6]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[   4]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[   2]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ---[   0]---> Adder-cost: 1960   maxlim: 79069134   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  651899  2325349 |  217299       0        0     nan |  0.000 % |
c |       100 |  651899  2325349 |  239028     100      305     3.0 | 13.317 % |
c |       250 |  651867  2325243 |  262931     246      773     3.1 | 13.321 % |
c |       475 |  651867  2325243 |  289224     471     1478     3.1 | 13.321 % |
c |       812 |  651811  2325057 |  318147     803     2650     3.3 | 13.329 % |
c |      1318 |  651787  2324977 |  349962    1307     4359     3.3 | 13.332 % |
c |      2077 |  651771  2324925 |  384958    2064     7054     3.4 | 13.334 % |
c |      3216 |  651682  2324628 |  423454    3191    11076     3.5 | 13.346 % |
c |      4924 |  651626  2324442 |  465799    4894    17215     3.5 | 13.353 % |
c |      7486 |  651498  2324018 |  512379    7443    27785     3.7 | 13.370 % |
c |     11330 |  651337  2323483 |  563617   11269    41701     3.7 | 13.392 % |
c |     17096 |  651199  2323027 |  619979   17014    62443     3.7 | 13.409 % |
c |     25745 |  651004  2322380 |  681977   25623    97565     3.8 | 13.433 % |
c |     38719 |  650862  2321906 |  750175   38559   152251     3.9 | 13.449 % |
c |     58180 |  650821  2321771 |  825192   58011   252817     4.4 | 13.453 % |
c |     87372 |  650778  2321626 |  907711   87181   424597     4.9 | 13.456 % |

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/28588/stat): 28588 (minisat+_script) R 28587 28588 6872 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793807245 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/28588/statm): 174 3 169 147 0 27 0
[pid=28588] 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=28589
New process pid=28590
New process pid=28591
execve syscall for /bin/sed executable
One traced child (pid=28590) 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=28591) exited with status: 0
One traced child (pid=28589) exited with status: 0
New process pid=28592
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-khb05250.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.95 0.90 1/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) T 28588 28588 6872 0 -1 0 7072 0 0 0 936 30 0 0 23 0 1 0 1793807249 32145408 6433 4294967295 134512640 135094434 3221224432 3221217340 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28592/statm): 7848 6433 145 145 0 7703 0
[pid=28592] vsize: 31392
Current children cumulated CPU time (s) 9.68
Current children cumulated vsize (Kb) 33516

[startup+20.0043 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13543 0 0 0 1875 60 0 0 25 0 1 0 1793807249 64716800 12838 4294967295 134512640 135094434 3221224432 3221223104 134556375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28592/statm): 15800 12838 145 145 0 15655 0
[pid=28592] vsize: 63200
Current children cumulated CPU time (s) 19.37
Current children cumulated vsize (Kb) 65324

[startup+30.006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13738 0 0 0 2871 61 0 0 25 0 1 0 1793807249 65511424 13033 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28592/statm): 15994 13033 145 145 0 15849 0
[pid=28592] vsize: 63976
Current children cumulated CPU time (s) 29.34
Current children cumulated vsize (Kb) 66100

[startup+40.0066 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13852 0 0 0 3868 62 0 0 25 0 1 0 1793807249 65998848 13147 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16113 13147 145 145 0 15968 0
[pid=28592] vsize: 64452
Current children cumulated CPU time (s) 39.32
Current children cumulated vsize (Kb) 66576

[startup+50.0084 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13941 0 0 0 4866 63 0 0 25 0 1 0 1793807249 66351104 13236 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16199 13236 145 145 0 16054 0
[pid=28592] vsize: 64796
Current children cumulated CPU time (s) 49.31
Current children cumulated vsize (Kb) 66920

[startup+60.0091 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 13996 0 0 0 5865 64 0 0 25 0 1 0 1793807249 66568192 13291 4294967295 134512640 135094434 3221224432 3221223108 134554883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16252 13291 145 145 0 16107 0
[pid=28592] vsize: 65008
Current children cumulated CPU time (s) 59.31
Current children cumulated vsize (Kb) 67132

[startup+70.0098 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14038 0 0 0 6865 64 0 0 25 0 1 0 1793807249 66760704 13333 4294967295 134512640 135094434 3221224432 3221223184 134559288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16299 13333 145 145 0 16154 0
[pid=28592] vsize: 65196
Current children cumulated CPU time (s) 69.31
Current children cumulated vsize (Kb) 67320

[startup+80.0105 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14063 0 0 0 7865 64 0 0 25 0 1 0 1793807249 66859008 13358 4294967295 134512640 135094434 3221224432 3221223044 134563057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16323 13358 145 145 0 16178 0
[pid=28592] vsize: 65292
Current children cumulated CPU time (s) 79.31
Current children cumulated vsize (Kb) 67416

[startup+90.0112 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14087 0 0 0 8865 64 0 0 25 0 1 0 1793807249 67014656 13382 4294967295 134512640 135094434 3221224432 3221223108 134554883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16361 13382 145 145 0 16216 0
[pid=28592] vsize: 65444
Current children cumulated CPU time (s) 89.31
Current children cumulated vsize (Kb) 67568

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14110 0 0 0 9865 64 0 0 25 0 1 0 1793807249 67096576 13405 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16381 13405 145 145 0 16236 0
[pid=28592] vsize: 65524
Current children cumulated CPU time (s) 99.31
Current children cumulated vsize (Kb) 67648

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14128 0 0 0 10865 64 0 0 25 0 1 0 1793807249 67166208 13423 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16398 13423 145 145 0 16253 0
[pid=28592] vsize: 65592
Current children cumulated CPU time (s) 109.31
Current children cumulated vsize (Kb) 67716

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14143 0 0 0 11864 65 0 0 25 0 1 0 1793807249 67223552 13438 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16412 13438 145 145 0 16267 0
[pid=28592] vsize: 65648
Current children cumulated CPU time (s) 119.31
Current children cumulated vsize (Kb) 67772

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14154 0 0 0 12864 65 0 0 25 0 1 0 1793807249 67264512 13449 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16422 13449 145 145 0 16277 0
[pid=28592] vsize: 65688
Current children cumulated CPU time (s) 129.31
Current children cumulated vsize (Kb) 67812

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14170 0 0 0 13864 65 0 0 25 0 1 0 1793807249 67321856 13465 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16436 13465 145 145 0 16291 0
[pid=28592] vsize: 65744
Current children cumulated CPU time (s) 139.31
Current children cumulated vsize (Kb) 67868

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14180 0 0 0 14865 65 0 0 25 0 1 0 1793807249 67358720 13475 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16445 13475 145 145 0 16300 0
[pid=28592] vsize: 65780
Current children cumulated CPU time (s) 149.32
Current children cumulated vsize (Kb) 67904

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14193 0 0 0 15864 65 0 0 25 0 1 0 1793807249 67407872 13488 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16457 13488 145 145 0 16312 0
[pid=28592] vsize: 65828
Current children cumulated CPU time (s) 159.31
Current children cumulated vsize (Kb) 67952

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14205 0 0 0 16865 65 0 0 25 0 1 0 1793807249 67448832 13500 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16467 13500 145 145 0 16322 0
[pid=28592] vsize: 65868
Current children cumulated CPU time (s) 169.32
Current children cumulated vsize (Kb) 67992

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14215 0 0 0 17864 65 0 0 25 0 1 0 1793807249 67481600 13510 4294967295 134512640 135094434 3221224432 3221223120 134554859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16475 13510 145 145 0 16330 0
[pid=28592] vsize: 65900
Current children cumulated CPU time (s) 179.31
Current children cumulated vsize (Kb) 68024

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14227 0 0 0 18864 65 0 0 25 0 1 0 1793807249 67526656 13522 4294967295 134512640 135094434 3221224432 3221223176 134559249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16486 13522 145 145 0 16341 0
[pid=28592] vsize: 65944
Current children cumulated CPU time (s) 189.31
Current children cumulated vsize (Kb) 68068

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14233 0 0 0 19864 65 0 0 25 0 1 0 1793807249 67547136 13528 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16491 13528 145 145 0 16346 0
[pid=28592] vsize: 65964
Current children cumulated CPU time (s) 199.31
Current children cumulated vsize (Kb) 68088

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14245 0 0 0 20864 65 0 0 25 0 1 0 1793807249 67592192 13540 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16502 13540 145 145 0 16357 0
[pid=28592] vsize: 66008
Current children cumulated CPU time (s) 209.31
Current children cumulated vsize (Kb) 68132

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14253 0 0 0 21864 65 0 0 25 0 1 0 1793807249 67620864 13548 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16509 13548 145 145 0 16364 0
[pid=28592] vsize: 66036
Current children cumulated CPU time (s) 219.31
Current children cumulated vsize (Kb) 68160

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14259 0 0 0 22865 65 0 0 25 0 1 0 1793807249 67645440 13554 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16515 13554 145 145 0 16370 0
[pid=28592] vsize: 66060
Current children cumulated CPU time (s) 229.32
Current children cumulated vsize (Kb) 68184

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14297 0 0 0 23865 66 0 0 25 0 1 0 1793807249 67919872 13592 4294967295 134512640 135094434 3221224432 3221223088 134561778 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16582 13592 145 145 0 16437 0
[pid=28592] vsize: 66328
Current children cumulated CPU time (s) 239.33
Current children cumulated vsize (Kb) 68452

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14297 0 0 0 24865 66 0 0 25 0 1 0 1793807249 67919872 13592 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16582 13592 145 145 0 16437 0
[pid=28592] vsize: 66328
Current children cumulated CPU time (s) 249.33
Current children cumulated vsize (Kb) 68452

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14298 0 0 0 25865 66 0 0 25 0 1 0 1793807249 67919872 13593 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16582 13593 145 145 0 16437 0
[pid=28592] vsize: 66328
Current children cumulated CPU time (s) 259.33
Current children cumulated vsize (Kb) 68452

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14299 0 0 0 26865 66 0 0 25 0 1 0 1793807249 67919872 13594 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16582 13594 145 145 0 16437 0
[pid=28592] vsize: 66328
Current children cumulated CPU time (s) 269.33
Current children cumulated vsize (Kb) 68452

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14304 0 0 0 27866 66 0 0 25 0 1 0 1793807249 67936256 13599 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16586 13599 145 145 0 16441 0
[pid=28592] vsize: 66344
Current children cumulated CPU time (s) 279.34
Current children cumulated vsize (Kb) 68468

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14312 0 0 0 28866 66 0 0 25 0 1 0 1793807249 67969024 13607 4294967295 134512640 135094434 3221224432 3221223084 134561606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16594 13607 145 145 0 16449 0
[pid=28592] vsize: 66376
Current children cumulated CPU time (s) 289.34
Current children cumulated vsize (Kb) 68500

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14320 0 0 0 29866 66 0 0 25 0 1 0 1793807249 67997696 13615 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16601 13615 145 145 0 16456 0
[pid=28592] vsize: 66404
Current children cumulated CPU time (s) 299.34
Current children cumulated vsize (Kb) 68528

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14330 0 0 0 30865 66 0 0 25 0 1 0 1793807249 68034560 13625 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16610 13625 145 145 0 16465 0
[pid=28592] vsize: 66440
Current children cumulated CPU time (s) 309.33
Current children cumulated vsize (Kb) 68564

[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14343 0 0 0 31865 66 0 0 25 0 1 0 1793807249 68083712 13638 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16622 13638 145 145 0 16477 0
[pid=28592] vsize: 66488
Current children cumulated CPU time (s) 319.33
Current children cumulated vsize (Kb) 68612

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14356 0 0 0 32865 66 0 0 25 0 1 0 1793807249 68132864 13651 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16634 13651 145 145 0 16489 0
[pid=28592] vsize: 66536
Current children cumulated CPU time (s) 329.33
Current children cumulated vsize (Kb) 68660

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14364 0 0 0 33865 66 0 0 25 0 1 0 1793807249 68161536 13659 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16641 13659 145 145 0 16496 0
[pid=28592] vsize: 66564
Current children cumulated CPU time (s) 339.33
Current children cumulated vsize (Kb) 68688

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14370 0 0 0 34865 67 0 0 25 0 1 0 1793807249 68182016 13665 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16646 13665 145 145 0 16501 0
[pid=28592] vsize: 66584
Current children cumulated CPU time (s) 349.34
Current children cumulated vsize (Kb) 68708

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14393 0 0 0 35865 67 0 0 25 0 1 0 1793807249 68268032 13688 4294967295 134512640 135094434 3221224432 3221223044 134563012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16667 13688 145 145 0 16522 0
[pid=28592] vsize: 66668
Current children cumulated CPU time (s) 359.34
Current children cumulated vsize (Kb) 68792

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14407 0 0 0 36865 67 0 0 25 0 1 0 1793807249 68321280 13702 4294967295 134512640 135094434 3221224432 3221223088 134550405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16680 13702 145 145 0 16535 0
[pid=28592] vsize: 66720
Current children cumulated CPU time (s) 369.34
Current children cumulated vsize (Kb) 68844

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14412 0 0 0 37865 67 0 0 25 0 1 0 1793807249 68341760 13707 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16685 13707 145 145 0 16540 0
[pid=28592] vsize: 66740
Current children cumulated CPU time (s) 379.34
Current children cumulated vsize (Kb) 68864

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14428 0 0 0 38865 67 0 0 25 0 1 0 1793807249 68403200 13723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16700 13723 145 145 0 16555 0
[pid=28592] vsize: 66800
Current children cumulated CPU time (s) 389.34
Current children cumulated vsize (Kb) 68924

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14447 0 0 0 39865 67 0 0 25 0 1 0 1793807249 68472832 13742 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16717 13742 145 145 0 16572 0
[pid=28592] vsize: 66868
Current children cumulated CPU time (s) 399.34
Current children cumulated vsize (Kb) 68992

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14454 0 0 0 40865 67 0 0 25 0 1 0 1793807249 68497408 13749 4294967295 134512640 135094434 3221224432 3221223072 134562090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16723 13749 145 145 0 16578 0
[pid=28592] vsize: 66892
Current children cumulated CPU time (s) 409.34
Current children cumulated vsize (Kb) 69016

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14469 0 0 0 41865 67 0 0 25 0 1 0 1793807249 68550656 13764 4294967295 134512640 135094434 3221224432 3221223072 134562048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16736 13764 145 145 0 16591 0
[pid=28592] vsize: 66944
Current children cumulated CPU time (s) 419.34
Current children cumulated vsize (Kb) 69068

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14473 0 0 0 42865 67 0 0 25 0 1 0 1793807249 68567040 13768 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16740 13768 145 145 0 16595 0
[pid=28592] vsize: 66960
Current children cumulated CPU time (s) 429.34
Current children cumulated vsize (Kb) 69084

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14489 0 0 0 43865 67 0 0 25 0 1 0 1793807249 68628480 13784 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16755 13784 145 145 0 16610 0
[pid=28592] vsize: 67020
Current children cumulated CPU time (s) 439.34
Current children cumulated vsize (Kb) 69144

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14497 0 0 0 44865 67 0 0 25 0 1 0 1793807249 68657152 13792 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16762 13792 145 145 0 16617 0
[pid=28592] vsize: 67048
Current children cumulated CPU time (s) 449.34
Current children cumulated vsize (Kb) 69172

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14513 0 0 0 45865 68 0 0 25 0 1 0 1793807249 68718592 13808 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16777 13808 145 145 0 16632 0
[pid=28592] vsize: 67108
Current children cumulated CPU time (s) 459.35
Current children cumulated vsize (Kb) 69232

[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14520 0 0 0 46865 68 0 0 25 0 1 0 1793807249 68743168 13815 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16783 13815 145 145 0 16638 0
[pid=28592] vsize: 67132
Current children cumulated CPU time (s) 469.35
Current children cumulated vsize (Kb) 69256

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14536 0 0 0 47865 68 0 0 25 0 1 0 1793807249 68804608 13831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16798 13831 145 145 0 16653 0
[pid=28592] vsize: 67192
Current children cumulated CPU time (s) 479.35
Current children cumulated vsize (Kb) 69316

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14549 0 0 0 48865 68 0 0 25 0 1 0 1793807249 68853760 13844 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16810 13844 145 145 0 16665 0
[pid=28592] vsize: 67240
Current children cumulated CPU time (s) 489.35
Current children cumulated vsize (Kb) 69364

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14562 0 0 0 49864 68 0 0 25 0 1 0 1793807249 68902912 13857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28592/statm): 16822 13857 145 145 0 16677 0
[pid=28592] vsize: 67288
Current children cumulated CPU time (s) 499.34
Current children cumulated vsize (Kb) 69412

[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14578 0 0 0 50864 68 0 0 25 0 1 0 1793807249 68964352 13873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16837 13873 145 145 0 16692 0
[pid=28592] vsize: 67348
Current children cumulated CPU time (s) 509.34
Current children cumulated vsize (Kb) 69472

[startup+520.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14593 0 0 0 51864 68 0 0 25 0 1 0 1793807249 69021696 13888 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16851 13888 145 145 0 16706 0
[pid=28592] vsize: 67404
Current children cumulated CPU time (s) 519.34
Current children cumulated vsize (Kb) 69528

[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14601 0 0 0 52864 68 0 0 25 0 1 0 1793807249 69050368 13896 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16858 13896 145 145 0 16713 0
[pid=28592] vsize: 67432
Current children cumulated CPU time (s) 529.34
Current children cumulated vsize (Kb) 69556

[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14615 0 0 0 53864 68 0 0 25 0 1 0 1793807249 69103616 13910 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16871 13910 145 145 0 16726 0
[pid=28592] vsize: 67484
Current children cumulated CPU time (s) 539.34
Current children cumulated vsize (Kb) 69608

[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14624 0 0 0 54864 69 0 0 25 0 1 0 1793807249 69140480 13919 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16880 13919 145 145 0 16735 0
[pid=28592] vsize: 67520
Current children cumulated CPU time (s) 549.35
Current children cumulated vsize (Kb) 69644

[startup+560.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14635 0 0 0 55864 69 0 0 25 0 1 0 1793807249 69181440 13930 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16890 13930 145 145 0 16745 0
[pid=28592] vsize: 67560
Current children cumulated CPU time (s) 559.35
Current children cumulated vsize (Kb) 69684

[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14645 0 0 0 56864 69 0 0 25 0 1 0 1793807249 69218304 13940 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16899 13940 145 145 0 16754 0
[pid=28592] vsize: 67596
Current children cumulated CPU time (s) 569.35
Current children cumulated vsize (Kb) 69720

[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14657 0 0 0 57864 69 0 0 25 0 1 0 1793807249 69525504 13952 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16974 13952 145 145 0 16829 0
[pid=28592] vsize: 67896
Current children cumulated CPU time (s) 579.35
Current children cumulated vsize (Kb) 70020

[startup+590.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14672 0 0 0 58864 69 0 0 25 0 1 0 1793807249 69582848 13967 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 16988 13967 145 145 0 16843 0
[pid=28592] vsize: 67952
Current children cumulated CPU time (s) 589.35
Current children cumulated vsize (Kb) 70076

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14685 0 0 0 59864 69 0 0 25 0 1 0 1793807249 69632000 13980 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17000 13980 145 145 0 16855 0
[pid=28592] vsize: 68000
Current children cumulated CPU time (s) 599.35
Current children cumulated vsize (Kb) 70124

[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14694 0 0 0 60864 70 0 0 25 0 1 0 1793807249 69664768 13989 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17008 13989 145 145 0 16863 0
[pid=28592] vsize: 68032
Current children cumulated CPU time (s) 609.36
Current children cumulated vsize (Kb) 70156

[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14703 0 0 0 61864 70 0 0 25 0 1 0 1793807249 69701632 13998 4294967295 134512640 135094434 3221224432 3221223088 134561763 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17017 13998 145 145 0 16872 0
[pid=28592] vsize: 68068
Current children cumulated CPU time (s) 619.36
Current children cumulated vsize (Kb) 70192

[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14712 0 0 0 62864 70 0 0 25 0 1 0 1793807249 69734400 14007 4294967295 134512640 135094434 3221224432 3221223056 134562985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17025 14007 145 145 0 16880 0
[pid=28592] vsize: 68100
Current children cumulated CPU time (s) 629.36
Current children cumulated vsize (Kb) 70224

[startup+640.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14727 0 0 0 63864 70 0 0 25 0 1 0 1793807249 69791744 14022 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17039 14022 145 145 0 16894 0
[pid=28592] vsize: 68156
Current children cumulated CPU time (s) 639.36
Current children cumulated vsize (Kb) 70280

[startup+650.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14746 0 0 0 64864 70 0 0 25 0 1 0 1793807249 69865472 14041 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17057 14041 145 145 0 16912 0
[pid=28592] vsize: 68228
Current children cumulated CPU time (s) 649.36
Current children cumulated vsize (Kb) 70352

[startup+660.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14760 0 0 0 65864 70 0 0 25 0 1 0 1793807249 69918720 14055 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17070 14055 145 145 0 16925 0
[pid=28592] vsize: 68280
Current children cumulated CPU time (s) 659.36
Current children cumulated vsize (Kb) 70404

[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14777 0 0 0 66864 70 0 0 25 0 1 0 1793807249 69984256 14072 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17086 14072 145 145 0 16941 0
[pid=28592] vsize: 68344
Current children cumulated CPU time (s) 669.36
Current children cumulated vsize (Kb) 70468

[startup+680.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14791 0 0 0 67864 70 0 0 25 0 1 0 1793807249 70037504 14086 4294967295 134512640 135094434 3221224432 3221223072 134562115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17099 14086 145 145 0 16954 0
[pid=28592] vsize: 68396
Current children cumulated CPU time (s) 679.36
Current children cumulated vsize (Kb) 70520

[startup+690.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14801 0 0 0 68864 70 0 0 25 0 1 0 1793807249 70074368 14096 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17108 14096 145 145 0 16963 0
[pid=28592] vsize: 68432
Current children cumulated CPU time (s) 689.36
Current children cumulated vsize (Kb) 70556

[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14814 0 0 0 69864 70 0 0 25 0 1 0 1793807249 70123520 14109 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17120 14109 145 145 0 16975 0
[pid=28592] vsize: 68480
Current children cumulated CPU time (s) 699.36
Current children cumulated vsize (Kb) 70604

[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14828 0 0 0 70864 70 0 0 25 0 1 0 1793807249 70176768 14123 4294967295 134512640 135094434 3221224432 3221223088 134561660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17133 14123 145 145 0 16988 0
[pid=28592] vsize: 68532
Current children cumulated CPU time (s) 709.36
Current children cumulated vsize (Kb) 70656

[startup+720.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14841 0 0 0 71864 70 0 0 25 0 1 0 1793807249 70225920 14136 4294967295 134512640 135094434 3221224432 3221223136 134554526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17145 14136 145 145 0 17000 0
[pid=28592] vsize: 68580
Current children cumulated CPU time (s) 719.36
Current children cumulated vsize (Kb) 70704

[startup+730.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14850 0 0 0 72864 71 0 0 25 0 1 0 1793807249 70262784 14145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17154 14145 145 145 0 17009 0
[pid=28592] vsize: 68616
Current children cumulated CPU time (s) 729.37
Current children cumulated vsize (Kb) 70740

[startup+740.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14865 0 0 0 73864 71 0 0 25 0 1 0 1793807249 70320128 14160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17168 14160 145 145 0 17023 0
[pid=28592] vsize: 68672
Current children cumulated CPU time (s) 739.37
Current children cumulated vsize (Kb) 70796

[startup+750.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14875 0 0 0 74864 71 0 0 25 0 1 0 1793807249 70356992 14170 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17177 14170 145 145 0 17032 0
[pid=28592] vsize: 68708
Current children cumulated CPU time (s) 749.37
Current children cumulated vsize (Kb) 70832

[startup+760.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14889 0 0 0 75864 71 0 0 25 0 1 0 1793807249 70410240 14184 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17190 14184 145 145 0 17045 0
[pid=28592] vsize: 68760
Current children cumulated CPU time (s) 759.37
Current children cumulated vsize (Kb) 70884

[startup+770.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14903 0 0 0 76864 71 0 0 25 0 1 0 1793807249 70463488 14198 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17203 14198 145 145 0 17058 0
[pid=28592] vsize: 68812
Current children cumulated CPU time (s) 769.37
Current children cumulated vsize (Kb) 70936

[startup+780.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14915 0 0 0 77864 71 0 0 25 0 1 0 1793807249 70508544 14210 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17214 14210 145 145 0 17069 0
[pid=28592] vsize: 68856
Current children cumulated CPU time (s) 779.37
Current children cumulated vsize (Kb) 70980

[startup+790.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14922 0 0 0 78864 71 0 0 25 0 1 0 1793807249 70537216 14217 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17221 14217 145 145 0 17076 0
[pid=28592] vsize: 68884
Current children cumulated CPU time (s) 789.37
Current children cumulated vsize (Kb) 71008

[startup+800.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14934 0 0 0 79864 71 0 0 25 0 1 0 1793807249 70582272 14229 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17232 14229 145 145 0 17087 0
[pid=28592] vsize: 68928
Current children cumulated CPU time (s) 799.37
Current children cumulated vsize (Kb) 71052

[startup+810.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14946 0 0 0 80865 71 0 0 25 0 1 0 1793807249 70627328 14241 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17243 14241 145 145 0 17098 0
[pid=28592] vsize: 68972
Current children cumulated CPU time (s) 809.38
Current children cumulated vsize (Kb) 71096

[startup+820.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14958 0 0 0 81864 71 0 0 25 0 1 0 1793807249 70672384 14253 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28592/statm): 17254 14253 145 145 0 17109 0
[pid=28592] vsize: 69016
Current children cumulated CPU time (s) 819.37
Current children cumulated vsize (Kb) 71140

[startup+830.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14970 0 0 0 82863 72 0 0 25 0 1 0 1793807249 70717440 14265 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28592/statm): 17265 14265 145 145 0 17120 0
[pid=28592] vsize: 69060
Current children cumulated CPU time (s) 829.37
Current children cumulated vsize (Kb) 71184

[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14981 0 0 0 83863 72 0 0 25 0 1 0 1793807249 70758400 14276 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17275 14276 145 145 0 17130 0
[pid=28592] vsize: 69100
Current children cumulated CPU time (s) 839.37
Current children cumulated vsize (Kb) 71224

[startup+850.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 14994 0 0 0 84863 72 0 0 25 0 1 0 1793807249 70807552 14289 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17287 14289 145 145 0 17142 0
[pid=28592] vsize: 69148
Current children cumulated CPU time (s) 849.37
Current children cumulated vsize (Kb) 71272

[startup+860.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15004 0 0 0 85863 72 0 0 25 0 1 0 1793807249 70848512 14299 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17297 14299 145 145 0 17152 0
[pid=28592] vsize: 69188
Current children cumulated CPU time (s) 859.37
Current children cumulated vsize (Kb) 71312

[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15020 0 0 0 86863 72 0 0 25 0 1 0 1793807249 70909952 14315 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17312 14315 145 145 0 17167 0
[pid=28592] vsize: 69248
Current children cumulated CPU time (s) 869.37
Current children cumulated vsize (Kb) 71372

[startup+880.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15030 0 0 0 87862 73 0 0 25 0 1 0 1793807249 70946816 14325 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17321 14325 145 145 0 17176 0
[pid=28592] vsize: 69284
Current children cumulated CPU time (s) 879.37
Current children cumulated vsize (Kb) 71408

[startup+890.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15046 0 0 0 88862 73 0 0 25 0 1 0 1793807249 71008256 14341 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17336 14341 145 145 0 17191 0
[pid=28592] vsize: 69344
Current children cumulated CPU time (s) 889.37
Current children cumulated vsize (Kb) 71468

[startup+900.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15063 0 0 0 89862 73 0 0 25 0 1 0 1793807249 71069696 14358 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17351 14358 145 145 0 17206 0
[pid=28592] vsize: 69404
Current children cumulated CPU time (s) 899.37
Current children cumulated vsize (Kb) 71528

[startup+910.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15083 0 0 0 90862 73 0 0 25 0 1 0 1793807249 71143424 14378 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17369 14378 145 145 0 17224 0
[pid=28592] vsize: 69476
Current children cumulated CPU time (s) 909.37
Current children cumulated vsize (Kb) 71600

[startup+920.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15096 0 0 0 91862 73 0 0 25 0 1 0 1793807249 71192576 14391 4294967295 134512640 135094434 3221224432 3221223084 134561520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17381 14391 145 145 0 17236 0
[pid=28592] vsize: 69524
Current children cumulated CPU time (s) 919.37
Current children cumulated vsize (Kb) 71648

[startup+930.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15117 0 0 0 92861 73 0 0 25 0 1 0 1793807249 71274496 14412 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17401 14412 145 145 0 17256 0
[pid=28592] vsize: 69604
Current children cumulated CPU time (s) 929.36
Current children cumulated vsize (Kb) 71728

[startup+940.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15128 0 0 0 93861 74 0 0 25 0 1 0 1793807249 71311360 14423 4294967295 134512640 135094434 3221224432 3221223088 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17410 14423 145 145 0 17265 0
[pid=28592] vsize: 69640
Current children cumulated CPU time (s) 939.37
Current children cumulated vsize (Kb) 71764

[startup+950.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15163 0 0 0 94861 74 0 0 25 0 1 0 1793807249 71450624 14458 4294967295 134512640 135094434 3221224432 3221223088 134557768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17444 14458 145 145 0 17299 0
[pid=28592] vsize: 69776
Current children cumulated CPU time (s) 949.37
Current children cumulated vsize (Kb) 71900

[startup+960.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15176 0 0 0 95861 74 0 0 25 0 1 0 1793807249 71499776 14471 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17456 14471 145 145 0 17311 0
[pid=28592] vsize: 69824
Current children cumulated CPU time (s) 959.37
Current children cumulated vsize (Kb) 71948

[startup+970.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15186 0 0 0 96861 74 0 0 25 0 1 0 1793807249 71536640 14481 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17465 14481 145 145 0 17320 0
[pid=28592] vsize: 69860
Current children cumulated CPU time (s) 969.37
Current children cumulated vsize (Kb) 71984

[startup+980.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15219 0 0 0 97861 74 0 0 25 0 1 0 1793807249 71667712 14514 4294967295 134512640 135094434 3221224432 3221223044 134563137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17497 14514 145 145 0 17352 0
[pid=28592] vsize: 69988
Current children cumulated CPU time (s) 979.37
Current children cumulated vsize (Kb) 72112

[startup+990.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15235 0 0 0 98861 74 0 0 25 0 1 0 1793807249 71720960 14530 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17510 14530 145 145 0 17365 0
[pid=28592] vsize: 70040
Current children cumulated CPU time (s) 989.37
Current children cumulated vsize (Kb) 72164

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15263 0 0 0 99861 74 0 0 25 0 1 0 1793807249 71827456 14558 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17536 14558 145 145 0 17391 0
[pid=28592] vsize: 70144
Current children cumulated CPU time (s) 999.37
Current children cumulated vsize (Kb) 72268

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15283 0 0 0 100861 75 0 0 25 0 1 0 1793807249 71905280 14578 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17555 14578 145 145 0 17410 0
[pid=28592] vsize: 70220
Current children cumulated CPU time (s) 1009.38
Current children cumulated vsize (Kb) 72344

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15294 0 0 0 101861 75 0 0 25 0 1 0 1793807249 71950336 14589 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17566 14589 145 145 0 17421 0
[pid=28592] vsize: 70264
Current children cumulated CPU time (s) 1019.38
Current children cumulated vsize (Kb) 72388

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15306 0 0 0 102861 75 0 0 25 0 1 0 1793807249 71995392 14601 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17577 14601 145 145 0 17432 0
[pid=28592] vsize: 70308
Current children cumulated CPU time (s) 1029.38
Current children cumulated vsize (Kb) 72432

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15328 0 0 0 103861 75 0 0 25 0 1 0 1793807249 72081408 14623 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17598 14623 145 145 0 17453 0
[pid=28592] vsize: 70392
Current children cumulated CPU time (s) 1039.38
Current children cumulated vsize (Kb) 72516

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15350 0 0 0 104860 75 0 0 25 0 1 0 1793807249 72163328 14645 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17618 14645 145 145 0 17473 0
[pid=28592] vsize: 70472
Current children cumulated CPU time (s) 1049.37
Current children cumulated vsize (Kb) 72596

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15370 0 0 0 105860 75 0 0 25 0 1 0 1793807249 72237056 14665 4294967295 134512640 135094434 3221224432 3221223136 134554398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17636 14665 145 145 0 17491 0
[pid=28592] vsize: 70544
Current children cumulated CPU time (s) 1059.37
Current children cumulated vsize (Kb) 72668

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15386 0 0 0 106860 75 0 0 25 0 1 0 1793807249 72298496 14681 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17651 14681 145 145 0 17506 0
[pid=28592] vsize: 70604
Current children cumulated CPU time (s) 1069.37
Current children cumulated vsize (Kb) 72728

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15410 0 0 0 107860 76 0 0 25 0 1 0 1793807249 72392704 14705 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17674 14705 145 145 0 17529 0
[pid=28592] vsize: 70696
Current children cumulated CPU time (s) 1079.38
Current children cumulated vsize (Kb) 72820

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15427 0 0 0 108860 76 0 0 25 0 1 0 1793807249 72458240 14722 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17690 14722 145 145 0 17545 0
[pid=28592] vsize: 70760
Current children cumulated CPU time (s) 1089.38
Current children cumulated vsize (Kb) 72884

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15442 0 0 0 109859 76 0 0 25 0 1 0 1793807249 72515584 14737 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17704 14737 145 145 0 17559 0
[pid=28592] vsize: 70816
Current children cumulated CPU time (s) 1099.37
Current children cumulated vsize (Kb) 72940

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15458 0 0 0 110859 76 0 0 25 0 1 0 1793807249 72577024 14753 4294967295 134512640 135094434 3221224432 3221223100 134550364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17719 14753 145 145 0 17574 0
[pid=28592] vsize: 70876
Current children cumulated CPU time (s) 1109.37
Current children cumulated vsize (Kb) 73000

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15468 0 0 0 111859 76 0 0 25 0 1 0 1793807249 72617984 14763 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17729 14763 145 145 0 17584 0
[pid=28592] vsize: 70916
Current children cumulated CPU time (s) 1119.37
Current children cumulated vsize (Kb) 73040

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15478 0 0 0 112860 76 0 0 25 0 1 0 1793807249 72654848 14773 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17738 14773 145 145 0 17593 0
[pid=28592] vsize: 70952
Current children cumulated CPU time (s) 1129.38
Current children cumulated vsize (Kb) 73076

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15499 0 0 0 113859 76 0 0 25 0 1 0 1793807249 72736768 14794 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17758 14794 145 145 0 17613 0
[pid=28592] vsize: 71032
Current children cumulated CPU time (s) 1139.37
Current children cumulated vsize (Kb) 73156

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15507 0 0 0 114859 76 0 0 25 0 1 0 1793807249 72765440 14802 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17765 14802 145 145 0 17620 0
[pid=28592] vsize: 71060
Current children cumulated CPU time (s) 1149.37
Current children cumulated vsize (Kb) 73184

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15516 0 0 0 115860 76 0 0 25 0 1 0 1793807249 72798208 14811 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17773 14811 145 145 0 17628 0
[pid=28592] vsize: 71092
Current children cumulated CPU time (s) 1159.38
Current children cumulated vsize (Kb) 73216

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15535 0 0 0 116859 76 0 0 25 0 1 0 1793807249 72871936 14830 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17791 14830 145 145 0 17646 0
[pid=28592] vsize: 71164
Current children cumulated CPU time (s) 1169.37
Current children cumulated vsize (Kb) 73288

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15546 0 0 0 117859 76 0 0 25 0 1 0 1793807249 72912896 14841 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17801 14841 145 145 0 17656 0
[pid=28592] vsize: 71204
Current children cumulated CPU time (s) 1179.37
Current children cumulated vsize (Kb) 73328

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15562 0 0 0 118859 77 0 0 25 0 1 0 1793807249 72974336 14857 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17816 14857 145 145 0 17671 0
[pid=28592] vsize: 71264
Current children cumulated CPU time (s) 1189.38
Current children cumulated vsize (Kb) 73388

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15590 0 0 0 119859 77 0 0 25 0 1 0 1793807249 73084928 14885 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17843 14885 145 145 0 17698 0
[pid=28592] vsize: 71372
Current children cumulated CPU time (s) 1199.38
Current children cumulated vsize (Kb) 73496

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15623 0 0 0 120859 77 0 0 25 0 1 0 1793807249 73211904 14918 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17874 14918 145 145 0 17729 0
[pid=28592] vsize: 71496
Current children cumulated CPU time (s) 1209.38
Current children cumulated vsize (Kb) 73620



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28592
Raw data (/proc/28588/stat): 28588 (minisat+_script) S 28587 28588 6872 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1793807245 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28588/statm): 531 226 485 147 0 384 0
[pid=28588] vsize: 2124
Raw data (/proc/28592/stat): 28592 (minisat+_64-bit) R 28588 28588 6872 0 -1 0 15623 0 0 0 120859 77 0 0 25 0 1 0 1793807249 73211904 14918 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28592/statm): 17874 14918 145 145 0 17729 0
[pid=28592] vsize: 71496
Current children cumulated CPU time (s) 1209.38
Current children cumulated vsize (Kb) 73620

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

Child status: 0
Real time (s): 1210.12
CPU time (s): 1209.4
CPU user time (s): 1208.59
CPU system time (s): 0.806877
CPU usage (%): 99.9403
Max. virtual memory (cumulated for all children) (Kb): 73620

Verifier Data

ERROR: no interpretation found !