Some explanations

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

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core4872-1529.opb
MD5SUM7eea141e02c7a2753145fd63f1e9087d
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 253696000000000
Optimality of the best value was proved NO
Number of terms in the objective function 24865
Biggest coefficient in the objective function 52428800000000000
Number of bits for the biggest coefficient in the objective function 56
Sum of the numbers in the objective function 226690477012582900
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 1280000000000000000000
Number of bits of the biggest number in a constraint 71
Biggest sum of numbers in a constraint 1280226690477012549632
Number of bits of the biggest sum of numbers71
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1206.48
Number of variables24865
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 constraint24865

Trace number 6325

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        888236 kB
Buffers:         32976 kB
Cached:          85732 kB
SwapCached:        700 kB
Active:          47940 kB
Inactive:        73428 kB
HighTotal:      131008 kB
HighFree:        41384 kB
LowTotal:       903652 kB
LowFree:        846852 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            19380 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:55:06 (client local time) WITH STATUS 0 IN 1208.74 SECONDS
stats: 3487 7 1208.74 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      778     3.1 |  0.091 % |
c |       475 |  254172  1062419 |  112767     475     1456     3.1 |  0.091 % |
c |       812 |  254172  1062419 |  124044     812     2487     3.1 |  0.091 % |
c |      1318 |  254172  1062419 |  136448    1318     4056     3.1 |  0.091 % |
c |      2077 |  254172  1062419 |  150093    2077     6476     3.1 |  0.091 % |
c |      3216 |  254172  1062419 |  165103    3216     9993     3.1 |  0.091 % |
c |      4924 |  254172  1062419 |  181613    4924    15694     3.2 |  0.091 % |
c |      7487 |  254172  1062419 |  199774    7487    24396     3.3 |  0.091 % |
c |     11333 |  254172  1062419 |  219752   11333    37608     3.3 |  0.091 % |
c |     17099 |  254172  1062419 |  241727   17099    59148     3.5 |  0.091 % |
c |     25748 |  254172  1062419 |  265900   25748    92223     3.6 |  0.091 % |
c |     38722 |  254172  1062419 |  292490   38722   148384     3.8 |  0.091 % |
c |     58183 |  254172  1062419 |  321739   58183   255683     4.4 |  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/22739/stat): 22739 (minisat+_script) R 22738 22739 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797849082 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/22739/statm): 174 3 169 147 0 27 0
[pid=22739] 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=22740
New process pid=22741
New process pid=22742
execve syscall for /bin/sed executable
One traced child (pid=22741) 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=22742) exited with status: 0
One traced child (pid=22740) exited with status: 0
New process pid=22743
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-core4872-1529.opb
One traced child (pid=22743) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=22744
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-core4872-1529.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.95 0.90 1/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) T 22739 22739 1333 0 -1 0 3444 0 4 0 904 25 0 0 25 0 1 0 1797849119 14757888 3392 4294967295 134512640 135167914 3221224432 3221223272 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22744/statm): 3603 3392 162 162 0 3441 0
[pid=22744] vsize: 14412
Current children cumulated CPU time (s) 9.57
Current children cumulated vsize (Kb) 16540

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.95 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 8955 0 4 0 1857 50 0 0 25 0 1 0 1797849119 27009024 6385 4294967295 134512640 135167914 3221224432 3217706560 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6594 6385 162 162 0 6432 0
[pid=22744] vsize: 26376
Current children cumulated CPU time (s) 19.35
Current children cumulated vsize (Kb) 28504

