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/miplib/normalized-mps-v2-20-10-khb05250.opb
MD5SUM18d2c1f575fe90b4288795c634aa1a5b
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 benchmark1205.48
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 3860

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        861492 kB
Buffers:         36936 kB
Cached:         108560 kB
SwapCached:        228 kB
Active:          71232 kB
Inactive:        77180 kB
HighTotal:      131008 kB
HighFree:        53424 kB
LowTotal:       903652 kB
LowFree:        808068 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18912 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:27:06 (client local time) WITH STATUS 0 IN 1209.48 SECONDS
stats: 2858 7 1209.48 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/2745/stat): 2745 (minisat+_script) R 2744 2745 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788336612 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/2745/statm): 174 3 169 147 0 27 0
[pid=2745] 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=2746
New process pid=2747
New process pid=2748
execve syscall for /bin/sed executable
One traced child (pid=2747) 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=2748) exited with status: 0
One traced child (pid=2746) exited with status: 0
New process pid=2749
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-khb05250.opb

[startup+10.0039 s]
Raw data (loadavg): 1.11 1.09 1.06 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 6840 0 0 0 939 31 0 0 24 0 1 0 1788336617 31391744 6201 4294967295 134512640 135094434 3221224432 3221221984 134780516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2749/statm): 7664 6201 145 145 0 7519 0
[pid=2749] vsize: 30656
Current children cumulated CPU time (s) 9.72
Current children cumulated vsize (Kb) 32780

[startup+20.0045 s]
Raw data (loadavg): 1.09 1.09 1.06 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13538 0 0 0 1874 63 0 0 25 0 1 0 1788336617 64696320 12833 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2749/statm): 15795 12833 145 145 0 15650 0
[pid=2749] vsize: 63180
Current children cumulated CPU time (s) 19.39
Current children cumulated vsize (Kb) 65304

[startup+30.0061 s]
Raw data (loadavg): 1.08 1.09 1.06 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13735 0 0 0 2870 65 0 0 25 0 1 0 1788336617 65499136 13030 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 15991 13030 145 145 0 15846 0
[pid=2749] vsize: 63964
Current children cumulated CPU time (s) 29.37
Current children cumulated vsize (Kb) 66088

[startup+40.0066 s]
Raw data (loadavg): 1.06 1.08 1.06 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13850 0 0 0 3869 66 0 0 25 0 1 0 1788336617 65990656 13145 4294967295 134512640 135094434 3221224432 3221223044 134563148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16111 13145 145 145 0 15966 0
[pid=2749] vsize: 64444
Current children cumulated CPU time (s) 39.37
Current children cumulated vsize (Kb) 66568

[startup+50.0072 s]
Raw data (loadavg): 1.05 1.08 1.06 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13938 0 0 0 4868 66 0 0 25 0 1 0 1788336617 66338816 13233 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16196 13233 145 145 0 16051 0
[pid=2749] vsize: 64784
Current children cumulated CPU time (s) 49.36
Current children cumulated vsize (Kb) 66908

[startup+60.0077 s]
Raw data (loadavg): 1.05 1.08 1.06 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 13994 0 0 0 5867 66 0 0 25 0 1 0 1788336617 66560000 13289 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16250 13289 145 145 0 16105 0
[pid=2749] vsize: 65000
Current children cumulated CPU time (s) 59.35
Current children cumulated vsize (Kb) 67124

[startup+70.0083 s]
Raw data (loadavg): 1.04 1.07 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14037 0 0 0 6866 66 0 0 25 0 1 0 1788336617 66756608 13332 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16298 13332 145 145 0 16153 0
[pid=2749] vsize: 65192
Current children cumulated CPU time (s) 69.34
Current children cumulated vsize (Kb) 67316

[startup+80.0089 s]
Raw data (loadavg): 1.03 1.07 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14062 0 0 0 7866 67 0 0 25 0 1 0 1788336617 66854912 13357 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16322 13357 145 145 0 16177 0
[pid=2749] vsize: 65288
Current children cumulated CPU time (s) 79.35
Current children cumulated vsize (Kb) 67412

[startup+90.0094 s]
Raw data (loadavg): 1.03 1.07 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14085 0 0 0 8865 67 0 0 25 0 1 0 1788336617 67006464 13380 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16359 13380 145 145 0 16214 0
[pid=2749] vsize: 65436
Current children cumulated CPU time (s) 89.34
Current children cumulated vsize (Kb) 67560

[startup+100.009 s]
Raw data (loadavg): 1.02 1.07 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14108 0 0 0 9865 67 0 0 25 0 1 0 1788336617 67088384 13403 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16379 13403 145 145 0 16234 0
[pid=2749] vsize: 65516
Current children cumulated CPU time (s) 99.34
Current children cumulated vsize (Kb) 67640

[startup+110.01 s]
Raw data (loadavg): 1.02 1.06 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14127 0 0 0 10865 68 0 0 25 0 1 0 1788336617 67162112 13422 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16397 13422 145 145 0 16252 0
[pid=2749] vsize: 65588
Current children cumulated CPU time (s) 109.35
Current children cumulated vsize (Kb) 67712

