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/MIPLIB/miplib/normalized-mps-v2-13-7-modglob.opb
MD5SUM6a1cb641fd0d264267e84120b98acbe3
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 6578
Biggest coefficient in the objective function 21493710848000000
Number of bits for the biggest coefficient in the objective function 55
Sum of the numbers in the objective function 1450509811657714210
Number of bits of the sum of numbers in the objective function 61
Biggest number in a constraint 21493710848000000
Number of bits of the biggest number in a constraint 55
Biggest sum of numbers in a constraint 1450509811657714210
Number of bits of the biggest sum of numbers61
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables6578
Total number of constraints389
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)98
Number of constraints which are nor clauses,nor cardinality constraints291
Minimum length of a constraint1
Maximum length of a constraint180

Trace number 6098

Launcher Data

LAUNCH ON wulflinc25 THE 2005-09-20 03:16:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3254 boxname=wulflinc25 idbench=910 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6a1cb641fd0d264267e84120b98acbe3  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-modglob.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-modglob.opb
IDLAUNCH: 3254
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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	: 3
cpu MHz		: 451.220
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:        917408 kB
Buffers:          7764 kB
Cached:          81688 kB
SwapCached:        852 kB
Active:          20484 kB
Inactive:        71564 kB
HighTotal:      131008 kB
HighFree:        45948 kB
LowTotal:       903652 kB
LowFree:        871460 kB
SwapTotal:     2097892 kB
SwapFree:      2096524 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            19392 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:36:37 (client local time) WITH STATUS 0 IN 1206.54 SECONDS
stats: 3254 7 1206.54 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 426] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...

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/27219/stat): 27219 (minisat+_script) R 27218 27219 4419 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855253322 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27219/statm): 174 3 169 147 0 27 0
[pid=27219] 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=27220
New process pid=27221
New process pid=27222
execve syscall for /bin/sed executable
One traced child (pid=27221) 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=27222) exited with status: 0
One traced child (pid=27220) exited with status: 0
New process pid=27223
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-modglob.opb
One traced child (pid=27223) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=27224
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-modglob.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 5497 0 0 0 941 25 0 0 25 0 1 0 1855253328 20221952 4824 4294967295 134512640 135167914 3221224448 3221205024 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27224/statm): 4937 4824 162 162 0 4775 0
[pid=27224] vsize: 19748
Current children cumulated CPU time (s) 9.68
Current children cumulated vsize (Kb) 21876

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) T 27219 27219 4419 0 -1 0 11115 0 0 0 1888 48 0 0 25 0 1 0 1855253328 40534016 9783 4294967295 134512640 135167914 3221224448 3221201148 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27224/statm): 9896 9783 162 162 0 9734 0
[pid=27224] vsize: 39584
Current children cumulated CPU time (s) 19.38
Current children cumulated vsize (Kb) 41712

[startup+30.0054 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 17825 0 0 0 2838 73 0 0 25 0 1 0 1855253328 62619648 15175 4294967295 134512640 135167914 3221224448 3221204832 134695973 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27224/statm): 15288 15175 162 162 0 15126 0
[pid=27224] vsize: 61152
Current children cumulated CPU time (s) 29.13
Current children cumulated vsize (Kb) 63280

[startup+40.006 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 27253 0 0 0 3778 105 0 0 25 0 1 0 1855253328 101236736 24603 4294967295 134512640 135167914 3221224448 3221203104 134625512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27224/statm): 24716 24603 162 162 0 24554 0
[pid=27224] vsize: 98864
Current children cumulated CPU time (s) 38.85
Current children cumulated vsize (Kb) 100992

[startup+50.0066 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 30992 0 0 0 4734 123 0 0 25 0 1 0 1855253328 105750528 25705 4294967295 134512640 135167914 3221224448 3221201552 134621109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 25818 25705 162 162 0 25656 0
[pid=27224] vsize: 103272
Current children cumulated CPU time (s) 48.59
Current children cumulated vsize (Kb) 105400

[startup+60.0072 s]
Raw data (loadavg): 0.97 0.97 0.91 1/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) T 27219 27219 4419 0 -1 0 35456 0 0 0 5686 142 0 0 25 0 1 0 1855253328 124035072 30169 4294967295 134512640 135167914 3221224448 3221202812 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27224/statm): 30282 30169 162 162 0 30120 0
[pid=27224] vsize: 121128
Current children cumulated CPU time (s) 58.3
Current children cumulated vsize (Kb) 123256

[startup+70.0078 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 39830 0 0 0 6637 162 0 0 25 0 1 0 1855253328 141950976 34543 4294967295 134512640 135167914 3221224448 3221202428 134522361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27224/statm): 34656 34543 162 162 0 34494 0
[pid=27224] vsize: 138624
Current children cumulated CPU time (s) 68.01
Current children cumulated vsize (Kb) 140752

