From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 17 Apr 2007 08:22:49 +0000 (+0000)
Subject: ...
X-Git-Tag: 0.4.95@7852~529
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13583dde3f1abdf21a2f72f9a8a2cc079b8558b5;p=helm.git

...
---

diff --git a/matita/tests/TPTP/hne_problems.txt b/matita/tests/TPTP/hne_problems.txt
new file mode 100644
index 000000000..7e54a9d98
--- /dev/null
+++ b/matita/tests/TPTP/hne_problems.txt
@@ -0,0 +1,90 @@
+Unsatisfiable/ANA003-2.ma
+Unsatisfiable/LCL001-1.ma
+Unsatisfiable/LCL002-1.ma
+Unsatisfiable/LCL005-1.ma
+Unsatisfiable/LCL019-1.ma
+Unsatisfiable/LCL020-1.ma
+Unsatisfiable/LCL021-1.ma
+Unsatisfiable/LCL024-1.ma
+Unsatisfiable/LCL032-1.ma
+Unsatisfiable/LCL037-1.ma
+Unsatisfiable/LCL038-1.ma
+Unsatisfiable/LCL061-1.ma
+Unsatisfiable/LCL062-1.ma
+Unsatisfiable/LCL063-1.ma
+Unsatisfiable/LCL074-1.ma
+Unsatisfiable/LCL084-2.ma
+Unsatisfiable/LCL084-3.ma
+Unsatisfiable/LCL085-1.ma
+Unsatisfiable/LCL105-1.ma
+Unsatisfiable/LCL119-1.ma
+Unsatisfiable/LCL122-1.ma
+Unsatisfiable/LCL124-1.ma
+Unsatisfiable/LCL125-1.ma
+Unsatisfiable/LCL166-1.ma
+Unsatisfiable/LCL167-1.ma
+Unsatisfiable/LCL218-1.ma
+Unsatisfiable/LCL227-1.ma
+Unsatisfiable/LCL230-1.ma
+Unsatisfiable/LCL231-1.ma
+Unsatisfiable/LCL249-1.ma
+Unsatisfiable/LCL253-1.ma
+Unsatisfiable/LCL369-1.ma
+Unsatisfiable/LCL375-1.ma
+Unsatisfiable/LCL377-1.ma
+Unsatisfiable/LCL393-1.ma
+Unsatisfiable/LCL394-1.ma
+Unsatisfiable/LCL395-1.ma
+Unsatisfiable/LCL423-1.ma
+Unsatisfiable/LCL425-1.ma
+Unsatisfiable/NUM017-1.ma
+Unsatisfiable/PLA001-1.ma
+Unsatisfiable/PLA004-1.ma
+Unsatisfiable/PLA004-2.ma
+Unsatisfiable/PLA005-1.ma
+Unsatisfiable/PLA005-2.ma
+Unsatisfiable/PLA007-1.ma
+Unsatisfiable/PLA008-1.ma
+Unsatisfiable/PLA009-1.ma
+Unsatisfiable/PLA009-2.ma
+Unsatisfiable/PLA010-1.ma
+Unsatisfiable/PLA011-1.ma
+Unsatisfiable/PLA011-2.ma
+Unsatisfiable/PLA012-1.ma
+Unsatisfiable/PLA013-1.ma
+Unsatisfiable/PLA014-1.ma
+Unsatisfiable/PLA014-2.ma
+Unsatisfiable/PLA015-1.ma
+Unsatisfiable/PLA016-1.ma
+Unsatisfiable/PLA018-1.ma
+Unsatisfiable/PLA019-1.ma
+Unsatisfiable/PLA021-1.ma
+Unsatisfiable/PLA023-1.ma
+Unsatisfiable/PUZ039-1.ma
+Unsatisfiable/PUZ040-1.ma
+Unsatisfiable/PUZ042-1.ma
+Unsatisfiable/PUZ050-1.ma
+Unsatisfiable/RNG001-2.ma
+Unsatisfiable/RNG004-3.ma
+Unsatisfiable/SWV014-1.ma
+Unsatisfiable/SYN556-1.ma
+Unsatisfiable/SYN598-1.ma
+Unsatisfiable/SYN599-1.ma
+Unsatisfiable/SYN600-1.ma
+Unsatisfiable/SYN614-1.ma
+Unsatisfiable/SYN615-1.ma
+Unsatisfiable/SYN617-1.ma
+Unsatisfiable/SYN628-1.ma
+Unsatisfiable/SYN631-1.ma
+Unsatisfiable/SYN639-1.ma
+Unsatisfiable/SYN640-1.ma
+Unsatisfiable/SYN646-1.ma
+Unsatisfiable/SYN647-1.ma
+Unsatisfiable/SYN649-1.ma
+Unsatisfiable/SYN653-1.ma
+Unsatisfiable/SYN654-1.ma
+Unsatisfiable/SYN655-1.ma
+Unsatisfiable/SYN704-1.ma
+Unsatisfiable/SYN707-1.ma
+Unsatisfiable/SYN708-1.ma
+Unsatisfiable/SYN711-1.ma