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 4946

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        924920 kB
Buffers:         34712 kB
Cached:          53448 kB
SwapCached:       2144 kB
Active:          57772 kB
Inactive:        35436 kB
HighTotal:      131008 kB
HighFree:        73668 kB
LowTotal:       903652 kB
LowFree:        851252 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11032 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:17:58 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 1850 7 1200.19 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.80 0.84 0.86 2/54 587
Raw data (stat): 587 (runsolver) R 586 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420784732 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0009 s]
Raw data (loadavg): 0.83 0.84 0.86 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1252 0 0 0 996 2 0 0 25 0 1 0 420784732 6549504 1191 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1599 1191 603 41 0 1558 0
vsize: 6396
[startup+20.0014 s]
Raw data (loadavg): 0.86 0.85 0.86 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1252 0 0 0 1995 2 0 0 25 0 1 0 420784732 6549504 1191 4294967295 134512640 134672761 3221224640 3221223776 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.0013 s]
Raw data (loadavg): 0.88 0.85 0.86 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1252 0 0 0 2995 2 0 0 25 0 1 0 420784732 6549504 1191 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1599 1191 603 41 0 1558 0
vsize: 6396
[startup+40.0014 s]
Raw data (loadavg): 0.90 0.85 0.86 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1252 0 0 0 3995 2 0 0 25 0 1 0 420784732 6549504 1191 4294967295 134512640 134672761 3221224640 3221223808 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1599 1191 603 41 0 1558 0
vsize: 6396
[startup+50.0019 s]
Raw data (loadavg): 0.91 0.86 0.86 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1292 0 0 0 4995 2 0 0 25 0 1 0 420784732 6828032 1231 4294967295 134512640 134672761 3221224640 3221223744 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1667 1231 603 41 0 1626 0
vsize: 6668
[startup+60.0027 s]
Raw data (loadavg): 0.92 0.86 0.87 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1334 0 0 0 5995 2 0 0 25 0 1 0 420784732 6967296 1273 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1701 1273 603 41 0 1660 0
vsize: 6804
[startup+70.0029 s]
Raw data (loadavg): 0.94 0.87 0.87 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1342 0 0 0 6995 2 0 0 25 0 1 0 420784732 6967296 1281 4294967295 134512640 134672761 3221224640 3221223840 134557828 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.0023 s]
Raw data (loadavg): 0.95 0.87 0.87 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1355 0 0 0 7995 2 0 0 25 0 1 0 420784732 7114752 1294 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1737 1294 603 41 0 1696 0
vsize: 6948
[startup+90.0022 s]
Raw data (loadavg): 0.95 0.87 0.87 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1360 0 0 0 8995 2 0 0 25 0 1 0 420784732 7114752 1299 4294967295 134512640 134672761 3221224640 3221223744 134560191 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.96 0.88 0.87 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1366 0 0 0 9996 2 0 0 25 0 1 0 420784732 7114752 1305 4294967295 134512640 134672761 3221224640 3221223808 134561266 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.003 s]
Raw data (loadavg): 0.97 0.88 0.87 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1372 0 0 0 10996 2 0 0 25 0 1 0 420784732 7114752 1311 4294967295 134512640 134672761 3221224640 3221223744 134559862 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.004 s]
Raw data (loadavg): 0.97 0.89 0.87 2/54 587
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1397 0 0 0 11996 3 0 0 25 0 1 0 420784732 7249920 1336 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.008 s]
Raw data (loadavg): 0.97 0.89 0.87 2/56 628
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1433 0 0 0 12996 3 0 0 25 0 1 0 420784732 7385088 1372 4294967295 134512640 134672761 3221224640 3221223744 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1803 1372 603 41 0 1762 0
vsize: 7212
[startup+140.009 s]
Raw data (loadavg): 0.98 0.89 0.87 2/54 640
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1442 0 0 0 13996 3 0 0 25 0 1 0 420784732 7524352 1381 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1837 1381 603 41 0 1796 0
vsize: 7348
[startup+150.009 s]
Raw data (loadavg): 0.98 0.89 0.87 2/54 640
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1473 0 0 0 14996 4 0 0 25 0 1 0 420784732 7663616 1412 4294967295 134512640 134672761 3221224640 3221223840 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1412 603 41 0 1830 0
vsize: 7484
[startup+160.01 s]
Raw data (loadavg): 0.98 0.90 0.87 2/54 640
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1486 0 0 0 15995 4 0 0 25 0 1 0 420784732 7663616 1425 4294967295 134512640 134672761 3221224640 3221223744 134560034 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.01 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 640
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1499 0 0 0 16995 5 0 0 25 0 1 0 420784732 7663616 1438 4294967295 134512640 134672761 3221224640 3221223824 134559161 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.01 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 640
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1527 0 0 0 17995 5 0 0 25 0 1 0 420784732 7798784 1466 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.01 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 640
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1536 0 0 0 18994 6 0 0 25 0 1 0 420784732 7938048 1475 4294967295 134512640 134672761 3221224640 3221223808 134561008 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.011 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1541 0 0 0 19994 6 0 0 25 0 1 0 420784732 7938048 1480 4294967295 134512640 134672761 3221224640 3221223744 134554673 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.011 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1541 0 0 0 20994 7 0 0 25 0 1 0 420784732 7938048 1480 4294967295 134512640 134672761 3221224640 3221223808 134560903 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.012 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1549 0 0 0 21993 7 0 0 25 0 1 0 420784732 7938048 1488 4294967295 134512640 134672761 3221224640 3221223824 134559310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1488 603 41 0 1897 0
vsize: 7752
[startup+230.012 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1550 0 0 0 22993 8 0 0 25 0 1 0 420784732 7938048 1489 4294967295 134512640 134672761 3221224640 3221223808 134561229 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.012 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1550 0 0 0 23993 8 0 0 25 0 1 0 420784732 7938048 1489 4294967295 134512640 134672761 3221224640 3221223792 134561035 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.012 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1556 0 0 0 24992 9 0 0 25 0 1 0 420784732 7938048 1495 4294967295 134512640 134672761 3221224640 3221223808 134560885 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.013 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1558 0 0 0 25992 9 0 0 25 0 1 0 420784732 7938048 1497 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1497 603 41 0 1897 0
vsize: 7752
[startup+270.013 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1582 0 0 0 26992 10 0 0 25 0 1 0 420784732 8097792 1521 4294967295 134512640 134672761 3221224640 3221223776 134565045 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.013 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1585 0 0 0 27992 10 0 0 25 0 1 0 420784732 8097792 1524 4294967295 134512640 134672761 3221224640 3221223840 134557911 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.014 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1585 0 0 0 28991 11 0 0 25 0 1 0 420784732 8097792 1524 4294967295 134512640 134672761 3221224640 3221223808 134560956 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.014 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1585 0 0 0 29991 11 0 0 25 0 1 0 420784732 8097792 1524 4294967295 134512640 134672761 3221224640 3221223840 134557895 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.015 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1585 0 0 0 30991 11 0 0 25 0 1 0 420784732 8097792 1524 4294967295 134512640 134672761 3221224640 3221223808 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+320.016 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1592 0 0 0 31991 11 0 0 25 0 1 0 420784732 8261632 1531 4294967295 134512640 134672761 3221224640 3221223808 134561011 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.016 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1600 0 0 0 32992 11 0 0 25 0 1 0 420784732 8261632 1539 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1539 603 41 0 1976 0
vsize: 8068
[startup+340.016 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1600 0 0 0 33991 12 0 0 25 0 1 0 420784732 8261632 1539 4294967295 134512640 134672761 3221224640 3221223808 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.016 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1606 0 0 0 34991 13 0 0 25 0 1 0 420784732 8261632 1545 4294967295 134512640 134672761 3221224640 3221223776 134565092 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.017 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1607 0 0 0 35991 13 0 0 25 0 1 0 420784732 8261632 1546 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.017 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1607 0 0 0 36990 13 0 0 25 0 1 0 420784732 8261632 1546 4294967295 134512640 134672761 3221224640 3221223840 134557842 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.017 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1607 0 0 0 37990 13 0 0 25 0 1 0 420784732 8261632 1546 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2017 1546 603 41 0 1976 0
vsize: 8068
[startup+390.017 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1607 0 0 0 38990 14 0 0 25 0 1 0 420784732 8261632 1546 4294967295 134512640 134672761 3221224640 3221223744 134559966 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.017 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1639 0 0 0 39990 14 0 0 25 0 1 0 420784732 8396800 1578 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1578 603 41 0 2009 0
vsize: 8200
[startup+410.018 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1645 0 0 0 40990 15 0 0 25 0 1 0 420784732 8396800 1584 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2050 1584 603 41 0 2009 0
vsize: 8200
[startup+420.018 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1648 0 0 0 41989 15 0 0 25 0 1 0 420784732 8396800 1587 4294967295 134512640 134672761 3221224640 3221223744 134560191 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.018 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1648 0 0 0 42989 16 0 0 25 0 1 0 420784732 8396800 1587 4294967295 134512640 134672761 3221224640 3221223776 134560688 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.019 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1648 0 0 0 43989 16 0 0 25 0 1 0 420784732 8396800 1587 4294967295 134512640 134672761 3221224640 3221223808 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+450.018 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1648 0 0 0 44989 16 0 0 25 0 1 0 420784732 8396800 1587 4294967295 134512640 134672761 3221224640 3221223808 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+460.02 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1661 0 0 0 45989 17 0 0 25 0 1 0 420784732 8552448 1600 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1600 603 41 0 2047 0
vsize: 8352
[startup+470.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1662 0 0 0 46989 17 0 0 25 0 1 0 420784732 8552448 1601 4294967295 134512640 134672761 3221224640 3221223776 134560709 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.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 642
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1672 0 0 0 47989 17 0 0 25 0 1 0 420784732 8552448 1611 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1611 603 41 0 2047 0
vsize: 8352
[startup+490.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1673 0 0 0 48989 17 0 0 25 0 1 0 420784732 8552448 1612 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1684 0 0 0 49989 18 0 0 25 0 1 0 420784732 8716288 1623 4294967295 134512640 134672761 3221224640 3221223744 134560246 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.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1684 0 0 0 50989 18 0 0 25 0 1 0 420784732 8716288 1623 4294967295 134512640 134672761 3221224640 3221223808 134560869 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.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1684 0 0 0 51989 18 0 0 25 0 1 0 420784732 8716288 1623 4294967295 134512640 134672761 3221224640 3221223800 134561238 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.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1685 0 0 0 52988 19 0 0 25 0 1 0 420784732 8716288 1624 4294967295 134512640 134672761 3221224640 3221223808 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+540.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1685 0 0 0 53988 19 0 0 25 0 1 0 420784732 8716288 1624 4294967295 134512640 134672761 3221224640 3221223808 134560970 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.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1685 0 0 0 54988 19 0 0 25 0 1 0 420784732 8716288 1624 4294967295 134512640 134672761 3221224640 3221223776 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1624 603 41 0 2087 0
vsize: 8512
[startup+560.023 s]
Raw data (loadavg): 1.15 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1705 0 0 0 55988 19 0 0 25 0 1 0 420784732 8716288 1644 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1644 603 41 0 2087 0
vsize: 8512
[startup+570.024 s]
Raw data (loadavg): 1.12 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1707 0 0 0 56988 19 0 0 25 0 1 0 420784732 8716288 1646 4294967295 134512640 134672761 3221224640 3221223596 1075349975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1646 603 41 0 2087 0
vsize: 8512
[startup+580.024 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1745 0 0 0 57987 20 0 0 25 0 1 0 420784732 8851456 1684 4294967295 134512640 134672761 3221224640 3221223824 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2161 1684 603 41 0 2120 0
vsize: 8644
[startup+590.024 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1747 0 0 0 58987 20 0 0 25 0 1 0 420784732 8851456 1686 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2161 1686 603 41 0 2120 0
vsize: 8644
[startup+600.024 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1748 0 0 0 59987 20 0 0 25 0 1 0 420784732 8851456 1687 4294967295 134512640 134672761 3221224640 3221223776 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2161 1687 603 41 0 2120 0
vsize: 8644
[startup+610.025 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1750 0 0 0 60987 20 0 0 25 0 1 0 420784732 8851456 1689 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2161 1689 603 41 0 2120 0
vsize: 8644
[startup+620.025 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1759 0 0 0 61988 20 0 0 25 0 1 0 420784732 9048064 1698 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1698 603 41 0 2168 0
vsize: 8836
[startup+630.025 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1767 0 0 0 62988 20 0 0 25 0 1 0 420784732 9048064 1706 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1706 603 41 0 2168 0
vsize: 8836
[startup+640.026 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1767 0 0 0 63988 20 0 0 25 0 1 0 420784732 9048064 1706 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1706 603 41 0 2168 0
vsize: 8836
[startup+650.025 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1767 0 0 0 64988 20 0 0 25 0 1 0 420784732 9048064 1706 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1706 603 41 0 2168 0
vsize: 8836
[startup+660.026 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1767 0 0 0 65988 20 0 0 25 0 1 0 420784732 9048064 1706 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1706 603 41 0 2168 0
vsize: 8836
[startup+670.026 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1767 0 0 0 66989 20 0 0 25 0 1 0 420784732 9048064 1706 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1706 603 41 0 2168 0
vsize: 8836
[startup+680.026 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1767 0 0 0 67989 20 0 0 25 0 1 0 420784732 9048064 1706 4294967295 134512640 134672761 3221224640 3221223776 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1706 603 41 0 2168 0
vsize: 8836
[startup+690.027 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1767 0 0 0 68989 20 0 0 25 0 1 0 420784732 9048064 1706 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1706 603 41 0 2168 0
vsize: 8836
[startup+700.027 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1777 0 0 0 69989 20 0 0 25 0 1 0 420784732 9048064 1716 4294967295 134512640 134672761 3221224640 3221223776 134565134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1716 603 41 0 2168 0
vsize: 8836
[startup+710.028 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1778 0 0 0 70989 20 0 0 25 0 1 0 420784732 9048064 1717 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1717 603 41 0 2168 0
vsize: 8836
[startup+720.027 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1778 0 0 0 71989 20 0 0 25 0 1 0 420784732 9048064 1717 4294967295 134512640 134672761 3221224640 3221223808 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1717 603 41 0 2168 0
vsize: 8836
[startup+730.028 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1778 0 0 0 72990 20 0 0 25 0 1 0 420784732 9048064 1717 4294967295 134512640 134672761 3221224640 3221223808 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1717 603 41 0 2168 0
vsize: 8836
[startup+740.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1778 0 0 0 73990 20 0 0 25 0 1 0 420784732 9048064 1717 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1717 603 41 0 2168 0
vsize: 8836
[startup+750.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1778 0 0 0 74990 20 0 0 25 0 1 0 420784732 9048064 1717 4294967295 134512640 134672761 3221224640 3221223824 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1717 603 41 0 2168 0
vsize: 8836
[startup+760.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1780 0 0 0 75990 20 0 0 25 0 1 0 420784732 9048064 1719 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1719 603 41 0 2168 0
vsize: 8836
[startup+770.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1780 0 0 0 76990 20 0 0 25 0 1 0 420784732 9048064 1719 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1719 603 41 0 2168 0
vsize: 8836
[startup+780.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1780 0 0 0 77991 20 0 0 25 0 1 0 420784732 9048064 1719 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1719 603 41 0 2168 0
vsize: 8836
[startup+790.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1780 0 0 0 78991 20 0 0 25 0 1 0 420784732 9048064 1719 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1719 603 41 0 2168 0
vsize: 8836
[startup+800.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1780 0 0 0 79991 20 0 0 25 0 1 0 420784732 9048064 1719 4294967295 134512640 134672761 3221224640 3221223824 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1719 603 41 0 2168 0
vsize: 8836
[startup+810.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1780 0 0 0 80991 20 0 0 25 0 1 0 420784732 9048064 1719 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1719 603 41 0 2168 0
vsize: 8836
[startup+820.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1780 0 0 0 81991 20 0 0 25 0 1 0 420784732 9048064 1719 4294967295 134512640 134672761 3221224640 3221223808 134553610 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1719 603 41 0 2168 0
vsize: 8836
[startup+830.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1780 0 0 0 82991 20 0 0 25 0 1 0 420784732 9048064 1719 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1719 603 41 0 2168 0
vsize: 8836
[startup+840.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1787 0 0 0 83992 20 0 0 25 0 1 0 420784732 9048064 1726 4294967295 134512640 134672761 3221224640 3221223776 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1726 603 41 0 2168 0
vsize: 8836
[startup+850.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1787 0 0 0 84992 20 0 0 25 0 1 0 420784732 9048064 1726 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1726 603 41 0 2168 0
vsize: 8836
[startup+860.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1794 0 0 0 85992 20 0 0 25 0 1 0 420784732 9211904 1733 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2249 1733 603 41 0 2208 0
vsize: 8996
[startup+870.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1794 0 0 0 86992 20 0 0 25 0 1 0 420784732 9211904 1733 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2249 1733 603 41 0 2208 0
vsize: 8996
[startup+880.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1795 0 0 0 87992 20 0 0 25 0 1 0 420784732 9211904 1734 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2249 1734 603 41 0 2208 0
vsize: 8996
[startup+890.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1865 0 0 0 88992 20 0 0 25 0 1 0 420784732 9474048 1804 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2313 1804 603 41 0 2272 0
vsize: 9252
[startup+900.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1865 0 0 0 89992 20 0 0 25 0 1 0 420784732 9474048 1804 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2313 1804 603 41 0 2272 0
vsize: 9252
[startup+910.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1873 0 0 0 90992 20 0 0 25 0 1 0 420784732 9474048 1812 4294967295 134512640 134672761 3221224640 3221223744 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2313 1812 603 41 0 2272 0
vsize: 9252
[startup+920.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1873 0 0 0 91992 20 0 0 25 0 1 0 420784732 9474048 1812 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2313 1812 603 41 0 2272 0
vsize: 9252
[startup+930.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1884 0 0 0 92992 20 0 0 25 0 1 0 420784732 9609216 1823 4294967295 134512640 134672761 3221224640 3221223824 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1823 603 41 0 2305 0
vsize: 9384
[startup+940.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1884 0 0 0 93993 20 0 0 25 0 1 0 420784732 9609216 1823 4294967295 134512640 134672761 3221224640 3221223804 134565024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1823 603 41 0 2305 0
vsize: 9384
[startup+950.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1896 0 0 0 94993 20 0 0 25 0 1 0 420784732 9609216 1835 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1835 603 41 0 2305 0
vsize: 9384
[startup+960.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1898 0 0 0 95993 21 0 0 25 0 1 0 420784732 9609216 1837 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+970.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1898 0 0 0 96993 21 0 0 25 0 1 0 420784732 9609216 1837 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+980.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1898 0 0 0 97993 21 0 0 25 0 1 0 420784732 9609216 1837 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+990.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1898 0 0 0 98993 21 0 0 25 0 1 0 420784732 9609216 1837 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1898 0 0 0 99993 21 0 0 25 0 1 0 420784732 9609216 1837 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1898 0 0 0 100994 21 0 0 25 0 1 0 420784732 9609216 1837 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1898 0 0 0 101994 21 0 0 25 0 1 0 420784732 9609216 1837 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1837 603 41 0 2305 0
vsize: 9384
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1899 0 0 0 102994 21 0 0 25 0 1 0 420784732 9609216 1838 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1899 0 0 0 103994 21 0 0 25 0 1 0 420784732 9609216 1838 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1899 0 0 0 104994 21 0 0 25 0 1 0 420784732 9609216 1838 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1899 0 0 0 105994 21 0 0 25 0 1 0 420784732 9609216 1838 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1899 0 0 0 106995 21 0 0 25 0 1 0 420784732 9609216 1838 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1899 0 0 0 107995 21 0 0 25 0 1 0 420784732 9609216 1838 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1838 603 41 0 2305 0
vsize: 9384
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1911 0 0 0 108995 21 0 0 25 0 1 0 420784732 9609216 1850 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1911 0 0 0 109995 21 0 0 25 0 1 0 420784732 9609216 1850 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1911 0 0 0 110995 21 0 0 25 0 1 0 420784732 9609216 1850 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1911 0 0 0 111995 21 0 0 25 0 1 0 420784732 9609216 1850 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1911 0 0 0 112995 21 0 0 25 0 1 0 420784732 9609216 1850 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1911 0 0 0 113996 21 0 0 25 0 1 0 420784732 9609216 1850 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1911 0 0 0 114996 21 0 0 25 0 1 0 420784732 9609216 1850 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1850 603 41 0 2305 0
vsize: 9384
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1920 0 0 0 115996 21 0 0 25 0 1 0 420784732 9805824 1859 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1859 603 41 0 2353 0
vsize: 9576
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1920 0 0 0 116996 21 0 0 25 0 1 0 420784732 9805824 1859 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1859 603 41 0 2353 0
vsize: 9576
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1922 0 0 0 117996 21 0 0 25 0 1 0 420784732 9805824 1861 4294967295 134512640 134672761 3221224640 3221223824 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1861 603 41 0 2353 0
vsize: 9576
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1923 0 0 0 118996 21 0 0 25 0 1 0 420784732 9805824 1862 4294967295 134512640 134672761 3221224640 3221223824 134559156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1862 603 41 0 2353 0
vsize: 9576
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 644
Raw data (stat): 587 (minisat+) R 586 29151 29150 0 -1 0 1924 0 0 0 119996 21 0 0 25 0 1 0 420784732 9805824 1863 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2394 1863 603 41 0 2353 0
vsize: 9576
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 644
Raw data (stat): 587 (minisat+) Z 586 29151 29150 0 -1 12 1926 0 0 0 119996 21 0 0 25 0 1 0 420784732 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.04
CPU time (s): 1200.19
CPU user time (s): 1199.97
CPU system time (s): 0.219966
CPU usage (%): 100.012
Max. virtual memory (Kb): 9576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####