Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-rd-rplusc-21.opb
MD5SUMd2b612d978c6eb050af622d4cf2ae598
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 48
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2160590747
Number of bits of the sum of numbers in the objective function 32
Biggest number in a constraint 2962281908055777280
Number of bits of the biggest number in a constraint 62
Biggest sum of numbers in a constraint 6289973478481187311
Number of bits of the biggest sum of numbers63
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark708.041
Number of variables3616
Total number of constraints126450
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)699
Number of constraints which are nor clauses,nor cardinality constraints125751
Minimum length of a constraint1
Maximum length of a constraint189

Trace number 3926

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        648496 kB
Buffers:         37252 kB
Cached:         315856 kB
SwapCached:        764 kB
Active:         295448 kB
Inactive:        60288 kB
HighTotal:      131008 kB
HighFree:         3724 kB
LowTotal:       903652 kB
LowFree:        644772 kB
SwapTotal:     2097892 kB
SwapFree:      2096616 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            24664 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 04:08:49 (client local time) WITH STATUS 20 IN 708.041 SECONDS
stats: 2939 7 708.041 20

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 1180] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 125843 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppp  -- Detecting intervals from adjacent constraints: =====================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================#######=====##########################################################################################################=======================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#========================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================
c   -- Clauses(.)/Splits(s): s
s UNSATISFIABLE
c _______________________________________________________________________________
c 
c restarts              : 0
c conflicts             : 0              (0 /sec)
c decisions             : 0              (0 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 694.799 s
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/15524/stat): 15524 (minisat+_script) R 15523 15524 28974 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1846811408 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/15524/statm): 174 3 169 147 0 27 0
[pid=15524] 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=15525
New process pid=15526
New process pid=15527
execve syscall for /bin/sed executable
One traced child (pid=15526) 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=15527) exited with status: 0
One traced child (pid=15525) exited with status: 0
New process pid=15528
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-rd-rplusc-21.opb
One traced child (pid=15528) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=15529
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-rd-rplusc-21.opb

[startup+10.0036 s]
Raw data (loadavg): 1.02 0.97 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 2281 0 0 0 955 17 0 0 25 0 1 0 1846811417 9707520 2267 4294967295 134512640 135167914 3221224432 3221222784 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 2370 2267 162 162 0 2208 0
[pid=15529] vsize: 9480
Current children cumulated CPU time (s) 9.76
Current children cumulated vsize (Kb) 11608

[startup+20.0055 s]
Raw data (loadavg): 1.01 0.97 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 4426 0 0 0 1919 35 0 0 25 0 1 0 1846811417 18485248 4412 4294967295 134512640 135167914 3221224432 3221223184 134588422 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 4513 4412 162 162 0 4351 0
[pid=15529] vsize: 18052
Current children cumulated CPU time (s) 19.58
Current children cumulated vsize (Kb) 20180

[startup+30.0063 s]
Raw data (loadavg): 1.09 0.99 0.95 1/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) T 15524 15524 28974 0 -1 0 6580 0 0 0 2884 53 0 0 25 0 1 0 1846811417 27332608 6566 4294967295 134512640 135167914 3221224432 3221223272 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15529/statm): 6673 6566 162 162 0 6511 0
[pid=15529] vsize: 26692
Current children cumulated CPU time (s) 29.41
Current children cumulated vsize (Kb) 28820

[startup+40.0081 s]
Raw data (loadavg): 1.08 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 8740 0 0 0 3849 69 0 0 25 0 1 0 1846811417 36171776 8726 4294967295 134512640 135167914 3221224432 3221221196 134516612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 8831 8726 162 162 0 8669 0
[pid=15529] vsize: 35324
Current children cumulated CPU time (s) 39.22
Current children cumulated vsize (Kb) 37452

[startup+50.009 s]
Raw data (loadavg): 1.06 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 10916 0 0 0 4812 88 0 0 25 0 1 0 1846811417 45117440 10902 4294967295 134512640 135167914 3221224432 3221221824 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 11015 10902 162 162 0 10853 0
[pid=15529] vsize: 44060
Current children cumulated CPU time (s) 49.04
Current children cumulated vsize (Kb) 46188

[startup+60.0098 s]
Raw data (loadavg): 1.05 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 13077 0 0 0 5776 106 0 0 25 0 1 0 1846811417 53960704 13063 4294967295 134512640 135167914 3221224432 3221223276 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 13174 13063 162 162 0 13012 0
[pid=15529] vsize: 52696
Current children cumulated CPU time (s) 58.86
Current children cumulated vsize (Kb) 54824

