Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-israel.opb
MD5SUM7ba5c7ed3d893d37e85d9935730a0f21
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -86917125500
Optimality of the best value was proved NO
Number of terms in the objective function 2670
Biggest coefficient in the objective function 807185416192000
Number of bits for the biggest coefficient in the objective function 50
Sum of the numbers in the objective function 9901243932822396
Number of bits of the sum of numbers in the objective function 54
Biggest number in a constraint 807185416192000
Number of bits of the biggest number in a constraint 50
Biggest sum of numbers in a constraint 9901243932822396
Number of bits of the biggest sum of numbers54
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark731.752
Number of variables4260
Total number of constraints174
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints174
Minimum length of a constraint30
Maximum length of a constraint3540

Trace number 2656

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        920872 kB
Buffers:         34592 kB
Cached:          51888 kB
SwapCached:        832 kB
Active:          61864 kB
Inactive:        27248 kB
HighTotal:      131008 kB
HighFree:        78372 kB
LowTotal:       903652 kB
LowFree:        842500 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            19100 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:41:04 (client local time) WITH STATUS 0 IN 1209.83 SECONDS
stats: 2783 7 1209.83 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 146] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 174 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssssss
c ---[ 181]---> Adder-cost: 1424   maxlim: 155461596   bits: 28/28
c ---[ 179]---> Sorter-cost: 3962     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 178]---> Sorter-cost: 4599     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 177]---> Sorter-cost: 4395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 176]---> Sorter-cost: 4395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 175]---> Sorter-cost: 4395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 174]---> Sorter-cost: 4395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 173]---> Sorter-cost: 4455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2
c ---[ 172]---> Sorter-cost: 4295     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2
c ---[ 171]---> Sorter-cost: 4295     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 4942     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 3789     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 2167     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 166]---> Sorter-cost: 1672     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[ 165]---> Sorter-cost: 1735     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 163]---> Sorter-cost: 2351     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 3110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 2860     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 160]---> Sorter-cost: 2983     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 159]---> Sorter-cost: 3410     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 158]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 157]---> Sorter-cost: 3209     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2
c ---[ 156]---> Sorter-cost: 2871     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2
c ---[ 155]---> Sorter-cost: 2914     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 154]---> Sorter-cost: 2827     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 153]---> Sorter-cost: 2826     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 152]---> Sorter-cost: 2826     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 151]---> Sorter-cost: 2825     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 150]---> Sorter-cost: 2825     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 149]---> Sorter-cost: 2825     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 148]---> Sorter-cost: 2826     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 147]---> Adder-cost: 616   maxlim: 600882799   bits: 30/30
c ---[ 146]---> Sorter-cost: 2822     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 145]---> Sorter-cost: 2826     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 144]---> Sorter-cost: 2825     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 143]---> Adder-cost: 608   maxlim: 681572099   bits: 30/30
c ---[ 142]---> Adder-cost: 567   maxlim: 366999295   bits: 29/29
c ---[ 141]---> Adder-cost: 576   maxlim: 366999291   bits: 29/29
c ---[ 140]---> Adder-cost: 564   maxlim: 366999287   bits: 29/29
c ---[ 139]---> Adder-cost: 564   maxlim: 366999283   bits: 29/29
c ---[ 138]---> Adder-cost: 564   maxlim: 366999279   bits: 29/29
c ---[ 137]---> Adder-cost: 564   maxlim: 366999275   bits: 29/29
c ---[ 136]---> Sorter-cost: 1225     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Adder-cost: 564   maxlim: 366999270   bits: 29/29
c ---

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/13256/stat): 13256 (minisat+_script) R 13255 13256 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844075397 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/13256/statm): 174 3 169 147 0 27 0
[pid=13256] 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=13257
New process pid=13258
New process pid=13259
execve syscall for /bin/sed executable
One traced child (pid=13258) 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=13259) exited with status: 0
One traced child (pid=13257) exited with status: 0
New process pid=13260
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-israel.opb
One traced child (pid=13260) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=13261
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-israel.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.95 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1577 0 3 0 957 11 0 0 25 0 1 0 1844075403 6258688 1390 4294967295 134512640 135167914 3221224448 3221220400 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 1528 1390 162 162 0 1366 0
[pid=13261] vsize: 6112
Current children cumulated CPU time (s) 9.7
Current children cumulated vsize (Kb) 8240

