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/miplib3/normalized-mps-v2-20-10-gesa2_o.opb
MD5SUM70d38efa2ca4db2a9200144005e211ed
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 10368
Biggest coefficient in the objective function 418848431931392
Number of bits for the biggest coefficient in the objective function 49
Sum of the numbers in the objective function 180197911475330400
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 418848431931392
Number of bits of the biggest number in a constraint 49
Biggest sum of numbers in a constraint 180197911475330400
Number of bits of the biggest sum of numbers58
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables16224
Total number of constraints1584
Number of constraints which are clauses192
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1392
Minimum length of a constraint2
Maximum length of a constraint309

Trace number 4518

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        902440 kB
Buffers:         29100 kB
Cached:          77808 kB
SwapCached:        736 kB
Active:          31368 kB
Inactive:        78140 kB
HighTotal:      131008 kB
HighFree:        49532 kB
LowTotal:       903652 kB
LowFree:        852908 kB
SwapTotal:     2097136 kB
SwapFree:      2095896 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            16952 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:12:25 (client local time) WITH STATUS 0 IN 1201.73 SECONDS
stats: 2975 7 1201.73 0

Solver Data

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

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/3756/stat): 3756 (minisat+_script) R 3755 3756 15400 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793636831 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3756/statm): 174 3 169 147 0 27 0
[pid=3756] 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=3757
New process pid=3758
New process pid=3759
execve syscall for /bin/sed executable
One traced child (pid=3758) 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=3759) exited with status: 0
One traced child (pid=3757) exited with status: 0
New process pid=3760
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-gesa2_o.opb
One traced child (pid=3760) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=3761
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-gesa2_o.opb

[startup+10.0046 s]
Raw data (loadavg): 0.94 0.98 0.79 1/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 4379 0 3 0 934 23 0 0 25 0 1 0 1793636837 17514496 3982 4294967295 134512640 135167914 3221224448 3221193084 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 4276 3982 162 162 0 4114 0
[pid=3761] vsize: 17104
Current children cumulated CPU time (s) 9.59
Current children cumulated vsize (Kb) 19232

[startup+20.0072 s]
Raw data (loadavg): 0.95 0.98 0.79 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 10452 0 3 0 1883 51 0 0 25 0 1 0 1793636837 38338560 9066 4294967295 134512640 135167914 3221224448 3221193408 134522502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 9360 9066 162 162 0 9198 0
[pid=3761] vsize: 37440
Current children cumulated CPU time (s) 19.36
Current children cumulated vsize (Kb) 39568

[startup+30.0079 s]
Raw data (loadavg): 0.95 0.98 0.80 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 17021 0 3 0 2832 76 0 0 25 0 1 0 1793636837 59846656 14317 4294967295 134512640 135167914 3221224448 3221199064 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 14611 14317 162 162 0 14449 0
[pid=3761] vsize: 58444
Current children cumulated CPU time (s) 29.1
Current children cumulated vsize (Kb) 60572

[startup+40.0085 s]
Raw data (loadavg): 0.96 0.98 0.80 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 21393 0 3 0 3783 97 0 0 25 0 1 0 1793636837 77754368 18689 4294967295 134512640 135167914 3221224448 3221197952 134620469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 18983 18689 162 162 0 18821 0
[pid=3761] vsize: 75932
Current children cumulated CPU time (s) 38.82
Current children cumulated vsize (Kb) 78060

[startup+50.0092 s]
Raw data (loadavg): 0.97 0.98 0.80 1/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 30083 0 3 0 4734 127 0 0 25 0 1 0 1793636837 102551552 24742 4294967295 134512640 135167914 3221224448 3221195548 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 25037 24742 162 162 0 24875 0
[pid=3761] vsize: 100148
Current children cumulated CPU time (s) 48.63
Current children cumulated vsize (Kb) 102276

[startup+60.0098 s]
Raw data (loadavg): 0.97 0.98 0.80 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 34387 0 3 0 5691 144 0 0 25 0 1 0 1793636837 120176640 29046 4294967295 134512640 135167914 3221224448 3221193288 134847145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3761/statm): 29340 29046 162 162 0 29178 0
[pid=3761] vsize: 117360
Current children cumulated CPU time (s) 58.37
Current children cumulated vsize (Kb) 119488

