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-par32-2.opb
MD5SUM	48ed39004ec868a1cad026c865b17eb2
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	6352
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	6352
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6352
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	6352
Total number of constraints	13429
Number of constraints which are clauses	13429
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	1
Maximum length of a constraint	3
Trace number 5147

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-13 22:14:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3590 boxname=wulflinc26 idbench=206 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  48ed39004ec868a1cad026c865b17eb2  /oldhome/oroussel/tmp/wulflinc26/normalized-par32-2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-par32-2.opb /oldhome/oroussel/tmp/wulflinc26/normalized-par32-2.opb
IDLAUNCH: 3590
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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:        853652 kB
Buffers:         34124 kB
Cached:         106676 kB
SwapCached:       2476 kB
Active:          52228 kB
Inactive:        93968 kB
HighTotal:      131008 kB
HighFree:        21196 kB
LowTotal:       903652 kB
LowFree:        832456 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29292 kB
Committed_AS:    63604 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:34:45 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 3590 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13025 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9776    24386 |    3258       0        0     nan |  0.000 % |
c |       101 |    9776    24386 |    3583     101     1054    10.4 | 24.686 % |
c |       251 |    9776    24386 |    3942     251     5083    20.3 | 24.685 % |
c |       477 |    9776    24386 |    4336     477     7978    16.7 | 24.685 % |
c |       815 |    9776    24386 |    4770     815    19982    24.5 | 24.685 % |
c |      1322 |    9776    24386 |    5247    1322    33851    25.6 | 24.685 % |
c |      2082 |    9776    24386 |    5771    2082    53893    25.9 | 24.685 % |
c |      3222 |    9776    24386 |    6348    3222    85157    26.4 | 24.685 % |
c |      4930 |    9776    24386 |    6983    4930   135935    27.6 | 24.685 % |
c |      7493 |    9776    24386 |    7682    7493   211186    28.2 | 24.685 % |
c |     11337 |    9766    24364 |    8450    6645   174908    26.3 | 24.748 % |
c |     17104 |    9766    24364 |    9295    7259   205059    28.2 | 24.748 % |
c |     25753 |    9766    24364 |   10224   10390   302144    29.1 | 24.748 % |
c |     38728 |    9766    24364 |   11247   11443   271075    23.7 | 24.748 % |
c |     58190 |    9766    24364 |   12372   11483   266509    23.2 | 24.748 % |
c |     87382 |    9766    24364 |   13609   12488   344337    27.6 | 24.748 % |
c |    131171 |    9766    24364 |   14970   10333   228609    22.1 | 24.748 % |
c |    196855 |    9766    24364 |   16467    9460   209327    22.1 | 24.748 % |
c |    295382 |    9766    24364 |   18114   17181   397699    23.1 | 24.748 % |
c |    443171 |    9766    24364 |   19925   16694   376985    22.6 | 24.748 % |
#### 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.85 0.95 0.90 2/54 26124
Raw data (stat): 26124 (runsolver) R 26123 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479474490 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.0001 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1252 0 0 0 994 3 0 0 25 0 1 0 479474490 6549504 1191 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1599 1191 603 41 0 1558 0
vsize: 6396
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1252 0 0 0 1994 3 0 0 25 0 1 0 479474490 6549504 1191 4294967295 134512640 134672761 3221224560 3221223744 134558671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1599 1191 603 41 0 1558 0
vsize: 6396
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1252 0 0 0 2993 4 0 0 25 0 1 0 479474490 6549504 1191 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1599 1191 603 41 0 1558 0
vsize: 6396
[startup+40.0023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1253 0 0 0 3994 4 0 0 25 0 1 0 479474490 6553600 1192 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1600 1192 603 41 0 1559 0
vsize: 6400
[startup+50.0034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1293 0 0 0 4994 4 0 0 25 0 1 0 479474490 6832128 1232 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1668 1232 603 41 0 1627 0
vsize: 6672
[startup+60.0031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1331 0 0 0 5994 4 0 0 25 0 1 0 479474490 6967296 1270 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1701 1270 603 41 0 1660 0
vsize: 6804
[startup+70.0035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1341 0 0 0 6994 4 0 0 25 0 1 0 479474490 6967296 1280 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1701 1280 603 41 0 1660 0
vsize: 6804
[startup+80.0035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1353 0 0 0 7994 5 0 0 25 0 1 0 479474490 7114752 1292 4294967295 134512640 134672761 3221224560 3221223744 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1737 1292 603 41 0 1696 0
vsize: 6948
[startup+90.0042 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1360 0 0 0 8994 5 0 0 25 0 1 0 479474490 7114752 1299 4294967295 134512640 134672761 3221224560 3221223696 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1737 1299 603 41 0 1696 0
vsize: 6948
[startup+100.004 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1366 0 0 0 9994 5 0 0 25 0 1 0 479474490 7114752 1305 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1737 1305 603 41 0 1696 0
vsize: 6948
[startup+110.004 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1366 0 0 0 10994 5 0 0 25 0 1 0 479474490 7114752 1305 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1737 1305 603 41 0 1696 0
vsize: 6948
[startup+120.004 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1394 0 0 0 11994 5 0 0 25 0 1 0 479474490 7249920 1333 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1770 1333 603 41 0 1729 0
vsize: 7080
[startup+130.004 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1405 0 0 0 12994 5 0 0 25 0 1 0 479474490 7249920 1344 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1770 1344 603 41 0 1729 0
vsize: 7080
[startup+140.004 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1440 0 0 0 13994 5 0 0 25 0 1 0 479474490 7524352 1379 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1837 1379 603 41 0 1796 0
vsize: 7348
[startup+150.005 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1469 0 0 0 14995 5 0 0 25 0 1 0 479474490 7524352 1408 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1837 1408 603 41 0 1796 0
vsize: 7348
[startup+160.004 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1486 0 0 0 15995 5 0 0 25 0 1 0 479474490 7663616 1425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1425 603 41 0 1830 0
vsize: 7484
[startup+170.004 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1498 0 0 0 16995 5 0 0 25 0 1 0 479474490 7663616 1437 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1437 603 41 0 1830 0
vsize: 7484
[startup+180.005 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1523 0 0 0 17994 5 0 0 25 0 1 0 479474490 7798784 1462 4294967295 134512640 134672761 3221224560 3221223696 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1904 1462 603 41 0 1863 0
vsize: 7616
[startup+190.004 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1536 0 0 0 18994 5 0 0 25 0 1 0 479474490 7938048 1475 4294967295 134512640 134672761 3221224560 3221223664 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1475 603 41 0 1897 0
vsize: 7752
[startup+200.004 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1541 0 0 0 19994 5 0 0 25 0 1 0 479474490 7938048 1480 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1480 603 41 0 1897 0
vsize: 7752
[startup+210.004 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1541 0 0 0 20994 5 0 0 25 0 1 0 479474490 7938048 1480 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1480 603 41 0 1897 0
vsize: 7752
[startup+220.004 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1541 0 0 0 21994 6 0 0 25 0 1 0 479474490 7938048 1480 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1480 603 41 0 1897 0
vsize: 7752
[startup+230.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1550 0 0 0 22995 6 0 0 25 0 1 0 479474490 7938048 1489 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1489 603 41 0 1897 0
vsize: 7752
[startup+240.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1550 0 0 0 23995 6 0 0 25 0 1 0 479474490 7938048 1489 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1489 603 41 0 1897 0
vsize: 7752
[startup+250.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1556 0 0 0 24995 6 0 0 25 0 1 0 479474490 7938048 1495 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1495 603 41 0 1897 0
vsize: 7752
[startup+260.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1557 0 0 0 25995 6 0 0 25 0 1 0 479474490 7938048 1496 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1496 603 41 0 1897 0
vsize: 7752
[startup+270.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1582 0 0 0 26995 6 0 0 25 0 1 0 479474490 8097792 1521 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1977 1521 603 41 0 1936 0
vsize: 7908
[startup+280.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1585 0 0 0 27995 6 0 0 25 0 1 0 479474490 8097792 1524 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1977 1524 603 41 0 1936 0
vsize: 7908
[startup+290.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1585 0 0 0 28995 6 0 0 25 0 1 0 479474490 8097792 1524 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1977 1524 603 41 0 1936 0
vsize: 7908
[startup+300.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1585 0 0 0 29996 6 0 0 25 0 1 0 479474490 8097792 1524 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1977 1524 603 41 0 1936 0
vsize: 7908
[startup+310.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1585 0 0 0 30996 6 0 0 25 0 1 0 479474490 8097792 1524 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1977 1524 603 41 0 1936 0
vsize: 7908
[startup+320.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1591 0 0 0 31996 6 0 0 25 0 1 0 479474490 8261632 1530 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1530 603 41 0 1976 0
vsize: 8068
[startup+330.003 s]
Raw data (loadavg): 1.08 1.01 0.92 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1593 0 0 0 32996 6 0 0 25 0 1 0 479474490 8261632 1532 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1532 603 41 0 1976 0
vsize: 8068
[startup+340.003 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1600 0 0 0 33996 6 0 0 25 0 1 0 479474490 8261632 1539 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1539 603 41 0 1976 0
vsize: 8068
[startup+350.003 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1600 0 0 0 34996 6 0 0 25 0 1 0 479474490 8261632 1539 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1539 603 41 0 1976 0
vsize: 8068
[startup+360.003 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1607 0 0 0 35996 6 0 0 25 0 1 0 479474490 8261632 1546 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+370.004 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1607 0 0 0 36997 6 0 0 25 0 1 0 479474490 8261632 1546 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+380.004 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1607 0 0 0 37997 6 0 0 25 0 1 0 479474490 8261632 1546 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+390.003 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1607 0 0 0 38997 6 0 0 25 0 1 0 479474490 8261632 1546 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+400.004 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1633 0 0 0 39997 6 0 0 25 0 1 0 479474490 8396800 1572 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1572 603 41 0 2009 0
vsize: 8200
[startup+410.004 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1644 0 0 0 40997 6 0 0 25 0 1 0 479474490 8396800 1583 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1583 603 41 0 2009 0
vsize: 8200
[startup+420.005 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1648 0 0 0 41997 6 0 0 25 0 1 0 479474490 8396800 1587 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1587 603 41 0 2009 0
vsize: 8200
[startup+430.005 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1648 0 0 0 42997 6 0 0 25 0 1 0 479474490 8396800 1587 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1587 603 41 0 2009 0
vsize: 8200
[startup+440.005 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1648 0 0 0 43997 6 0 0 25 0 1 0 479474490 8396800 1587 4294967295 134512640 134672761 3221224560 3221223664 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1587 603 41 0 2009 0
vsize: 8200
[startup+450.005 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1648 0 0 0 44998 6 0 0 25 0 1 0 479474490 8396800 1587 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1587 603 41 0 2009 0
vsize: 8200
[startup+460.004 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1653 0 0 0 45998 6 0 0 25 0 1 0 479474490 8396800 1592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1592 603 41 0 2009 0
vsize: 8200
[startup+470.005 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1661 0 0 0 46998 6 0 0 25 0 1 0 479474490 8552448 1600 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2088 1600 603 41 0 2047 0
vsize: 8352
[startup+480.005 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1667 0 0 0 47998 6 0 0 25 0 1 0 479474490 8552448 1606 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2088 1606 603 41 0 2047 0
vsize: 8352
[startup+490.005 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1673 0 0 0 48998 6 0 0 25 0 1 0 479474490 8552448 1612 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2088 1612 603 41 0 2047 0
vsize: 8352
[startup+500.006 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1680 0 0 0 49998 6 0 0 25 0 1 0 479474490 8552448 1619 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2088 1619 603 41 0 2047 0
vsize: 8352
[startup+510.006 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1684 0 0 0 50999 6 0 0 25 0 1 0 479474490 8716288 1623 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1623 603 41 0 2087 0
vsize: 8512
[startup+520.006 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1684 0 0 0 51999 6 0 0 25 0 1 0 479474490 8716288 1623 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1623 603 41 0 2087 0
vsize: 8512
[startup+530.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1684 0 0 0 52999 6 0 0 25 0 1 0 479474490 8716288 1623 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1623 603 41 0 2087 0
vsize: 8512
[startup+540.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1685 0 0 0 53999 6 0 0 25 0 1 0 479474490 8716288 1624 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1624 603 41 0 2087 0
vsize: 8512
[startup+550.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1685 0 0 0 54999 6 0 0 25 0 1 0 479474490 8716288 1624 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1624 603 41 0 2087 0
vsize: 8512
[startup+560.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1685 0 0 0 55999 6 0 0 25 0 1 0 479474490 8716288 1624 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1624 603 41 0 2087 0
vsize: 8512
[startup+570.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1706 0 0 0 57000 6 0 0 25 0 1 0 479474490 8716288 1645 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1645 603 41 0 2087 0
vsize: 8512
[startup+580.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1715 0 0 0 57999 6 0 0 25 0 1 0 479474490 8716288 1654 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1654 603 41 0 2087 0
vsize: 8512
[startup+590.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1745 0 0 0 58999 7 0 0 25 0 1 0 479474490 8982528 1684 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1684 603 41 0 2152 0
vsize: 8772
[startup+600.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1748 0 0 0 59999 7 0 0 25 0 1 0 479474490 8982528 1687 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1687 603 41 0 2152 0
vsize: 8772
[startup+610.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1748 0 0 0 61000 7 0 0 25 0 1 0 479474490 8982528 1687 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1687 603 41 0 2152 0
vsize: 8772
[startup+620.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1750 0 0 0 62000 7 0 0 25 0 1 0 479474490 8982528 1689 4294967295 134512640 134672761 3221224560 3221223744 134558700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1689 603 41 0 2152 0
vsize: 8772
[startup+630.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1759 0 0 0 63000 7 0 0 25 0 1 0 479474490 8982528 1698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1698 603 41 0 2152 0
vsize: 8772
[startup+640.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1767 0 0 0 64000 7 0 0 25 0 1 0 479474490 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+650.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1767 0 0 0 65000 7 0 0 25 0 1 0 479474490 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+660.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1767 0 0 0 66000 7 0 0 25 0 1 0 479474490 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+670.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1767 0 0 0 67001 7 0 0 25 0 1 0 479474490 8982528 1706 4294967295 134512640 134672761 3221224560 3221223696 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+680.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1767 0 0 0 68001 7 0 0 25 0 1 0 479474490 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+690.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1767 0 0 0 69001 7 0 0 25 0 1 0 479474490 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+700.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1767 0 0 0 70001 7 0 0 25 0 1 0 479474490 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+710.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1777 0 0 0 71001 7 0 0 25 0 1 0 479474490 9146368 1716 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1716 603 41 0 2192 0
vsize: 8932
[startup+720.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1778 0 0 0 72001 7 0 0 25 0 1 0 479474490 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+730.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1778 0 0 0 73002 7 0 0 25 0 1 0 479474490 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+740.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1778 0 0 0 74002 7 0 0 25 0 1 0 479474490 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+750.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1778 0 0 0 75002 7 0 0 25 0 1 0 479474490 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+760.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1779 0 0 0 76002 7 0 0 25 0 1 0 479474490 9146368 1718 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1718 603 41 0 2192 0
vsize: 8932
[startup+770.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1780 0 0 0 77002 7 0 0 25 0 1 0 479474490 9146368 1719 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+780.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1780 0 0 0 78002 7 0 0 25 0 1 0 479474490 9146368 1719 4294967295 134512640 134672761 3221224560 3221223716 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+790.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1780 0 0 0 79002 7 0 0 25 0 1 0 479474490 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+800.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1780 0 0 0 80002 7 0 0 25 0 1 0 479474490 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+810.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1780 0 0 0 81003 7 0 0 25 0 1 0 479474490 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+820.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1780 0 0 0 82003 7 0 0 25 0 1 0 479474490 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+830.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1780 0 0 0 83003 7 0 0 25 0 1 0 479474490 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+840.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1780 0 0 0 84003 7 0 0 25 0 1 0 479474490 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+850.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1787 0 0 0 85003 7 0 0 25 0 1 0 479474490 9146368 1726 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1726 603 41 0 2192 0
vsize: 8932
[startup+860.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1792 0 0 0 86003 7 0 0 25 0 1 0 479474490 9146368 1731 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1731 603 41 0 2192 0
vsize: 8932
[startup+870.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1794 0 0 0 87003 7 0 0 25 0 1 0 479474490 9146368 1733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1733 603 41 0 2192 0
vsize: 8932
[startup+880.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1794 0 0 0 88004 8 0 0 25 0 1 0 479474490 9146368 1733 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1733 603 41 0 2192 0
vsize: 8932
[startup+890.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1795 0 0 0 89003 8 0 0 25 0 1 0 479474490 9146368 1734 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1734 603 41 0 2192 0
vsize: 8932
[startup+900.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1865 0 0 0 90003 8 0 0 25 0 1 0 479474490 9412608 1804 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2298 1804 603 41 0 2257 0
vsize: 9192
[startup+910.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1865 0 0 0 91003 8 0 0 25 0 1 0 479474490 9412608 1804 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2298 1804 603 41 0 2257 0
vsize: 9192
[startup+920.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1873 0 0 0 92003 8 0 0 25 0 1 0 479474490 9412608 1812 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2298 1812 603 41 0 2257 0
vsize: 9192
[startup+930.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1874 0 0 0 93003 8 0 0 25 0 1 0 479474490 9412608 1813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2298 1813 603 41 0 2257 0
vsize: 9192
[startup+940.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1884 0 0 0 94003 9 0 0 25 0 1 0 479474490 9609216 1823 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1823 603 41 0 2305 0
vsize: 9384
[startup+950.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1884 0 0 0 95003 9 0 0 25 0 1 0 479474490 9609216 1823 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1823 603 41 0 2305 0
vsize: 9384
[startup+960.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1898 0 0 0 96003 9 0 0 25 0 1 0 479474490 9609216 1837 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+970.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1898 0 0 0 97003 9 0 0 25 0 1 0 479474490 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+980.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1898 0 0 0 98004 9 0 0 25 0 1 0 479474490 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+990.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1898 0 0 0 99004 9 0 0 25 0 1 0 479474490 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1898 0 0 0 100004 9 0 0 25 0 1 0 479474490 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1898 0 0 0 101004 9 0 0 25 0 1 0 479474490 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1898 0 0 0 102004 9 0 0 25 0 1 0 479474490 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1899 0 0 0 103004 9 0 0 25 0 1 0 479474490 9609216 1838 4294967295 134512640 134672761 3221224560 3221223760 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1899 0 0 0 104004 9 0 0 25 0 1 0 479474490 9609216 1838 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1899 0 0 0 105005 9 0 0 25 0 1 0 479474490 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1899 0 0 0 106005 9 0 0 25 0 1 0 479474490 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1899 0 0 0 107005 9 0 0 25 0 1 0 479474490 9609216 1838 4294967295 134512640 134672761 3221224560 3221223664 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1899 0 0 0 108005 9 0 0 25 0 1 0 479474490 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1900 0 0 0 109005 9 0 0 25 0 1 0 479474490 9609216 1839 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1839 603 41 0 2305 0
vsize: 9384
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1911 0 0 0 110005 10 0 0 25 0 1 0 479474490 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1911 0 0 0 111005 10 0 0 25 0 1 0 479474490 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1911 0 0 0 112006 10 0 0 25 0 1 0 479474490 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1911 0 0 0 113006 10 0 0 25 0 1 0 479474490 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1911 0 0 0 114006 10 0 0 25 0 1 0 479474490 9609216 1850 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1911 0 0 0 115006 10 0 0 25 0 1 0 479474490 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1911 0 0 0 116006 10 0 0 25 0 1 0 479474490 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134559131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1920 0 0 0 117006 10 0 0 25 0 1 0 479474490 9805824 1859 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1859 603 41 0 2353 0
vsize: 9576
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1920 0 0 0 118007 10 0 0 25 0 1 0 479474490 9805824 1859 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1859 603 41 0 2353 0
vsize: 9576
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1923 0 0 0 119007 10 0 0 25 0 1 0 479474490 9805824 1862 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1862 603 41 0 2353 0
vsize: 9576
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26124
Raw data (stat): 26124 (minisat+) R 26123 22612 22611 0 -1 0 1923 0 0 0 120007 10 0 0 25 0 1 0 479474490 9805824 1862 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1862 603 41 0 2353 0
vsize: 9576
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 26124
Raw data (stat): 26124 (minisat+) Z 26123 22612 22611 0 -1 12 1925 0 0 0 120007 10 0 0 25 0 1 0 479474490 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.02
CPU time (s): 1200.18
CPU user time (s): 1200.07
CPU system time (s): 0.108983
CPU usage (%): 100.014
Max. virtual memory (Kb): 9576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####