[startup+120.01 s]
Raw data (loadavg): 1.02 1.06 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14142 0 0 0 11864 68 0 0 25 0 1 0 1788336617 67219456 13437 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16411 13437 145 145 0 16266 0
[pid=2749] vsize: 65644
Current children cumulated CPU time (s) 119.34
Current children cumulated vsize (Kb) 67768

[startup+130.011 s]
Raw data (loadavg): 1.01 1.06 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14153 0 0 0 12865 68 0 0 25 0 1 0 1788336617 67260416 13448 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16421 13448 145 145 0 16276 0
[pid=2749] vsize: 65684
Current children cumulated CPU time (s) 129.35
Current children cumulated vsize (Kb) 67808

[startup+140.011 s]
Raw data (loadavg): 1.01 1.06 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14168 0 0 0 13865 68 0 0 25 0 1 0 1788336617 67313664 13463 4294967295 134512640 135094434 3221224432 3221223072 134562082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16434 13463 145 145 0 16289 0
[pid=2749] vsize: 65736
Current children cumulated CPU time (s) 139.35
Current children cumulated vsize (Kb) 67860

[startup+150.012 s]
Raw data (loadavg): 1.01 1.05 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14179 0 0 0 14865 68 0 0 25 0 1 0 1788336617 67354624 13474 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16444 13474 145 145 0 16299 0
[pid=2749] vsize: 65776
Current children cumulated CPU time (s) 149.35
Current children cumulated vsize (Kb) 67900

[startup+160.012 s]
Raw data (loadavg): 1.01 1.05 1.05 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14188 0 0 0 15865 68 0 0 25 0 1 0 1788336617 67391488 13483 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16453 13483 145 145 0 16308 0
[pid=2749] vsize: 65812
Current children cumulated CPU time (s) 159.35
Current children cumulated vsize (Kb) 67936

[startup+170.013 s]
Raw data (loadavg): 1.00 1.05 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14203 0 0 0 16865 68 0 0 25 0 1 0 1788336617 67444736 13498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16466 13498 145 145 0 16321 0
[pid=2749] vsize: 65864
Current children cumulated CPU time (s) 169.35
Current children cumulated vsize (Kb) 67988

[startup+180.013 s]
Raw data (loadavg): 1.00 1.05 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14214 0 0 0 17865 68 0 0 25 0 1 0 1788336617 67477504 13509 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16474 13509 145 145 0 16329 0
[pid=2749] vsize: 65896
Current children cumulated CPU time (s) 179.35
Current children cumulated vsize (Kb) 68020

[startup+190.014 s]
Raw data (loadavg): 1.00 1.05 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14225 0 0 0 18865 68 0 0 25 0 1 0 1788336617 67518464 13520 4294967295 134512640 135094434 3221224432 3221223072 134562113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16484 13520 145 145 0 16339 0
[pid=2749] vsize: 65936
Current children cumulated CPU time (s) 189.35
Current children cumulated vsize (Kb) 68060

[startup+200.014 s]
Raw data (loadavg): 1.00 1.04 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14233 0 0 0 19865 68 0 0 25 0 1 0 1788336617 67547136 13528 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16491 13528 145 145 0 16346 0
[pid=2749] vsize: 65964
Current children cumulated CPU time (s) 199.35
Current children cumulated vsize (Kb) 68088

[startup+210.014 s]
Raw data (loadavg): 1.00 1.04 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14243 0 0 0 20865 68 0 0 25 0 1 0 1788336617 67584000 13538 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16500 13538 145 145 0 16355 0
[pid=2749] vsize: 66000
Current children cumulated CPU time (s) 209.35
Current children cumulated vsize (Kb) 68124

[startup+220.015 s]
Raw data (loadavg): 1.00 1.04 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14252 0 0 0 21864 69 0 0 25 0 1 0 1788336617 67616768 13547 4294967295 134512640 135094434 3221224432 3221223088 134561688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16508 13547 145 145 0 16363 0
[pid=2749] vsize: 66032
Current children cumulated CPU time (s) 219.35
Current children cumulated vsize (Kb) 68156

[startup+230.015 s]
Raw data (loadavg): 1.00 1.04 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14258 0 0 0 22864 70 0 0 25 0 1 0 1788336617 67641344 13553 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16514 13553 145 145 0 16369 0
[pid=2749] vsize: 66056
Current children cumulated CPU time (s) 229.36
Current children cumulated vsize (Kb) 68180

[startup+240.016 s]
Raw data (loadavg): 1.00 1.04 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14296 0 0 0 23863 71 0 0 25 0 1 0 1788336617 67919872 13591 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16582 13591 145 145 0 16437 0
[pid=2749] vsize: 66328
Current children cumulated CPU time (s) 239.36
Current children cumulated vsize (Kb) 68452

[startup+250.015 s]
Raw data (loadavg): 1.00 1.03 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14297 0 0 0 24863 71 0 0 25 0 1 0 1788336617 67919872 13592 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16582 13592 145 145 0 16437 0
[pid=2749] vsize: 66328
Current children cumulated CPU time (s) 249.36
Current children cumulated vsize (Kb) 68452