[startup+80.0084 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 53704 0 0 0 7578 201 0 0 25 0 1 0 1855253328 198782976 48417 4294967295 134512640 135167914 3221224448 3221203224 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27224/statm): 48531 48417 162 162 0 48369 0
[pid=27224] vsize: 194124
Current children cumulated CPU time (s) 77.81
Current children cumulated vsize (Kb) 196252

[startup+90.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 57139 0 0 0 8541 217 0 0 25 0 1 0 1855253328 191254528 46579 4294967295 134512640 135167914 3221224448 3221201600 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27224/statm): 46693 46579 162 162 0 46531 0
[pid=27224] vsize: 186772
Current children cumulated CPU time (s) 87.6
Current children cumulated vsize (Kb) 188900

[startup+100.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 61403 0 0 0 9492 238 0 0 25 0 1 0 1855253328 208719872 50843 4294967295 134512640 135167914 3221224448 3221205028 134624813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 50957 50843 162 162 0 50795 0
[pid=27224] vsize: 203828
Current children cumulated CPU time (s) 97.32
Current children cumulated vsize (Kb) 205956

[startup+110.01 s]
Raw data (loadavg): 0.98 0.97 0.91 1/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) T 27219 27219 4419 0 -1 0 65691 0 0 0 10444 261 0 0 25 0 1 0 1855253328 226283520 55131 4294967295 134512640 135167914 3221224448 3221203068 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27224/statm): 55245 55131 162 162 0 55083 0
[pid=27224] vsize: 220980
Current children cumulated CPU time (s) 107.07
Current children cumulated vsize (Kb) 223108

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 69935 0 0 0 11401 280 0 0 25 0 1 0 1855253328 243666944 59375 4294967295 134512640 135167914 3221224448 3221203456 134624381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27224/statm): 59489 59375 162 162 0 59327 0
[pid=27224] vsize: 237956
Current children cumulated CPU time (s) 116.83
Current children cumulated vsize (Kb) 240084

