Merge branch 'master' of github.com:leoprover/Leo-III

README.md

@@ -7,7 +7,7 @@ It is based on a paramodulation calculus with ordering constraints and, in tradi
 
 In addition for its HOL reasoning capabilities, Leo-III supports reasoning in many higher-order quantified modal logics [GS18,GSB17].
 
-Leo-III is developed at Freie Universität Berlin and the University of Luxembourg. From 2014 - 2018, it was supported by the German National Research Foundation (DFG) under project BE 2501/11-1 (Leo-III). Since 2018, Leo-III is maintained and developed at the University of Luxembourg. The main contributors are (sorted alphabetically): Christoph Benzmüller, Alexander Steen and Max Wisniewski. For a full list of contributors to the project and used and third-party libraries, please refer to the `AUTHORS` file in the source distribution.
+Leo-III was initially developed at Freie Universität Berlin, and then at University of Luxembourg (until 2021). From 2014 - 2018, it was supported by the German National Research Foundation (DFG) under project BE 2501/11-1 (Leo-III). Since 2022, Leo-III is maintained and developed at the University of Greifswald, Germany. The main contributors are (sorted alphabetically): Christoph Benzmüller, Alexander Steen and Max Wisniewski. For a full list of contributors to the project and used and third-party libraries, please refer to the `AUTHORS` file in the source distribution.
 
 Leo-III may be cited as [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.4435994.svg)](https://doi.org/10.5281/zenodo.4435994)
 

USAGE.md

@@ -49,7 +49,7 @@ The most important parameters are
 | Parameter flag  | Effect |
 | ------------- | ------------- |
 | -p  | Output a refutation proof, if one was found <br><br> Default: false (not set) |
-| -t `s`  | Set the timeout to `s` seconds, meaning that Leo-III will try to proof the problem and return `SZS_Timeout` if not successful after approximately `s`  seconds <br><br> Default value: 60<br>Valid values: non-negative numbers|
+| -t `s`  | Set the timeout to `s` seconds, meaning that Leo-III will try to proof the problem and return `SZS_Timeout` if not successful after approximately `s`  seconds <br><br> Default value: 60<br>Valid values: non-negative numbers <br><br> :warning: **The timeout -t is a best-effort parameter. It __does not guarantee__ that Leo-III will actually terminate after at most `s` seconds, but it will try. If a strict timeout is important to you (or if you want to make sure that Leo-III terminates), please use system-specific tools like `ulimit` or `timeout`.** |
 | --atp `system` | Use `system` for external cooperation. See further below. <br><br> Default: none set <br> Valid values: See "External cooperation" below.|
 | --primsubst `level` | Use the "itensity" `level` for instantiating flexible heads according to the primitive substitution rule <br><br> Default: 1<br>Valid values: 1-6 |
 | --unifiers `n` | During unification, use at most `n` distinct unifiers<br> <br> Default: 1<br> Valud values: non-negative numbers |