[startup+260.016 s]
Raw data (loadavg): 1.00 1.03 1.04 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14298 0 0 0 25863 71 0 0 25 0 1 0 1788336617 67919872 13593 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16582 13593 145 145 0 16437 0
[pid=2749] vsize: 66328
Current children cumulated CPU time (s) 259.36
Current children cumulated vsize (Kb) 68452

[startup+270.017 s]
Raw data (loadavg): 1.00 1.03 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14299 0 0 0 26863 71 0 0 25 0 1 0 1788336617 67919872 13594 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16582 13594 145 145 0 16437 0
[pid=2749] vsize: 66328
Current children cumulated CPU time (s) 269.36
Current children cumulated vsize (Kb) 68452

[startup+280.017 s]
Raw data (loadavg): 1.00 1.03 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14302 0 0 0 27863 72 0 0 25 0 1 0 1788336617 67932160 13597 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16585 13597 145 145 0 16440 0
[pid=2749] vsize: 66340
Current children cumulated CPU time (s) 279.37
Current children cumulated vsize (Kb) 68464

[startup+290.019 s]
Raw data (loadavg): 1.00 1.03 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14310 0 0 0 28863 72 0 0 25 0 1 0 1788336617 67960832 13605 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16592 13605 145 145 0 16447 0
[pid=2749] vsize: 66368
Current children cumulated CPU time (s) 289.37
Current children cumulated vsize (Kb) 68492

[startup+300.019 s]
Raw data (loadavg): 1.00 1.03 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14318 0 0 0 29863 72 0 0 25 0 1 0 1788336617 67989504 13613 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16599 13613 145 145 0 16454 0
[pid=2749] vsize: 66396
Current children cumulated CPU time (s) 299.37
Current children cumulated vsize (Kb) 68520

[startup+310.02 s]
Raw data (loadavg): 1.00 1.03 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14328 0 0 0 30862 72 0 0 25 0 1 0 1788336617 68026368 13623 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2749/statm): 16608 13623 145 145 0 16463 0
[pid=2749] vsize: 66432
Current children cumulated CPU time (s) 309.36
Current children cumulated vsize (Kb) 68556

[startup+320.02 s]
Raw data (loadavg): 1.00 1.02 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14333 0 0 0 31862 73 0 0 25 0 1 0 1788336617 68046848 13628 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16613 13628 145 145 0 16468 0
[pid=2749] vsize: 66452
Current children cumulated CPU time (s) 319.37
Current children cumulated vsize (Kb) 68576

[startup+330.021 s]
Raw data (loadavg): 1.00 1.02 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14349 0 0 0 32862 73 0 0 25 0 1 0 1788336617 68104192 13644 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16627 13644 145 145 0 16482 0
[pid=2749] vsize: 66508
Current children cumulated CPU time (s) 329.37
Current children cumulated vsize (Kb) 68632

[startup+340.022 s]
Raw data (loadavg): 1.00 1.02 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14359 0 0 0 33862 73 0 0 25 0 1 0 1788336617 68141056 13654 4294967295 134512640 135094434 3221224432 3221223088 134561448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16636 13654 145 145 0 16491 0
[pid=2749] vsize: 66544
Current children cumulated CPU time (s) 339.37
Current children cumulated vsize (Kb) 68668

[startup+350.022 s]
Raw data (loadavg): 1.00 1.02 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14369 0 0 0 34862 73 0 0 25 0 1 0 1788336617 68177920 13664 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16645 13664 145 145 0 16500 0
[pid=2749] vsize: 66580
Current children cumulated CPU time (s) 349.37
Current children cumulated vsize (Kb) 68704

[startup+360.023 s]
Raw data (loadavg): 1.00 1.02 1.03 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14386 0 0 0 35862 73 0 0 25 0 1 0 1788336617 68243456 13681 4294967295 134512640 135094434 3221224432 3221223076 134561789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16661 13681 145 145 0 16516 0
[pid=2749] vsize: 66644
Current children cumulated CPU time (s) 359.37
Current children cumulated vsize (Kb) 68768

[startup+370.023 s]
Raw data (loadavg): 1.00 1.02 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14400 0 0 0 36862 73 0 0 25 0 1 0 1788336617 68296704 13695 4294967295 134512640 135094434 3221224432 3221223136 134554440 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16674 13695 145 145 0 16529 0
[pid=2749] vsize: 66696
Current children cumulated CPU time (s) 369.37
Current children cumulated vsize (Kb) 68820

[startup+380.024 s]
Raw data (loadavg): 1.00 1.02 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14409 0 0 0 37862 74 0 0 25 0 1 0 1788336617 68329472 13704 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16682 13704 145 145 0 16537 0
[pid=2749] vsize: 66728
Current children cumulated CPU time (s) 379.38
Current children cumulated vsize (Kb) 68852

[startup+390.024 s]
Raw data (loadavg): 1.00 1.02 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14414 0 0 0 38862 74 0 0 25 0 1 0 1788336617 68349952 13709 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16687 13709 145 145 0 16542 0
[pid=2749] vsize: 66748
Current children cumulated CPU time (s) 389.38
Current children cumulated vsize (Kb) 68872

