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 6301

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-14 04:10:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4718 boxname=wulflinc12 idbench=206 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  48ed39004ec868a1cad026c865b17eb2  /oldhome/oroussel/tmp/wulflinc12/normalized-par32-2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc12/normalized-par32-2.opb /oldhome/oroussel/tmp/wulflinc12/normalized-par32-2.opb
IDLAUNCH: 4718
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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	: 2
cpu MHz		: 451.091
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:        899760 kB
Buffers:         36048 kB
Cached:          79468 kB
SwapCached:         16 kB
Active:          62712 kB
Inactive:        55668 kB
HighTotal:      131008 kB
HighFree:        47600 kB
LowTotal:       903652 kB
LowFree:        852160 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11060 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:30:36 (client local time) WITH STATUS 0 IN 1200.1 SECONDS
stats: 4718 7 1200.1 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.87 0.91 0.89 2/54 32643
Raw data (stat): 32643 (runsolver) R 32642 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423380803 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.89 0.91 0.89 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1252 0 0 0 995 3 0 0 25 0 1 0 423380803 6549504 1191 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.0016 s]
Raw data (loadavg): 0.90 0.91 0.89 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1252 0 0 0 1994 4 0 0 25 0 1 0 423380803 6549504 1191 4294967295 134512640 134672761 3221224560 3221223728 134560855 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.002 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1252 0 0 0 2994 4 0 0 25 0 1 0 423380803 6549504 1191 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.0024 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1253 0 0 0 3994 4 0 0 25 0 1 0 423380803 6553600 1192 4294967295 134512640 134672761 3221224560 3221223720 134561029 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.0041 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1293 0 0 0 4994 5 0 0 25 0 1 0 423380803 6832128 1232 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.0045 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1331 0 0 0 5993 5 0 0 25 0 1 0 423380803 6967296 1270 4294967295 134512640 134672761 3221224560 3221223744 134558651 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.0052 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1341 0 0 0 6993 6 0 0 25 0 1 0 423380803 6967296 1280 4294967295 134512640 134672761 3221224560 3221223744 134559031 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.0067 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1353 0 0 0 7993 6 0 0 25 0 1 0 423380803 7114752 1292 4294967295 134512640 134672761 3221224560 3221223560 1075350371 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.007 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1360 0 0 0 8992 6 0 0 25 0 1 0 423380803 7114752 1299 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.008 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1366 0 0 0 9992 7 0 0 25 0 1 0 423380803 7114752 1305 4294967295 134512640 134672761 3221224560 3221223744 134559542 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.009 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1366 0 0 0 10992 7 0 0 25 0 1 0 423380803 7114752 1305 4294967295 134512640 134672761 3221224560 3221223576 1075352980 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.01 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1394 0 0 0 11991 8 0 0 25 0 1 0 423380803 7249920 1333 4294967295 134512640 134672761 3221224560 3221223728 134561375 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.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1405 0 0 0 12991 8 0 0 25 0 1 0 423380803 7249920 1344 4294967295 134512640 134672761 3221224560 3221223728 134560956 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.012 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1440 0 0 0 13990 8 0 0 25 0 1 0 423380803 7524352 1379 4294967295 134512640 134672761 3221224560 3221223744 134559033 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.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1469 0 0 0 14990 9 0 0 25 0 1 0 423380803 7524352 1408 4294967295 134512640 134672761 3221224560 3221223728 134560983 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.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1486 0 0 0 15990 9 0 0 25 0 1 0 423380803 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.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1499 0 0 0 16989 9 0 0 25 0 1 0 423380803 7663616 1438 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1438 603 41 0 1830 0
vsize: 7484
[startup+180.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1526 0 0 0 17989 10 0 0 25 0 1 0 423380803 7798784 1465 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1904 1465 603 41 0 1863 0
vsize: 7616
[startup+190.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1536 0 0 0 18989 10 0 0 25 0 1 0 423380803 7938048 1475 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.016 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1541 0 0 0 19988 10 0 0 25 0 1 0 423380803 7938048 1480 4294967295 134512640 134672761 3221224560 3221223760 134557842 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.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1541 0 0 0 20988 10 0 0 25 0 1 0 423380803 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.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1548 0 0 0 21987 11 0 0 25 0 1 0 423380803 7938048 1487 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1487 603 41 0 1897 0
vsize: 7752
[startup+230.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1550 0 0 0 22987 11 0 0 25 0 1 0 423380803 7938048 1489 4294967295 134512640 134672761 3221224560 3221223696 134560677 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.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1550 0 0 0 23986 12 0 0 25 0 1 0 423380803 7938048 1489 4294967295 134512640 134672761 3221224560 3221223696 134560604 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.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1556 0 0 0 24986 12 0 0 25 0 1 0 423380803 7938048 1495 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1557 0 0 0 25986 12 0 0 25 0 1 0 423380803 7938048 1496 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1582 0 0 0 26985 12 0 0 25 0 1 0 423380803 8097792 1521 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1585 0 0 0 27985 13 0 0 25 0 1 0 423380803 8097792 1524 4294967295 134512640 134672761 3221224560 3221223664 134554671 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.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1585 0 0 0 28985 13 0 0 25 0 1 0 423380803 8097792 1524 4294967295 134512640 134672761 3221224560 3221223664 134555314 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.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1585 0 0 0 29984 13 0 0 25 0 1 0 423380803 8097792 1524 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1585 0 0 0 30984 14 0 0 25 0 1 0 423380803 8097792 1524 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1592 0 0 0 31984 14 0 0 25 0 1 0 423380803 8261632 1531 4294967295 134512640 134672761 3221224560 3221223744 134558555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1531 603 41 0 1976 0
vsize: 8068
[startup+330.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1593 0 0 0 32983 14 0 0 25 0 1 0 423380803 8261632 1532 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1600 0 0 0 33983 14 0 0 25 0 1 0 423380803 8261632 1539 4294967295 134512640 134672761 3221224560 3221223728 134561382 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.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1605 0 0 0 34983 15 0 0 25 0 1 0 423380803 8261632 1544 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1544 603 41 0 1976 0
vsize: 8068
[startup+360.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1607 0 0 0 35982 15 0 0 25 0 1 0 423380803 8261632 1546 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1607 0 0 0 36982 15 0 0 25 0 1 0 423380803 8261632 1546 4294967295 134512640 134672761 3221224560 3221223696 134565080 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.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1607 0 0 0 37982 15 0 0 25 0 1 0 423380803 8261632 1546 4294967295 134512640 134672761 3221224560 3221223728 134560871 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.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1607 0 0 0 38982 15 0 0 25 0 1 0 423380803 8261632 1546 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1636 0 0 0 39981 16 0 0 25 0 1 0 423380803 8396800 1575 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1575 603 41 0 2009 0
vsize: 8200
[startup+410.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1645 0 0 0 40981 16 0 0 25 0 1 0 423380803 8396800 1584 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1584 603 41 0 2009 0
vsize: 8200
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1648 0 0 0 41981 16 0 0 25 0 1 0 423380803 8396800 1587 4294967295 134512640 134672761 3221224560 3221223696 134565076 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1648 0 0 0 42980 16 0 0 25 0 1 0 423380803 8396800 1587 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1587 603 41 0 2009 0
vsize: 8200
[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1648 0 0 0 43981 16 0 0 25 0 1 0 423380803 8396800 1587 4294967295 134512640 134672761 3221224560 3221223728 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1587 603 41 0 2009 0
vsize: 8200
[startup+450.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1648 0 0 0 44981 16 0 0 25 0 1 0 423380803 8396800 1587 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1587 603 41 0 2009 0
vsize: 8200
[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1653 0 0 0 45981 16 0 0 25 0 1 0 423380803 8396800 1592 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1592 603 41 0 2009 0
vsize: 8200
[startup+470.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1662 0 0 0 46981 16 0 0 25 0 1 0 423380803 8552448 1601 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1601 603 41 0 2047 0
vsize: 8352
[startup+480.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1667 0 0 0 47981 16 0 0 25 0 1 0 423380803 8552448 1606 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1606 603 41 0 2047 0
vsize: 8352
[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1673 0 0 0 48981 17 0 0 25 0 1 0 423380803 8552448 1612 4294967295 134512640 134672761 3221224560 3221223664 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1612 603 41 0 2047 0
vsize: 8352
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1683 0 0 0 49982 17 0 0 25 0 1 0 423380803 8716288 1622 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1622 603 41 0 2087 0
vsize: 8512
[startup+510.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1684 0 0 0 50982 17 0 0 25 0 1 0 423380803 8716288 1623 4294967295 134512640 134672761 3221224560 3221223728 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1623 603 41 0 2087 0
vsize: 8512
[startup+520.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1684 0 0 0 51982 17 0 0 25 0 1 0 423380803 8716288 1623 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1623 603 41 0 2087 0
vsize: 8512
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1684 0 0 0 52982 17 0 0 25 0 1 0 423380803 8716288 1623 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1623 603 41 0 2087 0
vsize: 8512
[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1685 0 0 0 53982 17 0 0 25 0 1 0 423380803 8716288 1624 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1624 603 41 0 2087 0
vsize: 8512
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1685 0 0 0 54983 17 0 0 25 0 1 0 423380803 8716288 1624 4294967295 134512640 134672761 3221224560 3221223696 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1624 603 41 0 2087 0
vsize: 8512
[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1698 0 0 0 55983 17 0 0 25 0 1 0 423380803 8716288 1637 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1637 603 41 0 2087 0
vsize: 8512
[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1706 0 0 0 56983 17 0 0 25 0 1 0 423380803 8716288 1645 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1645 603 41 0 2087 0
vsize: 8512
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1745 0 0 0 57983 17 0 0 25 0 1 0 423380803 8982528 1684 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1684 603 41 0 2152 0
vsize: 8772
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1745 0 0 0 58983 17 0 0 25 0 1 0 423380803 8982528 1684 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1684 603 41 0 2152 0
vsize: 8772
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1748 0 0 0 59983 17 0 0 25 0 1 0 423380803 8982528 1687 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1687 603 41 0 2152 0
vsize: 8772
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1748 0 0 0 60983 17 0 0 25 0 1 0 423380803 8982528 1687 4294967295 134512640 134672761 3221224560 3221223744 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1687 603 41 0 2152 0
vsize: 8772
[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1759 0 0 0 61983 17 0 0 25 0 1 0 423380803 8982528 1698 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1698 603 41 0 2152 0
vsize: 8772
[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1765 0 0 0 62984 17 0 0 25 0 1 0 423380803 8982528 1704 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1704 603 41 0 2152 0
vsize: 8772
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1767 0 0 0 63984 17 0 0 25 0 1 0 423380803 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+650.038 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1767 0 0 0 64984 17 0 0 25 0 1 0 423380803 8982528 1706 4294967295 134512640 134672761 3221224560 3221223744 134558382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+660.037 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1767 0 0 0 65984 17 0 0 25 0 1 0 423380803 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+670.038 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1767 0 0 0 66984 17 0 0 25 0 1 0 423380803 8982528 1706 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+680.038 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1767 0 0 0 67985 17 0 0 25 0 1 0 423380803 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+690.038 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1767 0 0 0 68985 17 0 0 25 0 1 0 423380803 8982528 1706 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+700.038 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1767 0 0 0 69985 17 0 0 25 0 1 0 423380803 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1706 603 41 0 2152 0
vsize: 8772
[startup+710.039 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1778 0 0 0 70985 17 0 0 25 0 1 0 423380803 9146368 1717 4294967295 134512640 134672761 3221224560 3221223684 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+720.038 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1778 0 0 0 71985 17 0 0 25 0 1 0 423380803 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+730.039 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1778 0 0 0 72985 17 0 0 25 0 1 0 423380803 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+740.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1778 0 0 0 73986 17 0 0 25 0 1 0 423380803 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+750.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1778 0 0 0 74986 17 0 0 25 0 1 0 423380803 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1717 603 41 0 2192 0
vsize: 8932
[startup+760.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 75986 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+770.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 76986 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+780.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 77986 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+790.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 78986 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+800.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 79987 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+810.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 80987 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+820.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 81987 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+830.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 82987 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+840.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1780 0 0 0 83987 17 0 0 25 0 1 0 423380803 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1719 603 41 0 2192 0
vsize: 8932
[startup+850.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1787 0 0 0 84988 17 0 0 25 0 1 0 423380803 9146368 1726 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1726 603 41 0 2192 0
vsize: 8932
[startup+860.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1787 0 0 0 85988 17 0 0 25 0 1 0 423380803 9146368 1726 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1726 603 41 0 2192 0
vsize: 8932
[startup+870.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1794 0 0 0 86988 17 0 0 25 0 1 0 423380803 9146368 1733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1733 603 41 0 2192 0
vsize: 8932
[startup+880.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1794 0 0 0 87988 17 0 0 25 0 1 0 423380803 9146368 1733 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1733 603 41 0 2192 0
vsize: 8932
[startup+890.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1795 0 0 0 88988 17 0 0 25 0 1 0 423380803 9146368 1734 4294967295 134512640 134672761 3221224560 3221223728 134560797 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.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1865 0 0 0 89985 18 0 0 25 0 1 0 423380803 9412608 1804 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1865 0 0 0 90985 18 0 0 25 0 1 0 423380803 9412608 1804 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1873 0 0 0 91984 18 0 0 25 0 1 0 423380803 9412608 1812 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1812 603 41 0 2257 0
vsize: 9192
[startup+930.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1874 0 0 0 92984 18 0 0 25 0 1 0 423380803 9412608 1813 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1813 603 41 0 2257 0
vsize: 9192
[startup+940.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1884 0 0 0 93985 18 0 0 25 0 1 0 423380803 9609216 1823 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1823 603 41 0 2305 0
vsize: 9384
[startup+950.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1884 0 0 0 94985 18 0 0 25 0 1 0 423380803 9609216 1823 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1823 603 41 0 2305 0
vsize: 9384
[startup+960.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1897 0 0 0 95985 18 0 0 25 0 1 0 423380803 9609216 1836 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1836 603 41 0 2305 0
vsize: 9384
[startup+970.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1898 0 0 0 96985 18 0 0 25 0 1 0 423380803 9609216 1837 4294967295 134512640 134672761 3221224560 3221223744 134558557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+980.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1898 0 0 0 97985 18 0 0 25 0 1 0 423380803 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+990.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1898 0 0 0 98986 18 0 0 25 0 1 0 423380803 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1898 0 0 0 99986 18 0 0 25 0 1 0 423380803 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1898 0 0 0 100986 18 0 0 25 0 1 0 423380803 9609216 1837 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1898 0 0 0 101986 18 0 0 25 0 1 0 423380803 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1899 0 0 0 102986 18 0 0 25 0 1 0 423380803 9609216 1838 4294967295 134512640 134672761 3221224560 3221223696 134565058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1899 0 0 0 103987 18 0 0 25 0 1 0 423380803 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1899 0 0 0 104987 18 0 0 25 0 1 0 423380803 9609216 1838 4294967295 134512640 134672761 3221224560 3221223776 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1899 0 0 0 105987 18 0 0 25 0 1 0 423380803 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1899 0 0 0 106987 18 0 0 25 0 1 0 423380803 9609216 1838 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1899 0 0 0 107987 18 0 0 25 0 1 0 423380803 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1900 0 0 0 108988 18 0 0 25 0 1 0 423380803 9609216 1839 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1839 603 41 0 2305 0
vsize: 9384
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1911 0 0 0 109988 18 0 0 25 0 1 0 423380803 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1911 0 0 0 110988 18 0 0 25 0 1 0 423380803 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1911 0 0 0 111988 18 0 0 25 0 1 0 423380803 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1911 0 0 0 112988 18 0 0 25 0 1 0 423380803 9609216 1850 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1911 0 0 0 113989 18 0 0 25 0 1 0 423380803 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1911 0 0 0 114989 18 0 0 25 0 1 0 423380803 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1911 0 0 0 115989 18 0 0 25 0 1 0 423380803 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1920 0 0 0 116989 18 0 0 25 0 1 0 423380803 9805824 1859 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1859 603 41 0 2353 0
vsize: 9576
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1920 0 0 0 117989 18 0 0 25 0 1 0 423380803 9805824 1859 4294967295 134512640 134672761 3221224560 3221223744 134558382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1859 603 41 0 2353 0
vsize: 9576
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1922 0 0 0 118990 18 0 0 25 0 1 0 423380803 9805824 1861 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1861 603 41 0 2353 0
vsize: 9576
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32643
Raw data (stat): 32643 (minisat+) R 32642 25285 25284 0 -1 0 1923 0 0 0 119990 18 0 0 25 0 1 0 423380803 9805824 1862 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1862 603 41 0 2353 0
vsize: 9576
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 32643
Raw data (stat): 32643 (minisat+) Z 32642 25285 25284 0 -1 12 1925 0 0 0 119990 19 0 0 25 0 1 0 423380803 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.06
CPU time (s): 1200.1
CPU user time (s): 1199.9
CPU system time (s): 0.19397
CPU usage (%): 100.003
Max. virtual memory (Kb): 9576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####