[startup+70.0104 s]
Raw data (loadavg): 0.97 0.98 0.80 1/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 38582 0 3 0 6645 164 0 0 25 0 1 0 1793636837 137359360 33241 4294967295 134512640 135167914 3221224448 3221194652 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 33535 33241 162 162 0 33373 0
[pid=3761] vsize: 134140
Current children cumulated CPU time (s) 68.11
Current children cumulated vsize (Kb) 136268

[startup+80.0121 s]
Raw data (loadavg): 0.98 0.98 0.81 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 42729 0 3 0 7600 184 0 0 25 0 1 0 1793636837 154345472 37388 4294967295 134512640 135167914 3221224448 3221194144 134621031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 37682 37388 162 162 0 37520 0
[pid=3761] vsize: 150728
Current children cumulated CPU time (s) 77.86
Current children cumulated vsize (Kb) 152856

[startup+90.0127 s]
Raw data (loadavg): 0.98 0.98 0.81 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 55572 0 3 0 8551 219 0 0 25 0 1 0 1793636837 185352192 44958 4294967295 134512640 135167914 3221224448 3221195680 134694410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 45252 44958 162 162 0 45090 0
[pid=3761] vsize: 181008
Current children cumulated CPU time (s) 87.72
Current children cumulated vsize (Kb) 183136

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.81 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 59713 0 3 0 9504 238 0 0 25 0 1 0 1793636837 202313728 49099 4294967295 134512640 135167914 3221224448 3221195264 134620419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 49393 49099 162 162 0 49231 0
[pid=3761] vsize: 197572
Current children cumulated CPU time (s) 97.44
Current children cumulated vsize (Kb) 199700

[startup+110.013 s]
Raw data (loadavg): 0.99 0.98 0.81 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 63837 0 3 0 10455 259 0 0 25 0 1 0 1793636837 219213824 53223 4294967295 134512640 135167914 3221224448 3221194480 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 53519 53223 162 162 0 53357 0
[pid=3761] vsize: 214076
Current children cumulated CPU time (s) 107.16
Current children cumulated vsize (Kb) 216204

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.81 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 67836 0 3 0 11412 276 0 0 25 0 1 0 1793636837 235593728 57222 4294967295 134512640 135167914 3221224448 3221196112 134522462 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 57518 57222 162 162 0 57356 0
[pid=3761] vsize: 230072
Current children cumulated CPU time (s) 116.9
Current children cumulated vsize (Kb) 232200

[startup+130.014 s]
Raw data (loadavg): 0.99 0.98 0.82 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 71888 0 3 0 12365 298 0 0 25 0 1 0 1793636837 252190720 61274 4294967295 134512640 135167914 3221224448 3221194828 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3761/statm): 61570 61274 162 162 0 61408 0
[pid=3761] vsize: 246280
Current children cumulated CPU time (s) 126.65
Current children cumulated vsize (Kb) 248408

[startup+140.015 s]
Raw data (loadavg): 1.06 1.00 0.82 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 75866 0 3 0 13322 315 0 0 25 0 1 0 1793636837 268480512 65252 4294967295 134512640 135167914 3221224448 3221194796 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 65547 65252 162 162 0 65385 0
[pid=3761] vsize: 262188
Current children cumulated CPU time (s) 136.39
Current children cumulated vsize (Kb) 264316

[startup+150.016 s]
Raw data (loadavg): 1.05 1.00 0.82 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 79779 0 3 0 14276 334 0 0 25 0 1 0 1793636837 284508160 69165 4294967295 134512640 135167914 3221224448 3221194332 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 69460 69165 162 162 0 69298 0
[pid=3761] vsize: 277840
Current children cumulated CPU time (s) 146.12
Current children cumulated vsize (Kb) 279968

[startup+160.016 s]
Raw data (loadavg): 1.04 1.00 0.82 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 83549 0 3 0 15233 352 0 0 25 0 1 0 1793636837 299950080 72935 4294967295 134512640 135167914 3221224448 3221194396 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 73230 72935 162 162 0 73068 0
[pid=3761] vsize: 292920
Current children cumulated CPU time (s) 155.87
Current children cumulated vsize (Kb) 295048

[startup+170.016 s]
Raw data (loadavg): 1.04 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 107591 0 3 0 16151 414 0 0 25 0 1 0 1793636837 398426112 96977 4294967295 134512640 135167914 3221224448 3221194072 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 97272 96977 162 162 0 97110 0
[pid=3761] vsize: 389088
Current children cumulated CPU time (s) 165.67
Current children cumulated vsize (Kb) 391216