[startup+400.025 s]
Raw data (loadavg): 1.00 1.02 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14436 0 0 0 39862 74 0 0 25 0 1 0 1788336617 68431872 13731 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16707 13731 145 145 0 16562 0
[pid=2749] vsize: 66828
Current children cumulated CPU time (s) 399.38
Current children cumulated vsize (Kb) 68952

[startup+410.025 s]
Raw data (loadavg): 1.00 1.02 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14450 0 0 0 40862 74 0 0 25 0 1 0 1788336617 68485120 13745 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16720 13745 145 145 0 16575 0
[pid=2749] vsize: 66880
Current children cumulated CPU time (s) 409.38
Current children cumulated vsize (Kb) 69004

[startup+420.025 s]
Raw data (loadavg): 1.00 1.02 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14460 0 0 0 41862 74 0 0 25 0 1 0 1788336617 68517888 13755 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16728 13755 145 145 0 16583 0
[pid=2749] vsize: 66912
Current children cumulated CPU time (s) 419.38
Current children cumulated vsize (Kb) 69036

[startup+430.026 s]
Raw data (loadavg): 1.00 1.01 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14471 0 0 0 42862 74 0 0 25 0 1 0 1788336617 68558848 13766 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16738 13766 145 145 0 16593 0
[pid=2749] vsize: 66952
Current children cumulated CPU time (s) 429.38
Current children cumulated vsize (Kb) 69076

[startup+440.026 s]
Raw data (loadavg): 1.00 1.01 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14484 0 0 0 43862 74 0 0 25 0 1 0 1788336617 68608000 13779 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16750 13779 145 145 0 16605 0
[pid=2749] vsize: 67000
Current children cumulated CPU time (s) 439.38
Current children cumulated vsize (Kb) 69124

[startup+450.026 s]
Raw data (loadavg): 1.00 1.01 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14492 0 0 0 44862 75 0 0 25 0 1 0 1788336617 68636672 13787 4294967295 134512640 135094434 3221224432 3221223072 134562115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16757 13787 145 145 0 16612 0
[pid=2749] vsize: 67028
Current children cumulated CPU time (s) 449.39
Current children cumulated vsize (Kb) 69152

[startup+460.026 s]
Raw data (loadavg): 1.00 1.01 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14505 0 0 0 45861 75 0 0 25 0 1 0 1788336617 68685824 13800 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16769 13800 145 145 0 16624 0
[pid=2749] vsize: 67076
Current children cumulated CPU time (s) 459.38
Current children cumulated vsize (Kb) 69200

[startup+470.027 s]
Raw data (loadavg): 1.00 1.01 1.02 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14517 0 0 0 46861 75 0 0 25 0 1 0 1788336617 68730880 13812 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16780 13812 145 145 0 16635 0
[pid=2749] vsize: 67120
Current children cumulated CPU time (s) 469.38
Current children cumulated vsize (Kb) 69244

[startup+480.027 s]
Raw data (loadavg): 1.00 1.01 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14528 0 0 0 47861 75 0 0 25 0 1 0 1788336617 68775936 13823 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16791 13823 145 145 0 16646 0
[pid=2749] vsize: 67164
Current children cumulated CPU time (s) 479.38
Current children cumulated vsize (Kb) 69288

[startup+490.028 s]
Raw data (loadavg): 1.00 1.01 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14539 0 0 0 48861 75 0 0 25 0 1 0 1788336617 68816896 13834 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16801 13834 145 145 0 16656 0
[pid=2749] vsize: 67204
Current children cumulated CPU time (s) 489.38
Current children cumulated vsize (Kb) 69328

[startup+500.029 s]
Raw data (loadavg): 1.00 1.01 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14554 0 0 0 49860 76 0 0 25 0 1 0 1788336617 68874240 13849 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2749/statm): 16815 13849 145 145 0 16670 0
[pid=2749] vsize: 67260
Current children cumulated CPU time (s) 499.38
Current children cumulated vsize (Kb) 69384

[startup+510.029 s]
Raw data (loadavg): 1.00 1.01 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14568 0 0 0 50860 76 0 0 25 0 1 0 1788336617 68927488 13863 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16828 13863 145 145 0 16683 0
[pid=2749] vsize: 67312
Current children cumulated CPU time (s) 509.38
Current children cumulated vsize (Kb) 69436

[startup+520.03 s]
Raw data (loadavg): 1.00 1.01 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14587 0 0 0 51860 77 0 0 25 0 1 0 1788336617 68997120 13882 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16845 13882 145 145 0 16700 0
[pid=2749] vsize: 67380
Current children cumulated CPU time (s) 519.39
Current children cumulated vsize (Kb) 69504