[startup+20.0043 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1577 0 3 0 1957 11 0 0 25 0 1 0 1844075403 6258688 1390 4294967295 134512640 135167914 3221224448 3221220016 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 1528 1390 162 162 0 1366 0
[pid=13261] vsize: 6112
Current children cumulated CPU time (s) 19.7
Current children cumulated vsize (Kb) 8240

[startup+30.0051 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1589 0 3 0 2956 11 0 0 25 0 1 0 1844075403 6455296 1402 4294967295 134512640 135167914 3221224448 3221220204 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 1576 1402 162 162 0 1414 0
[pid=13261] vsize: 6304
Current children cumulated CPU time (s) 29.69
Current children cumulated vsize (Kb) 8432

[startup+40.0069 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1703 0 3 0 3955 12 0 0 25 0 1 0 1844075403 6643712 1474 4294967295 134512640 135167914 3221224448 3221219360 134629285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 1622 1474 162 162 0 1460 0
[pid=13261] vsize: 6488
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 8616

[startup+50.0077 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1738 0 3 0 4955 12 0 0 25 0 1 0 1844075403 7127040 1509 4294967295 134512640 135167914 3221224448 3221221088 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 1740 1509 162 162 0 1578 0
[pid=13261] vsize: 6960
Current children cumulated CPU time (s) 49.69
Current children cumulated vsize (Kb) 9088

[startup+60.0076 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1807 0 3 0 5955 12 0 0 25 0 1 0 1844075403 7307264 1578 4294967295 134512640 135167914 3221224448 3221219792 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 1784 1578 162 162 0 1622 0
[pid=13261] vsize: 7136
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 9264

[startup+70.0094 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2036 0 3 0 6953 13 0 0 25 0 1 0 1844075403 7806976 1724 4294967295 134512640 135167914 3221224448 3221220576 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 1906 1724 162 162 0 1744 0
[pid=13261] vsize: 7624
Current children cumulated CPU time (s) 69.68
Current children cumulated vsize (Kb) 9752

[startup+80.0102 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2142 0 3 0 7952 14 0 0 25 0 1 0 1844075403 8081408 1830 4294967295 134512640 135167914 3221224448 3221221792 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 1973 1830 162 162 0 1811 0
[pid=13261] vsize: 7892
Current children cumulated CPU time (s) 79.68
Current children cumulated vsize (Kb) 10020

[startup+90.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2295 0 3 0 8951 14 0 0 25 0 1 0 1844075403 9265152 1983 4294967295 134512640 135167914 3221224448 3221221948 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 2262 1983 162 162 0 2100 0
[pid=13261] vsize: 9048
Current children cumulated CPU time (s) 89.67
Current children cumulated vsize (Kb) 11176

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2738 0 3 0 9950 15 0 0 25 0 1 0 1844075403 10235904 2261 4294967295 134512640 135167914 3221224448 3221221824 134630940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 2499 2261 162 162 0 2337 0
[pid=13261] vsize: 9996
Current children cumulated CPU time (s) 99.67
Current children cumulated vsize (Kb) 12124

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2798 0 3 0 10949 16 0 0 25 0 1 0 1844075403 10407936 2321 4294967295 134512640 135167914 3221224448 3221220940 134693728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 2541 2321 162 162 0 2379 0
[pid=13261] vsize: 10164
Current children cumulated CPU time (s) 109.67
Current children cumulated vsize (Kb) 12292

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2866 0 3 0 11949 16 0 0 25 0 1 0 1844075403 10571776 2389 4294967295 134512640 135167914 3221224448 3221221792 134843015 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 2581 2389 162 162 0 2419 0
[pid=13261] vsize: 10324
Current children cumulated CPU time (s) 119.67
Current children cumulated vsize (Kb) 12452

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2934 0 3 0 12948 16 0 0 25 0 1 0 1844075403 10752000 2457 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 2625 2457 162 162 0 2463 0
[pid=13261] vsize: 10500
Current children cumulated CPU time (s) 129.66
Current children cumulated vsize (Kb) 12628

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2950 0 3 0 13948 17 0 0 25 0 1 0 1844075403 10792960 2473 4294967295 134512640 135167914 3221224448 3221221740 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 2635 2473 162 162 0 2473 0
[pid=13261] vsize: 10540
Current children cumulated CPU time (s) 139.67
Current children cumulated vsize (Kb) 12668

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2982 0 3 0 14948 17 0 0 25 0 1 0 1844075403 10874880 2505 4294967295 134512640 135167914 3221224448 3221219632 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13261/statm): 2655 2505 162 162 0 2493 0
[pid=13261] vsize: 10620
Current children cumulated CPU time (s) 149.67
Current children cumulated vsize (Kb) 12748

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2997 0 3 0 15946 19 0 0 25 0 1 0 1844075403 10915840 2520 4294967295 134512640 135167914 3221224448 3221220912 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 2665 2520 162 162 0 2503 0
[pid=13261] vsize: 10660
Current children cumulated CPU time (s) 159.67
Current children cumulated vsize (Kb) 12788

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3011 0 3 0 16946 19 0 0 25 0 1 0 1844075403 10948608 2534 4294967295 134512640 135167914 3221224448 3221220832 134845903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 2673 2534 162 162 0 2511 0
[pid=13261] vsize: 10692
Current children cumulated CPU time (s) 169.67
Current children cumulated vsize (Kb) 12820

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3027 0 3 0 17946 19 0 0 25 0 1 0 1844075403 12558336 2550 4294967295 134512640 135167914 3221224448 3221220672 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3066 2550 162 162 0 2904 0
[pid=13261] vsize: 12264
Current children cumulated CPU time (s) 179.67
Current children cumulated vsize (Kb) 14392

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3130 0 3 0 18945 19 0 0 25 0 1 0 1844075403 12832768 2653 4294967295 134512640 135167914 3221224448 3221221840 134844668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3133 2653 162 162 0 2971 0
[pid=13261] vsize: 12532
Current children cumulated CPU time (s) 189.66
Current children cumulated vsize (Kb) 14660

[startup+200.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3193 0 3 0 19945 19 0 0 25 0 1 0 1844075403 13029376 2716 4294967295 134512640 135167914 3221224448 3221220724 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3181 2716 162 162 0 3019 0
[pid=13261] vsize: 12724
Current children cumulated CPU time (s) 199.66
Current children cumulated vsize (Kb) 14852

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3193 0 3 0 20945 19 0 0 25 0 1 0 1844075403 13029376 2716 4294967295 134512640 135167914 3221224448 3221220180 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3181 2716 162 162 0 3019 0
[pid=13261] vsize: 12724
Current children cumulated CPU time (s) 209.66
Current children cumulated vsize (Kb) 14852

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3193 0 3 0 21945 20 0 0 25 0 1 0 1844075403 13029376 2716 4294967295 134512640 135167914 3221224448 3221221904 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3181 2716 162 162 0 3019 0
[pid=13261] vsize: 12724
Current children cumulated CPU time (s) 219.67
Current children cumulated vsize (Kb) 14852

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3207 0 3 0 22946 20 0 0 25 0 1 0 1844075403 13029376 2730 4294967295 134512640 135167914 3221224448 3221188076 134618900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3181 2730 162 162 0 3019 0
[pid=13261] vsize: 12724
Current children cumulated CPU time (s) 229.68
Current children cumulated vsize (Kb) 14852

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3215 0 3 0 23946 20 0 0 25 0 1 0 1844075403 13062144 2738 4294967295 134512640 135167914 3221224448 3221218912 134696738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3189 2738 162 162 0 3027 0
[pid=13261] vsize: 12756
Current children cumulated CPU time (s) 239.68
Current children cumulated vsize (Kb) 14884

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3215 0 3 0 24946 20 0 0 25 0 1 0 1844075403 13062144 2738 4294967295 134512640 135167914 3221224448 3221220220 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3189 2738 162 162 0 3027 0
[pid=13261] vsize: 12756
Current children cumulated CPU time (s) 249.68
Current children cumulated vsize (Kb) 14884

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3215 0 3 0 25946 20 0 0 25 0 1 0 1844075403 13062144 2738 4294967295 134512640 135167914 3221224448 3221220176 134718188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3189 2738 162 162 0 3027 0
[pid=13261] vsize: 12756
Current children cumulated CPU time (s) 259.68
Current children cumulated vsize (Kb) 14884

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3215 0 3 0 26946 20 0 0 25 0 1 0 1844075403 13062144 2738 4294967295 134512640 135167914 3221224448 3221222192 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3189 2738 162 162 0 3027 0
[pid=13261] vsize: 12756
Current children cumulated CPU time (s) 269.68
Current children cumulated vsize (Kb) 14884

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 27946 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221220152 134693621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0
[pid=13261] vsize: 12820
Current children cumulated CPU time (s) 279.68
Current children cumulated vsize (Kb) 14948

[startup+290.027 s]
Raw data (loadavg): 1.07 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 28946 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221221004 134718182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0
[pid=13261] vsize: 12820
Current children cumulated CPU time (s) 289.68
Current children cumulated vsize (Kb) 14948

[startup+300.028 s]
Raw data (loadavg): 1.06 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 29947 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221221052 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0
[pid=13261] vsize: 12820
Current children cumulated CPU time (s) 299.69
Current children cumulated vsize (Kb) 14948

[startup+310.028 s]
Raw data (loadavg): 1.05 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 30946 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221222160 134849110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0
[pid=13261] vsize: 12820
Current children cumulated CPU time (s) 309.68
Current children cumulated vsize (Kb) 14948

[startup+320.029 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 31947 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221221888 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0
[pid=13261] vsize: 12820
Current children cumulated CPU time (s) 319.69
Current children cumulated vsize (Kb) 14948

[startup+330.029 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 32947 20 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221220928 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 329.69
Current children cumulated vsize (Kb) 15004

[startup+340.03 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 33947 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221219616 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 339.7
Current children cumulated vsize (Kb) 15004

[startup+350.031 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 34947 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221416 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 349.7
Current children cumulated vsize (Kb) 15004

[startup+360.032 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 35948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221024 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 359.71
Current children cumulated vsize (Kb) 15004

[startup+370.033 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 36948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221152 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 369.71
Current children cumulated vsize (Kb) 15004

[startup+380.032 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 37948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221219644 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 379.71
Current children cumulated vsize (Kb) 15004

[startup+390.033 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 38948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221220304 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 389.71
Current children cumulated vsize (Kb) 15004

[startup+400.034 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 39948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221024 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 399.71
Current children cumulated vsize (Kb) 15004

[startup+410.034 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 40948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221616 134849122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 409.71
Current children cumulated vsize (Kb) 15004

[startup+420.035 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 41949 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221424 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0
[pid=13261] vsize: 12876
Current children cumulated CPU time (s) 419.72
Current children cumulated vsize (Kb) 15004

[startup+430.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3276 0 3 0 42949 21 0 0 25 0 1 0 1844075403 13238272 2799 4294967295 134512640 135167914 3221224448 3221220764 134694480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3232 2799 162 162 0 3070 0
[pid=13261] vsize: 12928
Current children cumulated CPU time (s) 429.72
Current children cumulated vsize (Kb) 15056

[startup+440.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3276 0 3 0 43949 21 0 0 25 0 1 0 1844075403 13238272 2799 4294967295 134512640 135167914 3221224448 3221221440 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3232 2799 162 162 0 3070 0
[pid=13261] vsize: 12928
Current children cumulated CPU time (s) 439.72
Current children cumulated vsize (Kb) 15056

[startup+450.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3280 0 3 0 44949 21 0 0 25 0 1 0 1844075403 13238272 2803 4294967295 134512640 135167914 3221224448 3221220704 134849110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3232 2803 162 162 0 3070 0
[pid=13261] vsize: 12928
Current children cumulated CPU time (s) 449.72
Current children cumulated vsize (Kb) 15056

[startup+460.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3280 0 3 0 45950 21 0 0 25 0 1 0 1844075403 13238272 2803 4294967295 134512640 135167914 3221224448 3221220528 134722521 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3232 2803 162 162 0 3070 0
[pid=13261] vsize: 12928
Current children cumulated CPU time (s) 459.73
Current children cumulated vsize (Kb) 15056

[startup+470.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3304 0 3 0 46950 21 0 0 25 0 1 0 1844075403 13295616 2827 4294967295 134512640 135167914 3221224448 3221220116 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3246 2827 162 162 0 3084 0
[pid=13261] vsize: 12984
Current children cumulated CPU time (s) 469.73
Current children cumulated vsize (Kb) 15112

[startup+480.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3304 0 3 0 47950 21 0 0 25 0 1 0 1844075403 13295616 2827 4294967295 134512640 135167914 3221224448 3221220848 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3246 2827 162 162 0 3084 0
[pid=13261] vsize: 12984
Current children cumulated CPU time (s) 479.73
Current children cumulated vsize (Kb) 15112

[startup+490.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3304 0 3 0 48950 21 0 0 25 0 1 0 1844075403 13295616 2827 4294967295 134512640 135167914 3221224448 3221221456 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3246 2827 162 162 0 3084 0
[pid=13261] vsize: 12984
Current children cumulated CPU time (s) 489.73
Current children cumulated vsize (Kb) 15112

[startup+500.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 49950 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221220656 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0
[pid=13261] vsize: 13032
Current children cumulated CPU time (s) 499.73
Current children cumulated vsize (Kb) 15160

[startup+510.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 50950 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221220912 134694517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0
[pid=13261] vsize: 13032
Current children cumulated CPU time (s) 509.73
Current children cumulated vsize (Kb) 15160

[startup+520.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 51951 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221219488 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0
[pid=13261] vsize: 13032
Current children cumulated CPU time (s) 519.74
Current children cumulated vsize (Kb) 15160

[startup+530.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 52951 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221221744 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0
[pid=13261] vsize: 13032
Current children cumulated CPU time (s) 529.74
Current children cumulated vsize (Kb) 15160

[startup+540.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 53951 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221221964 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0
[pid=13261] vsize: 13032
Current children cumulated CPU time (s) 539.74
Current children cumulated vsize (Kb) 15160

[startup+550.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3370 0 3 0 54951 22 0 0 25 0 1 0 1844075403 13537280 2893 4294967295 134512640 135167914 3221224448 3221221792 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3305 2893 162 162 0 3143 0
[pid=13261] vsize: 13220
Current children cumulated CPU time (s) 549.75
Current children cumulated vsize (Kb) 15348

[startup+560.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 4096 0 3 0 55949 23 0 0 25 0 1 0 1844075403 15024128 3289 4294967295 134512640 135167914 3221224448 3221222112 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3668 3289 162 162 0 3506 0
[pid=13261] vsize: 14672
Current children cumulated CPU time (s) 559.74
Current children cumulated vsize (Kb) 16800

[startup+570.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 4101 0 3 0 56949 23 0 0 25 0 1 0 1844075403 15024128 3294 4294967295 134512640 135167914 3221224448 3221221728 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 3668 3294 162 162 0 3506 0
[pid=13261] vsize: 14672
Current children cumulated CPU time (s) 569.74
Current children cumulated vsize (Kb) 16800

[startup+580.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 57934 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217744 134843012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 579.68
Current children cumulated vsize (Kb) 21728

[startup+590.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 58934 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217216 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 589.68
Current children cumulated vsize (Kb) 21728

[startup+600.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 59934 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217680 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 599.68
Current children cumulated vsize (Kb) 21728

[startup+610.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 60935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218016 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 609.69
Current children cumulated vsize (Kb) 21728

[startup+620.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 61935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217856 134696298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 619.69
Current children cumulated vsize (Kb) 21728

[startup+630.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 62935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218032 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 629.69
Current children cumulated vsize (Kb) 21728

[startup+640.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 63935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217912 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 639.69
Current children cumulated vsize (Kb) 21728

[startup+650.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 64935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218468 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 649.69
Current children cumulated vsize (Kb) 21728

[startup+660.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 65935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217944 134693553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 659.69
Current children cumulated vsize (Kb) 21728

[startup+670.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 66936 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218596 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 669.7
Current children cumulated vsize (Kb) 21728

[startup+680.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 67936 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217720 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 679.7
Current children cumulated vsize (Kb) 21728

[startup+690.053 s]
Raw data (loadavg): 1.08 1.00 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 68936 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218076 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 689.7
Current children cumulated vsize (Kb) 21728

[startup+700.053 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 69936 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218060 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 699.7
Current children cumulated vsize (Kb) 21728

[startup+710.054 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 70937 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218224 134696598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 709.71
Current children cumulated vsize (Kb) 21728

[startup+720.055 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 71937 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218824 134696561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 719.71
Current children cumulated vsize (Kb) 21728

[startup+730.056 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 72937 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218032 134844689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 729.71
Current children cumulated vsize (Kb) 21728

[startup+740.057 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 73937 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218020 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 739.71
Current children cumulated vsize (Kb) 21728

[startup+750.057 s]
Raw data (loadavg): 1.11 1.02 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 74938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218040 134693686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 749.72
Current children cumulated vsize (Kb) 21728

[startup+760.058 s]
Raw data (loadavg): 1.09 1.02 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 75938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217280 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 759.72
Current children cumulated vsize (Kb) 21728

[startup+770.059 s]
Raw data (loadavg): 1.08 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 76938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218128 134630738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 769.72
Current children cumulated vsize (Kb) 21728

[startup+780.06 s]
Raw data (loadavg): 1.06 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 77938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218400 134723225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 779.72
Current children cumulated vsize (Kb) 21728

[startup+790.061 s]
Raw data (loadavg): 1.05 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 78938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218928 134696587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 789.72
Current children cumulated vsize (Kb) 21728

[startup+800.061 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 79939 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218192 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 799.73
Current children cumulated vsize (Kb) 21728

[startup+810.061 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 80939 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217708 134723206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 809.73
Current children cumulated vsize (Kb) 21728

[startup+820.063 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 81939 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217936 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 819.74
Current children cumulated vsize (Kb) 21728

[startup+830.063 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 82939 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217568 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 829.74
Current children cumulated vsize (Kb) 21728

[startup+840.064 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 83939 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218260 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 839.74
Current children cumulated vsize (Kb) 21728

[startup+850.064 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 84939 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221219200 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 849.74
Current children cumulated vsize (Kb) 21728

[startup+860.064 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 85940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218292 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 859.75
Current children cumulated vsize (Kb) 21728

[startup+870.065 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 86940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217376 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 869.75
Current children cumulated vsize (Kb) 21728

[startup+880.066 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 87940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218320 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 879.75
Current children cumulated vsize (Kb) 21728

[startup+890.067 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 88940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218640 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 889.75
Current children cumulated vsize (Kb) 21728

[startup+900.067 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 89940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221219200 134629448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 899.75
Current children cumulated vsize (Kb) 21728

[startup+910.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 90941 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217884 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 909.76
Current children cumulated vsize (Kb) 21728

[startup+920.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 91941 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217888 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 919.76
Current children cumulated vsize (Kb) 21728

[startup+930.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 92941 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218652 134694480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 929.76
Current children cumulated vsize (Kb) 21728

[startup+940.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 93941 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218112 134522189 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 939.76
Current children cumulated vsize (Kb) 21728

[startup+950.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 94942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218400 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 949.77
Current children cumulated vsize (Kb) 21728

[startup+960.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 95942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218496 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 959.77
Current children cumulated vsize (Kb) 21728

[startup+970.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 96942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218652 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 969.77
Current children cumulated vsize (Kb) 21728

[startup+980.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 97942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218736 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 979.77
Current children cumulated vsize (Kb) 21728

[startup+990.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 98942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217920 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 989.77
Current children cumulated vsize (Kb) 21728

[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 99943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218448 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 999.78
Current children cumulated vsize (Kb) 21728

[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 100943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218288 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1009.78
Current children cumulated vsize (Kb) 21728

[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 101943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218920 134693629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1019.78
Current children cumulated vsize (Kb) 21728

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 102943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218800 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1029.78
Current children cumulated vsize (Kb) 21728

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 103943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221219308 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1039.78
Current children cumulated vsize (Kb) 21728

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 104944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218972 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1049.79
Current children cumulated vsize (Kb) 21728

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 105944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218080 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1059.79
Current children cumulated vsize (Kb) 21728

[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 106944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217568 134849113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1069.79
Current children cumulated vsize (Kb) 21728

[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 107944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218448 134694504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1079.79
Current children cumulated vsize (Kb) 21728

[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 108944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218464 134849071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1089.79
Current children cumulated vsize (Kb) 21728

[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 109945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217392 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1099.8
Current children cumulated vsize (Kb) 21728

[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 110945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218284 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1109.8
Current children cumulated vsize (Kb) 21728

[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 111945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218468 134522233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1119.8
Current children cumulated vsize (Kb) 21728

[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 112945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218796 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1129.8
Current children cumulated vsize (Kb) 21728

[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 113945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218048 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1139.8
Current children cumulated vsize (Kb) 21728

[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 114946 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218448 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1149.81
Current children cumulated vsize (Kb) 21728

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 115946 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218240 134695313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1159.81
Current children cumulated vsize (Kb) 21728

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 116946 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218252 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1169.81
Current children cumulated vsize (Kb) 21728

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 117946 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218736 134696395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1179.81
Current children cumulated vsize (Kb) 21728

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 118947 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218032 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1189.82
Current children cumulated vsize (Kb) 21728

[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 119947 34 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217856 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1199.83
Current children cumulated vsize (Kb) 21728

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 120947 34 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217920 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1209.83
Current children cumulated vsize (Kb) 21728



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 13261
Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13256/statm): 532 234 485 147 0 385 0
[pid=13256] vsize: 2128
Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 120947 34 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217920 134849110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0
[pid=13261] vsize: 19600
Current children cumulated CPU time (s) 1209.83
Current children cumulated vsize (Kb) 21728

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

Child status: 0
Real time (s): 1210.1
CPU time (s): 1209.83
CPU user time (s): 1209.48
CPU system time (s): 0.350946
CPU usage (%): 99.9771
Max. virtual memory (cumulated for all children) (Kb): 21728

Verifier Data

ERROR: no interpretation found !