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/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-core4872-1529.opb
MD5SUM21523a021e6bde8cb1bd98f2664add6c
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2030592000000000
Optimality of the best value was proved NO
Number of terms in the objective function 24975
Biggest coefficient in the objective function 53687091200000000000
Number of bits for the biggest coefficient in the objective function 66
Sum of the numbers in the objective function 226603053881884901376
Number of bits of the sum of numbers in the objective function 68
Biggest number in a constraint 10240000000000000000000
Number of bits of the biggest number in a constraint 74
Biggest sum of numbers in a constraint 10466603053881885720576
Number of bits of the biggest sum of numbers74
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1206.69
Number of variables24975
Total number of constraints29520
Number of constraints which are clauses4872
Number of constraints which are cardinality constraints (but not clauses)24647
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint24975

Trace number 5922

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        921640 kB
Buffers:          6948 kB
Cached:          78344 kB
SwapCached:        796 kB
Active:          24104 kB
Inactive:        63776 kB
HighTotal:      131008 kB
HighFree:        49420 kB
LowTotal:       903652 kB
LowFree:        872220 kB
SwapTotal:     2097136 kB
SwapFree:      2095788 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5552 kB
Slab:            19384 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:25:53 (client local time) WITH STATUS 0 IN 1207.92 SECONDS
stats: 3102 7 1207.92 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 24660] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 4760 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===================================
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 325]---> Adder-cost: 35658   maxlim: 8607   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  254172  1062419 |   84724       0        0     nan |  0.000 % |
c |       100 |  254172  1062419 |   93196     100      307     3.1 |  0.091 % |
c |       250 |  254172  1062419 |  102516     250      759     3.0 |  0.091 % |
c |       475 |  254172  1062419 |  112767     475     1530     3.2 |  0.091 % |
c |       812 |  254172  1062419 |  124044     812     2547     3.1 |  0.091 % |
c |      1318 |  254172  1062419 |  136448    1318     4099     3.1 |  0.091 % |
c |      2077 |  254172  1062419 |  150093    2077     6461     3.1 |  0.091 % |
c |      3216 |  254172  1062419 |  165103    3216    10253     3.2 |  0.091 % |
c |      4925 |  254172  1062419 |  181613    4925    15984     3.2 |  0.091 % |
c |      7487 |  254172  1062419 |  199774    7487    24911     3.3 |  0.091 % |
c |     11331 |  254172  1062419 |  219752   11331    38495     3.4 |  0.091 % |
c |     17097 |  254172  1062419 |  241727   17097    59086     3.5 |  0.091 % |
c |     25746 |  254172  1062419 |  265900   25746    92685     3.6 |  0.091 % |
c |     38720 |  254172  1062419 |  292490   38720   146314     3.8 |  0.091 % |
c |     58181 |  254172  1062419 |  321739   58181   247647     4.3 |  0.091 % |

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/26501/stat): 26501 (minisat+_script) R 26500 26501 5299 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854812399 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26501/statm): 174 3 169 147 0 27 0
[pid=26501] 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=26502
New process pid=26503
New process pid=26504
execve syscall for /bin/sed executable
One traced child (pid=26503) 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=26504) exited with status: 0
One traced child (pid=26502) exited with status: 0
New process pid=26505
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-core4872-1529.opb
One traced child (pid=26505) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=26506
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-core4872-1529.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 3172 0 0 0 838 21 0 0 25 0 1 0 1854812514 13623296 3116 4294967295 134512640 135167914 3221224432 3221222168 134581185 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 3326 3116 162 162 0 3164 0
[pid=26506] vsize: 13304
Current children cumulated CPU time (s) 8.86
Current children cumulated vsize (Kb) 15432

[startup+20.0043 s]
Raw data (loadavg): 0.94 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 8962 0 0 0 1785 46 0 0 25 0 1 0 1854812514 26963968 6377 4294967295 134512640 135167914 3221224432 3217629872 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6583 6377 162 162 0 6421 0
[pid=26506] vsize: 26332
Current children cumulated CPU time (s) 18.58
Current children cumulated vsize (Kb) 28460

[startup+30.0049 s]
Raw data (loadavg): 0.95 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 8996 0 0 0 2786 46 0 0 25 0 1 0 1854812514 27103232 6411 4294967295 134512640 135167914 3221224432 3218106576 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6617 6411 162 162 0 6455 0
[pid=26506] vsize: 26468
Current children cumulated CPU time (s) 28.59
Current children cumulated vsize (Kb) 28596

[startup+40.0056 s]
Raw data (loadavg): 0.96 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9014 0 0 0 3786 46 0 0 25 0 1 0 1854812514 27209728 6429 4294967295 134512640 135167914 3221224432 3218396432 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6643 6429 162 162 0 6481 0
[pid=26506] vsize: 26572
Current children cumulated CPU time (s) 38.59
Current children cumulated vsize (Kb) 28700

[startup+50.0062 s]
Raw data (loadavg): 0.96 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9058 0 0 0 4786 46 0 0 25 0 1 0 1854812514 27377664 6473 4294967295 134512640 135167914 3221224432 3218621280 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6684 6473 162 162 0 6522 0
[pid=26506] vsize: 26736
Current children cumulated CPU time (s) 48.59
Current children cumulated vsize (Kb) 28864

[startup+60.0069 s]
Raw data (loadavg): 0.97 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9061 0 0 0 5786 46 0 0 25 0 1 0 1854812514 27377664 6476 4294967295 134512640 135167914 3221224432 3218809520 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6684 6476 162 162 0 6522 0
[pid=26506] vsize: 26736
Current children cumulated CPU time (s) 58.59
Current children cumulated vsize (Kb) 28864

