Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-gesa2-o.opb
MD5SUM97cd691a4b46f7816d8643c161590ce9
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 7248
Biggest coefficient in the objective function 409031671808
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 178209334735200
Number of bits of the sum of numbers in the objective function 48
Biggest number in a constraint 409031671808
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 178209334735200
Number of bits of the biggest sum of numbers48
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables11184
Total number of constraints1968
Number of constraints which are clauses192
Number of constraints which are cardinality constraints (but not clauses)384
Number of constraints which are nor clauses,nor cardinality constraints1392
Minimum length of a constraint1
Maximum length of a constraint209

Trace number 6132

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        919356 kB
Buffers:          6808 kB
Cached:          79208 kB
SwapCached:        820 kB
Active:          19668 kB
Inactive:        68956 kB
HighTotal:      131008 kB
HighFree:        47684 kB
LowTotal:       903652 kB
LowFree:        871672 kB
SwapTotal:     2097892 kB
SwapFree:      2096508 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5640 kB
Slab:            20872 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:59:01 (client local time) WITH STATUS 0 IN 1208.21 SECONDS
stats: 3295 7 1208.21 0

Solver Data

c Parsing PB file...
c Converting 1608 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss..............................................
c ---[1772]---> BDD-cost:    2
c ---[1767]---> BDD-cost:    2
c ---[1762]---> BDD-cost:    2
c ---[1757]---> BDD-cost:    2
c ---[1752]---> BDD-cost:    2
c ---[1747]---> BDD-cost:    2
c ---[1742]---> BDD-cost:    2
c ---[1737]---> BDD-cost:    2
c ---[1732]---> BDD-cost:    2
c ---[1727]---> BDD-cost:    2
c ---[1722]---> BDD-cost:    2
c ---[1717]---> BDD-cost:    2
c ---[1712]---> BDD-cost:    2
c ---[1707]---> BDD-cost:    2
c ---[1702]---> BDD-cost:    2
c ---[1697]---> BDD-cost:    2
c ---[1692]---> BDD-cost:    2
c ---[1687]---> BDD-cost:    2
c ---[1682]---> BDD-cost:    2
c ---[1677]---> BDD-cost:    2
c ---[1672]---> BDD-cost:    2
c ---[1667]---> BDD-cost:    2
c ---[1662]---> BDD-cost:    2
c ---[1657]---> BDD-cost:    2
c ---[1652]---> BDD-cost:    2
c ---[1647]---> BDD-cost:    2
c ---[1642]---> BDD-cost:    2
c ---[1637]---> BDD-cost:    2
c ---[1632]---> BDD-cost:    2
c ---[1627]---> BDD-cost:    2
c ---[1622]---> BDD-cost:    2
c ---[1617]---> BDD-cost:    2
c ---[1612]---> BDD-cost:    2
c ---[1607]---> BDD-cost:    2
c ---[1602]---> BDD-cost:    2
c ---[1597]---> BDD-cost:    2
c ---[1592]---> BDD-cost:    2
c ---[1587]---> BDD-cost:    2
c ---[1582]---> BDD-cost:    2
c ---[1577]---> BDD-cost:    2
c ---[1572]---> BDD-cost:    2
c ---[1567]---> BDD-cost:    2
c ---[1562]---> BDD-cost:    2
c ---[1557]---> BDD-cost:    2
c ---[1552]---> BDD-cost:    2
c ---[1547]---> BDD-cost:    2
c ---[1542]---> BDD-cost:    2
c ---[1537]---> BDD-cost:    2
c ---[1534]---> Adder-cost: 1880   maxlim: 21444920106   bits: 35/35
c ---[1532]---> Adder-cost: 1880   maxlim: 17881656106   bits: 35/35
c ---[1530]---> BDD-cost:  110
c ---[1529]---> BDD-cost:    9
c ---[1528]---> BDD-cost:    9
c ---[1527]---> BDD-cost:    9
c ---[1526]---> BDD-cost:    9
c ---[1518]---> BDD-cost:  110
c ---[1506]---> BDD-cost:  110
c ---[1494]---> BDD-cost:  110
c ---[1482]---> BDD-cost:  110
c ---[1470]---> BDD-cost:  110
c ---[1469]---> BDD-cost:    9
c ---[1468]---> BDD-cost:    9
c ---[1467]---> BDD-cost:    9
c ---[1466]---> BDD-cost:    9
c ---[1465]---> BDD-cost:    9
c ---[1464]---> BDD-cost:    9
c ---[1463]---> BDD-cost:    9
c ---[1462]---> BDD-cost:    9
c ---[1461]---> BDD-cost:    9
c ---[1460]---> BDD-cost:    9
c ---[1458]---> BDD-cost:  108
c ---[1457]---> BDD-cost:    9
c ---[1456]---> BDD-cost:    9
c ---[1455]---> BDD-cost:    9
c ---[1454]---> BDD-cost:    9
c ---[1453]---> BDD-cost:    9
c ---[1452]---> BDD-cost:    9
c ---[1451]---> BDD-cost:    9
c ---[1450]---> BDD-cost:    9
c ---[1449]---> BDD-cost:    9
c ---[1448]---> BDD-cost:    9
c ---[1446]---> BDD-cost:  110
c ---[1445]---> BDD-cost:    9
c ---[1444]---> BDD-cost:    9
c ---[1443]---> BDD-cost:    9
c ---[1434]---> BDD-cost:  110
c ---[1422]---> BDD-cost:  110
c ---[1410]---> Adder-cost: 1880   maxlim: 17790008106   bits: 35/35
c ---[1408]---> BDD-cost:  110
c ---[1396]---> BDD-cost:  110
c ---[1386]---> BDD-cost:   18
c ---[1384]---> BDD-cost:  110
c ---[1383]---> BDD-cost:   18
c ---[1382]---> BDD-cost:   18
c ---[1381]---> BDD-cost:   18
c ---[1380]---> BDD-cost:   18
c ---[1379]---> BDD-cost:   18
c ---[1378]---> BDD-cost:   18
c ---[1377]---> BDD-cost:   18
c ---[1376]---> BDD-cost:   18
c ---[137

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/28530/stat): 28530 (minisat+_script) R 28529 28530 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855360409 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/28530/statm): 174 3 169 147 0 27 0
[pid=28530] 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=28531
New process pid=28532
New process pid=28533
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
One traced child (pid=28532) exited with status: 0
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=28533) exited with status: 0
One traced child (pid=28531) exited with status: 0
New process pid=28534
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-gesa2-o.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 877 69 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221219264 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 9.47
Current children cumulated vsize (Kb) 37220