[startup+180.016 s]
Raw data (loadavg): 1.03 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 108790 0 3 0 17137 422 0 0 25 0 1 0 1793636837 360140800 87630 4294967295 134512640 135167914 3221224448 3221194256 134624994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 87925 87630 162 162 0 87763 0
[pid=3761] vsize: 351700
Current children cumulated CPU time (s) 175.61
Current children cumulated vsize (Kb) 353828

[startup+190.017 s]
Raw data (loadavg): 1.03 1.00 0.83 1/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 112488 0 3 0 18097 439 0 0 25 0 1 0 1793636837 375287808 91328 4294967295 134512640 135167914 3221224448 3221193756 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 91623 91328 162 162 0 91461 0
[pid=3761] vsize: 366492
Current children cumulated CPU time (s) 185.38
Current children cumulated vsize (Kb) 368620

[startup+200.017 s]
Raw data (loadavg): 1.02 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 116214 0 3 0 19058 455 0 0 25 0 1 0 1793636837 390549504 95054 4294967295 134512640 135167914 3221224448 3221194880 134844641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 95349 95054 162 162 0 95187 0
[pid=3761] vsize: 381396
Current children cumulated CPU time (s) 195.15
Current children cumulated vsize (Kb) 383524

[startup+210.017 s]
Raw data (loadavg): 1.02 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 119976 0 3 0 20018 470 0 0 25 0 1 0 1793636837 405958656 98816 4294967295 134512640 135167914 3221224448 3221198460 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 99111 98816 162 162 0 98949 0
[pid=3761] vsize: 396444
Current children cumulated CPU time (s) 204.9
Current children cumulated vsize (Kb) 398572

[startup+220.018 s]
Raw data (loadavg): 1.01 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 123768 0 3 0 20975 488 0 0 25 0 1 0 1793636837 421490688 102608 4294967295 134512640 135167914 3221224448 3221193760 134844694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 102903 102608 162 162 0 102741 0
[pid=3761] vsize: 411612
Current children cumulated CPU time (s) 214.65
Current children cumulated vsize (Kb) 413740

[startup+230.019 s]
Raw data (loadavg): 1.01 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 127392 0 3 0 21937 505 0 0 25 0 1 0 1793636837 436334592 106232 4294967295 134512640 135167914 3221224448 3221195840 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 106527 106232 162 162 0 106365 0
[pid=3761] vsize: 426108
Current children cumulated CPU time (s) 224.44
Current children cumulated vsize (Kb) 428236

[startup+240.019 s]
Raw data (loadavg): 1.01 1.00 0.83 1/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 130994 0 3 0 22899 521 0 0 25 0 1 0 1793636837 451088384 109834 4294967295 134512640 135167914 3221224448 3221192988 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 110129 109834 162 162 0 109967 0
[pid=3761] vsize: 440516
Current children cumulated CPU time (s) 234.22
Current children cumulated vsize (Kb) 442644

[startup+250.02 s]
Raw data (loadavg): 1.01 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 134717 0 3 0 23862 536 0 0 25 0 1 0 1793636837 466337792 113557 4294967295 134512640 135167914 3221224448 3221197184 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 113852 113557 162 162 0 113690 0
[pid=3761] vsize: 455408
Current children cumulated CPU time (s) 244
Current children cumulated vsize (Kb) 457536

[startup+260.021 s]
Raw data (loadavg): 1.01 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 138480 0 3 0 24823 551 0 0 25 0 1 0 1793636837 481751040 117320 4294967295 134512640 135167914 3221224448 3221194912 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 117615 117320 162 162 0 117453 0
[pid=3761] vsize: 470460
Current children cumulated CPU time (s) 253.76
Current children cumulated vsize (Kb) 472588