[startup+70.0065 s]
Raw data (loadavg): 0.97 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9064 0 0 0 6786 46 0 0 25 0 1 0 1854812514 27381760 6479 4294967295 134512640 135167914 3221224432 3218972128 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6685 6479 162 162 0 6523 0
[pid=26506] vsize: 26740
Current children cumulated CPU time (s) 68.59
Current children cumulated vsize (Kb) 28868

[startup+80.0071 s]
Raw data (loadavg): 0.98 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9092 0 0 0 7786 46 0 0 25 0 1 0 1854812514 27590656 6507 4294967295 134512640 135167914 3221224432 3219118192 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6736 6507 162 162 0 6574 0
[pid=26506] vsize: 26944
Current children cumulated CPU time (s) 78.59
Current children cumulated vsize (Kb) 29072

[startup+90.0068 s]
Raw data (loadavg): 0.98 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 8786 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3218493260 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0
[pid=26506] vsize: 26944
Current children cumulated CPU time (s) 88.59
Current children cumulated vsize (Kb) 29072

[startup+100.007 s]
Raw data (loadavg): 0.98 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 9786 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3218293424 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0
[pid=26506] vsize: 26944
Current children cumulated CPU time (s) 98.59
Current children cumulated vsize (Kb) 29072

[startup+110.008 s]
Raw data (loadavg): 0.98 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 10787 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3218139984 134694428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0
[pid=26506] vsize: 26944
Current children cumulated CPU time (s) 108.6
Current children cumulated vsize (Kb) 29072