[startup+530.03 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14595 0 0 0 52860 77 0 0 25 0 1 0 1788336617 69029888 13890 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16853 13890 145 145 0 16708 0
[pid=2749] vsize: 67412
Current children cumulated CPU time (s) 529.39
Current children cumulated vsize (Kb) 69536

[startup+540.031 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14605 0 0 0 53860 77 0 0 25 0 1 0 1788336617 69066752 13900 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16862 13900 145 145 0 16717 0
[pid=2749] vsize: 67448
Current children cumulated CPU time (s) 539.39
Current children cumulated vsize (Kb) 69572

[startup+550.03 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14618 0 0 0 54860 77 0 0 25 0 1 0 1788336617 69115904 13913 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16874 13913 145 145 0 16729 0
[pid=2749] vsize: 67496
Current children cumulated CPU time (s) 549.39
Current children cumulated vsize (Kb) 69620

[startup+560.031 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14629 0 0 0 55860 77 0 0 25 0 1 0 1788336617 69156864 13924 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16884 13924 145 145 0 16739 0
[pid=2749] vsize: 67536
Current children cumulated CPU time (s) 559.39
Current children cumulated vsize (Kb) 69660

[startup+570.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14639 0 0 0 56859 77 0 0 25 0 1 0 1788336617 69193728 13934 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16893 13934 145 145 0 16748 0
[pid=2749] vsize: 67572
Current children cumulated CPU time (s) 569.38
Current children cumulated vsize (Kb) 69696

[startup+580.032 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14650 0 0 0 57860 77 0 0 25 0 1 0 1788336617 69238784 13945 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16904 13945 145 145 0 16759 0
[pid=2749] vsize: 67616
Current children cumulated CPU time (s) 579.39
Current children cumulated vsize (Kb) 69740

[startup+590.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14659 0 0 0 58860 77 0 0 25 0 1 0 1788336617 69533696 13954 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16976 13954 145 145 0 16831 0
[pid=2749] vsize: 67904
Current children cumulated CPU time (s) 589.39
Current children cumulated vsize (Kb) 70028

[startup+600.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14675 0 0 0 59860 78 0 0 25 0 1 0 1788336617 69595136 13970 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 16991 13970 145 145 0 16846 0
[pid=2749] vsize: 67964
Current children cumulated CPU time (s) 599.4
Current children cumulated vsize (Kb) 70088

[startup+610.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14687 0 0 0 60860 78 0 0 25 0 1 0 1788336617 69640192 13982 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17002 13982 145 145 0 16857 0
[pid=2749] vsize: 68008
Current children cumulated CPU time (s) 609.4
Current children cumulated vsize (Kb) 70132

[startup+620.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14697 0 0 0 61860 78 0 0 25 0 1 0 1788336617 69677056 13992 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17011 13992 145 145 0 16866 0
[pid=2749] vsize: 68044
Current children cumulated CPU time (s) 619.4
Current children cumulated vsize (Kb) 70168

[startup+630.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14704 0 0 0 62860 78 0 0 25 0 1 0 1788336617 69705728 13999 4294967295 134512640 135094434 3221224432 3221223088 134561778 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17018 13999 145 145 0 16873 0
[pid=2749] vsize: 68072
Current children cumulated CPU time (s) 629.4
Current children cumulated vsize (Kb) 70196

[startup+640.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14717 0 0 0 63860 78 0 0 25 0 1 0 1788336617 69754880 14012 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17030 14012 145 145 0 16885 0
[pid=2749] vsize: 68120
Current children cumulated CPU time (s) 639.4
Current children cumulated vsize (Kb) 70244

[startup+650.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14729 0 0 0 64860 78 0 0 25 0 1 0 1788336617 69799936 14024 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17041 14024 145 145 0 16896 0
[pid=2749] vsize: 68164
Current children cumulated CPU time (s) 649.4
Current children cumulated vsize (Kb) 70288

[startup+660.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14748 0 0 0 65860 78 0 0 25 0 1 0 1788336617 69873664 14043 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17059 14043 145 145 0 16914 0
[pid=2749] vsize: 68236
Current children cumulated CPU time (s) 659.4
Current children cumulated vsize (Kb) 70360

[startup+670.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14763 0 0 0 66860 78 0 0 25 0 1 0 1788336617 69931008 14058 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17073 14058 145 145 0 16928 0
[pid=2749] vsize: 68292
Current children cumulated CPU time (s) 669.4
Current children cumulated vsize (Kb) 70416

[startup+680.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14779 0 0 0 67860 78 0 0 25 0 1 0 1788336617 69992448 14074 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17088 14074 145 145 0 16943 0
[pid=2749] vsize: 68352
Current children cumulated CPU time (s) 679.4
Current children cumulated vsize (Kb) 70476

[startup+690.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14793 0 0 0 68860 78 0 0 25 0 1 0 1788336617 70045696 14088 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17101 14088 145 145 0 16956 0
[pid=2749] vsize: 68404
Current children cumulated CPU time (s) 689.4
Current children cumulated vsize (Kb) 70528

[startup+700.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14801 0 0 0 69860 78 0 0 25 0 1 0 1788336617 70074368 14096 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17108 14096 145 145 0 16963 0
[pid=2749] vsize: 68432
Current children cumulated CPU time (s) 699.4
Current children cumulated vsize (Kb) 70556

[startup+710.039 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14815 0 0 0 70860 79 0 0 25 0 1 0 1788336617 70127616 14110 4294967295 134512640 135094434 3221224432 3221223072 134562144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17121 14110 145 145 0 16976 0
[pid=2749] vsize: 68484
Current children cumulated CPU time (s) 709.41
Current children cumulated vsize (Kb) 70608

[startup+720.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14828 0 0 0 71860 79 0 0 25 0 1 0 1788336617 70176768 14123 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17133 14123 145 145 0 16988 0
[pid=2749] vsize: 68532
Current children cumulated CPU time (s) 719.41
Current children cumulated vsize (Kb) 70656

[startup+730.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14842 0 0 0 72861 79 0 0 25 0 1 0 1788336617 70230016 14137 4294967295 134512640 135094434 3221224432 3221223156 134558440 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17146 14137 145 145 0 17001 0
[pid=2749] vsize: 68584
Current children cumulated CPU time (s) 729.42
Current children cumulated vsize (Kb) 70708

[startup+740.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14851 0 0 0 73861 79 0 0 25 0 1 0 1788336617 70266880 14146 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17155 14146 145 145 0 17010 0
[pid=2749] vsize: 68620
Current children cumulated CPU time (s) 739.42
Current children cumulated vsize (Kb) 70744

[startup+750.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14865 0 0 0 74861 79 0 0 25 0 1 0 1788336617 70320128 14160 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17168 14160 145 145 0 17023 0
[pid=2749] vsize: 68672
Current children cumulated CPU time (s) 749.42
Current children cumulated vsize (Kb) 70796

[startup+760.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14876 0 0 0 75861 79 0 0 25 0 1 0 1788336617 70361088 14171 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17178 14171 145 145 0 17033 0
[pid=2749] vsize: 68712
Current children cumulated CPU time (s) 759.42
Current children cumulated vsize (Kb) 70836

[startup+770.042 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14890 0 0 0 76861 79 0 0 25 0 1 0 1788336617 70414336 14185 4294967295 134512640 135094434 3221224432 3221223072 134538541 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17191 14185 145 145 0 17046 0
[pid=2749] vsize: 68764
Current children cumulated CPU time (s) 769.42
Current children cumulated vsize (Kb) 70888

[startup+780.042 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14903 0 0 0 77861 79 0 0 25 0 1 0 1788336617 70463488 14198 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17203 14198 145 145 0 17058 0
[pid=2749] vsize: 68812
Current children cumulated CPU time (s) 779.42
Current children cumulated vsize (Kb) 70936

[startup+790.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14915 0 0 0 78861 79 0 0 25 0 1 0 1788336617 70508544 14210 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17214 14210 145 145 0 17069 0
[pid=2749] vsize: 68856
Current children cumulated CPU time (s) 789.42
Current children cumulated vsize (Kb) 70980

[startup+800.042 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14922 0 0 0 79861 80 0 0 25 0 1 0 1788336617 70537216 14217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17221 14217 145 145 0 17076 0
[pid=2749] vsize: 68884
Current children cumulated CPU time (s) 799.43
Current children cumulated vsize (Kb) 71008

[startup+810.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14934 0 0 0 80861 80 0 0 25 0 1 0 1788336617 70582272 14229 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17232 14229 145 145 0 17087 0
[pid=2749] vsize: 68928
Current children cumulated CPU time (s) 809.43
Current children cumulated vsize (Kb) 71052

[startup+820.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14946 0 0 0 81860 80 0 0 25 0 1 0 1788336617 70627328 14241 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17243 14241 145 145 0 17098 0
[pid=2749] vsize: 68972
Current children cumulated CPU time (s) 819.42
Current children cumulated vsize (Kb) 71096

[startup+830.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14958 0 0 0 82859 82 0 0 25 0 1 0 1788336617 70672384 14253 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17254 14253 145 145 0 17109 0
[pid=2749] vsize: 69016
Current children cumulated CPU time (s) 829.43
Current children cumulated vsize (Kb) 71140

[startup+840.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14970 0 0 0 83859 82 0 0 25 0 1 0 1788336617 70717440 14265 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17265 14265 145 145 0 17120 0
[pid=2749] vsize: 69060
Current children cumulated CPU time (s) 839.43
Current children cumulated vsize (Kb) 71184

[startup+850.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14981 0 0 0 84858 82 0 0 25 0 1 0 1788336617 70758400 14276 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17275 14276 145 145 0 17130 0
[pid=2749] vsize: 69100
Current children cumulated CPU time (s) 849.42
Current children cumulated vsize (Kb) 71224

[startup+860.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 14994 0 0 0 85858 82 0 0 25 0 1 0 1788336617 70807552 14289 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17287 14289 145 145 0 17142 0
[pid=2749] vsize: 69148
Current children cumulated CPU time (s) 859.42
Current children cumulated vsize (Kb) 71272

[startup+870.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15003 0 0 0 86858 83 0 0 25 0 1 0 1788336617 70844416 14298 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17296 14298 145 145 0 17151 0
[pid=2749] vsize: 69184
Current children cumulated CPU time (s) 869.43
Current children cumulated vsize (Kb) 71308

[startup+880.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15019 0 0 0 87858 83 0 0 25 0 1 0 1788336617 70905856 14314 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17311 14314 145 145 0 17166 0
[pid=2749] vsize: 69244
Current children cumulated CPU time (s) 879.43
Current children cumulated vsize (Kb) 71368

[startup+890.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15029 0 0 0 88858 83 0 0 25 0 1 0 1788336617 70942720 14324 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17320 14324 145 145 0 17175 0
[pid=2749] vsize: 69280
Current children cumulated CPU time (s) 889.43
Current children cumulated vsize (Kb) 71404

[startup+900.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15045 0 0 0 89857 83 0 0 25 0 1 0 1788336617 71004160 14340 4294967295 134512640 135094434 3221224432 3221223044 134563127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17335 14340 145 145 0 17190 0
[pid=2749] vsize: 69340
Current children cumulated CPU time (s) 899.42
Current children cumulated vsize (Kb) 71464

[startup+910.051 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15061 0 0 0 90857 84 0 0 25 0 1 0 1788336617 71061504 14356 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17349 14356 145 145 0 17204 0
[pid=2749] vsize: 69396
Current children cumulated CPU time (s) 909.43
Current children cumulated vsize (Kb) 71520

[startup+920.051 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15079 0 0 0 91857 84 0 0 25 0 1 0 1788336617 71131136 14374 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17366 14374 145 145 0 17221 0
[pid=2749] vsize: 69464
Current children cumulated CPU time (s) 919.43
Current children cumulated vsize (Kb) 71588

[startup+930.052 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15094 0 0 0 92857 84 0 0 25 0 1 0 1788336617 71188480 14389 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17380 14389 145 145 0 17235 0
[pid=2749] vsize: 69520
Current children cumulated CPU time (s) 929.43
Current children cumulated vsize (Kb) 71644

[startup+940.052 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15116 0 0 0 93857 84 0 0 25 0 1 0 1788336617 71270400 14411 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17400 14411 145 145 0 17255 0
[pid=2749] vsize: 69600
Current children cumulated CPU time (s) 939.43
Current children cumulated vsize (Kb) 71724

[startup+950.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15126 0 0 0 94857 84 0 0 25 0 1 0 1788336617 71307264 14421 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17409 14421 145 145 0 17264 0
[pid=2749] vsize: 69636
Current children cumulated CPU time (s) 949.43
Current children cumulated vsize (Kb) 71760

[startup+960.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15162 0 0 0 95857 84 0 0 25 0 1 0 1788336617 71446528 14457 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17443 14457 145 145 0 17298 0
[pid=2749] vsize: 69772
Current children cumulated CPU time (s) 959.43
Current children cumulated vsize (Kb) 71896

[startup+970.054 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15174 0 0 0 96857 85 0 0 25 0 1 0 1788336617 71491584 14469 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17454 14469 145 145 0 17309 0
[pid=2749] vsize: 69816
Current children cumulated CPU time (s) 969.44
Current children cumulated vsize (Kb) 71940

[startup+980.054 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15184 0 0 0 97857 85 0 0 25 0 1 0 1788336617 71528448 14479 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17463 14479 145 145 0 17318 0
[pid=2749] vsize: 69852
Current children cumulated CPU time (s) 979.44
Current children cumulated vsize (Kb) 71976

[startup+990.055 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15195 0 0 0 98857 85 0 0 25 0 1 0 1788336617 71573504 14490 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17474 14490 145 145 0 17329 0
[pid=2749] vsize: 69896
Current children cumulated CPU time (s) 989.44
Current children cumulated vsize (Kb) 72020

[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15231 0 0 0 99857 85 0 0 25 0 1 0 1788336617 71712768 14526 4294967295 134512640 135094434 3221224432 3221223044 134563057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17508 14526 145 145 0 17363 0
[pid=2749] vsize: 70032
Current children cumulated CPU time (s) 999.44
Current children cumulated vsize (Kb) 72156

[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15260 0 0 0 100856 85 0 0 25 0 1 0 1788336617 71819264 14555 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17534 14555 145 145 0 17389 0
[pid=2749] vsize: 70136
Current children cumulated CPU time (s) 1009.43
Current children cumulated vsize (Kb) 72260

[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15278 0 0 0 101856 86 0 0 25 0 1 0 1788336617 71888896 14573 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17551 14573 145 145 0 17406 0
[pid=2749] vsize: 70204
Current children cumulated CPU time (s) 1019.44
Current children cumulated vsize (Kb) 72328

[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15291 0 0 0 102856 86 0 0 25 0 1 0 1788336617 71938048 14586 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17563 14586 145 145 0 17418 0
[pid=2749] vsize: 70252
Current children cumulated CPU time (s) 1029.44
Current children cumulated vsize (Kb) 72376

[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15302 0 0 0 103856 86 0 0 25 0 1 0 1788336617 71979008 14597 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17573 14597 145 145 0 17428 0
[pid=2749] vsize: 70292
Current children cumulated CPU time (s) 1039.44
Current children cumulated vsize (Kb) 72416

[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15320 0 0 0 104855 87 0 0 25 0 1 0 1788336617 72048640 14615 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17590 14615 145 145 0 17445 0
[pid=2749] vsize: 70360
Current children cumulated CPU time (s) 1049.44
Current children cumulated vsize (Kb) 72484

[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15345 0 0 0 105856 87 0 0 25 0 1 0 1788336617 72146944 14640 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17614 14640 145 145 0 17469 0
[pid=2749] vsize: 70456
Current children cumulated CPU time (s) 1059.45
Current children cumulated vsize (Kb) 72580

[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15364 0 0 0 106856 87 0 0 25 0 1 0 1788336617 72216576 14659 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17631 14659 145 145 0 17486 0
[pid=2749] vsize: 70524
Current children cumulated CPU time (s) 1069.45
Current children cumulated vsize (Kb) 72648

[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15381 0 0 0 107855 87 0 0 25 0 1 0 1788336617 72282112 14676 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17647 14676 145 145 0 17502 0
[pid=2749] vsize: 70588
Current children cumulated CPU time (s) 1079.44
Current children cumulated vsize (Kb) 72712

[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15394 0 0 0 108855 87 0 0 25 0 1 0 1788336617 72331264 14689 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17659 14689 145 145 0 17514 0
[pid=2749] vsize: 70636
Current children cumulated CPU time (s) 1089.44
Current children cumulated vsize (Kb) 72760

[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15423 0 0 0 109855 87 0 0 25 0 1 0 1788336617 72445952 14718 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17687 14718 145 145 0 17542 0
[pid=2749] vsize: 70748
Current children cumulated CPU time (s) 1099.44
Current children cumulated vsize (Kb) 72872

[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15435 0 0 0 110855 87 0 0 25 0 1 0 1788336617 72491008 14730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17698 14730 145 145 0 17553 0
[pid=2749] vsize: 70792
Current children cumulated CPU time (s) 1109.44
Current children cumulated vsize (Kb) 72916

[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15451 0 0 0 111855 87 0 0 25 0 1 0 1788336617 72552448 14746 4294967295 134512640 135094434 3221224432 3221223088 134561476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17713 14746 145 145 0 17568 0
[pid=2749] vsize: 70852
Current children cumulated CPU time (s) 1119.44
Current children cumulated vsize (Kb) 72976

[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15465 0 0 0 112855 88 0 0 25 0 1 0 1788336617 72605696 14760 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17726 14760 145 145 0 17581 0
[pid=2749] vsize: 70904
Current children cumulated CPU time (s) 1129.45
Current children cumulated vsize (Kb) 73028

[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15476 0 0 0 113855 88 0 0 25 0 1 0 1788336617 72646656 14771 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17736 14771 145 145 0 17591 0
[pid=2749] vsize: 70944
Current children cumulated CPU time (s) 1139.45
Current children cumulated vsize (Kb) 73068

[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15483 0 0 0 114855 88 0 0 25 0 1 0 1788336617 72675328 14778 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17743 14778 145 145 0 17598 0
[pid=2749] vsize: 70972
Current children cumulated CPU time (s) 1149.45
Current children cumulated vsize (Kb) 73096

[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15503 0 0 0 115855 88 0 0 25 0 1 0 1788336617 72753152 14798 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17762 14798 145 145 0 17617 0
[pid=2749] vsize: 71048
Current children cumulated CPU time (s) 1159.45
Current children cumulated vsize (Kb) 73172

[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15513 0 0 0 116855 88 0 0 25 0 1 0 1788336617 72790016 14808 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17771 14808 145 145 0 17626 0
[pid=2749] vsize: 71084
Current children cumulated CPU time (s) 1169.45
Current children cumulated vsize (Kb) 73208

[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15528 0 0 0 117855 88 0 0 25 0 1 0 1788336617 72843264 14823 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17784 14823 145 145 0 17639 0
[pid=2749] vsize: 71136
Current children cumulated CPU time (s) 1179.45
Current children cumulated vsize (Kb) 73260

[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15539 0 0 0 118856 88 0 0 25 0 1 0 1788336617 72888320 14834 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17795 14834 145 145 0 17650 0
[pid=2749] vsize: 71180
Current children cumulated CPU time (s) 1189.46
Current children cumulated vsize (Kb) 73304

[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15554 0 0 0 119855 89 0 0 25 0 1 0 1788336617 72945664 14849 4294967295 134512640 135094434 3221224432 3221223088 134561505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17809 14849 145 145 0 17664 0
[pid=2749] vsize: 71236
Current children cumulated CPU time (s) 1199.46
Current children cumulated vsize (Kb) 73360

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15583 0 0 0 120855 89 0 0 25 0 1 0 1788336617 73056256 14878 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17836 14878 145 145 0 17691 0
[pid=2749] vsize: 71344
Current children cumulated CPU time (s) 1209.46
Current children cumulated vsize (Kb) 73468



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 2749
Raw data (/proc/2745/stat): 2745 (minisat+_script) S 2744 2745 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788336612 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2745/statm): 531 226 485 147 0 384 0
[pid=2745] vsize: 2124
Raw data (/proc/2749/stat): 2749 (minisat+_64-bit) R 2745 2745 22582 0 -1 0 15583 0 0 0 120855 89 0 0 25 0 1 0 1788336617 73056256 14878 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2749/statm): 17836 14878 145 145 0 17691 0
[pid=2749] vsize: 71344
Current children cumulated CPU time (s) 1209.46
Current children cumulated vsize (Kb) 73468

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

Child status: 0
Real time (s): 1210.1
CPU time (s): 1209.48
CPU user time (s): 1208.56
CPU system time (s): 0.922859
CPU usage (%): 99.9489
Max. virtual memory (cumulated for all children) (Kb): 73468

Verifier Data

ERROR: no interpretation found !