[startup+270.021 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 142256 0 3 0 25784 566 0 0 25 0 1 0 1793636837 497217536 121096 4294967295 134512640 135167914 3221224448 3221196416 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 121391 121096 162 162 0 121229 0
[pid=3761] vsize: 485564
Current children cumulated CPU time (s) 263.52
Current children cumulated vsize (Kb) 487692

[startup+280.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 145907 0 3 0 26747 582 0 0 25 0 1 0 1793636837 512172032 124747 4294967295 134512640 135167914 3221224448 3221195008 134843068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 125042 124747 162 162 0 124880 0
[pid=3761] vsize: 500168
Current children cumulated CPU time (s) 273.31
Current children cumulated vsize (Kb) 502296

[startup+290.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 149530 0 3 0 27705 600 0 0 25 0 1 0 1793636837 527007744 128370 4294967295 134512640 135167914 3221224448 3221194348 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 128664 128370 162 162 0 128502 0
[pid=3761] vsize: 514656
Current children cumulated CPU time (s) 283.07
Current children cumulated vsize (Kb) 516784

[startup+300.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 153227 0 3 0 28665 615 0 0 25 0 1 0 1793636837 542171136 132067 4294967295 134512640 135167914 3221224448 3221195232 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 132366 132067 162 162 0 132204 0
[pid=3761] vsize: 529464
Current children cumulated CPU time (s) 292.82
Current children cumulated vsize (Kb) 531592

[startup+310.023 s]
Raw data (loadavg): 1.00 1.00 0.84 1/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 156864 0 3 0 29628 631 0 0 25 0 1 0 1793636837 557068288 135704 4294967295 134512640 135167914 3221224448 3221194844 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136003 135704 162 162 0 135841 0
[pid=3761] vsize: 544012
Current children cumulated CPU time (s) 302.61
Current children cumulated vsize (Kb) 546140

[startup+320.023 s]
Raw data (loadavg): 1.00 1.00 0.84 1/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 160357 0 3 0 30591 648 0 0 25 0 1 0 1793636837 571375616 139197 4294967295 134512640 135167914 3221224448 3221194428 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 139496 139197 162 162 0 139334 0
[pid=3761] vsize: 557984
Current children cumulated CPU time (s) 312.41
Current children cumulated vsize (Kb) 560112

[startup+330.024 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 163858 0 3 0 31554 664 0 0 25 0 1 0 1793636837 585715712 142698 4294967295 134512640 135167914 3221224448 3221198324 134697299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 142997 142698 162 162 0 142835 0
[pid=3761] vsize: 571988
Current children cumulated CPU time (s) 322.2
Current children cumulated vsize (Kb) 574116

[startup+340.025 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 167525 0 3 0 32516 680 0 0 25 0 1 0 1793636837 600727552 146365 4294967295 134512640 135167914 3221224448 3221196412 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 146662 146365 162 162 0 146500 0
[pid=3761] vsize: 586648
Current children cumulated CPU time (s) 331.98
Current children cumulated vsize (Kb) 588776

[startup+350.024 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 173474 0 3 0 33471 703 0 0 25 0 1 0 1793636837 788549632 152314 4294967295 134512640 135167914 3221224448 3221196608 134625368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 192517 152321 162 162 0 192355 0
[pid=3761] vsize: 770068
Current children cumulated CPU time (s) 341.76
Current children cumulated vsize (Kb) 772196

[startup+360.025 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 213380 0 3 0 34372 803 0 0 25 0 1 0 1793636837 788549632 192220 4294967295 134512640 135167914 3221224448 3221196576 134624957 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 192517 192220 162 162 0 192355 0
[pid=3761] vsize: 770068
Current children cumulated CPU time (s) 351.77
Current children cumulated vsize (Kb) 772196

[startup+370.026 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 214235 0 3 0 35359 811 0 0 25 0 1 0 1793636837 705662976 171984 4294967295 134512640 135167914 3221224448 3221194620 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 172281 171984 162 162 0 172119 0
[pid=3761] vsize: 689124
Current children cumulated CPU time (s) 361.72
Current children cumulated vsize (Kb) 691252

[startup+380.026 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 217817 0 3 0 36318 829 0 0 25 0 1 0 1793636837 720334848 175566 4294967295 134512640 135167914 3221224448 3221195964 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3761/statm): 175863 175566 162 162 0 175701 0
[pid=3761] vsize: 703452
Current children cumulated CPU time (s) 371.49
Current children cumulated vsize (Kb) 705580

[startup+390.027 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220785 0 3 0 37286 843 0 0 25 0 1 0 1793636837 732491776 178534 4294967295 134512640 135167914 3221224448 3221223200 134693573 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 178831 178534 162 162 0 178669 0
[pid=3761] vsize: 715324
Current children cumulated CPU time (s) 381.31
Current children cumulated vsize (Kb) 717452

[startup+400.027 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 38278 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221222984 134846907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 391.31
Current children cumulated vsize (Kb) 548724

[startup+410.028 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 39278 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221222984 134846907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 401.31
Current children cumulated vsize (Kb) 548724

[startup+420.029 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 40278 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219440 134844713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 411.31
Current children cumulated vsize (Kb) 548724

[startup+430.03 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 41279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219712 134630858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 421.32
Current children cumulated vsize (Kb) 548724

[startup+440.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 42279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220400 134849096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 431.32
Current children cumulated vsize (Kb) 548724

[startup+450.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 43279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219804 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 441.32
Current children cumulated vsize (Kb) 548724

[startup+460.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 44279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219452 134723267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 451.32
Current children cumulated vsize (Kb) 548724

[startup+470.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 45279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220224 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 461.32
Current children cumulated vsize (Kb) 548724

[startup+480.031 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 46279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219716 134629088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 471.32
Current children cumulated vsize (Kb) 548724

[startup+490.032 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 47280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220432 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 481.33
Current children cumulated vsize (Kb) 548724

[startup+500.033 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 48280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219792 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 491.33
Current children cumulated vsize (Kb) 548724

[startup+510.033 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 49280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219692 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 501.33
Current children cumulated vsize (Kb) 548724

[startup+520.034 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 50280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219776 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 511.33
Current children cumulated vsize (Kb) 548724

[startup+530.035 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 51280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220144 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 521.33
Current children cumulated vsize (Kb) 548724

[startup+540.035 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 52281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219896 134629265 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 531.34
Current children cumulated vsize (Kb) 548724

[startup+550.036 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 53281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219532 134694320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 541.34
Current children cumulated vsize (Kb) 548724

[startup+560.037 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 54281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219856 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 551.34
Current children cumulated vsize (Kb) 548724

[startup+570.037 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 55281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220368 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 561.34
Current children cumulated vsize (Kb) 548724

[startup+580.038 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 56281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219616 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 571.34
Current children cumulated vsize (Kb) 548724

[startup+590.038 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 57282 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220560 134694377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 581.35
Current children cumulated vsize (Kb) 548724

[startup+600.039 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 58282 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220220 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 591.35
Current children cumulated vsize (Kb) 548724

[startup+610.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 59282 852 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220528 134720503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 601.36
Current children cumulated vsize (Kb) 548724

[startup+620.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 60281 852 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219836 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 611.35
Current children cumulated vsize (Kb) 548724

[startup+630.041 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 61281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220144 134844691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 621.36
Current children cumulated vsize (Kb) 548724

[startup+640.042 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 62281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219392 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 631.36
Current children cumulated vsize (Kb) 548724

[startup+650.041 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 63281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220400 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 641.36
Current children cumulated vsize (Kb) 548724

[startup+660.042 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 64281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220496 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 651.36
Current children cumulated vsize (Kb) 548724

[startup+670.043 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 65281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219656 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 661.36
Current children cumulated vsize (Kb) 548724

[startup+680.043 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 66282 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219904 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 671.37
Current children cumulated vsize (Kb) 548724

[startup+690.044 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 67282 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219692 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 681.37
Current children cumulated vsize (Kb) 548724

[startup+700.044 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 68282 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219712 134628817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 691.37
Current children cumulated vsize (Kb) 548724

[startup+710.045 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 69282 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219676 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 701.37
Current children cumulated vsize (Kb) 548724

[startup+720.045 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 70282 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220332 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 711.38
Current children cumulated vsize (Kb) 548724

[startup+730.045 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 71282 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220960 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 721.38
Current children cumulated vsize (Kb) 548724

[startup+740.046 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 72283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220752 134694329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 731.39
Current children cumulated vsize (Kb) 548724

[startup+750.046 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 73283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220672 134844713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 741.39
Current children cumulated vsize (Kb) 548724

[startup+760.046 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 74283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219452 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 751.39
Current children cumulated vsize (Kb) 548724

[startup+770.046 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 75283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220624 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 761.39
Current children cumulated vsize (Kb) 548724

[startup+780.047 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 76283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219744 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 771.39
Current children cumulated vsize (Kb) 548724

[startup+790.047 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 77284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220844 134718504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 781.4
Current children cumulated vsize (Kb) 548724

[startup+800.048 s]
Raw data (loadavg): 1.00 1.00 0.89 3/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 78283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220848 134844700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 791.39
Current children cumulated vsize (Kb) 548724

[startup+810.048 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 79284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219296 134718497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 801.4
Current children cumulated vsize (Kb) 548724

[startup+820.048 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 80284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221222284 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 811.4
Current children cumulated vsize (Kb) 548724

[startup+830.049 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 81284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220368 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 821.4
Current children cumulated vsize (Kb) 548724

[startup+840.049 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 82284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220412 134522184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 831.4
Current children cumulated vsize (Kb) 548724

[startup+850.049 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 83284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221932 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 841.4
Current children cumulated vsize (Kb) 548724

[startup+860.05 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 84285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220496 134696321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 851.41
Current children cumulated vsize (Kb) 548724

[startup+870.05 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 85285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219616 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 861.41
Current children cumulated vsize (Kb) 548724

[startup+880.051 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 86285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220412 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 871.41
Current children cumulated vsize (Kb) 548724

[startup+890.052 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 87285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219952 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 881.41
Current children cumulated vsize (Kb) 548724

[startup+900.052 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 88285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220208 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 891.41
Current children cumulated vsize (Kb) 548724

[startup+910.053 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 89286 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 901.42
Current children cumulated vsize (Kb) 548724

[startup+920.053 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 90286 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221808 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 911.42
Current children cumulated vsize (Kb) 548724

[startup+930.054 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 91286 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220144 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 921.42
Current children cumulated vsize (Kb) 548724

[startup+940.055 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 92286 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220400 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 931.42
Current children cumulated vsize (Kb) 548724

[startup+950.054 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 93286 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221176 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 941.43
Current children cumulated vsize (Kb) 548724

[startup+960.055 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 94287 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220756 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 951.44
Current children cumulated vsize (Kb) 548724

[startup+970.056 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 95287 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221024 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 961.44
Current children cumulated vsize (Kb) 548724

[startup+980.056 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 96287 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221104 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 971.44
Current children cumulated vsize (Kb) 548724

[startup+990.057 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 97287 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220048 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 981.44
Current children cumulated vsize (Kb) 548724

[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 98288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220960 134630883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 991.45
Current children cumulated vsize (Kb) 548724

[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 99288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220912 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1001.45
Current children cumulated vsize (Kb) 548724

[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 100288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220188 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1011.45
Current children cumulated vsize (Kb) 548724

[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 101288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220380 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1021.45
Current children cumulated vsize (Kb) 548724

[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 102288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219872 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1031.45
Current children cumulated vsize (Kb) 548724

[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 103288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220760 134694481 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1041.45
Current children cumulated vsize (Kb) 548724

[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 104289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220384 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1051.46
Current children cumulated vsize (Kb) 548724

[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 105289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219792 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1061.46
Current children cumulated vsize (Kb) 548724

[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 106289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219984 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1071.46
Current children cumulated vsize (Kb) 548724

[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 107289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220672 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1081.46
Current children cumulated vsize (Kb) 548724

[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 108289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220316 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1091.46
Current children cumulated vsize (Kb) 548724

[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 109289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220904 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1101.46
Current children cumulated vsize (Kb) 548724

[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 110290 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220764 134696560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1111.47
Current children cumulated vsize (Kb) 548724

[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 111290 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220892 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0
[pid=3761] vsize: 546596
Current children cumulated CPU time (s) 1121.47
Current children cumulated vsize (Kb) 548724

[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 112290 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221196384 134847159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1131.47
Current children cumulated vsize (Kb) 547244

[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 113290 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221196064 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1141.47
Current children cumulated vsize (Kb) 547244

[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 114290 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221194528 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1151.47
Current children cumulated vsize (Kb) 547244

[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 115291 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221194576 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1161.48
Current children cumulated vsize (Kb) 547244

[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 116291 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221194332 134722208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1171.48
Current children cumulated vsize (Kb) 547244

[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 117291 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221195840 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1181.48
Current children cumulated vsize (Kb) 547244

[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 118291 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221194048 134624188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1191.48
Current children cumulated vsize (Kb) 547244

[startup+1210.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 119291 856 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221195008 134624957 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1201.49
Current children cumulated vsize (Kb) 547244



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 3761
Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3756/statm): 532 234 485 147 0 385 0
[pid=3756] vsize: 2128
Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 119291 856 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221195040 134625423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0
[pid=3761] vsize: 545116
Current children cumulated CPU time (s) 1201.49
Current children cumulated vsize (Kb) 547244

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

Child status: 0
Real time (s): 1210.32
CPU time (s): 1201.73
CPU user time (s): 1192.91
CPU system time (s): 8.81466
CPU usage (%): 99.2902
Max. virtual memory (cumulated for all children) (Kb): 772196

Verifier Data

ERROR: no interpretation found !