[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 11787 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3217967528 134849087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0
[pid=26506] vsize: 26944
Current children cumulated CPU time (s) 118.6
Current children cumulated vsize (Kb) 29072

[startup+130.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 12787 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3217732768 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0
[pid=26506] vsize: 26944
Current children cumulated CPU time (s) 128.6
Current children cumulated vsize (Kb) 29072

[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 13787 47 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3217452224 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0
[pid=26506] vsize: 26944
Current children cumulated CPU time (s) 138.61
Current children cumulated vsize (Kb) 29072

[startup+150.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9160 0 0 0 14786 47 0 0 25 0 1 0 1854812514 27844608 6575 4294967295 134512640 135167914 3221224432 3217631072 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6798 6575 162 162 0 6636 0
[pid=26506] vsize: 27192
Current children cumulated CPU time (s) 148.6
Current children cumulated vsize (Kb) 29320

[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9258 0 0 0 15785 49 0 0 25 0 1 0 1854812514 28192768 6673 4294967295 134512640 135167914 3221224432 3218623172 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6883 6673 162 162 0 6721 0
[pid=26506] vsize: 27532
Current children cumulated CPU time (s) 158.61
Current children cumulated vsize (Kb) 29660

[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9282 0 0 0 16783 50 0 0 25 0 1 0 1854812514 28459008 6697 4294967295 134512640 135167914 3221224432 3219131852 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6948 6697 162 162 0 6786 0
[pid=26506] vsize: 27792
Current children cumulated CPU time (s) 168.6
Current children cumulated vsize (Kb) 29920

[startup+180.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9283 0 0 0 17783 51 0 0 25 0 1 0 1854812514 28463104 6698 4294967295 134512640 135167914 3221224432 3217868716 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6949 6698 162 162 0 6787 0
[pid=26506] vsize: 27796
Current children cumulated CPU time (s) 178.61
Current children cumulated vsize (Kb) 29924

[startup+190.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9324 0 0 0 18782 51 0 0 25 0 1 0 1854812514 28631040 6739 4294967295 134512640 135167914 3221224432 3217356240 134624000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 6990 6739 162 162 0 6828 0
[pid=26506] vsize: 27960
Current children cumulated CPU time (s) 188.6
Current children cumulated vsize (Kb) 30088

[startup+200.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9578 0 0 0 19781 52 0 0 25 0 1 0 1854812514 29265920 6909 4294967295 134512640 135167914 3221224432 3218399132 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7145 6909 162 162 0 6983 0
[pid=26506] vsize: 28580
Current children cumulated CPU time (s) 198.6
Current children cumulated vsize (Kb) 30708

[startup+210.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9610 0 0 0 20781 52 0 0 25 0 1 0 1854812514 29364224 6941 4294967295 134512640 135167914 3221224432 3218999184 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7169 6941 162 162 0 7007 0
[pid=26506] vsize: 28676
Current children cumulated CPU time (s) 208.6
Current children cumulated vsize (Kb) 30804

[startup+220.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9618 0 0 0 21781 52 0 0 25 0 1 0 1854812514 29388800 6949 4294967295 134512640 135167914 3221224432 3218470400 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7175 6949 162 162 0 7013 0
[pid=26506] vsize: 28700
Current children cumulated CPU time (s) 218.6
Current children cumulated vsize (Kb) 30828

[startup+230.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9618 0 0 0 22781 53 0 0 25 0 1 0 1854812514 29388800 6949 4294967295 134512640 135167914 3221224432 3217953840 134694428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7175 6949 162 162 0 7013 0
[pid=26506] vsize: 28700
Current children cumulated CPU time (s) 228.61
Current children cumulated vsize (Kb) 30828

[startup+240.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9618 0 0 0 23781 53 0 0 25 0 1 0 1854812514 29388800 6949 4294967295 134512640 135167914 3221224432 3217560272 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7175 6949 162 162 0 7013 0
[pid=26506] vsize: 28700
Current children cumulated CPU time (s) 238.61
Current children cumulated vsize (Kb) 30828

[startup+250.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9710 0 0 0 24779 54 0 0 25 0 1 0 1854812514 29741056 7041 4294967295 134512640 135167914 3221224432 3217676528 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7261 7041 162 162 0 7099 0
[pid=26506] vsize: 29044
Current children cumulated CPU time (s) 248.6
Current children cumulated vsize (Kb) 31172

[startup+260.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9757 0 0 0 25778 54 0 0 25 0 1 0 1854812514 29884416 7088 4294967295 134512640 135167914 3221224432 3218576272 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7296 7088 162 162 0 7134 0
[pid=26506] vsize: 29184
Current children cumulated CPU time (s) 258.59
Current children cumulated vsize (Kb) 31312

[startup+270.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9787 0 0 0 26778 55 0 0 25 0 1 0 1854812514 30371840 7118 4294967295 134512640 135167914 3221224432 3218648440 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7415 7118 162 162 0 7253 0
[pid=26506] vsize: 29660
Current children cumulated CPU time (s) 268.6
Current children cumulated vsize (Kb) 31788

[startup+280.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9859 0 0 0 27777 56 0 0 25 0 1 0 1854812514 30662656 7190 4294967295 134512640 135167914 3221224432 3217311008 134624420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7486 7190 162 162 0 7324 0
[pid=26506] vsize: 29944
Current children cumulated CPU time (s) 278.6
Current children cumulated vsize (Kb) 32072

[startup+290.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9927 0 0 0 28777 56 0 0 25 0 1 0 1854812514 30871552 7258 4294967295 134512640 135167914 3221224432 3218591616 134624732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7537 7258 162 162 0 7375 0
[pid=26506] vsize: 30148
Current children cumulated CPU time (s) 288.6
Current children cumulated vsize (Kb) 32276

[startup+300.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10286 0 0 0 29776 57 0 0 25 0 1 0 1854812514 31633408 7451 4294967295 134512640 135167914 3221224432 3219140640 134624732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7723 7451 162 162 0 7561 0
[pid=26506] vsize: 30892
Current children cumulated CPU time (s) 298.6
Current children cumulated vsize (Kb) 33020

[startup+310.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10287 0 0 0 30776 57 0 0 25 0 1 0 1854812514 31633408 7452 4294967295 134512640 135167914 3221224432 3218694320 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7723 7452 162 162 0 7561 0
[pid=26506] vsize: 30892
Current children cumulated CPU time (s) 308.6
Current children cumulated vsize (Kb) 33020

[startup+320.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10287 0 0 0 31776 57 0 0 25 0 1 0 1854812514 31633408 7452 4294967295 134512640 135167914 3221224432 3218312892 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7723 7452 162 162 0 7561 0
[pid=26506] vsize: 30892
Current children cumulated CPU time (s) 318.6
Current children cumulated vsize (Kb) 33020

[startup+330.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10287 0 0 0 32776 57 0 0 25 0 1 0 1854812514 31633408 7452 4294967295 134512640 135167914 3221224432 3217836280 134624136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7723 7452 162 162 0 7561 0
[pid=26506] vsize: 30892
Current children cumulated CPU time (s) 328.6
Current children cumulated vsize (Kb) 33020

[startup+340.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10361 0 0 0 33775 58 0 0 25 0 1 0 1854812514 31932416 7526 4294967295 134512640 135167914 3221224432 3217357960 134842997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7796 7526 162 162 0 7634 0
[pid=26506] vsize: 31184
Current children cumulated CPU time (s) 338.6
Current children cumulated vsize (Kb) 33312

[startup+350.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10409 0 0 0 34774 59 0 0 25 0 1 0 1854812514 32079872 7574 4294967295 134512640 135167914 3221224432 3218258080 134624772 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7832 7574 162 162 0 7670 0
[pid=26506] vsize: 31328
Current children cumulated CPU time (s) 348.6
Current children cumulated vsize (Kb) 33456

[startup+360.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10444 0 0 0 35774 59 0 0 25 0 1 0 1854812514 32186368 7609 4294967295 134512640 135167914 3221224432 3218925776 134694428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7858 7609 162 162 0 7696 0
[pid=26506] vsize: 31432
Current children cumulated CPU time (s) 358.6
Current children cumulated vsize (Kb) 33560

[startup+370.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10456 0 0 0 36774 59 0 0 25 0 1 0 1854812514 32223232 7621 4294967295 134512640 135167914 3221224432 3218341952 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7867 7621 162 162 0 7705 0
[pid=26506] vsize: 31468
Current children cumulated CPU time (s) 368.6
Current children cumulated vsize (Kb) 33596

[startup+380.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10475 0 0 0 37774 59 0 0 25 0 1 0 1854812514 32301056 7640 4294967295 134512640 135167914 3221224432 3217460592 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7886 7640 162 162 0 7724 0
[pid=26506] vsize: 31544
Current children cumulated CPU time (s) 378.6
Current children cumulated vsize (Kb) 33672

[startup+390.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10569 0 0 0 38773 60 0 0 25 0 1 0 1854812514 32641024 7734 4294967295 134512640 135167914 3221224432 3218090048 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 7969 7734 162 162 0 7807 0
[pid=26506] vsize: 31876
Current children cumulated CPU time (s) 388.6
Current children cumulated vsize (Kb) 34004

[startup+400.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10611 0 0 0 39772 60 0 0 25 0 1 0 1854812514 32772096 7776 4294967295 134512640 135167914 3221224432 3218877392 134694439 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 8001 7776 162 162 0 7839 0
[pid=26506] vsize: 32004
Current children cumulated CPU time (s) 398.59
Current children cumulated vsize (Kb) 34132

[startup+410.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 29645 0 0 0 40682 119 0 0 25 0 1 0 1854812514 110194688 24503 4294967295 134512640 135167914 3221224432 3221222176 134524032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 26903 24503 162 162 0 26741 0
[pid=26506] vsize: 107612
Current children cumulated CPU time (s) 408.28
Current children cumulated vsize (Kb) 109740

[startup+420.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36287 0 0 0 41633 145 0 0 25 0 1 0 1854812514 119820288 28409 4294967295 134512640 135167914 3221224432 3221223136 134566158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29253 28409 162 162 0 29091 0
[pid=26506] vsize: 117012
Current children cumulated CPU time (s) 418.05
Current children cumulated vsize (Kb) 119140

[startup+430.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36314 0 0 0 42632 146 0 0 25 0 1 0 1854812514 119934976 28436 4294967295 134512640 135167914 3221224432 3221223104 134562382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29281 28436 162 162 0 29119 0
[pid=26506] vsize: 117124
Current children cumulated CPU time (s) 428.05
Current children cumulated vsize (Kb) 119252

[startup+440.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36322 0 0 0 43632 146 0 0 25 0 1 0 1854812514 119963648 28444 4294967295 134512640 135167914 3221224432 3221223168 134559404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29288 28444 162 162 0 29126 0
[pid=26506] vsize: 117152
Current children cumulated CPU time (s) 438.05
Current children cumulated vsize (Kb) 119280

[startup+450.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36336 0 0 0 44632 146 0 0 25 0 1 0 1854812514 120012800 28458 4294967295 134512640 135167914 3221224432 3221223136 134563082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29300 28458 162 162 0 29138 0
[pid=26506] vsize: 117200
Current children cumulated CPU time (s) 448.05
Current children cumulated vsize (Kb) 119328

[startup+460.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36353 0 0 0 45632 146 0 0 25 0 1 0 1854812514 120107008 28475 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29323 28475 162 162 0 29161 0
[pid=26506] vsize: 117292
Current children cumulated CPU time (s) 458.05
Current children cumulated vsize (Kb) 119420

[startup+470.025 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36360 0 0 0 46632 146 0 0 25 0 1 0 1854812514 120131584 28482 4294967295 134512640 135167914 3221224432 3221223120 134566738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29329 28482 162 162 0 29167 0
[pid=26506] vsize: 117316
Current children cumulated CPU time (s) 468.05
Current children cumulated vsize (Kb) 119444

[startup+480.026 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36372 0 0 0 47632 147 0 0 25 0 1 0 1854812514 120168448 28494 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29338 28494 162 162 0 29176 0
[pid=26506] vsize: 117352
Current children cumulated CPU time (s) 478.06
Current children cumulated vsize (Kb) 119480

[startup+490.026 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36383 0 0 0 48633 147 0 0 25 0 1 0 1854812514 120205312 28505 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29347 28505 162 162 0 29185 0
[pid=26506] vsize: 117388
Current children cumulated CPU time (s) 488.07
Current children cumulated vsize (Kb) 119516

[startup+500.027 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36394 0 0 0 49632 147 0 0 25 0 1 0 1854812514 120246272 28516 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29357 28516 162 162 0 29195 0
[pid=26506] vsize: 117428
Current children cumulated CPU time (s) 498.06
Current children cumulated vsize (Kb) 119556

[startup+510.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36404 0 0 0 50632 147 0 0 25 0 1 0 1854812514 120283136 28526 4294967295 134512640 135167914 3221224432 3221223120 134566713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29366 28526 162 162 0 29204 0
[pid=26506] vsize: 117464
Current children cumulated CPU time (s) 508.06
Current children cumulated vsize (Kb) 119592

[startup+520.027 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36411 0 0 0 51632 147 0 0 25 0 1 0 1854812514 120311808 28533 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29373 28533 162 162 0 29211 0
[pid=26506] vsize: 117492
Current children cumulated CPU time (s) 518.06
Current children cumulated vsize (Kb) 119620

[startup+530.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36430 0 0 0 52632 147 0 0 25 0 1 0 1854812514 120446976 28552 4294967295 134512640 135167914 3221224432 3221223092 134567790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29406 28552 162 162 0 29244 0
[pid=26506] vsize: 117624
Current children cumulated CPU time (s) 528.06
Current children cumulated vsize (Kb) 119752

[startup+540.029 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36431 0 0 0 53632 147 0 0 25 0 1 0 1854812514 120446976 28553 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29406 28553 162 162 0 29244 0
[pid=26506] vsize: 117624
Current children cumulated CPU time (s) 538.06
Current children cumulated vsize (Kb) 119752

[startup+550.029 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36444 0 0 0 54632 147 0 0 25 0 1 0 1854812514 120483840 28566 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29415 28566 162 162 0 29253 0
[pid=26506] vsize: 117660
Current children cumulated CPU time (s) 548.06
Current children cumulated vsize (Kb) 119788

[startup+560.03 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36453 0 0 0 55633 147 0 0 25 0 1 0 1854812514 120516608 28575 4294967295 134512640 135167914 3221224432 3221223168 134559387 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29423 28575 162 162 0 29261 0
[pid=26506] vsize: 117692
Current children cumulated CPU time (s) 558.07
Current children cumulated vsize (Kb) 119820

[startup+570.031 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36464 0 0 0 56632 148 0 0 25 0 1 0 1854812514 120557568 28586 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29433 28586 162 162 0 29271 0
[pid=26506] vsize: 117732
Current children cumulated CPU time (s) 568.07
Current children cumulated vsize (Kb) 119860

[startup+580.031 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36472 0 0 0 57632 148 0 0 25 0 1 0 1854812514 120586240 28594 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29440 28594 162 162 0 29278 0
[pid=26506] vsize: 117760
Current children cumulated CPU time (s) 578.07
Current children cumulated vsize (Kb) 119888

[startup+590.032 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36483 0 0 0 58632 148 0 0 25 0 1 0 1854812514 120623104 28605 4294967295 134512640 135167914 3221224432 3221223092 134567717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29449 28605 162 162 0 29287 0
[pid=26506] vsize: 117796
Current children cumulated CPU time (s) 588.07
Current children cumulated vsize (Kb) 119924

[startup+600.032 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36490 0 0 0 59632 148 0 0 25 0 1 0 1854812514 120651776 28612 4294967295 134512640 135167914 3221224432 3221223092 134567717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29456 28612 162 162 0 29294 0
[pid=26506] vsize: 117824
Current children cumulated CPU time (s) 598.07
Current children cumulated vsize (Kb) 119952

[startup+610.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36499 0 0 0 60632 149 0 0 25 0 1 0 1854812514 120684544 28621 4294967295 134512640 135167914 3221224432 3221223092 134567717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29464 28621 162 162 0 29302 0
[pid=26506] vsize: 117856
Current children cumulated CPU time (s) 608.08
Current children cumulated vsize (Kb) 119984

[startup+620.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36508 0 0 0 61631 149 0 0 25 0 1 0 1854812514 120717312 28630 4294967295 134512640 135167914 3221224432 3221223168 134559407 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26506/statm): 29472 28630 162 162 0 29310 0
[pid=26506] vsize: 117888
Current children cumulated CPU time (s) 618.07
Current children cumulated vsize (Kb) 120016

[startup+630.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36517 0 0 0 62631 149 0 0 25 0 1 0 1854812514 120750080 28639 4294967295 134512640 135167914 3221224432 3221223136 134562815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29480 28639 162 162 0 29318 0
[pid=26506] vsize: 117920
Current children cumulated CPU time (s) 628.07
Current children cumulated vsize (Kb) 120048

[startup+640.034 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36525 0 0 0 63631 149 0 0 25 0 1 0 1854812514 120778752 28647 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29487 28647 162 162 0 29325 0
[pid=26506] vsize: 117948
Current children cumulated CPU time (s) 638.07
Current children cumulated vsize (Kb) 120076

[startup+650.035 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36534 0 0 0 64631 150 0 0 25 0 1 0 1854812514 120811520 28656 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29495 28656 162 162 0 29333 0
[pid=26506] vsize: 117980
Current children cumulated CPU time (s) 648.08
Current children cumulated vsize (Kb) 120108

[startup+660.035 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36542 0 0 0 65631 150 0 0 25 0 1 0 1854812514 120840192 28664 4294967295 134512640 135167914 3221224432 3221223116 134567636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29502 28664 162 162 0 29340 0
[pid=26506] vsize: 118008
Current children cumulated CPU time (s) 658.08
Current children cumulated vsize (Kb) 120136

[startup+670.036 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36550 0 0 0 66631 150 0 0 25 0 1 0 1854812514 120872960 28672 4294967295 134512640 135167914 3221224432 3221223136 134566347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29510 28672 162 162 0 29348 0
[pid=26506] vsize: 118040
Current children cumulated CPU time (s) 668.08
Current children cumulated vsize (Kb) 120168

[startup+680.037 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36559 0 0 0 67631 150 0 0 25 0 1 0 1854812514 120905728 28681 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29518 28681 162 162 0 29356 0
[pid=26506] vsize: 118072
Current children cumulated CPU time (s) 678.08
Current children cumulated vsize (Kb) 120200

[startup+690.037 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36566 0 0 0 68631 150 0 0 25 0 1 0 1854812514 120934400 28688 4294967295 134512640 135167914 3221224432 3221223136 134566316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29525 28688 162 162 0 29363 0
[pid=26506] vsize: 118100
Current children cumulated CPU time (s) 688.08
Current children cumulated vsize (Kb) 120228

[startup+700.038 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36599 0 0 0 69632 150 0 0 25 0 1 0 1854812514 121196544 28721 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29589 28721 162 162 0 29427 0
[pid=26506] vsize: 118356
Current children cumulated CPU time (s) 698.09
Current children cumulated vsize (Kb) 120484

[startup+710.038 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36600 0 0 0 70632 150 0 0 25 0 1 0 1854812514 121196544 28722 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29589 28722 162 162 0 29427 0
[pid=26506] vsize: 118356
Current children cumulated CPU time (s) 708.09
Current children cumulated vsize (Kb) 120484

[startup+720.038 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36601 0 0 0 71632 150 0 0 25 0 1 0 1854812514 121196544 28723 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29589 28723 162 162 0 29427 0
[pid=26506] vsize: 118356
Current children cumulated CPU time (s) 718.09
Current children cumulated vsize (Kb) 120484

[startup+730.039 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36602 0 0 0 72632 150 0 0 25 0 1 0 1854812514 121196544 28724 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29589 28724 162 162 0 29427 0
[pid=26506] vsize: 118356
Current children cumulated CPU time (s) 728.09
Current children cumulated vsize (Kb) 120484

[startup+740.039 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36606 0 0 0 73632 150 0 0 25 0 1 0 1854812514 121208832 28728 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29592 28728 162 162 0 29430 0
[pid=26506] vsize: 118368
Current children cumulated CPU time (s) 738.09
Current children cumulated vsize (Kb) 120496

[startup+750.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36614 0 0 0 74632 150 0 0 25 0 1 0 1854812514 121241600 28736 4294967295 134512640 135167914 3221224432 3221223136 134562874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29600 28736 162 162 0 29438 0
[pid=26506] vsize: 118400
Current children cumulated CPU time (s) 748.09
Current children cumulated vsize (Kb) 120528

[startup+760.041 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36622 0 0 0 75631 151 0 0 25 0 1 0 1854812514 121270272 28744 4294967295 134512640 135167914 3221224432 3221223092 134567727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29607 28744 162 162 0 29445 0
[pid=26506] vsize: 118428
Current children cumulated CPU time (s) 758.09
Current children cumulated vsize (Kb) 120556

[startup+770.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36628 0 0 0 76630 152 0 0 25 0 1 0 1854812514 121290752 28750 4294967295 134512640 135167914 3221224432 3221223156 134559539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26506/statm): 29612 28750 162 162 0 29450 0
[pid=26506] vsize: 118448
Current children cumulated CPU time (s) 768.09
Current children cumulated vsize (Kb) 120576

[startup+780.042 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36641 0 0 0 77628 153 0 0 25 0 1 0 1854812514 121339904 28763 4294967295 134512640 135167914 3221224432 3221223136 134562535 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29624 28763 162 162 0 29462 0
[pid=26506] vsize: 118496
Current children cumulated CPU time (s) 778.08
Current children cumulated vsize (Kb) 120624

[startup+790.043 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36648 0 0 0 78628 153 0 0 25 0 1 0 1854812514 121368576 28770 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29631 28770 162 162 0 29469 0
[pid=26506] vsize: 118524
Current children cumulated CPU time (s) 788.08
Current children cumulated vsize (Kb) 120652

[startup+800.043 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36656 0 0 0 79628 153 0 0 25 0 1 0 1854812514 121397248 28778 4294967295 134512640 135167914 3221224432 3221223128 134562693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29638 28778 162 162 0 29476 0
[pid=26506] vsize: 118552
Current children cumulated CPU time (s) 798.08
Current children cumulated vsize (Kb) 120680

[startup+810.044 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36666 0 0 0 80628 154 0 0 25 0 1 0 1854812514 121434112 28788 4294967295 134512640 135167914 3221224432 3221223092 134567722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29647 28788 162 162 0 29485 0
[pid=26506] vsize: 118588
Current children cumulated CPU time (s) 808.09
Current children cumulated vsize (Kb) 120716

[startup+820.044 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36674 0 0 0 81627 154 0 0 25 0 1 0 1854812514 121462784 28796 4294967295 134512640 135167914 3221224432 3221223168 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29654 28796 162 162 0 29492 0
[pid=26506] vsize: 118616
Current children cumulated CPU time (s) 818.08
Current children cumulated vsize (Kb) 120744

[startup+830.044 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36683 0 0 0 82627 155 0 0 25 0 1 0 1854812514 121499648 28805 4294967295 134512640 135167914 3221224432 3221223136 134562502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29663 28805 162 162 0 29501 0
[pid=26506] vsize: 118652
Current children cumulated CPU time (s) 828.09
Current children cumulated vsize (Kb) 120780

[startup+840.045 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36692 0 0 0 83627 155 0 0 25 0 1 0 1854812514 121532416 28814 4294967295 134512640 135167914 3221224432 3221223092 134567786 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29671 28814 162 162 0 29509 0
[pid=26506] vsize: 118684
Current children cumulated CPU time (s) 838.09
Current children cumulated vsize (Kb) 120812

[startup+850.047 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36701 0 0 0 84627 155 0 0 25 0 1 0 1854812514 121565184 28823 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29679 28823 162 162 0 29517 0
[pid=26506] vsize: 118716
Current children cumulated CPU time (s) 848.09
Current children cumulated vsize (Kb) 120844

[startup+860.047 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36711 0 0 0 85627 155 0 0 25 0 1 0 1854812514 121602048 28833 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29688 28833 162 162 0 29526 0
[pid=26506] vsize: 118752
Current children cumulated CPU time (s) 858.09
Current children cumulated vsize (Kb) 120880

[startup+870.047 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36720 0 0 0 86627 155 0 0 25 0 1 0 1854812514 121634816 28842 4294967295 134512640 135167914 3221224432 3221223136 134562618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29696 28842 162 162 0 29534 0
[pid=26506] vsize: 118784
Current children cumulated CPU time (s) 868.09
Current children cumulated vsize (Kb) 120912

[startup+880.047 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36725 0 0 0 87627 156 0 0 25 0 1 0 1854812514 121655296 28847 4294967295 134512640 135167914 3221224432 3221223092 134567760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29701 28847 162 162 0 29539 0
[pid=26506] vsize: 118804
Current children cumulated CPU time (s) 878.1
Current children cumulated vsize (Kb) 120932

[startup+890.048 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36731 0 0 0 88627 156 0 0 25 0 1 0 1854812514 121675776 28853 4294967295 134512640 135167914 3221224432 3221223136 134562620 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29706 28853 162 162 0 29544 0
[pid=26506] vsize: 118824
Current children cumulated CPU time (s) 888.1
Current children cumulated vsize (Kb) 120952

[startup+900.049 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36741 0 0 0 89627 156 0 0 25 0 1 0 1854812514 121712640 28863 4294967295 134512640 135167914 3221224432 3221223136 134566415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29715 28863 162 162 0 29553 0
[pid=26506] vsize: 118860
Current children cumulated CPU time (s) 898.1
Current children cumulated vsize (Kb) 120988

[startup+910.049 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36749 0 0 0 90627 156 0 0 25 0 1 0 1854812514 121745408 28871 4294967295 134512640 135167914 3221224432 3221223200 134566311 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29723 28871 162 162 0 29561 0
[pid=26506] vsize: 118892
Current children cumulated CPU time (s) 908.1
Current children cumulated vsize (Kb) 121020

[startup+920.05 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36758 0 0 0 91627 156 0 0 25 0 1 0 1854812514 121778176 28880 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29731 28880 162 162 0 29569 0
[pid=26506] vsize: 118924
Current children cumulated CPU time (s) 918.1
Current children cumulated vsize (Kb) 121052

[startup+930.051 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36767 0 0 0 92627 156 0 0 25 0 1 0 1854812514 121810944 28889 4294967295 134512640 135167914 3221224432 3221223132 134566190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29739 28889 162 162 0 29577 0
[pid=26506] vsize: 118956
Current children cumulated CPU time (s) 928.1
Current children cumulated vsize (Kb) 121084

[startup+940.051 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36775 0 0 0 93627 156 0 0 25 0 1 0 1854812514 121843712 28897 4294967295 134512640 135167914 3221224432 3221223152 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29747 28897 162 162 0 29585 0
[pid=26506] vsize: 118988
Current children cumulated CPU time (s) 938.1
Current children cumulated vsize (Kb) 121116

[startup+950.052 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36786 0 0 0 94627 157 0 0 25 0 1 0 1854812514 121884672 28908 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29757 28908 162 162 0 29595 0
[pid=26506] vsize: 119028
Current children cumulated CPU time (s) 948.11
Current children cumulated vsize (Kb) 121156

[startup+960.053 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36794 0 0 0 95627 157 0 0 25 0 1 0 1854812514 121913344 28916 4294967295 134512640 135167914 3221224432 3221223120 134566795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29764 28916 162 162 0 29602 0
[pid=26506] vsize: 119056
Current children cumulated CPU time (s) 958.11
Current children cumulated vsize (Kb) 121184

[startup+970.053 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36810 0 0 0 96627 157 0 0 25 0 1 0 1854812514 121974784 28932 4294967295 134512640 135167914 3221224432 3221223092 134567697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29779 28932 162 162 0 29617 0
[pid=26506] vsize: 119116
Current children cumulated CPU time (s) 968.11
Current children cumulated vsize (Kb) 121244

[startup+980.054 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36822 0 0 0 97627 157 0 0 25 0 1 0 1854812514 122019840 28944 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29790 28944 162 162 0 29628 0
[pid=26506] vsize: 119160
Current children cumulated CPU time (s) 978.11
Current children cumulated vsize (Kb) 121288

[startup+990.054 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36834 0 0 0 98626 158 0 0 25 0 1 0 1854812514 122068992 28956 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29802 28956 162 162 0 29640 0
[pid=26506] vsize: 119208
Current children cumulated CPU time (s) 988.11
Current children cumulated vsize (Kb) 121336

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36842 0 0 0 99626 158 0 0 25 0 1 0 1854812514 122097664 28964 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29809 28964 162 162 0 29647 0
[pid=26506] vsize: 119236
Current children cumulated CPU time (s) 998.11
Current children cumulated vsize (Kb) 121364

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36855 0 0 0 100626 158 0 0 25 0 1 0 1854812514 122146816 28977 4294967295 134512640 135167914 3221224432 3221223092 134567763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29821 28977 162 162 0 29659 0
[pid=26506] vsize: 119284
Current children cumulated CPU time (s) 1008.11
Current children cumulated vsize (Kb) 121412

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36864 0 0 0 101626 158 0 0 25 0 1 0 1854812514 122179584 28986 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29829 28986 162 162 0 29667 0
[pid=26506] vsize: 119316
Current children cumulated CPU time (s) 1018.11
Current children cumulated vsize (Kb) 121444

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36879 0 0 0 102626 158 0 0 25 0 1 0 1854812514 122236928 29001 4294967295 134512640 135167914 3221224432 3221223120 134566732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29843 29001 162 162 0 29681 0
[pid=26506] vsize: 119372
Current children cumulated CPU time (s) 1028.11
Current children cumulated vsize (Kb) 121500

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36886 0 0 0 103626 158 0 0 25 0 1 0 1854812514 122265600 29008 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29850 29008 162 162 0 29688 0
[pid=26506] vsize: 119400
Current children cumulated CPU time (s) 1038.11
Current children cumulated vsize (Kb) 121528

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36900 0 0 0 104625 159 0 0 25 0 1 0 1854812514 122318848 29022 4294967295 134512640 135167914 3221224432 3221223136 134562604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29863 29022 162 162 0 29701 0
[pid=26506] vsize: 119452
Current children cumulated CPU time (s) 1048.11
Current children cumulated vsize (Kb) 121580

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36910 0 0 0 105625 159 0 0 25 0 1 0 1854812514 122355712 29032 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29872 29032 162 162 0 29710 0
[pid=26506] vsize: 119488
Current children cumulated CPU time (s) 1058.11
Current children cumulated vsize (Kb) 121616

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36922 0 0 0 106625 159 0 0 25 0 1 0 1854812514 122400768 29044 4294967295 134512640 135167914 3221224432 3221223092 134567739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29883 29044 162 162 0 29721 0
[pid=26506] vsize: 119532
Current children cumulated CPU time (s) 1068.11
Current children cumulated vsize (Kb) 121660

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36933 0 0 0 107625 159 0 0 25 0 1 0 1854812514 122445824 29055 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29894 29055 162 162 0 29732 0
[pid=26506] vsize: 119576
Current children cumulated CPU time (s) 1078.11
Current children cumulated vsize (Kb) 121704

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36942 0 0 0 108625 159 0 0 25 0 1 0 1854812514 122478592 29064 4294967295 134512640 135167914 3221224432 3221223120 134566760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29902 29064 162 162 0 29740 0
[pid=26506] vsize: 119608
Current children cumulated CPU time (s) 1088.11
Current children cumulated vsize (Kb) 121736

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36955 0 0 0 109625 159 0 0 25 0 1 0 1854812514 122527744 29077 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29914 29077 162 162 0 29752 0
[pid=26506] vsize: 119656
Current children cumulated CPU time (s) 1098.11
Current children cumulated vsize (Kb) 121784

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36967 0 0 0 110624 160 0 0 25 0 1 0 1854812514 122576896 29089 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29926 29089 162 162 0 29764 0
[pid=26506] vsize: 119704
Current children cumulated CPU time (s) 1108.11
Current children cumulated vsize (Kb) 121832

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36977 0 0 0 111624 160 0 0 25 0 1 0 1854812514 122875904 29099 4294967295 134512640 135167914 3221224432 3221223136 134562604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 29999 29099 162 162 0 29837 0
[pid=26506] vsize: 119996
Current children cumulated CPU time (s) 1118.11
Current children cumulated vsize (Kb) 122124

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36987 0 0 0 112624 160 0 0 25 0 1 0 1854812514 122912768 29109 4294967295 134512640 135167914 3221224432 3221223136 134562647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30008 29109 162 162 0 29846 0
[pid=26506] vsize: 120032
Current children cumulated CPU time (s) 1128.11
Current children cumulated vsize (Kb) 122160

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36996 0 0 0 113625 160 0 0 25 0 1 0 1854812514 122949632 29118 4294967295 134512640 135167914 3221224432 3221223092 134567736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30017 29118 162 162 0 29855 0
[pid=26506] vsize: 120068
Current children cumulated CPU time (s) 1138.12
Current children cumulated vsize (Kb) 122196

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37009 0 0 0 114625 160 0 0 25 0 1 0 1854812514 122998784 29131 4294967295 134512640 135167914 3221224432 3221223136 134566393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30029 29131 162 162 0 29867 0
[pid=26506] vsize: 120116
Current children cumulated CPU time (s) 1148.12
Current children cumulated vsize (Kb) 122244

[startup+1160.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37024 0 0 0 115625 160 0 0 25 0 1 0 1854812514 123056128 29146 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30043 29146 162 162 0 29881 0
[pid=26506] vsize: 120172
Current children cumulated CPU time (s) 1158.12
Current children cumulated vsize (Kb) 122300

[startup+1170.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37034 0 0 0 116624 160 0 0 25 0 1 0 1854812514 123092992 29156 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30052 29156 162 162 0 29890 0
[pid=26506] vsize: 120208
Current children cumulated CPU time (s) 1168.11
Current children cumulated vsize (Kb) 122336

[startup+1180.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37043 0 0 0 117624 160 0 0 25 0 1 0 1854812514 123129856 29165 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30061 29165 162 162 0 29899 0
[pid=26506] vsize: 120244
Current children cumulated CPU time (s) 1178.11
Current children cumulated vsize (Kb) 122372

[startup+1190.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37059 0 0 0 118624 161 0 0 25 0 1 0 1854812514 123191296 29181 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30076 29181 162 162 0 29914 0
[pid=26506] vsize: 120304
Current children cumulated CPU time (s) 1188.12
Current children cumulated vsize (Kb) 122432

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37073 0 0 0 119624 161 0 0 25 0 1 0 1854812514 123244544 29195 4294967295 134512640 135167914 3221224432 3221223136 134562874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30089 29195 162 162 0 29927 0
[pid=26506] vsize: 120356
Current children cumulated CPU time (s) 1198.12
Current children cumulated vsize (Kb) 122484

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37089 0 0 0 120624 161 0 0 25 0 1 0 1854812514 123305984 29211 4294967295 134512640 135167914 3221224432 3221223136 134562556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30104 29211 162 162 0 29942 0
[pid=26506] vsize: 120416
Current children cumulated CPU time (s) 1208.12
Current children cumulated vsize (Kb) 122544



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.95 2/57 26506
Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26501/statm): 532 234 485 147 0 385 0
[pid=26501] vsize: 2128
Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37089 0 0 0 120624 161 0 0 25 0 1 0 1854812514 123305984 29211 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26506/statm): 30104 29211 162 162 0 29942 0
[pid=26506] vsize: 120416
Current children cumulated CPU time (s) 1208.12
Current children cumulated vsize (Kb) 122544

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1207.92
CPU user time (s): 1206.25
CPU system time (s): 1.67174
CPU usage (%): 99.8175
Max. virtual memory (cumulated for all children) (Kb): 122544

Verifier Data

ERROR: no interpretation found !