PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-f1000.opb
MD5SUM	3b740c03d309134e8e181ea08fc4a1e3
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
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	2000
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	2000
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2000
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	2000
Total number of constraints	5250
Number of constraints which are clauses	5250
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	3
Trace number 5432

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-13 23:57:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3887 boxname=wulflinc22 idbench=127 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3b740c03d309134e8e181ea08fc4a1e3  /oldhome/oroussel/tmp/wulflinc22/normalized-f1000.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc22/normalized-f1000.opb /oldhome/oroussel/tmp/wulflinc22/normalized-f1000.opb
IDLAUNCH: 3887
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        855080 kB
Buffers:         31764 kB
Cached:         104664 kB
SwapCached:        524 kB
Active:          47112 kB
Inactive:        92768 kB
HighTotal:      131008 kB
HighFree:        22568 kB
LowTotal:       903652 kB
LowFree:        832512 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34248 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:17:10 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 3887 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5250 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.70 0.89 0.89 2/54 30312
Raw data (stat): 30312 (runsolver) R 30311 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480082520 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.74 0.90 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1059 0 0 0 996 2 0 0 25 0 1 0 480082520 5849088 1037 4294967295 134512640 134672761 3221224576 3221223760 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1428 1037 603 41 0 1387 0
vsize: 5712
[startup+19.9997 s]
Raw data (loadavg): 0.78 0.90 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1195 0 0 0 1995 3 0 0 25 0 1 0 480082520 6361088 1173 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1553 1173 603 41 0 1512 0
vsize: 6212
[startup+30.0007 s]
Raw data (loadavg): 0.81 0.90 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1295 0 0 0 2995 4 0 0 25 0 1 0 480082520 6823936 1273 4294967295 134512640 134672761 3221224576 3221223672 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1666 1273 603 41 0 1625 0
vsize: 6664
[startup+40.0004 s]
Raw data (loadavg): 0.84 0.91 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1325 0 0 0 3995 4 0 0 25 0 1 0 480082520 6950912 1303 4294967295 134512640 134672761 3221224576 3221223568 134565103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1303 603 41 0 1656 0
vsize: 6788
[startup+50.0009 s]
Raw data (loadavg): 0.87 0.91 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1425 0 0 0 4995 4 0 0 25 0 1 0 480082520 7401472 1403 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1403 603 41 0 1766 0
vsize: 7228
[startup+60.0011 s]
Raw data (loadavg): 0.89 0.91 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1468 0 0 0 5995 4 0 0 25 0 1 0 480082520 7532544 1446 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1839 1446 603 41 0 1798 0
vsize: 7356
[startup+70.0006 s]
Raw data (loadavg): 0.90 0.91 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1523 0 0 0 6995 4 0 0 25 0 1 0 480082520 7790592 1501 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1902 1501 603 41 0 1861 0
vsize: 7608
[startup+80.001 s]
Raw data (loadavg): 0.92 0.92 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1596 0 0 0 7995 5 0 0 25 0 1 0 480082520 8085504 1574 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1974 1574 603 41 0 1933 0
vsize: 7896
[startup+90.001 s]
Raw data (loadavg): 0.93 0.92 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1600 0 0 0 8995 5 0 0 25 0 1 0 480082520 8085504 1578 4294967295 134512640 134672761 3221224576 3221223712 134614583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1974 1578 603 41 0 1933 0
vsize: 7896
[startup+100.002 s]
Raw data (loadavg): 0.94 0.92 0.89 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1650 0 0 0 9995 5 0 0 25 0 1 0 480082520 8294400 1628 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2025 1628 603 41 0 1984 0
vsize: 8100
[startup+110.002 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1693 0 0 0 10995 5 0 0 25 0 1 0 480082520 8425472 1671 4294967295 134512640 134672761 3221224576 3221223744 134564705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2057 1671 603 41 0 2016 0
vsize: 8228
[startup+120.002 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1735 0 0 0 11995 6 0 0 25 0 1 0 480082520 8638464 1713 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1713 603 41 0 2068 0
vsize: 8436
[startup+130.003 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1735 0 0 0 12995 6 0 0 25 0 1 0 480082520 8638464 1713 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1713 603 41 0 2068 0
vsize: 8436
[startup+140.002 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1735 0 0 0 13995 6 0 0 25 0 1 0 480082520 8638464 1713 4294967295 134512640 134672761 3221224576 3221223712 134614800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1713 603 41 0 2068 0
vsize: 8436
[startup+150.003 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1788 0 0 0 14995 6 0 0 25 0 1 0 480082520 8863744 1766 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2164 1766 603 41 0 2123 0
vsize: 8656
[startup+160.003 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1788 0 0 0 15995 6 0 0 25 0 1 0 480082520 8863744 1766 4294967295 134512640 134672761 3221224576 3221223760 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2164 1766 603 41 0 2123 0
vsize: 8656
[startup+170.002 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 30312
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1831 0 0 0 16995 6 0 0 25 0 1 0 480082520 8994816 1809 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2196 1809 603 41 0 2155 0
vsize: 8784
[startup+180.01 s]
Raw data (loadavg): 0.98 0.94 0.90 2/58 30355
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1955 0 0 0 17995 7 0 0 25 0 1 0 480082520 9482240 1933 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2315 1933 603 41 0 2274 0
vsize: 9260
[startup+190.011 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 30365
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1964 0 0 0 18995 7 0 0 25 0 1 0 480082520 9576448 1942 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2338 1942 603 41 0 2297 0
vsize: 9352
[startup+200.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30365
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1976 0 0 0 19995 7 0 0 25 0 1 0 480082520 9576448 1954 4294967295 134512640 134672761 3221224576 3221223672 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2338 1954 603 41 0 2297 0
vsize: 9352
[startup+210.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30365
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 1976 0 0 0 20995 7 0 0 25 0 1 0 480082520 9576448 1954 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2338 1954 603 41 0 2297 0
vsize: 9352
[startup+220.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30365
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2021 0 0 0 21995 8 0 0 25 0 1 0 480082520 9809920 1999 4294967295 134512640 134672761 3221224576 3221223760 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2395 1999 603 41 0 2354 0
vsize: 9580
[startup+230.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30365
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2028 0 0 0 22996 8 0 0 25 0 1 0 480082520 9809920 2006 4294967295 134512640 134672761 3221224576 3221223760 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2395 2006 603 41 0 2354 0
vsize: 9580
[startup+240.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30365
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2028 0 0 0 23996 8 0 0 25 0 1 0 480082520 9809920 2006 4294967295 134512640 134672761 3221224576 3221223024 134645479 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2395 2006 603 41 0 2354 0
vsize: 9580
[startup+250.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30365
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2028 0 0 0 24996 8 0 0 25 0 1 0 480082520 9809920 2006 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2395 2006 603 41 0 2354 0
vsize: 9580
[startup+260.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2028 0 0 0 25996 8 0 0 25 0 1 0 480082520 9809920 2006 4294967295 134512640 134672761 3221224576 3221223712 134614670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2395 2006 603 41 0 2354 0
vsize: 9580
[startup+270.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2059 0 0 0 26996 8 0 0 25 0 1 0 480082520 9940992 2037 4294967295 134512640 134672761 3221224576 3221223616 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2427 2037 603 41 0 2386 0
vsize: 9708
[startup+280.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2062 0 0 0 27996 8 0 0 25 0 1 0 480082520 9940992 2040 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2427 2040 603 41 0 2386 0
vsize: 9708
[startup+290.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2066 0 0 0 28996 8 0 0 25 0 1 0 480082520 9940992 2044 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2427 2044 603 41 0 2386 0
vsize: 9708
[startup+300.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2069 0 0 0 29996 8 0 0 25 0 1 0 480082520 9940992 2047 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2427 2047 603 41 0 2386 0
vsize: 9708
[startup+310.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2073 0 0 0 30996 8 0 0 25 0 1 0 480082520 10014720 2051 4294967295 134512640 134672761 3221224576 3221223760 134615722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2051 603 41 0 2404 0
vsize: 9780
[startup+320.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2076 0 0 0 31997 8 0 0 25 0 1 0 480082520 10014720 2054 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2054 603 41 0 2404 0
vsize: 9780
[startup+330.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2078 0 0 0 32997 8 0 0 25 0 1 0 480082520 10014720 2056 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2056 603 41 0 2404 0
vsize: 9780
[startup+340.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2100 0 0 0 33997 8 0 0 25 0 1 0 480082520 10133504 2078 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2474 2078 603 41 0 2433 0
vsize: 9896
[startup+350.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2121 0 0 0 34997 9 0 0 25 0 1 0 480082520 10211328 2099 4294967295 134512640 134672761 3221224576 3221223712 134614741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2493 2099 603 41 0 2452 0
vsize: 9972
[startup+360.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2172 0 0 0 35997 9 0 0 25 0 1 0 480082520 10424320 2150 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2545 2150 603 41 0 2504 0
vsize: 10180
[startup+370.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2182 0 0 0 36997 9 0 0 25 0 1 0 480082520 10424320 2160 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2545 2160 603 41 0 2504 0
vsize: 10180
[startup+380.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2182 0 0 0 37997 9 0 0 25 0 1 0 480082520 10424320 2160 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2545 2160 603 41 0 2504 0
vsize: 10180
[startup+390.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2196 0 0 0 38997 9 0 0 25 0 1 0 480082520 10493952 2174 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2562 2174 603 41 0 2521 0
vsize: 10248
[startup+400.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2201 0 0 0 39997 9 0 0 25 0 1 0 480082520 10493952 2179 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2562 2179 603 41 0 2521 0
vsize: 10248
[startup+410.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2228 0 0 0 40997 9 0 0 25 0 1 0 480082520 10629120 2206 4294967295 134512640 134672761 3221224576 3221223616 134612601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2595 2206 603 41 0 2554 0
vsize: 10380
[startup+420.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2267 0 0 0 41997 10 0 0 25 0 1 0 480082520 10784768 2245 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2633 2245 603 41 0 2592 0
vsize: 10532
[startup+430.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2309 0 0 0 42997 10 0 0 25 0 1 0 480082520 10985472 2287 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2682 2287 603 41 0 2641 0
vsize: 10728
[startup+440.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2313 0 0 0 43997 10 0 0 25 0 1 0 480082520 10985472 2291 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2682 2291 603 41 0 2641 0
vsize: 10728
[startup+450.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2313 0 0 0 44997 10 0 0 25 0 1 0 480082520 10985472 2291 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2682 2291 603 41 0 2641 0
vsize: 10728
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2313 0 0 0 45997 10 0 0 25 0 1 0 480082520 10985472 2291 4294967295 134512640 134672761 3221224576 3221223712 134614670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2682 2291 603 41 0 2641 0
vsize: 10728
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2328 0 0 0 46997 10 0 0 25 0 1 0 480082520 11063296 2306 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2306 603 41 0 2660 0
vsize: 10804
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2335 0 0 0 47997 10 0 0 25 0 1 0 480082520 11063296 2313 4294967295 134512640 134672761 3221224576 3221223632 134644281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2313 603 41 0 2660 0
vsize: 10804
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2366 0 0 0 48997 11 0 0 25 0 1 0 480082520 11194368 2344 4294967295 134512640 134672761 3221224576 3221223712 134614814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2733 2344 603 41 0 2692 0
vsize: 10932
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2366 0 0 0 49997 11 0 0 25 0 1 0 480082520 11194368 2344 4294967295 134512640 134672761 3221224576 3221223616 134612966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2733 2344 603 41 0 2692 0
vsize: 10932
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2383 0 0 0 50998 11 0 0 25 0 1 0 480082520 11264000 2361 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2750 2361 603 41 0 2709 0
vsize: 11000
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2416 0 0 0 51998 11 0 0 25 0 1 0 480082520 11362304 2394 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2774 2394 603 41 0 2733 0
vsize: 11096
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2425 0 0 0 52998 11 0 0 25 0 1 0 480082520 11444224 2403 4294967295 134512640 134672761 3221224576 3221223616 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2794 2403 603 41 0 2753 0
vsize: 11176
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30367
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2448 0 0 0 53998 11 0 0 25 0 1 0 480082520 11546624 2426 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2819 2426 603 41 0 2778 0
vsize: 11276
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2451 0 0 0 54998 11 0 0 25 0 1 0 480082520 11546624 2429 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2819 2429 603 41 0 2778 0
vsize: 11276
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2451 0 0 0 55998 11 0 0 25 0 1 0 480082520 11546624 2429 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2819 2429 603 41 0 2778 0
vsize: 11276
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2451 0 0 0 56998 11 0 0 25 0 1 0 480082520 11546624 2429 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2819 2429 603 41 0 2778 0
vsize: 11276
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2453 0 0 0 57998 11 0 0 25 0 1 0 480082520 11546624 2431 4294967295 134512640 134672761 3221224576 3221223760 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2819 2431 603 41 0 2778 0
vsize: 11276
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2456 0 0 0 58999 11 0 0 25 0 1 0 480082520 11546624 2434 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2819 2434 603 41 0 2778 0
vsize: 11276
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2463 0 0 0 59999 11 0 0 25 0 1 0 480082520 11616256 2441 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2441 603 41 0 2795 0
vsize: 11344
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2466 0 0 0 60999 11 0 0 25 0 1 0 480082520 11616256 2444 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2444 603 41 0 2795 0
vsize: 11344
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2469 0 0 0 61999 11 0 0 25 0 1 0 480082520 11616256 2447 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2447 603 41 0 2795 0
vsize: 11344
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2469 0 0 0 62999 11 0 0 25 0 1 0 480082520 11616256 2447 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2447 603 41 0 2795 0
vsize: 11344
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2472 0 0 0 63999 11 0 0 25 0 1 0 480082520 11616256 2450 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2450 603 41 0 2795 0
vsize: 11344
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2573 0 0 0 64999 12 0 0 25 0 1 0 480082520 12013568 2551 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2933 2551 603 41 0 2892 0
vsize: 11732
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2637 0 0 0 65999 12 0 0 25 0 1 0 480082520 12275712 2615 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2997 2615 603 41 0 2956 0
vsize: 11988
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2690 0 0 0 66999 12 0 0 25 0 1 0 480082520 12476416 2668 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3046 2668 603 41 0 3005 0
vsize: 12184
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2690 0 0 0 67999 12 0 0 25 0 1 0 480082520 12476416 2668 4294967295 134512640 134672761 3221224576 3221223672 134616194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3046 2668 603 41 0 3005 0
vsize: 12184
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2690 0 0 0 68999 12 0 0 25 0 1 0 480082520 12476416 2668 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3046 2668 603 41 0 3005 0
vsize: 12184
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2690 0 0 0 69999 12 0 0 25 0 1 0 480082520 12476416 2668 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2668 603 41 0 3005 0
vsize: 12184
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2691 0 0 0 70998 13 0 0 25 0 1 0 480082520 12476416 2669 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3046 2669 603 41 0 3005 0
vsize: 12184
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2696 0 0 0 71998 13 0 0 25 0 1 0 480082520 12554240 2674 4294967295 134512640 134672761 3221224576 3221223760 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3065 2674 603 41 0 3024 0
vsize: 12260
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2731 0 0 0 72999 13 0 0 25 0 1 0 480082520 12685312 2709 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3097 2709 603 41 0 3056 0
vsize: 12388
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2760 0 0 0 73999 13 0 0 25 0 1 0 480082520 12820480 2738 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3130 2738 603 41 0 3089 0
vsize: 12520
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2760 0 0 0 74999 13 0 0 25 0 1 0 480082520 12820480 2738 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3130 2738 603 41 0 3089 0
vsize: 12520
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2760 0 0 0 75999 13 0 0 25 0 1 0 480082520 12820480 2738 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3130 2738 603 41 0 3089 0
vsize: 12520
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2760 0 0 0 76999 13 0 0 25 0 1 0 480082520 12771328 2738 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3118 2738 603 41 0 3077 0
vsize: 12472
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2760 0 0 0 77999 13 0 0 25 0 1 0 480082520 12771328 2738 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3118 2738 603 41 0 3077 0
vsize: 12472
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2760 0 0 0 78999 13 0 0 25 0 1 0 480082520 12771328 2738 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3118 2738 603 41 0 3077 0
vsize: 12472
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2760 0 0 0 79999 13 0 0 25 0 1 0 480082520 12771328 2738 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3118 2738 603 41 0 3077 0
vsize: 12472
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2777 0 0 0 80999 13 0 0 25 0 1 0 480082520 12890112 2755 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2755 603 41 0 3106 0
vsize: 12588
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2803 0 0 0 82000 13 0 0 25 0 1 0 480082520 12996608 2781 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3173 2781 603 41 0 3132 0
vsize: 12692
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2805 0 0 0 83000 13 0 0 25 0 1 0 480082520 12996608 2783 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3173 2783 603 41 0 3132 0
vsize: 12692
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2817 0 0 0 84000 14 0 0 25 0 1 0 480082520 12996608 2795 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3173 2795 603 41 0 3132 0
vsize: 12692
[startup+850.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2883 0 0 0 85000 14 0 0 25 0 1 0 480082520 13258752 2861 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3237 2861 603 41 0 3196 0
vsize: 12948
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 86000 14 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 87000 14 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 88000 14 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 89000 14 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 90000 14 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223568 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 91000 14 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 92000 14 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 93000 14 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 94001 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 95001 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 96001 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 97001 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 98001 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 99001 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 100001 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223568 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 101001 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2890 0 0 0 102002 15 0 0 25 0 1 0 480082520 13348864 2868 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2868 603 41 0 3218 0
vsize: 13036
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2937 0 0 0 103002 15 0 0 25 0 1 0 480082520 13479936 2915 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3291 2915 603 41 0 3250 0
vsize: 13164
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2969 0 0 0 104002 15 0 0 25 0 1 0 480082520 13611008 2947 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3323 2947 603 41 0 3282 0
vsize: 13292
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2969 0 0 0 105002 15 0 0 25 0 1 0 480082520 13611008 2947 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3323 2947 603 41 0 3282 0
vsize: 13292
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2969 0 0 0 106002 15 0 0 25 0 1 0 480082520 13611008 2947 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3323 2947 603 41 0 3282 0
vsize: 13292
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2974 0 0 0 107002 15 0 0 25 0 1 0 480082520 13688832 2952 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3342 2952 603 41 0 3301 0
vsize: 13368
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2978 0 0 0 108002 15 0 0 25 0 1 0 480082520 13688832 2956 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3342 2956 603 41 0 3301 0
vsize: 13368
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 2986 0 0 0 109003 15 0 0 25 0 1 0 480082520 13688832 2964 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3342 2964 603 41 0 3301 0
vsize: 13368
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3048 0 0 0 110003 15 0 0 25 0 1 0 480082520 13950976 3026 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3406 3026 603 41 0 3365 0
vsize: 13624
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3048 0 0 0 111003 16 0 0 25 0 1 0 480082520 13950976 3026 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3406 3026 603 41 0 3365 0
vsize: 13624
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3048 0 0 0 112003 16 0 0 25 0 1 0 480082520 13950976 3026 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3406 3026 603 41 0 3365 0
vsize: 13624
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3048 0 0 0 113003 16 0 0 25 0 1 0 480082520 13950976 3026 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3406 3026 603 41 0 3365 0
vsize: 13624
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3058 0 0 0 114003 16 0 0 25 0 1 0 480082520 14032896 3036 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3426 3036 603 41 0 3385 0
vsize: 13704
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3072 0 0 0 115003 16 0 0 25 0 1 0 480082520 14032896 3050 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3426 3050 603 41 0 3385 0
vsize: 13704
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3072 0 0 0 116003 16 0 0 25 0 1 0 480082520 14032896 3050 4294967295 134512640 134672761 3221224576 3221223616 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3426 3050 603 41 0 3385 0
vsize: 13704
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3072 0 0 0 117003 16 0 0 25 0 1 0 480082520 14032896 3050 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3426 3050 603 41 0 3385 0
vsize: 13704
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3081 0 0 0 118003 16 0 0 25 0 1 0 480082520 14127104 3059 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3449 3059 603 41 0 3408 0
vsize: 13796
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3121 0 0 0 119004 16 0 0 25 0 1 0 480082520 14262272 3099 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3482 3099 603 41 0 3441 0
vsize: 13928
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30369
Raw data (stat): 30312 (minisat+) R 30311 26298 26297 0 -1 0 3127 0 0 0 120004 16 0 0 25 0 1 0 480082520 14262272 3105 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3482 3105 603 41 0 3441 0
vsize: 13928
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30369
Raw data (stat): 30312 (minisat+) Z 30311 26298 26297 0 -1 12 3127 0 0 0 120004 17 0 0 25 0 1 0 480082520 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.03
CPU time (s): 1200.22
CPU user time (s): 1200.04
CPU system time (s): 0.173973
CPU usage (%): 100.016
Max. virtual memory (Kb): 13928
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####