[startup+70.0106 s]
Raw data (loadavg): 1.04 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 15236 0 0 0 6741 123 0 0 25 0 1 0 1846811417 62799872 15222 4294967295 134512640 135167914 3221224432 3221222804 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 15332 15222 162 162 0 15170 0
[pid=15529] vsize: 61328
Current children cumulated CPU time (s) 68.68
Current children cumulated vsize (Kb) 63456

[startup+80.0114 s]
Raw data (loadavg): 1.04 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 17370 0 0 0 7704 140 0 0 25 0 1 0 1846811417 71512064 17356 4294967295 134512640 135167914 3221224432 3221223104 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15529/statm): 17459 17356 162 162 0 17297 0
[pid=15529] vsize: 69836
Current children cumulated CPU time (s) 78.48
Current children cumulated vsize (Kb) 71964

[startup+90.0123 s]
Raw data (loadavg): 1.03 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 19524 0 0 0 8668 157 0 0 25 0 1 0 1846811417 80343040 19510 4294967295 134512640 135167914 3221224432 3221223272 134865821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 19615 19510 162 162 0 19453 0
[pid=15529] vsize: 78460
Current children cumulated CPU time (s) 88.29
Current children cumulated vsize (Kb) 80588

[startup+100.013 s]
Raw data (loadavg): 1.03 0.99 0.95 1/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) T 15524 15524 28974 0 -1 0 21690 0 0 0 9634 175 0 0 25 0 1 0 1846811417 89260032 21676 4294967295 134512640 135167914 3221224432 3221223320 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15529/statm): 21792 21676 162 162 0 21630 0
[pid=15529] vsize: 87168
Current children cumulated CPU time (s) 98.13
Current children cumulated vsize (Kb) 89296

[startup+110.014 s]
Raw data (loadavg): 1.02 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 23850 0 0 0 10598 193 0 0 25 0 1 0 1846811417 98103296 23836 4294967295 134512640 135167914 3221224432 3221223376 134579322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 23951 23836 162 162 0 23789 0
[pid=15529] vsize: 95804
Current children cumulated CPU time (s) 107.95
Current children cumulated vsize (Kb) 97932

[startup+120.016 s]
Raw data (loadavg): 1.02 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 26009 0 0 0 11562 210 0 0 25 0 1 0 1846811417 106942464 25995 4294967295 134512640 135167914 3221224432 3221221724 134693643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 26109 25995 162 162 0 25947 0
[pid=15529] vsize: 104436
Current children cumulated CPU time (s) 117.76
Current children cumulated vsize (Kb) 106564