[startup+20.0044 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 1876 69 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221219644 134778873 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 19.46
Current children cumulated vsize (Kb) 37220

[startup+30.0051 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 2876 69 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221220640 134676341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 29.46
Current children cumulated vsize (Kb) 37220

[startup+40.0058 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 3875 69 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221220132 134677077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 39.45
Current children cumulated vsize (Kb) 37220

[startup+50.0065 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 4875 70 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221219840 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 49.46
Current children cumulated vsize (Kb) 37220

[startup+60.0072 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 5875 70 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221220320 134676999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 59.46
Current children cumulated vsize (Kb) 37220

[startup+70.008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 6875 70 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221220224 134677239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 69.46
Current children cumulated vsize (Kb) 37220

[startup+80.0097 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 7875 70 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221220724 134676992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 79.46
Current children cumulated vsize (Kb) 37220

[startup+90.0104 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 8875 71 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221221024 134676376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 89.47
Current children cumulated vsize (Kb) 37220

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 9874 71 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 99.46
Current children cumulated vsize (Kb) 37220

[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 10874 72 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221219872 134676545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 109.47
Current children cumulated vsize (Kb) 37220

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 11874 72 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221220576 134600301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 119.47
Current children cumulated vsize (Kb) 37220

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 12874 72 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 129.47
Current children cumulated vsize (Kb) 37220

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 13874 72 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221219392 134677233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 139.47
Current children cumulated vsize (Kb) 37220

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 19194 0 0 0 14874 72 0 0 25 0 1 0 1855360414 35938304 8608 4294967295 134512640 135094434 3221224432 3221220928 134677248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8608 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 149.47
Current children cumulated vsize (Kb) 37220

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 15863 82 0 0 25 0 1 0 1855360414 46739456 11255 4294967295 134512640 135094434 3221224432 3221199760 134596997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 11411 11255 145 145 0 11266 0
[pid=28534] vsize: 45644
Current children cumulated CPU time (s) 159.46
Current children cumulated vsize (Kb) 47768

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 16862 83 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221220636 134677378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 169.46
Current children cumulated vsize (Kb) 37220

[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 17862 83 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221219872 134601161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 179.46
Current children cumulated vsize (Kb) 37220

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 18862 84 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221219344 134600116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 189.47
Current children cumulated vsize (Kb) 37220

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 19862 84 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221219616 134677021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 199.47
Current children cumulated vsize (Kb) 37220

[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 20862 84 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221221080 134676241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 209.47
Current children cumulated vsize (Kb) 37220

[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 21861 85 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221220648 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 219.47
Current children cumulated vsize (Kb) 37220

[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 22861 85 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221221376 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 229.47
Current children cumulated vsize (Kb) 37220

[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 23861 86 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221219404 134676610 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 239.48
Current children cumulated vsize (Kb) 37220

[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 24860 86 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221221096 134600155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 249.47
Current children cumulated vsize (Kb) 37220

[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 25860 87 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221221088 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 259.48
Current children cumulated vsize (Kb) 37220

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 26860 87 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221220400 134677327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 269.48
Current children cumulated vsize (Kb) 37220

[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 27860 87 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221221076 134676244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 279.48
Current children cumulated vsize (Kb) 37220

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 28860 87 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221220752 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 289.48
Current children cumulated vsize (Kb) 37220

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 29859 87 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221221456 134600307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 299.47
Current children cumulated vsize (Kb) 37220

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 23159 0 0 0 30860 87 0 0 25 0 1 0 1855360414 35938304 8618 4294967295 134512640 135094434 3221224432 3221220120 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8774 8618 145 145 0 8629 0
[pid=28534] vsize: 35096
Current children cumulated CPU time (s) 309.48
Current children cumulated vsize (Kb) 37220

[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 31811 123 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 319.35
Current children cumulated vsize (Kb) 37276

[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 32811 123 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221219344 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 329.35
Current children cumulated vsize (Kb) 37276

[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 33810 123 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221220048 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 339.34
Current children cumulated vsize (Kb) 37276

[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 34810 123 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221219520 134677313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 349.34
Current children cumulated vsize (Kb) 37276

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 35810 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221219492 134676244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 359.35
Current children cumulated vsize (Kb) 37276

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 36810 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221219856 134600738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 369.35
Current children cumulated vsize (Kb) 37276

[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 37810 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221219680 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 379.35
Current children cumulated vsize (Kb) 37276

[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 38810 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 389.35
Current children cumulated vsize (Kb) 37276

[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 39811 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221220400 134600144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 399.36
Current children cumulated vsize (Kb) 37276

[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 40811 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221220108 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 409.36
Current children cumulated vsize (Kb) 37276

[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 41811 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 419.36
Current children cumulated vsize (Kb) 37276

[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 42811 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 429.36
Current children cumulated vsize (Kb) 37276

[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 43811 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 439.36
Current children cumulated vsize (Kb) 37276

[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 44811 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221219416 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 449.36
Current children cumulated vsize (Kb) 37276

[startup+460.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 45812 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221220032 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 459.37
Current children cumulated vsize (Kb) 37276

[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 34577 0 0 0 46812 124 0 0 25 0 1 0 1855360414 35995648 8632 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8788 8632 145 145 0 8643 0
[pid=28534] vsize: 35152
Current children cumulated CPU time (s) 469.37
Current children cumulated vsize (Kb) 37276

[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 47771 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221218912 134676301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 479.28
Current children cumulated vsize (Kb) 37228

[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 48771 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221219520 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 489.28
Current children cumulated vsize (Kb) 37228

[startup+500.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 49771 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220204 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 499.28
Current children cumulated vsize (Kb) 37228

[startup+510.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 50772 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220200 134677149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 509.29
Current children cumulated vsize (Kb) 37228

[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 51773 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 519.3
Current children cumulated vsize (Kb) 37228

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 52773 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220284 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 529.3
Current children cumulated vsize (Kb) 37228

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 53773 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 539.3
Current children cumulated vsize (Kb) 37228

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 54774 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221218992 134676489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 549.31
Current children cumulated vsize (Kb) 37228

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 55774 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 559.31
Current children cumulated vsize (Kb) 37228

[startup+570.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 56774 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221221984 134601029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 569.31
Current children cumulated vsize (Kb) 37228

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 57774 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 579.31
Current children cumulated vsize (Kb) 37228

[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 58774 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 589.31
Current children cumulated vsize (Kb) 37228

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28534
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 59774 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221219932 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 599.31
Current children cumulated vsize (Kb) 37228

[startup+610.05 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 28535
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 60775 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221219168 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 609.32
Current children cumulated vsize (Kb) 37228

[startup+620.053 s]
Raw data (loadavg): 1.15 1.00 0.92 2/57 28585
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 61775 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221221088 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 619.32
Current children cumulated vsize (Kb) 37228

[startup+630.054 s]
Raw data (loadavg): 1.12 1.00 0.92 2/57 28585
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 45233 0 0 0 62775 156 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221221072 134518676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 629.32
Current children cumulated vsize (Kb) 37228

[startup+640.054 s]
Raw data (loadavg): 1.10 1.00 0.92 2/57 28585
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 63751 181 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220372 134676992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 639.33
Current children cumulated vsize (Kb) 37228

[startup+650.055 s]
Raw data (loadavg): 1.09 1.00 0.92 2/57 28585
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 64751 181 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 649.33
Current children cumulated vsize (Kb) 37228

[startup+660.056 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 28585
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 65751 181 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220032 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 659.33
Current children cumulated vsize (Kb) 37228

[startup+670.056 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 28585
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 66752 181 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220224 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 669.34
Current children cumulated vsize (Kb) 37228

[startup+680.057 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 28585
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 67752 181 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220224 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 679.34
Current children cumulated vsize (Kb) 37228

[startup+690.058 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 68751 182 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220400 134600274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 689.34
Current children cumulated vsize (Kb) 37228

[startup+700.058 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 69750 183 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 699.34
Current children cumulated vsize (Kb) 37228

[startup+710.058 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 70750 183 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220648 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 709.34
Current children cumulated vsize (Kb) 37228

[startup+720.059 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 71750 183 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220048 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 719.34
Current children cumulated vsize (Kb) 37228

[startup+730.06 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 72751 183 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220576 134600215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 729.35
Current children cumulated vsize (Kb) 37228

[startup+740.061 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 73751 183 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220576 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 739.35
Current children cumulated vsize (Kb) 37228

[startup+750.06 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 74751 184 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220400 134600019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 749.36
Current children cumulated vsize (Kb) 37228

[startup+760.061 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 75751 184 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221219696 134600191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 759.36
Current children cumulated vsize (Kb) 37228

[startup+770.062 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 76751 184 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221220496 134677069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 769.36
Current children cumulated vsize (Kb) 37228

[startup+780.063 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 77751 184 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221221000 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 779.36
Current children cumulated vsize (Kb) 37228

[startup+790.063 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 54461 0 0 0 78751 184 0 0 25 0 1 0 1855360414 35946496 8620 4294967295 134512640 135094434 3221224432 3221199408 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8776 8620 145 145 0 8631 0
[pid=28534] vsize: 35104
Current children cumulated CPU time (s) 789.36
Current children cumulated vsize (Kb) 37228

[startup+800.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 79609 270 0 0 25 0 1 0 1855360414 116072448 28182 4294967295 134512640 135094434 3221224432 3221223232 134596735 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 28338 28182 145 145 0 28193 0
[pid=28534] vsize: 113352
Current children cumulated CPU time (s) 798.8
Current children cumulated vsize (Kb) 115476

[startup+810.065 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 80604 274 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221219240 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 808.79
Current children cumulated vsize (Kb) 37336

[startup+820.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 81604 274 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221220928 134677287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 818.79
Current children cumulated vsize (Kb) 37336

[startup+830.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 82604 274 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221219872 134600904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 828.79
Current children cumulated vsize (Kb) 37336

[startup+840.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 83604 274 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221219944 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 838.79
Current children cumulated vsize (Kb) 37336

[startup+850.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 84605 274 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221220724 134676380 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 848.8
Current children cumulated vsize (Kb) 37336

[startup+860.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 85605 274 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221220400 134599935 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 858.8
Current children cumulated vsize (Kb) 37336

[startup+870.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 86605 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221219792 134676251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 868.81
Current children cumulated vsize (Kb) 37336

[startup+880.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 87605 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221220900 134676380 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 878.81
Current children cumulated vsize (Kb) 37336

[startup+890.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 88605 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 888.81
Current children cumulated vsize (Kb) 37336

[startup+900.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 89605 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221219520 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 898.81
Current children cumulated vsize (Kb) 37336

[startup+910.07 s]
Raw data (loadavg): 1.07 1.02 0.93 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 90605 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221220224 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 908.81
Current children cumulated vsize (Kb) 37336

[startup+920.071 s]
Raw data (loadavg): 1.06 1.01 0.93 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 91606 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221221280 134600175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 918.82
Current children cumulated vsize (Kb) 37336

[startup+930.071 s]
Raw data (loadavg): 1.05 1.01 0.93 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 92606 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221220280 134676609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 928.82
Current children cumulated vsize (Kb) 37336

[startup+940.072 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 28589
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 93606 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221220752 134677354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 938.82
Current children cumulated vsize (Kb) 37336

[startup+950.073 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 83251 0 0 0 94606 275 0 0 25 0 1 0 1855360414 36057088 8647 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8803 8647 145 145 0 8658 0
[pid=28534] vsize: 35212
Current children cumulated CPU time (s) 948.82
Current children cumulated vsize (Kb) 37336

[startup+960.074 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 95578 300 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219328 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 958.79
Current children cumulated vsize (Kb) 37340

[startup+970.074 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 96578 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219872 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 968.8
Current children cumulated vsize (Kb) 37340

[startup+980.076 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 97578 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 978.8
Current children cumulated vsize (Kb) 37340

[startup+990.077 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 98578 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219664 134677147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 988.8
Current children cumulated vsize (Kb) 37340

[startup+1000.08 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 99579 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219924 134676608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 998.81
Current children cumulated vsize (Kb) 37340

[startup+1010.08 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 100579 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219944 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1008.81
Current children cumulated vsize (Kb) 37340

[startup+1020.08 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 101579 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1018.81
Current children cumulated vsize (Kb) 37340

[startup+1030.08 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 102579 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219688 134600234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1028.81
Current children cumulated vsize (Kb) 37340

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 103579 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221220928 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1038.81
Current children cumulated vsize (Kb) 37340

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 104579 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1048.81
Current children cumulated vsize (Kb) 37340

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 105580 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1058.82
Current children cumulated vsize (Kb) 37340

[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 106580 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221219872 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1068.82
Current children cumulated vsize (Kb) 37340

[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 107580 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1078.82
Current children cumulated vsize (Kb) 37340

[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 108580 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221220288 134676341 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1088.82
Current children cumulated vsize (Kb) 37340

[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 109580 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221220400 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1098.82
Current children cumulated vsize (Kb) 37340

[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 92960 0 0 0 110580 301 0 0 25 0 1 0 1855360414 36061184 8648 4294967295 134512640 135094434 3221224432 3221220928 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8804 8648 145 145 0 8659 0
[pid=28534] vsize: 35216
Current children cumulated CPU time (s) 1108.82
Current children cumulated vsize (Kb) 37340

[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 118963 0 0 0 111469 376 0 0 25 0 1 0 1855360414 126369792 30696 4294967295 134512640 135094434 3221224432 3221200672 134597418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28534/statm): 30852 30696 145 145 0 30707 0
[pid=28534] vsize: 123408
Current children cumulated CPU time (s) 1118.46
Current children cumulated vsize (Kb) 125532

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 112416 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221219968 134676321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1128.18
Current children cumulated vsize (Kb) 37248

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 113416 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221219416 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1138.18
Current children cumulated vsize (Kb) 37248

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 114416 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1148.18
Current children cumulated vsize (Kb) 37248

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 115416 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221220388 134600238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1158.18
Current children cumulated vsize (Kb) 37248

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 116416 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221220496 134677049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1168.18
Current children cumulated vsize (Kb) 37248

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 117417 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221219168 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1178.19
Current children cumulated vsize (Kb) 37248

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 118417 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1188.19
Current children cumulated vsize (Kb) 37248

[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 119417 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221219680 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1198.19
Current children cumulated vsize (Kb) 37248

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 120417 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1208.19
Current children cumulated vsize (Kb) 37248



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 28591
Raw data (/proc/28530/stat): 28530 (minisat+_script) S 28529 28530 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855360409 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28530/statm): 531 226 485 147 0 384 0
[pid=28530] vsize: 2124
Raw data (/proc/28534/stat): 28534 (minisat+_64-bit) R 28530 28530 2660 0 -1 0 123556 0 0 0 120417 401 0 0 25 0 1 0 1855360414 35966976 8625 4294967295 134512640 135094434 3221224432 3221220752 134676589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28534/statm): 8781 8625 145 145 0 8636 0
[pid=28534] vsize: 35124
Current children cumulated CPU time (s) 1208.19
Current children cumulated vsize (Kb) 37248

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

Child status: 0
Real time (s): 1210.11
CPU time (s): 1208.21
CPU user time (s): 1204.18
CPU system time (s): 4.02939
CPU usage (%): 99.8427
Max. virtual memory (cumulated for all children) (Kb): 125532

Verifier Data

ERROR: no interpretation found !