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 5938

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 02:20:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4342 boxname=wulflinc2 idbench=206 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  48ed39004ec868a1cad026c865b17eb2  /oldhome/oroussel/tmp/wulflinc2/normalized-par32-2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc2/normalized-par32-2.opb /oldhome/oroussel/tmp/wulflinc2/normalized-par32-2.opb
IDLAUNCH: 4342
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        898052 kB
Buffers:         35448 kB
Cached:          80556 kB
SwapCached:          4 kB
Active:          58184 kB
Inactive:        60724 kB
HighTotal:      131008 kB
HighFree:        46648 kB
LowTotal:       903652 kB
LowFree:        851404 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12256 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:40:27 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 4342 7 1200.16 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.83 0.93 0.90 2/54 25918
Raw data (stat): 25918 (runsolver) R 25917 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422724688 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.0006 s]
Raw data (loadavg): 0.86 0.93 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1252 0 0 0 995 3 0 0 25 0 1 0 422724688 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.0005 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1252 0 0 0 1994 3 0 0 25 0 1 0 422724688 6549504 1191 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1599 1191 603 41 0 1558 0
vsize: 6396
[startup+30.0014 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1252 0 0 0 2993 3 0 0 25 0 1 0 422724688 6549504 1191 4294967295 134512640 134672761 3221224560 3221223696 134565092 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.0005 s]
Raw data (loadavg): 0.91 0.93 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1253 0 0 0 3992 3 0 0 25 0 1 0 422724688 6553600 1192 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1600 1192 603 41 0 1559 0
vsize: 6400
[startup+50.0012 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1293 0 0 0 4993 3 0 0 25 0 1 0 422724688 6832128 1232 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1668 1232 603 41 0 1627 0
vsize: 6672
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1331 0 0 0 5992 4 0 0 25 0 1 0 422724688 6967296 1270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1701 1270 603 41 0 1660 0
vsize: 6804
[startup+70.0009 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1342 0 0 0 6992 4 0 0 25 0 1 0 422724688 6967296 1281 4294967295 134512640 134672761 3221224560 3221223696 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1701 1281 603 41 0 1660 0
vsize: 6804
[startup+80.0013 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1353 0 0 0 7992 4 0 0 25 0 1 0 422724688 7114752 1292 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1737 1292 603 41 0 1696 0
vsize: 6948
[startup+90.0013 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1360 0 0 0 8993 4 0 0 25 0 1 0 422724688 7114752 1299 4294967295 134512640 134672761 3221224560 3221223696 134565140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1737 1299 603 41 0 1696 0
vsize: 6948
[startup+100.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1366 0 0 0 9993 4 0 0 25 0 1 0 422724688 7114752 1305 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1737 1305 603 41 0 1696 0
vsize: 6948
[startup+110.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1372 0 0 0 10993 4 0 0 25 0 1 0 422724688 7114752 1311 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1737 1311 603 41 0 1696 0
vsize: 6948
[startup+120.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1397 0 0 0 11993 4 0 0 25 0 1 0 422724688 7249920 1336 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1336 603 41 0 1729 0
vsize: 7080
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1414 0 0 0 12993 4 0 0 25 0 1 0 422724688 7385088 1353 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1803 1353 603 41 0 1762 0
vsize: 7212
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1440 0 0 0 13993 4 0 0 25 0 1 0 422724688 7524352 1379 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1837 1379 603 41 0 1796 0
vsize: 7348
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1469 0 0 0 14993 5 0 0 25 0 1 0 422724688 7524352 1408 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1837 1408 603 41 0 1796 0
vsize: 7348
[startup+160.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1486 0 0 0 15993 5 0 0 25 0 1 0 422724688 7663616 1425 4294967295 134512640 134672761 3221224560 3221223664 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1425 603 41 0 1830 0
vsize: 7484
[startup+170.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1499 0 0 0 16992 5 0 0 25 0 1 0 422724688 7663616 1438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1438 603 41 0 1830 0
vsize: 7484
[startup+180.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1527 0 0 0 17992 6 0 0 25 0 1 0 422724688 7798784 1466 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1466 603 41 0 1863 0
vsize: 7616
[startup+190.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1536 0 0 0 18992 6 0 0 25 0 1 0 422724688 7938048 1475 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1475 603 41 0 1897 0
vsize: 7752
[startup+200.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1541 0 0 0 19992 6 0 0 25 0 1 0 422724688 7938048 1480 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1480 603 41 0 1897 0
vsize: 7752
[startup+210.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1541 0 0 0 20993 6 0 0 25 0 1 0 422724688 7938048 1480 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1480 603 41 0 1897 0
vsize: 7752
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1548 0 0 0 21993 6 0 0 25 0 1 0 422724688 7938048 1487 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1487 603 41 0 1897 0
vsize: 7752
[startup+230.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1550 0 0 0 22993 6 0 0 25 0 1 0 422724688 7938048 1489 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1489 603 41 0 1897 0
vsize: 7752
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1550 0 0 0 23993 6 0 0 25 0 1 0 422724688 7938048 1489 4294967295 134512640 134672761 3221224560 3221223744 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1489 603 41 0 1897 0
vsize: 7752
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1556 0 0 0 24993 6 0 0 25 0 1 0 422724688 7938048 1495 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1495 603 41 0 1897 0
vsize: 7752
[startup+260.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1557 0 0 0 25993 6 0 0 25 0 1 0 422724688 7938048 1496 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1496 603 41 0 1897 0
vsize: 7752
[startup+270.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1582 0 0 0 26993 6 0 0 25 0 1 0 422724688 8097792 1521 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1977 1521 603 41 0 1936 0
vsize: 7908
[startup+280.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1585 0 0 0 27994 6 0 0 25 0 1 0 422724688 8097792 1524 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1977 1524 603 41 0 1936 0
vsize: 7908
[startup+290.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1585 0 0 0 28994 6 0 0 25 0 1 0 422724688 8097792 1524 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1977 1524 603 41 0 1936 0
vsize: 7908
[startup+300.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1585 0 0 0 29994 6 0 0 25 0 1 0 422724688 8097792 1524 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1977 1524 603 41 0 1936 0
vsize: 7908
[startup+310 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1585 0 0 0 30994 6 0 0 25 0 1 0 422724688 8097792 1524 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1977 1524 603 41 0 1936 0
vsize: 7908
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1592 0 0 0 31994 6 0 0 25 0 1 0 422724688 8261632 1531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1531 603 41 0 1976 0
vsize: 8068
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1593 0 0 0 32995 6 0 0 25 0 1 0 422724688 8261632 1532 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1532 603 41 0 1976 0
vsize: 8068
[startup+340 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1600 0 0 0 33995 6 0 0 25 0 1 0 422724688 8261632 1539 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1539 603 41 0 1976 0
vsize: 8068
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1606 0 0 0 34995 6 0 0 25 0 1 0 422724688 8261632 1545 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1545 603 41 0 1976 0
vsize: 8068
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1607 0 0 0 35995 6 0 0 25 0 1 0 422724688 8261632 1546 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1607 0 0 0 36995 6 0 0 25 0 1 0 422724688 8261632 1546 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1607 0 0 0 37995 6 0 0 25 0 1 0 422724688 8261632 1546 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+389.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1607 0 0 0 38995 6 0 0 25 0 1 0 422724688 8261632 1546 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1637 0 0 0 39995 6 0 0 25 0 1 0 422724688 8396800 1576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1576 603 41 0 2009 0
vsize: 8200
[startup+409.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1645 0 0 0 40995 6 0 0 25 0 1 0 422724688 8396800 1584 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1584 603 41 0 2009 0
vsize: 8200
[startup+419.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1648 0 0 0 41996 6 0 0 25 0 1 0 422724688 8396800 1587 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1587 603 41 0 2009 0
vsize: 8200
[startup+430 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1648 0 0 0 42996 6 0 0 25 0 1 0 422724688 8396800 1587 4294967295 134512640 134672761 3221224560 3221223716 134561032 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1648 0 0 0 43996 6 0 0 25 0 1 0 422724688 8396800 1587 4294967295 134512640 134672761 3221224560 3221223620 1075346562 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1648 0 0 0 44996 6 0 0 25 0 1 0 422724688 8396800 1587 4294967295 134512640 134672761 3221224560 3221223728 134561188 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1653 0 0 0 45996 6 0 0 25 0 1 0 422724688 8396800 1592 4294967295 134512640 134672761 3221224560 3221223664 134560254 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1662 0 0 0 46997 6 0 0 25 0 1 0 422724688 8552448 1601 4294967295 134512640 134672761 3221224560 3221223728 134560920 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1667 0 0 0 47997 6 0 0 25 0 1 0 422724688 8552448 1606 4294967295 134512640 134672761 3221224560 3221223760 134557911 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1673 0 0 0 48997 6 0 0 25 0 1 0 422724688 8552448 1612 4294967295 134512640 134672761 3221224560 3221223712 134561244 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1684 0 0 0 49997 6 0 0 25 0 1 0 422724688 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+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1684 0 0 0 50997 6 0 0 25 0 1 0 422724688 8716288 1623 4294967295 134512640 134672761 3221224560 3221223696 134560709 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1684 0 0 0 51997 6 0 0 25 0 1 0 422724688 8716288 1623 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1684 0 0 0 52998 6 0 0 25 0 1 0 422724688 8716288 1623 4294967295 134512640 134672761 3221224560 3221223696 134565127 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1685 0 0 0 53998 6 0 0 25 0 1 0 422724688 8716288 1624 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1685 0 0 0 54998 6 0 0 25 0 1 0 422724688 8716288 1624 4294967295 134512640 134672761 3221224560 3221223728 134560842 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1699 0 0 0 55998 6 0 0 25 0 1 0 422724688 8716288 1638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1638 603 41 0 2087 0
vsize: 8512
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1706 0 0 0 56998 6 0 0 25 0 1 0 422724688 8716288 1645 4294967295 134512640 134672761 3221224560 3221223728 134561193 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1745 0 0 0 57998 6 0 0 25 0 1 0 422724688 8982528 1684 4294967295 134512640 134672761 3221224560 3221223728 134560825 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1746 0 0 0 58998 6 0 0 25 0 1 0 422724688 8982528 1685 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1685 603 41 0 2152 0
vsize: 8772
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1748 0 0 0 59999 6 0 0 25 0 1 0 422724688 8982528 1687 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1750 0 0 0 60999 6 0 0 25 0 1 0 422724688 8982528 1689 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1689 603 41 0 2152 0
vsize: 8772
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1759 0 0 0 61999 6 0 0 25 0 1 0 422724688 8982528 1698 4294967295 134512640 134672761 3221224560 3221223696 134565132 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1766 0 0 0 62999 6 0 0 25 0 1 0 422724688 8982528 1705 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1705 603 41 0 2152 0
vsize: 8772
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1767 0 0 0 63999 6 0 0 25 0 1 0 422724688 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134561382 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1767 0 0 0 64998 6 0 0 25 0 1 0 422724688 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1767 0 0 0 65998 6 0 0 25 0 1 0 422724688 8982528 1706 4294967295 134512640 134672761 3221224560 3221223696 134560566 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1767 0 0 0 66999 6 0 0 25 0 1 0 422724688 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+680.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1767 0 0 0 67999 6 0 0 25 0 1 0 422724688 8982528 1706 4294967295 134512640 134672761 3221224560 3221223684 134566029 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1767 0 0 0 68999 6 0 0 25 0 1 0 422724688 8982528 1706 4294967295 134512640 134672761 3221224560 3221223728 134561151 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1777 0 0 0 69999 6 0 0 25 0 1 0 422724688 9146368 1716 4294967295 134512640 134672761 3221224560 3221223664 134554647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1716 603 41 0 2192 0
vsize: 8932
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1778 0 0 0 70999 6 0 0 25 0 1 0 422724688 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+720.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1778 0 0 0 71999 6 0 0 25 0 1 0 422724688 9146368 1717 4294967295 134512640 134672761 3221224560 3221223664 134554636 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1778 0 0 0 73000 6 0 0 25 0 1 0 422724688 9146368 1717 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1778 0 0 0 74000 6 0 0 25 0 1 0 422724688 9146368 1717 4294967295 134512640 134672761 3221224560 3221223696 134565045 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1778 0 0 0 75000 6 0 0 25 0 1 0 422724688 9146368 1717 4294967295 134512640 134672761 3221224560 3221223696 134560729 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1780 0 0 0 76000 6 0 0 25 0 1 0 422724688 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+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1780 0 0 0 77000 6 0 0 25 0 1 0 422724688 9146368 1719 4294967295 134512640 134672761 3221224560 3221223744 134559121 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1780 0 0 0 78001 6 0 0 25 0 1 0 422724688 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+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1780 0 0 0 79001 6 0 0 25 0 1 0 422724688 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1780 0 0 0 80001 6 0 0 25 0 1 0 422724688 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1780 0 0 0 81001 6 0 0 25 0 1 0 422724688 9146368 1719 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1780 0 0 0 82001 6 0 0 25 0 1 0 422724688 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+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1780 0 0 0 83002 6 0 0 25 0 1 0 422724688 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+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1787 0 0 0 84002 6 0 0 25 0 1 0 422724688 9146368 1726 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1726 603 41 0 2192 0
vsize: 8932
[startup+850.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1787 0 0 0 85002 6 0 0 25 0 1 0 422724688 9146368 1726 4294967295 134512640 134672761 3221224560 3221223728 134560956 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1794 0 0 0 86002 6 0 0 25 0 1 0 422724688 9146368 1733 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1733 603 41 0 2192 0
vsize: 8932
[startup+870.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1794 0 0 0 87002 6 0 0 25 0 1 0 422724688 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1795 0 0 0 88002 7 0 0 25 0 1 0 422724688 9146368 1734 4294967295 134512640 134672761 3221224560 3221223744 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1734 603 41 0 2192 0
vsize: 8932
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1865 0 0 0 89001 7 0 0 25 0 1 0 422724688 9412608 1804 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1804 603 41 0 2257 0
vsize: 9192
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1865 0 0 0 90002 7 0 0 25 0 1 0 422724688 9412608 1804 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1804 603 41 0 2257 0
vsize: 9192
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1873 0 0 0 91002 7 0 0 25 0 1 0 422724688 9412608 1812 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1812 603 41 0 2257 0
vsize: 9192
[startup+920.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1873 0 0 0 92002 7 0 0 25 0 1 0 422724688 9412608 1812 4294967295 134512640 134672761 3221224560 3221223728 134561275 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1884 0 0 0 93002 7 0 0 25 0 1 0 422724688 9609216 1823 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1823 603 41 0 2305 0
vsize: 9384
[startup+940.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1884 0 0 0 94002 7 0 0 25 0 1 0 422724688 9609216 1823 4294967295 134512640 134672761 3221224560 3221223744 134558332 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1896 0 0 0 95003 7 0 0 25 0 1 0 422724688 9609216 1835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1835 603 41 0 2305 0
vsize: 9384
[startup+960.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1898 0 0 0 96003 7 0 0 25 0 1 0 422724688 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+970.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1898 0 0 0 97003 7 0 0 25 0 1 0 422724688 9609216 1837 4294967295 134512640 134672761 3221224560 3221223744 134559298 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1898 0 0 0 98003 7 0 0 25 0 1 0 422724688 9609216 1837 4294967295 134512640 134672761 3221224560 3221223712 134565153 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1898 0 0 0 99003 7 0 0 25 0 1 0 422724688 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1898 0 0 0 100004 7 0 0 25 0 1 0 422724688 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134561011 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1898 0 0 0 101004 7 0 0 25 0 1 0 422724688 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+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1898 0 0 0 102004 7 0 0 25 0 1 0 422724688 9609216 1837 4294967295 134512640 134672761 3221224560 3221223728 134560956 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1899 0 0 0 103004 7 0 0 25 0 1 0 422724688 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1899 0 0 0 104004 7 0 0 25 0 1 0 422724688 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134560983 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1899 0 0 0 105005 7 0 0 25 0 1 0 422724688 9609216 1838 4294967295 134512640 134672761 3221224560 3221223744 134559609 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1899 0 0 0 106005 7 0 0 25 0 1 0 422724688 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1899 0 0 0 107005 7 0 0 25 0 1 0 422724688 9609216 1838 4294967295 134512640 134672761 3221224560 3221223728 134561218 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1900 0 0 0 108005 7 0 0 25 0 1 0 422724688 9609216 1839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1839 603 41 0 2305 0
vsize: 9384
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1911 0 0 0 109005 7 0 0 25 0 1 0 422724688 9609216 1850 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1911 0 0 0 110006 7 0 0 25 0 1 0 422724688 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1911 0 0 0 111006 7 0 0 25 0 1 0 422724688 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134561212 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1911 0 0 0 112006 7 0 0 25 0 1 0 422724688 9609216 1850 4294967295 134512640 134672761 3221224560 3221223708 134565030 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1911 0 0 0 113006 7 0 0 25 0 1 0 422724688 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+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1911 0 0 0 114007 7 0 0 25 0 1 0 422724688 9609216 1850 4294967295 134512640 134672761 3221224560 3221223728 134560797 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1911 0 0 0 115007 7 0 0 25 0 1 0 422724688 9609216 1850 4294967295 134512640 134672761 3221224560 3221223696 134560688 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1920 0 0 0 116007 7 0 0 25 0 1 0 422724688 9805824 1859 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1859 603 41 0 2353 0
vsize: 9576
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1920 0 0 0 117007 7 0 0 25 0 1 0 422724688 9805824 1859 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1923 0 0 0 118007 7 0 0 25 0 1 0 422724688 9805824 1862 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1862 603 41 0 2353 0
vsize: 9576
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1923 0 0 0 119008 7 0 0 25 0 1 0 422724688 9805824 1862 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1862 603 41 0 2353 0
vsize: 9576
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 20937 20936 0 -1 0 1924 0 0 0 120008 7 0 0 25 0 1 0 422724688 9805824 1863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1863 603 41 0 2353 0
vsize: 9576
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25918
Raw data (stat): 25918 (minisat+) Z 25917 20937 20936 0 -1 12 1926 0 0 0 120008 7 0 0 25 0 1 0 422724688 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.02
CPU time (s): 1200.16
CPU user time (s): 1200.08
CPU system time (s): 0.078987
CPU usage (%): 100.012
Max. virtual memory (Kb): 9576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####