[startup+130.017 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 28479 0 0 0 12516 232 0 0 25 0 1 0 1846811417 117088256 28465 4294967295 134512640 135167914 3221224432 3221222848 134843012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 28586 28465 162 162 0 28424 0
[pid=15529] vsize: 114344
Current children cumulated CPU time (s) 127.52
Current children cumulated vsize (Kb) 116472

[startup+140.017 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 30997 0 0 0 13474 252 0 0 25 0 1 0 1846811417 127361024 30983 4294967295 134512640 135167914 3221224432 3221222176 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 31094 30983 162 162 0 30932 0
[pid=15529] vsize: 124376
Current children cumulated CPU time (s) 137.3
Current children cumulated vsize (Kb) 126504

[startup+150.018 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 33187 0 0 0 14435 270 0 0 25 0 1 0 1846811417 136339456 33173 4294967295 134512640 135167914 3221224432 3221223184 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 33286 33173 162 162 0 33124 0
[pid=15529] vsize: 133144
Current children cumulated CPU time (s) 147.09
Current children cumulated vsize (Kb) 135272

[startup+160.018 s]
Raw data (loadavg): 1.01 0.99 0.95 1/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) T 15524 15524 28974 0 -1 0 35338 0 0 0 15396 289 0 0 23 0 1 0 1846811417 145125376 35324 4294967295 134512640 135167914 3221224432 3221223272 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15529/statm): 35431 35324 162 162 0 35269 0
[pid=15529] vsize: 141724
Current children cumulated CPU time (s) 156.89
Current children cumulated vsize (Kb) 143852

[startup+170.019 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 37498 0 0 0 16359 306 0 0 25 0 1 0 1846811417 154099712 37484 4294967295 134512640 135167914 3221224432 3221223260 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 37622 37484 162 162 0 37460 0
[pid=15529] vsize: 150488
Current children cumulated CPU time (s) 166.69
Current children cumulated vsize (Kb) 152616

[startup+180.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 39642 0 0 0 17324 323 0 0 25 0 1 0 1846811417 162869248 39628 4294967295 134512640 135167914 3221224432 3221223344 134572069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 39763 39628 162 162 0 39601 0
[pid=15529] vsize: 159052
Current children cumulated CPU time (s) 176.51
Current children cumulated vsize (Kb) 161180

[startup+190.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 41793 0 0 0 18288 341 0 0 25 0 1 0 1846811417 171696128 41779 4294967295 134512640 135167914 3221224432 3221223216 134691301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 41918 41779 162 162 0 41756 0
[pid=15529] vsize: 167672
Current children cumulated CPU time (s) 186.33
Current children cumulated vsize (Kb) 169800

[startup+200.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 43922 0 0 0 19250 361 0 0 25 0 1 0 1846811417 180396032 43908 4294967295 134512640 135167914 3221224432 3221223244 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 44042 43908 162 162 0 43880 0
[pid=15529] vsize: 176168
Current children cumulated CPU time (s) 196.15
Current children cumulated vsize (Kb) 178296

[startup+210.023 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 46097 0 0 0 20213 379 0 0 25 0 1 0 1846811417 189308928 46083 4294967295 134512640 135167914 3221224432 3221222896 134591615 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 46218 46083 162 162 0 46056 0
[pid=15529] vsize: 184872
Current children cumulated CPU time (s) 205.96
Current children cumulated vsize (Kb) 187000

[startup+220.025 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 48260 0 0 0 21176 398 0 0 25 0 1 0 1846811417 198156288 48246 4294967295 134512640 135167914 3221224432 3221223296 134569893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 48378 48246 162 162 0 48216 0
[pid=15529] vsize: 193512
Current children cumulated CPU time (s) 215.78
Current children cumulated vsize (Kb) 195640

[startup+230.026 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 50426 0 0 0 22139 415 0 0 25 0 1 0 1846811417 207011840 50412 4294967295 134512640 135167914 3221224432 3221223264 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 50540 50412 162 162 0 50378 0
[pid=15529] vsize: 202160
Current children cumulated CPU time (s) 225.58
Current children cumulated vsize (Kb) 204288

[startup+240.027 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 52594 0 0 0 23103 432 0 0 25 0 1 0 1846811417 215867392 52580 4294967295 134512640 135167914 3221224432 3221222728 134846987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 52702 52580 162 162 0 52540 0
[pid=15529] vsize: 210808
Current children cumulated CPU time (s) 235.39
Current children cumulated vsize (Kb) 212936

[startup+250.028 s]
Raw data (loadavg): 1.00 0.99 0.95 1/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) T 15524 15524 28974 0 -1 0 54766 0 0 0 24066 449 0 0 25 0 1 0 1846811417 224776192 54752 4294967295 134512640 135167914 3221224432 3221223272 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15529/statm): 54877 54752 162 162 0 54715 0
[pid=15529] vsize: 219508
Current children cumulated CPU time (s) 245.19
Current children cumulated vsize (Kb) 221636

[startup+260.028 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 56944 0 0 0 25026 469 0 0 25 0 1 0 1846811417 233693184 56930 4294967295 134512640 135167914 3221224432 3221222720 134849430 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 57054 56930 162 162 0 56892 0
[pid=15529] vsize: 228216
Current children cumulated CPU time (s) 254.99
Current children cumulated vsize (Kb) 230344

[startup+270.029 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 59094 0 0 0 25990 488 0 0 25 0 1 0 1846811417 242475008 59080 4294967295 134512640 135167914 3221224432 3221222260 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15529/statm): 59198 59080 162 162 0 59036 0
[pid=15529] vsize: 236792
Current children cumulated CPU time (s) 264.82
Current children cumulated vsize (Kb) 238920

[startup+280.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 61251 0 0 0 26951 506 0 0 25 0 1 0 1846811417 251318272 61237 4294967295 134512640 135167914 3221224432 3221222176 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 61357 61237 162 162 0 61195 0
[pid=15529] vsize: 245428
Current children cumulated CPU time (s) 274.61
Current children cumulated vsize (Kb) 247556

[startup+290.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 63391 0 0 0 27918 522 0 0 25 0 1 0 1846811417 260079616 63377 4294967295 134512640 135167914 3221224432 3221222844 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 63496 63377 162 162 0 63334 0
[pid=15529] vsize: 253984
Current children cumulated CPU time (s) 284.44
Current children cumulated vsize (Kb) 256112

[startup+300.033 s]
Raw data (loadavg): 1.00 0.99 0.95 1/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) T 15524 15524 28974 0 -1 0 65522 0 0 0 28882 541 0 0 25 0 1 0 1846811417 268783616 65508 4294967295 134512640 135167914 3221224432 3221222620 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15529/statm): 65621 65508 162 162 0 65459 0
[pid=15529] vsize: 262484
Current children cumulated CPU time (s) 294.27
Current children cumulated vsize (Kb) 264612

[startup+310.036 s]
Raw data (loadavg): 1.00 0.99 0.95 1/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) T 15524 15524 28974 0 -1 0 67657 0 0 0 29841 559 0 0 25 0 1 0 1846811417 277536768 67643 4294967295 134512640 135167914 3221224432 3221223272 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15529/statm): 67758 67643 162 162 0 67596 0
[pid=15529] vsize: 271032
Current children cumulated CPU time (s) 304.04
Current children cumulated vsize (Kb) 273160

[startup+320.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 69822 0 0 0 30805 578 0 0 25 0 1 0 1846811417 286392320 69808 4294967295 134512640 135167914 3221224432 3221223216 134691319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 69920 69808 162 162 0 69758 0
[pid=15529] vsize: 279680
Current children cumulated CPU time (s) 313.87
Current children cumulated vsize (Kb) 281808

[startup+330.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 71984 0 0 0 31770 595 0 0 25 0 1 0 1846811417 295231488 71970 4294967295 134512640 135167914 3221224432 3221223184 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 72078 71970 162 162 0 71916 0
[pid=15529] vsize: 288312
Current children cumulated CPU time (s) 323.69
Current children cumulated vsize (Kb) 290440

[startup+340.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 74133 0 0 0 32731 616 0 0 25 0 1 0 1846811417 304021504 74119 4294967295 134512640 135167914 3221224432 3221221756 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 74224 74119 162 162 0 74062 0
[pid=15529] vsize: 296896
Current children cumulated CPU time (s) 333.51
Current children cumulated vsize (Kb) 299024

[startup+350.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 76286 0 0 0 33696 633 0 0 25 0 1 0 1846811417 312844288 76272 4294967295 134512640 135167914 3221224432 3221222720 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 76378 76272 162 162 0 76216 0
[pid=15529] vsize: 305512
Current children cumulated CPU time (s) 343.33
Current children cumulated vsize (Kb) 307640

[startup+360.043 s]
Raw data (loadavg): 1.00 0.99 0.95 1/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) T 15524 15524 28974 0 -1 0 78427 0 0 0 34658 653 0 0 25 0 1 0 1846811417 321871872 78413 4294967295 134512640 135167914 3221224432 3221223272 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15529/statm): 78582 78413 162 162 0 78420 0
[pid=15529] vsize: 314328
Current children cumulated CPU time (s) 353.15
Current children cumulated vsize (Kb) 316456

[startup+370.043 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 80539 0 0 0 35619 671 0 0 25 0 1 0 1846811417 330498048 80525 4294967295 134512640 135167914 3221224432 3221222856 134693621 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 80688 80525 162 162 0 80526 0
[pid=15529] vsize: 322752
Current children cumulated CPU time (s) 362.94
Current children cumulated vsize (Kb) 324880

[startup+380.044 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 82658 0 0 0 36583 687 0 0 25 0 1 0 1846811417 339177472 82644 4294967295 134512640 135167914 3221224432 3221222784 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 82807 82644 162 162 0 82645 0
[pid=15529] vsize: 331228
Current children cumulated CPU time (s) 372.74
Current children cumulated vsize (Kb) 333356

[startup+390.046 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 84783 0 0 0 37545 707 0 0 25 0 1 0 1846811417 347873280 84769 4294967295 134512640 135167914 3221224432 3221223152 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 84930 84769 162 162 0 84768 0
[pid=15529] vsize: 339720
Current children cumulated CPU time (s) 382.56
Current children cumulated vsize (Kb) 341848

[startup+400.048 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 86925 0 0 0 38509 725 0 0 25 0 1 0 1846811417 356638720 86911 4294967295 134512640 135167914 3221224432 3221222848 134581221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 87070 86911 162 162 0 86908 0
[pid=15529] vsize: 348280
Current children cumulated CPU time (s) 392.38
Current children cumulated vsize (Kb) 350408

[startup+410.048 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 89044 0 0 0 39471 744 0 0 25 0 1 0 1846811417 365318144 89030 4294967295 134512640 135167914 3221224432 3221222720 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15529/statm): 89189 89030 162 162 0 89027 0
[pid=15529] vsize: 356756
Current children cumulated CPU time (s) 402.19
Current children cumulated vsize (Kb) 358884

[startup+420.049 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 91166 0 0 0 40436 760 0 0 25 0 1 0 1846811417 374005760 91152 4294967295 134512640 135167914 3221224432 3221220912 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 91310 91152 162 162 0 91148 0
[pid=15529] vsize: 365240
Current children cumulated CPU time (s) 412
Current children cumulated vsize (Kb) 367368

[startup+430.049 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 93316 0 0 0 41402 777 0 0 25 0 1 0 1846811417 382787584 93302 4294967295 134512640 135167914 3221224432 3221223212 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 93454 93302 162 162 0 93292 0
[pid=15529] vsize: 373816
Current children cumulated CPU time (s) 421.83
Current children cumulated vsize (Kb) 375944

[startup+440.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 95441 0 0 0 42367 795 0 0 25 0 1 0 1846811417 391479296 95427 4294967295 134512640 135167914 3221224432 3221223200 134694588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15529/statm): 95576 95427 162 162 0 95414 0
[pid=15529] vsize: 382304
Current children cumulated CPU time (s) 431.66
Current children cumulated vsize (Kb) 384432

[startup+450.051 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 97571 0 0 0 43334 811 0 0 25 0 1 0 1846811417 400220160 97557 4294967295 134512640 135167914 3221224432 3221221792 134611849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 97710 97557 162 162 0 97548 0
[pid=15529] vsize: 390840
Current children cumulated CPU time (s) 441.49
Current children cumulated vsize (Kb) 392968

[startup+460.051 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 99697 0 0 0 44296 828 0 0 25 0 1 0 1846811417 408920064 99683 4294967295 134512640 135167914 3221224432 3221222844 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 99834 99683 162 162 0 99672 0
[pid=15529] vsize: 399336
Current children cumulated CPU time (s) 451.28
Current children cumulated vsize (Kb) 401464

[startup+470.053 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 101805 0 0 0 45259 847 0 0 25 0 1 0 1846811417 417538048 101791 4294967295 134512640 135167914 3221224432 3221221564 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 101938 101791 162 162 0 101776 0
[pid=15529] vsize: 407752
Current children cumulated CPU time (s) 461.1
Current children cumulated vsize (Kb) 409880

[startup+480.054 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 103932 0 0 0 46221 865 0 0 25 0 1 0 1846811417 426237952 103918 4294967295 134512640 135167914 3221224432 3221222800 134843015 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 104062 103918 162 162 0 103900 0
[pid=15529] vsize: 416248
Current children cumulated CPU time (s) 470.9
Current children cumulated vsize (Kb) 418376

[startup+490.055 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 106064 0 0 0 47181 884 0 0 25 0 1 0 1846811417 434978816 106050 4294967295 134512640 135167914 3221224432 3221223200 134695059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 106196 106050 162 162 0 106034 0
[pid=15529] vsize: 424784
Current children cumulated CPU time (s) 480.69
Current children cumulated vsize (Kb) 426912

[startup+500.056 s]
Raw data (loadavg): 1.07 1.01 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 108169 0 0 0 48138 902 0 0 25 0 1 0 1846811417 443596800 108155 4294967295 134512640 135167914 3221224432 3221222752 134612633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 108300 108155 162 162 0 108138 0
[pid=15529] vsize: 433200
Current children cumulated CPU time (s) 490.44
Current children cumulated vsize (Kb) 435328

[startup+510.056 s]
Raw data (loadavg): 1.06 1.01 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 110294 0 0 0 49103 918 0 0 25 0 1 0 1846811417 452292608 110280 4294967295 134512640 135167914 3221224432 3221223272 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 110423 110280 162 162 0 110261 0
[pid=15529] vsize: 441692
Current children cumulated CPU time (s) 500.25
Current children cumulated vsize (Kb) 443820

[startup+520.057 s]
Raw data (loadavg): 1.05 1.01 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 112438 0 0 0 50065 934 0 0 25 0 1 0 1846811417 461066240 112424 4294967295 134512640 135167914 3221224432 3221221276 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 112565 112424 162 162 0 112403 0
[pid=15529] vsize: 450260
Current children cumulated CPU time (s) 510.03
Current children cumulated vsize (Kb) 452388

[startup+530.058 s]
Raw data (loadavg): 1.04 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 114588 0 0 0 51028 951 0 0 25 0 1 0 1846811417 469848064 114574 4294967295 134512640 135167914 3221224432 3221222084 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 114709 114574 162 162 0 114547 0
[pid=15529] vsize: 458836
Current children cumulated CPU time (s) 519.83
Current children cumulated vsize (Kb) 460964

[startup+540.059 s]
Raw data (loadavg): 1.04 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 116698 0 0 0 51991 969 0 0 25 0 1 0 1846811417 478511104 116684 4294967295 134512640 135167914 3221224432 3221222624 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15529/statm): 116824 116684 162 162 0 116662 0
[pid=15529] vsize: 467296
Current children cumulated CPU time (s) 529.64
Current children cumulated vsize (Kb) 469424

[startup+550.06 s]
Raw data (loadavg): 1.03 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 118815 0 0 0 52953 987 0 0 25 0 1 0 1846811417 487145472 118801 4294967295 134512640 135167914 3221224432 3221223120 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 118932 118801 162 162 0 118770 0
[pid=15529] vsize: 475728
Current children cumulated CPU time (s) 539.44
Current children cumulated vsize (Kb) 477856

[startup+560.061 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 120931 0 0 0 53918 1005 0 0 25 0 1 0 1846811417 495820800 120917 4294967295 134512640 135167914 3221224432 3221222620 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 121050 120917 162 162 0 120888 0
[pid=15529] vsize: 484200
Current children cumulated CPU time (s) 549.27
Current children cumulated vsize (Kb) 486328

[startup+570.063 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 123068 0 0 0 54880 1024 0 0 25 0 1 0 1846811417 504578048 123054 4294967295 134512640 135167914 3221224432 3221222640 134522341 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 123188 123054 162 162 0 123026 0
[pid=15529] vsize: 492752
Current children cumulated CPU time (s) 559.08
Current children cumulated vsize (Kb) 494880

[startup+580.064 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 125189 0 0 0 55844 1043 0 0 25 0 1 0 1846811417 513261568 125175 4294967295 134512640 135167914 3221224432 3221221760 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 125308 125175 162 162 0 125146 0
[pid=15529] vsize: 501232
Current children cumulated CPU time (s) 568.91
Current children cumulated vsize (Kb) 503360

[startup+590.067 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 127329 0 0 0 56807 1060 0 0 25 0 1 0 1846811417 522022912 127315 4294967295 134512640 135167914 3221224432 3221222432 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 127447 127315 162 162 0 127285 0
[pid=15529] vsize: 509788
Current children cumulated CPU time (s) 578.71
Current children cumulated vsize (Kb) 511916

[startup+600.067 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 129457 0 0 0 57771 1077 0 0 25 0 1 0 1846811417 530722816 129443 4294967295 134512640 135167914 3221224432 3221223296 134569755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 129571 129443 162 162 0 129409 0
[pid=15529] vsize: 518284
Current children cumulated CPU time (s) 588.52
Current children cumulated vsize (Kb) 520412

[startup+610.068 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 131578 0 0 0 58739 1092 0 0 25 0 1 0 1846811417 539406336 131564 4294967295 134512640 135167914 3221224432 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 131691 131564 162 162 0 131529 0
[pid=15529] vsize: 526764
Current children cumulated CPU time (s) 598.35
Current children cumulated vsize (Kb) 528892

[startup+620.07 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 133690 0 0 0 59703 1108 0 0 25 0 1 0 1846811417 548032512 133676 4294967295 134512640 135167914 3221224432 3221221200 134611881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 133797 133676 162 162 0 133635 0
[pid=15529] vsize: 535188
Current children cumulated CPU time (s) 608.15
Current children cumulated vsize (Kb) 537316

[startup+630.071 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 135796 0 0 0 60665 1125 0 0 25 0 1 0 1846811417 556646400 135782 4294967295 134512640 135167914 3221224432 3221222704 134610320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15529/statm): 135900 135782 162 162 0 135738 0
[pid=15529] vsize: 543600
Current children cumulated CPU time (s) 617.94
Current children cumulated vsize (Kb) 545728

[startup+640.073 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 137903 0 0 0 61631 1141 0 0 25 0 1 0 1846811417 565301248 137889 4294967295 134512640 135167914 3221224432 3221222896 134591524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 138013 137889 162 162 0 137851 0
[pid=15529] vsize: 552052
Current children cumulated CPU time (s) 627.76
Current children cumulated vsize (Kb) 554180

[startup+650.074 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 140041 0 0 0 62592 1159 0 0 25 0 1 0 1846811417 574021632 140027 4294967295 134512640 135167914 3221224432 3221222864 134849096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 140142 140027 162 162 0 139980 0
[pid=15529] vsize: 560568
Current children cumulated CPU time (s) 637.55
Current children cumulated vsize (Kb) 562696

[startup+660.074 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 142154 0 0 0 63553 1177 0 0 25 0 1 0 1846811417 582688768 142140 4294967295 134512640 135167914 3221224432 3221221712 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 142258 142140 162 162 0 142096 0
[pid=15529] vsize: 569032
Current children cumulated CPU time (s) 647.34
Current children cumulated vsize (Kb) 571160

[startup+670.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 144277 0 0 0 64517 1193 0 0 25 0 1 0 1846811417 591380480 144263 4294967295 134512640 135167914 3221224432 3221221776 134522201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 144380 144263 162 162 0 144218 0
[pid=15529] vsize: 577520
Current children cumulated CPU time (s) 657.14
Current children cumulated vsize (Kb) 579648

[startup+680.077 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 146390 0 0 0 65480 1209 0 0 25 0 1 0 1846811417 600006656 146376 4294967295 134512640 135167914 3221224432 3221222624 134844893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 146486 146376 162 162 0 146324 0
[pid=15529] vsize: 585944
Current children cumulated CPU time (s) 666.93
Current children cumulated vsize (Kb) 588072

[startup+690.078 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 148520 0 0 0 66440 1227 0 0 25 0 1 0 1846811417 608747520 148506 4294967295 134512640 135167914 3221224432 3221223184 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 148620 148506 162 162 0 148458 0
[pid=15529] vsize: 594480
Current children cumulated CPU time (s) 676.71
Current children cumulated vsize (Kb) 596608

[startup+700.079 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 150640 0 0 0 67404 1245 0 0 25 0 1 0 1846811417 617431040 150626 4294967295 134512640 135167914 3221224432 3221222648 134722513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15529/statm): 150740 150626 162 162 0 150578 0
[pid=15529] vsize: 602960
Current children cumulated CPU time (s) 686.53
Current children cumulated vsize (Kb) 605088

[startup+710.08 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 152759 0 0 0 68367 1263 0 0 25 0 1 0 1846811417 626073600 152745 4294967295 134512640 135167914 3221224432 3221222096 134610708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 152850 152745 162 162 0 152688 0
[pid=15529] vsize: 611400
Current children cumulated CPU time (s) 696.34
Current children cumulated vsize (Kb) 613528

[startup+720.08 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 15529
Raw data (/proc/15524/stat): 15524 (minisat+_script) S 15523 15524 28974 0 -1 0 314 402 0 0 0 1 2 1 20 0 1 0 1846811408 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15524/statm): 532 234 485 147 0 385 0
[pid=15524] vsize: 2128
Raw data (/proc/15529/stat): 15529 (minisat+_bignum) R 15524 15524 28974 0 -1 0 162655 0 0 0 69334 1288 0 0 25 0 1 0 1846811417 666595328 162641 4294967295 134512640 135167914 3221224432 3221223064 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15529/statm): 162743 162641 162 162 0 162581 0
[pid=15529] vsize: 650972
Current children cumulated CPU time (s) 706.26
Current children cumulated vsize (Kb) 653100
One traced child (pid=15529) exited with status: 20
One traced child (pid=15524) exited with status: 20
All traced children have exited ! Game is over.

Child status: 20
Real time (s): 721.852
CPU time (s): 708.041
CPU user time (s): 694.824
CPU system time (s): 13.217
CPU usage (%): 98.0868
Max. virtual memory (cumulated for all children) (Kb): 653100

Verifier Data

ERROR: no interpretation found !