[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 74083 0 0 0 12351 298 0 0 25 0 1 0 1855253328 260653056 63523 4294967295 134512640 135167914 3221224448 3221203104 134847261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 63636 63523 162 162 0 63474 0
[pid=27224] vsize: 254544
Current children cumulated CPU time (s) 126.51
Current children cumulated vsize (Kb) 256672

[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 78184 0 0 0 13308 316 0 0 25 0 1 0 1855253328 277450752 67624 4294967295 134512640 135167914 3221224448 3221204412 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 67737 67624 162 162 0 67575 0
[pid=27224] vsize: 270948
Current children cumulated CPU time (s) 136.26
Current children cumulated vsize (Kb) 273076

[startup+150.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 14295 322 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221217300 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 146.19
Current children cumulated vsize (Kb) 235016

[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 15296 322 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218828 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 156.2
Current children cumulated vsize (Kb) 235016

[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 16296 322 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218784 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 166.2
Current children cumulated vsize (Kb) 235016

[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 17296 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218752 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 176.21
Current children cumulated vsize (Kb) 235016

[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 18296 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218596 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 186.21
Current children cumulated vsize (Kb) 235016

[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 19296 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218664 134629265 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 196.21
Current children cumulated vsize (Kb) 235016

[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 20296 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219616 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 206.21
Current children cumulated vsize (Kb) 235016

[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 21296 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219168 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 216.21
Current children cumulated vsize (Kb) 235016

[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 22296 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219360 134629358 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 226.21
Current children cumulated vsize (Kb) 235016

[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 23297 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219152 134843012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 236.22
Current children cumulated vsize (Kb) 235016

[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 24297 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219704 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 246.22
Current children cumulated vsize (Kb) 235016

[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 25297 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218780 134845882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 256.22
Current children cumulated vsize (Kb) 235016

[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 26297 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218624 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 266.22
Current children cumulated vsize (Kb) 235016

[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 27297 323 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219088 134844689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 276.22
Current children cumulated vsize (Kb) 235016

[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 28297 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218992 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 286.23
Current children cumulated vsize (Kb) 235016

[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 29298 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219588 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 296.24
Current children cumulated vsize (Kb) 235016

[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 30298 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220128 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 306.24
Current children cumulated vsize (Kb) 235016

[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 31298 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220304 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 316.24
Current children cumulated vsize (Kb) 235016

[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 32298 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218800 134694528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 326.24
Current children cumulated vsize (Kb) 235016

[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 33298 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219448 134693665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 336.24
Current children cumulated vsize (Kb) 235016

[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 34298 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219472 134522502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 346.24
Current children cumulated vsize (Kb) 235016

[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 35299 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220832 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 356.25
Current children cumulated vsize (Kb) 235016

[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 36299 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219824 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 366.25
Current children cumulated vsize (Kb) 235016

[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 37299 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219856 134694425 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 376.25
Current children cumulated vsize (Kb) 235016

[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 38299 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220480 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 386.25
Current children cumulated vsize (Kb) 235016

[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 39299 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219616 134844731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 396.25
Current children cumulated vsize (Kb) 235016

[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 40300 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220524 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 406.26
Current children cumulated vsize (Kb) 235016

[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 41300 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219612 134718504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 416.26
Current children cumulated vsize (Kb) 235016

[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 42300 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219856 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 426.26
Current children cumulated vsize (Kb) 235016

[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 43300 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220596 134629364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 436.26
Current children cumulated vsize (Kb) 235016

[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 44300 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220384 134694524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 446.26
Current children cumulated vsize (Kb) 235016

[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 45300 324 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220432 134629382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 456.26
Current children cumulated vsize (Kb) 235016

[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 46300 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219996 134845882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 466.27
Current children cumulated vsize (Kb) 235016

[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 47301 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219280 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 476.28
Current children cumulated vsize (Kb) 235016

[startup+490.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 48301 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219520 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 486.28
Current children cumulated vsize (Kb) 235016

[startup+500.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 49301 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219644 134845882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 496.28
Current children cumulated vsize (Kb) 235016

[startup+510.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 50301 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219728 134629010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 506.28
Current children cumulated vsize (Kb) 235016

[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 51301 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219792 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 516.28
Current children cumulated vsize (Kb) 235016

[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 52301 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219680 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 526.28
Current children cumulated vsize (Kb) 235016

[startup+540.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 53302 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219100 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 536.29
Current children cumulated vsize (Kb) 235016

[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 54302 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219728 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 546.29
Current children cumulated vsize (Kb) 235016

[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 55302 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219264 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 556.29
Current children cumulated vsize (Kb) 235016

[startup+570.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 56302 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219376 134629410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 566.29
Current children cumulated vsize (Kb) 235016

[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 57302 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219292 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 576.29
Current children cumulated vsize (Kb) 235016

[startup+590.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 58303 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219104 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 586.3
Current children cumulated vsize (Kb) 235016

[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 59303 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220400 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 596.3
Current children cumulated vsize (Kb) 235016

[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 60303 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220412 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 606.3
Current children cumulated vsize (Kb) 235016

[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 61303 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220524 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 616.3
Current children cumulated vsize (Kb) 235016

[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 62303 325 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219440 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 626.3
Current children cumulated vsize (Kb) 235016

[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 63303 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219328 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 636.31
Current children cumulated vsize (Kb) 235016

[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 64304 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219792 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 646.32
Current children cumulated vsize (Kb) 235016

[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 65304 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219996 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 656.32
Current children cumulated vsize (Kb) 235016

[startup+670.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 66304 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220000 134722527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 666.32
Current children cumulated vsize (Kb) 235016

[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 67304 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219648 134693566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 676.32
Current children cumulated vsize (Kb) 235016

[startup+690.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 68304 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221218652 134694320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 686.32
Current children cumulated vsize (Kb) 235016

[startup+700.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 69304 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219552 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 696.32
Current children cumulated vsize (Kb) 235016

[startup+710.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 70305 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219968 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 706.33
Current children cumulated vsize (Kb) 235016

[startup+720.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 71305 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219856 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 716.33
Current children cumulated vsize (Kb) 235016

[startup+730.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 72305 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220688 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 726.33
Current children cumulated vsize (Kb) 235016

[startup+740.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 73305 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220320 134844731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 736.33
Current children cumulated vsize (Kb) 235016

[startup+750.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 74305 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219152 134522744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 746.33
Current children cumulated vsize (Kb) 235016

[startup+760.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 75305 326 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219968 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 756.33
Current children cumulated vsize (Kb) 235016

[startup+770.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 76306 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219120 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 766.35
Current children cumulated vsize (Kb) 235016

[startup+780.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 77306 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220672 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 776.35
Current children cumulated vsize (Kb) 235016

[startup+790.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 78306 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220412 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 786.35
Current children cumulated vsize (Kb) 235016

[startup+800.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 79306 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219792 134844682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 796.35
Current children cumulated vsize (Kb) 235016

[startup+810.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 80306 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220940 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 806.35
Current children cumulated vsize (Kb) 235016

[startup+820.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 81307 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219168 134849110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 816.36
Current children cumulated vsize (Kb) 235016

[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 82307 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219904 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 826.36
Current children cumulated vsize (Kb) 235016

[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 83307 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219728 134629322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 836.36
Current children cumulated vsize (Kb) 235016

[startup+850.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 84307 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219780 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 846.36
Current children cumulated vsize (Kb) 235016

[startup+860.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 85307 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219856 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 856.36
Current children cumulated vsize (Kb) 235016

[startup+870.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 86307 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219504 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 866.36
Current children cumulated vsize (Kb) 235016

[startup+880.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 87308 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219392 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 876.37
Current children cumulated vsize (Kb) 235016

[startup+890.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 88308 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219712 134630875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 886.37
Current children cumulated vsize (Kb) 235016

[startup+900.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 89308 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219992 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 896.37
Current children cumulated vsize (Kb) 235016

[startup+910.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 90308 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219872 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 906.37
Current children cumulated vsize (Kb) 235016

[startup+920.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 91309 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219504 134694504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 916.38
Current children cumulated vsize (Kb) 235016

[startup+930.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 92309 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219668 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 926.38
Current children cumulated vsize (Kb) 235016

[startup+940.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 93309 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220096 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 936.38
Current children cumulated vsize (Kb) 235016

[startup+950.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 94309 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219072 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 946.38
Current children cumulated vsize (Kb) 235016

[startup+960.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 95309 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219648 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 956.38
Current children cumulated vsize (Kb) 235016

[startup+970.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 96310 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219328 134694407 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 966.39
Current children cumulated vsize (Kb) 235016

[startup+980.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 97310 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219328 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 976.39
Current children cumulated vsize (Kb) 235016

[startup+990.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 98310 327 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219392 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 986.39
Current children cumulated vsize (Kb) 235016

[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 99310 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220336 134696233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 996.4
Current children cumulated vsize (Kb) 235016

[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 100310 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219440 134844700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1006.4
Current children cumulated vsize (Kb) 235016

[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 101310 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219656 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1016.4
Current children cumulated vsize (Kb) 235016

[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 102310 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220080 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1026.4
Current children cumulated vsize (Kb) 235016

[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 103310 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219644 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1036.4
Current children cumulated vsize (Kb) 235016

[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 104310 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220188 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1046.4
Current children cumulated vsize (Kb) 235016

[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 105311 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219792 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1056.41
Current children cumulated vsize (Kb) 235016

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 106311 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220392 134849057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1066.41
Current children cumulated vsize (Kb) 235016

[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 107311 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220588 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1076.41
Current children cumulated vsize (Kb) 235016

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 108311 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219784 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1086.41
Current children cumulated vsize (Kb) 235016

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 109311 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219152 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1096.41
Current children cumulated vsize (Kb) 235016

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 110311 328 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219616 134844689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1106.41
Current children cumulated vsize (Kb) 235016

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 111311 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219696 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1116.42
Current children cumulated vsize (Kb) 235016

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 112312 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219568 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1126.43
Current children cumulated vsize (Kb) 235016

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 113312 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219468 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1136.43
Current children cumulated vsize (Kb) 235016

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 114312 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219704 134694481 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1146.43
Current children cumulated vsize (Kb) 235016

[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 115312 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221220764 134522184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1156.43
Current children cumulated vsize (Kb) 235016

[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 116313 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219680 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1166.44
Current children cumulated vsize (Kb) 235016

[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 117313 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219680 134694517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1176.44
Current children cumulated vsize (Kb) 235016

[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 118313 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219348 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1186.44
Current children cumulated vsize (Kb) 235016

[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 119313 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219096 134693621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1196.44
Current children cumulated vsize (Kb) 235016

[startup+1210.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 120313 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219664 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1206.44
Current children cumulated vsize (Kb) 235016



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27224
Raw data (/proc/27219/stat): 27219 (minisat+_script) S 27218 27219 4419 0 -1 0 314 332 0 0 0 1 0 1 21 0 1 0 1855253322 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27219/statm): 532 234 485 147 0 385 0
[pid=27219] vsize: 2128
Raw data (/proc/27224/stat): 27224 (minisat+_bignum) R 27219 27219 4419 0 -1 0 79211 0 0 0 120314 329 0 0 25 0 1 0 1855253328 238477312 58105 4294967295 134512640 135167914 3221224448 3221219504 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27224/statm): 58222 58105 162 162 0 58060 0
[pid=27224] vsize: 232888
Current children cumulated CPU time (s) 1206.45
Current children cumulated vsize (Kb) 235016

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

Child status: 0
Real time (s): 1210.18
CPU time (s): 1206.54
CPU user time (s): 1203.14
CPU system time (s): 3.40248
CPU usage (%): 99.6998
Max. virtual memory (cumulated for all children) (Kb): 273076

Verifier Data

ERROR: no interpretation found !