...

diff --git a/matita/tests/TPTP/hne_problems.txt b/matita/tests/TPTP/hne_problems.txt
new file mode 100644 (file)
index 0000000..7e54a9d
--- /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