[startup+30.0054 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 8996 0 4 0 2857 50 0 0 25 0 1 0 1797849119 27201536 6426 4294967295 134512640 135167914 3221224432 3218156540 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6641 6426 162 162 0 6479 0
[pid=22744] vsize: 26564
Current children cumulated CPU time (s) 29.35
Current children cumulated vsize (Kb) 28692

[startup+40.0061 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9041 0 4 0 3857 50 0 0 25 0 1 0 1797849119 27373568 6471 4294967295 134512640 135167914 3221224432 3218447856 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6683 6471 162 162 0 6521 0
[pid=22744] vsize: 26732
Current children cumulated CPU time (s) 39.35
Current children cumulated vsize (Kb) 28860

[startup+50.0067 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9044 0 4 0 4857 50 0 0 25 0 1 0 1797849119 27373568 6474 4294967295 134512640 135167914 3221224432 3218677388 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6683 6474 162 162 0 6521 0
[pid=22744] vsize: 26732
Current children cumulated CPU time (s) 49.35
Current children cumulated vsize (Kb) 28860

[startup+60.0074 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9047 0 4 0 5858 50 0 0 25 0 1 0 1797849119 27373568 6477 4294967295 134512640 135167914 3221224432 3218872012 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6683 6477 162 162 0 6521 0
[pid=22744] vsize: 26732
Current children cumulated CPU time (s) 59.36
Current children cumulated vsize (Kb) 28860

[startup+70.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9051 0 4 0 6858 50 0 0 25 0 1 0 1797849119 27385856 6481 4294967295 134512640 135167914 3221224432 3219043852 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6686 6481 162 162 0 6524 0
[pid=22744] vsize: 26744
Current children cumulated CPU time (s) 69.36
Current children cumulated vsize (Kb) 28872

[startup+80.0087 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 7858 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3218732716 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0
[pid=22744] vsize: 26940
Current children cumulated CPU time (s) 79.36
Current children cumulated vsize (Kb) 29068

[startup+90.0094 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 8858 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3218344656 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0
[pid=22744] vsize: 26940
Current children cumulated CPU time (s) 89.36
Current children cumulated vsize (Kb) 29068

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 9858 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3218179852 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0
[pid=22744] vsize: 26940
Current children cumulated CPU time (s) 99.36
Current children cumulated vsize (Kb) 29068

[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 10859 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3217994860 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0
[pid=22744] vsize: 26940
Current children cumulated CPU time (s) 109.37
Current children cumulated vsize (Kb) 29068

[startup+120.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 11859 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3217754952 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0
[pid=22744] vsize: 26940
Current children cumulated CPU time (s) 119.37
Current children cumulated vsize (Kb) 29068

[startup+130.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9078 0 4 0 12859 50 0 0 25 0 1 0 1797849119 27586560 6508 4294967295 134512640 135167914 3221224432 3217449836 134722229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6735 6508 162 162 0 6573 0
[pid=22744] vsize: 26940
Current children cumulated CPU time (s) 129.37
Current children cumulated vsize (Kb) 29068

[startup+140.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9231 0 4 0 13858 51 0 0 25 0 1 0 1797849119 28184576 6661 4294967295 134512640 135167914 3221224432 3217771532 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6881 6661 162 162 0 6719 0
[pid=22744] vsize: 27524
Current children cumulated CPU time (s) 139.37
Current children cumulated vsize (Kb) 29652

[startup+150.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9244 0 4 0 14858 51 0 0 25 0 1 0 1797849119 28188672 6674 4294967295 134512640 135167914 3221224432 3218700896 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6882 6674 162 162 0 6720 0
[pid=22744] vsize: 27528
Current children cumulated CPU time (s) 149.37
Current children cumulated vsize (Kb) 29656

[startup+160.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9268 0 4 0 15859 51 0 0 25 0 1 0 1797849119 28459008 6698 4294967295 134512640 135167914 3221224432 3218611152 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6948 6698 162 162 0 6786 0
[pid=22744] vsize: 27792
Current children cumulated CPU time (s) 159.38
Current children cumulated vsize (Kb) 29920

[startup+170.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9268 0 4 0 16859 51 0 0 25 0 1 0 1797849119 28459008 6698 4294967295 134512640 135167914 3221224432 3217686752 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 6948 6698 162 162 0 6786 0
[pid=22744] vsize: 27792
Current children cumulated CPU time (s) 169.38
Current children cumulated vsize (Kb) 29920

[startup+180.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9363 0 4 0 17858 51 0 0 25 0 1 0 1797849119 28819456 6793 4294967295 134512640 135167914 3221224432 3217755600 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7036 6793 162 162 0 6874 0
[pid=22744] vsize: 28144
Current children cumulated CPU time (s) 179.37
Current children cumulated vsize (Kb) 30272

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9578 0 4 0 18858 52 0 0 25 0 1 0 1797849119 29306880 6924 4294967295 134512640 135167914 3221224432 3218674220 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7155 6924 162 162 0 6993 0
[pid=22744] vsize: 28620
Current children cumulated CPU time (s) 189.38
Current children cumulated vsize (Kb) 30748

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9603 0 4 0 19858 52 0 0 25 0 1 0 1797849119 29384704 6949 4294967295 134512640 135167914 3221224432 3219026336 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7174 6949 162 162 0 7012 0
[pid=22744] vsize: 28696
Current children cumulated CPU time (s) 199.38
Current children cumulated vsize (Kb) 30824

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9603 0 4 0 20858 52 0 0 25 0 1 0 1797849119 29384704 6949 4294967295 134512640 135167914 3221224432 3218173120 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7174 6949 162 162 0 7012 0
[pid=22744] vsize: 28696
Current children cumulated CPU time (s) 209.38
Current children cumulated vsize (Kb) 30824

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9603 0 4 0 21858 52 0 0 25 0 1 0 1797849119 29384704 6949 4294967295 134512640 135167914 3221224432 3217769292 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7174 6949 162 162 0 7012 0
[pid=22744] vsize: 28696
Current children cumulated CPU time (s) 219.38
Current children cumulated vsize (Kb) 30824

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9653 0 4 0 22858 53 0 0 25 0 1 0 1797849119 29589504 6999 4294967295 134512640 135167914 3221224432 3217310512 134694419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7224 6999 162 162 0 7062 0
[pid=22744] vsize: 28896
Current children cumulated CPU time (s) 229.39
Current children cumulated vsize (Kb) 31024

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9725 0 4 0 23856 53 0 0 25 0 1 0 1797849119 29827072 7071 4294967295 134512640 135167914 3221224432 3218258416 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7282 7071 162 162 0 7120 0
[pid=22744] vsize: 29128
Current children cumulated CPU time (s) 239.37
Current children cumulated vsize (Kb) 31256

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9763 0 4 0 24856 53 0 0 25 0 1 0 1797849119 30339072 7109 4294967295 134512640 135167914 3221224432 3218984400 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7407 7109 162 162 0 7245 0
[pid=22744] vsize: 29628
Current children cumulated CPU time (s) 249.37
Current children cumulated vsize (Kb) 31756

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9772 0 4 0 25856 53 0 0 25 0 1 0 1797849119 30367744 7118 4294967295 134512640 135167914 3221224432 3217582608 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7414 7118 162 162 0 7252 0
[pid=22744] vsize: 29656
Current children cumulated CPU time (s) 259.37
Current children cumulated vsize (Kb) 31784

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 9896 0 4 0 26855 54 0 0 25 0 1 0 1797849119 30818304 7242 4294967295 134512640 135167914 3221224432 3218307312 134694419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7524 7242 162 162 0 7362 0
[pid=22744] vsize: 30096
Current children cumulated CPU time (s) 269.37
Current children cumulated vsize (Kb) 32224

[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10261 0 4 0 27854 55 0 0 25 0 1 0 1797849119 31936512 7524 4294967295 134512640 135167914 3221224432 3218944160 134524005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7797 7524 162 162 0 7635 0
[pid=22744] vsize: 31188
Current children cumulated CPU time (s) 279.37
Current children cumulated vsize (Kb) 33316

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10272 0 4 0 28854 55 0 0 25 0 1 0 1797849119 31629312 7452 4294967295 134512640 135167914 3221224432 3218831244 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7722 7452 162 162 0 7560 0
[pid=22744] vsize: 30888
Current children cumulated CPU time (s) 289.37
Current children cumulated vsize (Kb) 33016

[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10272 0 4 0 29854 55 0 0 25 0 1 0 1797849119 31629312 7452 4294967295 134512640 135167914 3221224432 3218484880 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7722 7452 162 162 0 7560 0
[pid=22744] vsize: 30888
Current children cumulated CPU time (s) 299.37
Current children cumulated vsize (Kb) 33016

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10272 0 4 0 30855 55 0 0 25 0 1 0 1797849119 31629312 7452 4294967295 134512640 135167914 3221224432 3218067504 134844723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7722 7452 162 162 0 7560 0
[pid=22744] vsize: 30888
Current children cumulated CPU time (s) 309.38
Current children cumulated vsize (Kb) 33016

[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10282 0 4 0 31855 55 0 0 25 0 1 0 1797849119 31670272 7462 4294967295 134512640 135167914 3221224432 3217502172 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7732 7462 162 162 0 7570 0
[pid=22744] vsize: 30928
Current children cumulated CPU time (s) 319.38
Current children cumulated vsize (Kb) 33056

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10373 0 4 0 32854 55 0 0 25 0 1 0 1797849119 32010240 7553 4294967295 134512640 135167914 3221224432 3217884320 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7815 7553 162 162 0 7653 0
[pid=22744] vsize: 31260
Current children cumulated CPU time (s) 329.37
Current children cumulated vsize (Kb) 33388

[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10412 0 4 0 33854 55 0 0 25 0 1 0 1797849119 32129024 7592 4294967295 134512640 135167914 3221224432 3218628224 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7844 7592 162 162 0 7682 0
[pid=22744] vsize: 31376
Current children cumulated CPU time (s) 339.37
Current children cumulated vsize (Kb) 33504

[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10441 0 4 0 34854 55 0 0 25 0 1 0 1797849119 32219136 7621 4294967295 134512640 135167914 3221224432 3218949888 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7866 7621 162 162 0 7704 0
[pid=22744] vsize: 31464
Current children cumulated CPU time (s) 349.37
Current children cumulated vsize (Kb) 33592

[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10441 0 4 0 35854 55 0 0 25 0 1 0 1797849119 32219136 7621 4294967295 134512640 135167914 3221224432 3217823920 134694439 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7866 7621 162 162 0 7704 0
[pid=22744] vsize: 31464
Current children cumulated CPU time (s) 359.37
Current children cumulated vsize (Kb) 33592

[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10526 0 4 0 36853 56 0 0 25 0 1 0 1797849119 32550912 7706 4294967295 134512640 135167914 3221224432 3217585608 134694369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7947 7706 162 162 0 7785 0
[pid=22744] vsize: 31788
Current children cumulated CPU time (s) 369.37
Current children cumulated vsize (Kb) 33916

[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10578 0 4 0 37852 56 0 0 25 0 1 0 1797849119 32710656 7758 4294967295 134512640 135167914 3221224432 3218555072 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 7986 7758 162 162 0 7824 0
[pid=22744] vsize: 31944
Current children cumulated CPU time (s) 379.36
Current children cumulated vsize (Kb) 34072

[startup+390.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 10639 0 4 0 38852 57 0 0 25 0 1 0 1797849119 32919552 7654 4294967295 134512640 135167914 3221224432 3221222384 134523161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 8037 7654 162 162 0 7875 0
[pid=22744] vsize: 32148
Current children cumulated CPU time (s) 389.37
Current children cumulated vsize (Kb) 34276

[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36239 0 4 0 39720 139 0 0 25 0 1 0 1797849119 119693312 28376 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22744/statm): 29222 28376 162 162 0 29060 0
[pid=22744] vsize: 116888
Current children cumulated CPU time (s) 398.87
Current children cumulated vsize (Kb) 119016

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36290 0 4 0 40718 140 0 0 25 0 1 0 1797849119 119910400 28427 4294967295 134512640 135167914 3221224432 3221223104 134567641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29275 28427 162 162 0 29113 0
[pid=22744] vsize: 117100
Current children cumulated CPU time (s) 408.86
Current children cumulated vsize (Kb) 119228

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36300 0 4 0 41719 140 0 0 25 0 1 0 1797849119 119947264 28437 4294967295 134512640 135167914 3221224432 3221223136 134562877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29284 28437 162 162 0 29122 0
[pid=22744] vsize: 117136
Current children cumulated CPU time (s) 418.87
Current children cumulated vsize (Kb) 119264

[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36312 0 4 0 42719 140 0 0 25 0 1 0 1797849119 119988224 28449 4294967295 134512640 135167914 3221224432 3221223232 134563952 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29294 28449 162 162 0 29132 0
[pid=22744] vsize: 117176
Current children cumulated CPU time (s) 428.87
Current children cumulated vsize (Kb) 119304

[startup+440.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36332 0 4 0 43719 140 0 0 25 0 1 0 1797849119 120094720 28469 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29320 28469 162 162 0 29158 0
[pid=22744] vsize: 117280
Current children cumulated CPU time (s) 438.87
Current children cumulated vsize (Kb) 119408

[startup+450.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36338 0 4 0 44719 140 0 0 25 0 1 0 1797849119 120102912 28475 4294967295 134512640 135167914 3221224432 3221223092 134567725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29322 28475 162 162 0 29160 0
[pid=22744] vsize: 117288
Current children cumulated CPU time (s) 448.87
Current children cumulated vsize (Kb) 119416

[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36349 0 4 0 45719 140 0 0 25 0 1 0 1797849119 120139776 28486 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29331 28486 162 162 0 29169 0
[pid=22744] vsize: 117324
Current children cumulated CPU time (s) 458.87
Current children cumulated vsize (Kb) 119452

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36358 0 4 0 46719 140 0 0 25 0 1 0 1797849119 120172544 28495 4294967295 134512640 135167914 3221224432 3221223136 134566390 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29339 28495 162 162 0 29177 0
[pid=22744] vsize: 117356
Current children cumulated CPU time (s) 468.87
Current children cumulated vsize (Kb) 119484

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36370 0 4 0 47719 140 0 0 25 0 1 0 1797849119 120213504 28507 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29349 28507 162 162 0 29187 0
[pid=22744] vsize: 117396
Current children cumulated CPU time (s) 478.87
Current children cumulated vsize (Kb) 119524

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36379 0 4 0 48719 140 0 0 25 0 1 0 1797849119 120246272 28516 4294967295 134512640 135167914 3221224432 3221223092 134567739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22744/statm): 29357 28516 162 162 0 29195 0
[pid=22744] vsize: 117428
Current children cumulated CPU time (s) 488.87
Current children cumulated vsize (Kb) 119556

[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36389 0 4 0 49718 141 0 0 25 0 1 0 1797849119 120283136 28526 4294967295 134512640 135167914 3221224432 3221223092 134567745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29366 28526 162 162 0 29204 0
[pid=22744] vsize: 117464
Current children cumulated CPU time (s) 498.87
Current children cumulated vsize (Kb) 119592

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36416 0 4 0 50718 141 0 0 25 0 1 0 1797849119 120451072 28553 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29407 28553 162 162 0 29245 0
[pid=22744] vsize: 117628
Current children cumulated CPU time (s) 508.87
Current children cumulated vsize (Kb) 119756

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36417 0 4 0 51719 141 0 0 25 0 1 0 1797849119 120451072 28554 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29407 28554 162 162 0 29245 0
[pid=22744] vsize: 117628
Current children cumulated CPU time (s) 518.88
Current children cumulated vsize (Kb) 119756

[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36418 0 4 0 52719 141 0 0 25 0 1 0 1797849119 120451072 28555 4294967295 134512640 135167914 3221224432 3221223092 134567725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29407 28555 162 162 0 29245 0
[pid=22744] vsize: 117628
Current children cumulated CPU time (s) 528.88
Current children cumulated vsize (Kb) 119756

[startup+540.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36425 0 4 0 53719 141 0 0 25 0 1 0 1797849119 120475648 28562 4294967295 134512640 135167914 3221224432 3221223092 134567777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29413 28562 162 162 0 29251 0
[pid=22744] vsize: 117652
Current children cumulated CPU time (s) 538.88
Current children cumulated vsize (Kb) 119780

[startup+550.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36434 0 4 0 54719 141 0 0 25 0 1 0 1797849119 120508416 28571 4294967295 134512640 135167914 3221224432 3221223204 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29421 28571 162 162 0 29259 0
[pid=22744] vsize: 117684
Current children cumulated CPU time (s) 548.88
Current children cumulated vsize (Kb) 119812

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36443 0 4 0 55719 141 0 0 25 0 1 0 1797849119 120541184 28580 4294967295 134512640 135167914 3221224432 3221223168 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29429 28580 162 162 0 29267 0
[pid=22744] vsize: 117716
Current children cumulated CPU time (s) 558.88
Current children cumulated vsize (Kb) 119844

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36451 0 4 0 56719 141 0 0 25 0 1 0 1797849119 120569856 28588 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29436 28588 162 162 0 29274 0
[pid=22744] vsize: 117744
Current children cumulated CPU time (s) 568.88
Current children cumulated vsize (Kb) 119872

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36461 0 4 0 57719 142 0 0 25 0 1 0 1797849119 120606720 28598 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29445 28598 162 162 0 29283 0
[pid=22744] vsize: 117780
Current children cumulated CPU time (s) 578.89
Current children cumulated vsize (Kb) 119908

[startup+590.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36469 0 4 0 58719 142 0 0 25 0 1 0 1797849119 120635392 28606 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29452 28606 162 162 0 29290 0
[pid=22744] vsize: 117808
Current children cumulated CPU time (s) 588.89
Current children cumulated vsize (Kb) 119936

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36478 0 4 0 59719 142 0 0 25 0 1 0 1797849119 120668160 28615 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29460 28615 162 162 0 29298 0
[pid=22744] vsize: 117840
Current children cumulated CPU time (s) 598.89
Current children cumulated vsize (Kb) 119968

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36489 0 4 0 60718 142 0 0 25 0 1 0 1797849119 120709120 28626 4294967295 134512640 135167914 3221224432 3221223184 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29470 28626 162 162 0 29308 0
[pid=22744] vsize: 117880
Current children cumulated CPU time (s) 608.88
Current children cumulated vsize (Kb) 120008

[startup+620.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36500 0 4 0 61718 142 0 0 25 0 1 0 1797849119 120750080 28637 4294967295 134512640 135167914 3221224432 3221223092 134567793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29480 28637 162 162 0 29318 0
[pid=22744] vsize: 117920
Current children cumulated CPU time (s) 618.88
Current children cumulated vsize (Kb) 120048

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36516 0 4 0 62718 142 0 0 25 0 1 0 1797849119 120811520 28653 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29495 28653 162 162 0 29333 0
[pid=22744] vsize: 117980
Current children cumulated CPU time (s) 628.88
Current children cumulated vsize (Kb) 120108

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36527 0 4 0 63718 142 0 0 25 0 1 0 1797849119 120852480 28664 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29505 28664 162 162 0 29343 0
[pid=22744] vsize: 118020
Current children cumulated CPU time (s) 638.88
Current children cumulated vsize (Kb) 120148

[startup+650.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36536 0 4 0 64719 142 0 0 25 0 1 0 1797849119 120885248 28673 4294967295 134512640 135167914 3221224432 3221223136 134562869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29513 28673 162 162 0 29351 0
[pid=22744] vsize: 118052
Current children cumulated CPU time (s) 648.89
Current children cumulated vsize (Kb) 120180

[startup+660.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36544 0 4 0 65719 142 0 0 25 0 1 0 1797849119 120913920 28681 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29520 28681 162 162 0 29358 0
[pid=22744] vsize: 118080
Current children cumulated CPU time (s) 658.89
Current children cumulated vsize (Kb) 120208

[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36552 0 4 0 66719 142 0 0 25 0 1 0 1797849119 120946688 28689 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29528 28689 162 162 0 29366 0
[pid=22744] vsize: 118112
Current children cumulated CPU time (s) 668.89
Current children cumulated vsize (Kb) 120240

[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36586 0 4 0 67719 142 0 0 25 0 1 0 1797849119 121212928 28723 4294967295 134512640 135167914 3221224432 3221223120 134566738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29593 28723 162 162 0 29431 0
[pid=22744] vsize: 118372
Current children cumulated CPU time (s) 678.89
Current children cumulated vsize (Kb) 120500

[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36587 0 4 0 68719 142 0 0 25 0 1 0 1797849119 121212928 28724 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29593 28724 162 162 0 29431 0
[pid=22744] vsize: 118372
Current children cumulated CPU time (s) 688.89
Current children cumulated vsize (Kb) 120500

[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36588 0 4 0 69719 142 0 0 25 0 1 0 1797849119 121212928 28725 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29593 28725 162 162 0 29431 0
[pid=22744] vsize: 118372
Current children cumulated CPU time (s) 698.89
Current children cumulated vsize (Kb) 120500

[startup+710.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36589 0 4 0 70720 142 0 0 25 0 1 0 1797849119 121212928 28726 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29593 28726 162 162 0 29431 0
[pid=22744] vsize: 118372
Current children cumulated CPU time (s) 708.9
Current children cumulated vsize (Kb) 120500

[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36592 0 4 0 71720 142 0 0 25 0 1 0 1797849119 121221120 28729 4294967295 134512640 135167914 3221224432 3221223092 134567766 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29595 28729 162 162 0 29433 0
[pid=22744] vsize: 118380
Current children cumulated CPU time (s) 718.9
Current children cumulated vsize (Kb) 120508

[startup+730.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36600 0 4 0 72720 142 0 0 25 0 1 0 1797849119 121253888 28737 4294967295 134512640 135167914 3221224432 3221223168 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29603 28737 162 162 0 29441 0
[pid=22744] vsize: 118412
Current children cumulated CPU time (s) 728.9
Current children cumulated vsize (Kb) 120540

[startup+740.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36608 0 4 0 73720 142 0 0 25 0 1 0 1797849119 121282560 28745 4294967295 134512640 135167914 3221224432 3221223168 134559387 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29610 28745 162 162 0 29448 0
[pid=22744] vsize: 118440
Current children cumulated CPU time (s) 738.9
Current children cumulated vsize (Kb) 120568

[startup+750.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36618 0 4 0 74720 143 0 0 25 0 1 0 1797849119 121319424 28755 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29619 28755 162 162 0 29457 0
[pid=22744] vsize: 118476
Current children cumulated CPU time (s) 748.91
Current children cumulated vsize (Kb) 120604

[startup+760.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36625 0 4 0 75720 143 0 0 25 0 1 0 1797849119 121344000 28762 4294967295 134512640 135167914 3221224432 3221223092 134567777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29625 28762 162 162 0 29463 0
[pid=22744] vsize: 118500
Current children cumulated CPU time (s) 758.91
Current children cumulated vsize (Kb) 120628

[startup+770.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36631 0 4 0 76720 143 0 0 25 0 1 0 1797849119 121364480 28768 4294967295 134512640 135167914 3221224432 3221223120 134566713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29630 28768 162 162 0 29468 0
[pid=22744] vsize: 118520
Current children cumulated CPU time (s) 768.91
Current children cumulated vsize (Kb) 120648

[startup+780.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36638 0 4 0 77720 143 0 0 25 0 1 0 1797849119 121393152 28775 4294967295 134512640 135167914 3221224432 3221223120 134566766 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29637 28775 162 162 0 29475 0
[pid=22744] vsize: 118548
Current children cumulated CPU time (s) 778.91
Current children cumulated vsize (Kb) 120676

[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36648 0 4 0 78720 143 0 0 25 0 1 0 1797849119 121430016 28785 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29646 28785 162 162 0 29484 0
[pid=22744] vsize: 118584
Current children cumulated CPU time (s) 788.91
Current children cumulated vsize (Kb) 120712

[startup+800.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36655 0 4 0 79720 143 0 0 25 0 1 0 1797849119 121454592 28792 4294967295 134512640 135167914 3221224432 3221223120 134566741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29652 28792 162 162 0 29490 0
[pid=22744] vsize: 118608
Current children cumulated CPU time (s) 798.91
Current children cumulated vsize (Kb) 120736

[startup+810.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36663 0 4 0 80720 143 0 0 25 0 1 0 1797849119 121483264 28800 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29659 28800 162 162 0 29497 0
[pid=22744] vsize: 118636
Current children cumulated CPU time (s) 808.91
Current children cumulated vsize (Kb) 120764

[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36672 0 4 0 81720 143 0 0 25 0 1 0 1797849119 121520128 28809 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29668 28809 162 162 0 29506 0
[pid=22744] vsize: 118672
Current children cumulated CPU time (s) 818.91
Current children cumulated vsize (Kb) 120800

[startup+830.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36684 0 4 0 82720 143 0 0 25 0 1 0 1797849119 121565184 28821 4294967295 134512640 135167914 3221224432 3221223168 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29679 28821 162 162 0 29517 0
[pid=22744] vsize: 118716
Current children cumulated CPU time (s) 828.91
Current children cumulated vsize (Kb) 120844

[startup+840.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36692 0 4 0 83720 144 0 0 25 0 1 0 1797849119 121593856 28829 4294967295 134512640 135167914 3221224432 3221223136 134562669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29686 28829 162 162 0 29524 0
[pid=22744] vsize: 118744
Current children cumulated CPU time (s) 838.92
Current children cumulated vsize (Kb) 120872

[startup+850.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36699 0 4 0 84720 144 0 0 25 0 1 0 1797849119 121618432 28836 4294967295 134512640 135167914 3221224432 3221223092 134567777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29692 28836 162 162 0 29530 0
[pid=22744] vsize: 118768
Current children cumulated CPU time (s) 848.92
Current children cumulated vsize (Kb) 120896

[startup+860.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36710 0 4 0 85720 144 0 0 25 0 1 0 1797849119 121659392 28847 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29702 28847 162 162 0 29540 0
[pid=22744] vsize: 118808
Current children cumulated CPU time (s) 858.92
Current children cumulated vsize (Kb) 120936

[startup+870.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36721 0 4 0 86720 144 0 0 25 0 1 0 1797849119 121700352 28858 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29712 28858 162 162 0 29550 0
[pid=22744] vsize: 118848
Current children cumulated CPU time (s) 868.92
Current children cumulated vsize (Kb) 120976

[startup+880.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36727 0 4 0 87721 144 0 0 25 0 1 0 1797849119 121724928 28864 4294967295 134512640 135167914 3221224432 3221223136 134566404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29718 28864 162 162 0 29556 0
[pid=22744] vsize: 118872
Current children cumulated CPU time (s) 878.93
Current children cumulated vsize (Kb) 121000

[startup+890.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36734 0 4 0 88721 144 0 0 25 0 1 0 1797849119 121749504 28871 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29724 28871 162 162 0 29562 0
[pid=22744] vsize: 118896
Current children cumulated CPU time (s) 888.93
Current children cumulated vsize (Kb) 121024

[startup+900.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36747 0 4 0 89721 144 0 0 25 0 1 0 1797849119 121798656 28884 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29736 28884 162 162 0 29574 0
[pid=22744] vsize: 118944
Current children cumulated CPU time (s) 898.93
Current children cumulated vsize (Kb) 121072

[startup+910.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36754 0 4 0 90721 144 0 0 25 0 1 0 1797849119 121827328 28891 4294967295 134512640 135167914 3221224432 3221223220 134563911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29743 28891 162 162 0 29581 0
[pid=22744] vsize: 118972
Current children cumulated CPU time (s) 908.93
Current children cumulated vsize (Kb) 121100

[startup+920.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36760 0 4 0 91721 144 0 0 25 0 1 0 1797849119 121847808 28897 4294967295 134512640 135167914 3221224432 3221223092 134567680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29748 28897 162 162 0 29586 0
[pid=22744] vsize: 118992
Current children cumulated CPU time (s) 918.93
Current children cumulated vsize (Kb) 121120

[startup+930.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36770 0 4 0 92721 144 0 0 25 0 1 0 1797849119 121884672 28907 4294967295 134512640 135167914 3221224432 3221223168 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29757 28907 162 162 0 29595 0
[pid=22744] vsize: 119028
Current children cumulated CPU time (s) 928.93
Current children cumulated vsize (Kb) 121156

[startup+940.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36783 0 4 0 93721 144 0 0 25 0 1 0 1797849119 121933824 28920 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29769 28920 162 162 0 29607 0
[pid=22744] vsize: 119076
Current children cumulated CPU time (s) 938.93
Current children cumulated vsize (Kb) 121204

[startup+950.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36790 0 4 0 94722 144 0 0 25 0 1 0 1797849119 121962496 28927 4294967295 134512640 135167914 3221224432 3221223136 134566167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29776 28927 162 162 0 29614 0
[pid=22744] vsize: 119104
Current children cumulated CPU time (s) 948.94
Current children cumulated vsize (Kb) 121232

[startup+960.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36797 0 4 0 95722 144 0 0 25 0 1 0 1797849119 121987072 28934 4294967295 134512640 135167914 3221224432 3221223104 134562347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29782 28934 162 162 0 29620 0
[pid=22744] vsize: 119128
Current children cumulated CPU time (s) 958.94
Current children cumulated vsize (Kb) 121256

[startup+970.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36809 0 4 0 96722 144 0 0 25 0 1 0 1797849119 122032128 28946 4294967295 134512640 135167914 3221224432 3221223136 134562682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29793 28946 162 162 0 29631 0
[pid=22744] vsize: 119172
Current children cumulated CPU time (s) 968.94
Current children cumulated vsize (Kb) 121300

[startup+980.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36825 0 4 0 97722 144 0 0 25 0 1 0 1797849119 122093568 28962 4294967295 134512640 135167914 3221224432 3221223092 134567680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29808 28962 162 162 0 29646 0
[pid=22744] vsize: 119232
Current children cumulated CPU time (s) 978.94
Current children cumulated vsize (Kb) 121360

[startup+990.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36850 0 4 0 98721 145 0 0 25 0 1 0 1797849119 122191872 28987 4294967295 134512640 135167914 3221224432 3221223104 134566760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29832 28987 162 162 0 29670 0
[pid=22744] vsize: 119328
Current children cumulated CPU time (s) 988.94
Current children cumulated vsize (Kb) 121456

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36859 0 4 0 99721 145 0 0 25 0 1 0 1797849119 122228736 28996 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29841 28996 162 162 0 29679 0
[pid=22744] vsize: 119364
Current children cumulated CPU time (s) 998.94
Current children cumulated vsize (Kb) 121492

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36873 0 4 0 100721 145 0 0 25 0 1 0 1797849119 122281984 29010 4294967295 134512640 135167914 3221224432 3221223132 134566190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29854 29010 162 162 0 29692 0
[pid=22744] vsize: 119416
Current children cumulated CPU time (s) 1008.94
Current children cumulated vsize (Kb) 121544

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36887 0 4 0 101721 145 0 0 25 0 1 0 1797849119 122335232 29024 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29867 29024 162 162 0 29705 0
[pid=22744] vsize: 119468
Current children cumulated CPU time (s) 1018.94
Current children cumulated vsize (Kb) 121596

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36902 0 4 0 102721 145 0 0 25 0 1 0 1797849119 122392576 29039 4294967295 134512640 135167914 3221224432 3221223136 134566158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29881 29039 162 162 0 29719 0
[pid=22744] vsize: 119524
Current children cumulated CPU time (s) 1028.94
Current children cumulated vsize (Kb) 121652

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36913 0 4 0 103721 145 0 0 25 0 1 0 1797849119 122433536 29050 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29891 29050 162 162 0 29729 0
[pid=22744] vsize: 119564
Current children cumulated CPU time (s) 1038.94
Current children cumulated vsize (Kb) 121692

[startup+1050.07 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36924 0 4 0 104721 145 0 0 25 0 1 0 1797849119 122478592 29061 4294967295 134512640 135167914 3221224432 3221223136 134562604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29902 29061 162 162 0 29740 0
[pid=22744] vsize: 119608
Current children cumulated CPU time (s) 1048.94
Current children cumulated vsize (Kb) 121736

[startup+1060.07 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36937 0 4 0 105721 145 0 0 25 0 1 0 1797849119 122527744 29074 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29914 29074 162 162 0 29752 0
[pid=22744] vsize: 119656
Current children cumulated CPU time (s) 1058.94
Current children cumulated vsize (Kb) 121784

[startup+1070.07 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36949 0 4 0 106721 145 0 0 25 0 1 0 1797849119 122572800 29086 4294967295 134512640 135167914 3221224432 3221223136 134566242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 29925 29086 162 162 0 29763 0
[pid=22744] vsize: 119700
Current children cumulated CPU time (s) 1068.94
Current children cumulated vsize (Kb) 121828

[startup+1080.07 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36963 0 4 0 107721 145 0 0 25 0 1 0 1797849119 122888192 29100 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30002 29100 162 162 0 29840 0
[pid=22744] vsize: 120008
Current children cumulated CPU time (s) 1078.94
Current children cumulated vsize (Kb) 122136

[startup+1090.07 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36974 0 4 0 108721 145 0 0 25 0 1 0 1797849119 122933248 29111 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30013 29111 162 162 0 29851 0
[pid=22744] vsize: 120052
Current children cumulated CPU time (s) 1088.94
Current children cumulated vsize (Kb) 122180

[startup+1100.07 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 36986 0 4 0 109721 145 0 0 25 0 1 0 1797849119 122978304 29123 4294967295 134512640 135167914 3221224432 3221223112 134562294 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30024 29123 162 162 0 29862 0
[pid=22744] vsize: 120096
Current children cumulated CPU time (s) 1098.94
Current children cumulated vsize (Kb) 122224

[startup+1110.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37003 0 4 0 110722 145 0 0 25 0 1 0 1797849119 123043840 29140 4294967295 134512640 135167914 3221224432 3221223120 134566795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30040 29140 162 162 0 29878 0
[pid=22744] vsize: 120160
Current children cumulated CPU time (s) 1108.95
Current children cumulated vsize (Kb) 122288

[startup+1120.08 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37012 0 4 0 111722 145 0 0 25 0 1 0 1797849119 123076608 29149 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30048 29149 162 162 0 29886 0
[pid=22744] vsize: 120192
Current children cumulated CPU time (s) 1118.95
Current children cumulated vsize (Kb) 122320

[startup+1130.08 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37024 0 4 0 112722 146 0 0 25 0 1 0 1797849119 123125760 29161 4294967295 134512640 135167914 3221224432 3221223136 134562869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30060 29161 162 162 0 29898 0
[pid=22744] vsize: 120240
Current children cumulated CPU time (s) 1128.96
Current children cumulated vsize (Kb) 122368

[startup+1140.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37044 0 4 0 113721 146 0 0 25 0 1 0 1797849119 123203584 29181 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30079 29181 162 162 0 29917 0
[pid=22744] vsize: 120316
Current children cumulated CPU time (s) 1138.95
Current children cumulated vsize (Kb) 122444

[startup+1150.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37056 0 4 0 114721 146 0 0 25 0 1 0 1797849119 123248640 29193 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30090 29193 162 162 0 29928 0
[pid=22744] vsize: 120360
Current children cumulated CPU time (s) 1148.95
Current children cumulated vsize (Kb) 122488

[startup+1160.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37067 0 4 0 115722 146 0 0 25 0 1 0 1797849119 123289600 29204 4294967295 134512640 135167914 3221224432 3221223092 134567760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30100 29204 162 162 0 29938 0
[pid=22744] vsize: 120400
Current children cumulated CPU time (s) 1158.96
Current children cumulated vsize (Kb) 122528

[startup+1170.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37083 0 4 0 116721 146 0 0 25 0 1 0 1797849119 123351040 29220 4294967295 134512640 135167914 3221224432 3221223136 134562502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30115 29220 162 162 0 29953 0
[pid=22744] vsize: 120460
Current children cumulated CPU time (s) 1168.95
Current children cumulated vsize (Kb) 122588

[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37104 0 4 0 117721 146 0 0 25 0 1 0 1797849119 123432960 29241 4294967295 134512640 135167914 3221224432 3221223168 134559387 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30135 29241 162 162 0 29973 0
[pid=22744] vsize: 120540
Current children cumulated CPU time (s) 1178.95
Current children cumulated vsize (Kb) 122668

[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37121 0 4 0 118721 146 0 0 25 0 1 0 1797849119 123502592 29258 4294967295 134512640 135167914 3221224432 3221223092 134567699 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30152 29258 162 162 0 29990 0
[pid=22744] vsize: 120608
Current children cumulated CPU time (s) 1188.95
Current children cumulated vsize (Kb) 122736

[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37137 0 4 0 119721 146 0 0 25 0 1 0 1797849119 123564032 29274 4294967295 134512640 135167914 3221224432 3221223092 134567699 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30167 29274 162 162 0 30005 0
[pid=22744] vsize: 120668
Current children cumulated CPU time (s) 1198.95
Current children cumulated vsize (Kb) 122796

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37156 0 4 0 120721 147 0 0 25 0 1 0 1797849119 123637760 29293 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30185 29293 162 162 0 30023 0
[pid=22744] vsize: 120740
Current children cumulated CPU time (s) 1208.96
Current children cumulated vsize (Kb) 122868



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 22744
Raw data (/proc/22739/stat): 22739 (minisat+_script) S 22738 22739 1333 0 -1 0 314 1251 0 0 0 1 19 8 17 0 1 0 1797849082 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22739/statm): 532 234 485 147 0 385 0
[pid=22739] vsize: 2128
Raw data (/proc/22744/stat): 22744 (minisat+_bignum) R 22739 22739 1333 0 -1 0 37156 0 4 0 120721 147 0 0 25 0 1 0 1797849119 123637760 29293 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22744/statm): 30185 29293 162 162 0 30023 0
[pid=22744] vsize: 120740
Current children cumulated CPU time (s) 1208.96
Current children cumulated vsize (Kb) 122868

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1208.74
CPU user time (s): 1207.21
CPU system time (s): 1.52477
CPU usage (%): 99.8842
Max. virtual memory (cumulated for all children) (Kb): 122868

Verifier Data

ERROR: no interpretation found !