X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2FREADME;h=98deef5ad7af639833fcbe8c61fdd7397b777911;hb=b52f57d8573a909a486d52a7317e017f56d07199;hp=d7cd0b98d505570cda18bd985640ea1c79a8ece9;hpb=39c621e194112d5695c39d070909a3ee957b387f;p=helm.git

diff --git a/helm/ocaml/paramodulation/README b/helm/ocaml/paramodulation/README
index d7cd0b98d..98deef5ad 100644
--- a/helm/ocaml/paramodulation/README
+++ b/helm/ocaml/paramodulation/README
@@ -19,3 +19,25 @@ Usage:
   -retrieve retrieve only
   -help  Display this list of options
   --help  Display this list of options
+
+
+./saturate -l 10 -demod-equalities
+
+dove -l 10 e` il timeout in secondi.
+
+Il programma legge da standard input il teorema, per esempio
+
+\forall n:nat.n + n = 2 * n
+
+l'input termina con una riga vuota (quindi basta un doppio invio alla fine)
+
+In output, oltre ai vari messaggi di debug, vengono stampati gli insiemi
+active e passive alla fine dell'esecuzione. Consiglio di redirigere l'output
+su file, per esempio usando tee:
+
+./saturate -l 10 -demod-equalities | tee output.txt
+
+Il formato di stampa e` quello per gli oggetti di tipo equality (usa la
+funzione Inference.string_of_equality)
+
+