From 19f17706f835cff0e0cc0e6c65b9cb65d64a53a4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 21 Aug 2006 08:35:45 +0000
Subject: [PATCH] ...

---
 .../matita/tests/TPTP/fetch_results_tptp.lua  |  43 +
 .../tests/TPTP/unit_equality_problems.txt     | 860 ++++++++++++++++++
 2 files changed, 903 insertions(+)
 create mode 100755 helm/software/matita/tests/TPTP/fetch_results_tptp.lua
 create mode 100644 helm/software/matita/tests/TPTP/unit_equality_problems.txt

diff --git a/helm/software/matita/tests/TPTP/fetch_results_tptp.lua b/helm/software/matita/tests/TPTP/fetch_results_tptp.lua
new file mode 100755
index 000000000..886e02336
--- /dev/null
+++ b/helm/software/matita/tests/TPTP/fetch_results_tptp.lua
@@ -0,0 +1,43 @@
+#! /usr/bin/lua50
+
+require "luasocket"
+
+SYSTEM = "Matita---0.1.0.UNS-Ref.s"
+URL = "http://www.cs.miami.edu/~tptp/cgi-bin/DVTPTP2WWW/view_file.pl?Category=Solutions&Domain=%s&File=%s&System=%s"
+
+function url_for(system, problem)
+	local domain = string.sub(problem,1,3)
+	local url = string.format(URL,domain,problem,system)
+	return url
+end
+
+function load_todo_list(file)
+	local f = io.open(file,"r")
+	local todo = {}
+	for l in f:lines() do
+		table.insert(todo,l)
+	end
+	f:close()
+	return todo
+end
+
+function main(argv)
+	assert(table.getn(argv) == 1,
+		"Only one paarmeter: the file containing the problems")
+	local todo = load_todo_list(argv[1])
+	local todo_size = table.getn(todo)
+	for i=1,todo_size do
+		local filename = todo[i]
+		local url = url_for(SYSTEM,filename)
+		print("Fetching "..filename.." ("..i.."/"..todo_size..") "..url)
+		local data,err = socket.http.get(url)
+		assert(data,err)
+		local logfilename = "log."..filename
+		local f = io.open(logfilename,"w")
+		f:write(data)
+		f:close()
+		os.execute("gzip "..logfilename)
+	end
+end
+
+main(arg)
diff --git a/helm/software/matita/tests/TPTP/unit_equality_problems.txt b/helm/software/matita/tests/TPTP/unit_equality_problems.txt
new file mode 100644
index 000000000..c394ddd95
--- /dev/null
+++ b/helm/software/matita/tests/TPTP/unit_equality_problems.txt
@@ -0,0 +1,860 @@
+ALG005-1
+ALG006-1
+ALG007-1
+BOO001-1
+BOO002-1
+BOO002-2
+BOO003-2
+BOO003-4
+BOO004-2
+BOO004-4
+BOO005-2
+BOO005-4
+BOO006-2
+BOO006-4
+BOO007-2
+BOO007-4
+BOO008-2
+BOO008-4
+BOO009-2
+BOO009-4
+BOO010-2
+BOO010-4
+BOO011-2
+BOO011-4
+BOO012-2
+BOO012-4
+BOO013-2
+BOO013-4
+BOO014-2
+BOO014-4
+BOO015-2
+BOO015-4
+BOO016-2
+BOO017-2
+BOO018-4
+BOO019-1
+BOO021-1
+BOO022-1
+BOO023-1
+BOO024-1
+BOO025-1
+BOO026-1
+BOO027-1
+BOO028-1
+BOO029-1
+BOO030-1
+BOO031-1
+BOO032-1
+BOO033-1
+BOO034-1
+BOO036-1
+BOO037-2
+BOO037-3
+BOO067-1
+BOO068-1
+BOO069-1
+BOO070-1
+BOO071-1
+BOO072-1
+BOO073-1
+BOO074-1
+BOO075-1
+BOO076-1
+BOO077-1
+BOO078-1
+BOO079-1
+BOO080-1
+BOO081-1
+BOO082-1
+BOO083-1
+BOO084-1
+BOO085-1
+BOO086-1
+BOO087-1
+BOO088-1
+BOO089-1
+BOO090-1
+BOO091-1
+BOO092-1
+BOO093-1
+BOO094-1
+BOO095-1
+BOO096-1
+BOO097-1
+BOO098-1
+BOO099-1
+BOO100-1
+BOO101-1
+BOO102-1
+BOO103-1
+BOO104-1
+BOO105-1
+BOO106-1
+BOO107-1
+BOO108-1
+COL001-1
+COL001-2
+COL002-1
+COL002-4
+COL002-5
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-2
+COL004-1
+COL004-3
+COL005-1
+COL006-1
+COL006-5
+COL006-6
+COL006-7
+COL007-1
+COL008-1
+COL009-1
+COL010-1
+COL011-1
+COL012-1
+COL013-1
+COL014-1
+COL015-1
+COL016-1
+COL017-1
+COL018-1
+COL019-1
+COL020-1
+COL021-1
+COL022-1
+COL023-1
+COL024-1
+COL025-1
+COL026-1
+COL027-1
+COL029-1
+COL030-1
+COL031-1
+COL032-1
+COL033-1
+COL034-1
+COL035-1
+COL036-1
+COL037-1
+COL038-1
+COL039-1
+COL041-1
+COL042-1
+COL042-6
+COL042-7
+COL042-8
+COL042-9
+COL043-1
+COL043-3
+COL044-1
+COL044-6
+COL044-7
+COL044-8
+COL044-9
+COL045-1
+COL046-1
+COL047-1
+COL048-1
+COL049-1
+COL050-1
+COL051-1
+COL052-1
+COL053-1
+COL056-1
+COL057-1
+COL058-1
+COL058-2
+COL058-3
+COL059-1
+COL060-1
+COL060-2
+COL060-3
+COL061-1
+COL061-2
+COL061-3
+COL062-1
+COL062-2
+COL062-3
+COL063-1
+COL063-2
+COL063-3
+COL063-4
+COL063-5
+COL063-6
+COL064-1
+COL064-2
+COL064-3
+COL064-4
+COL064-5
+COL064-6
+COL064-7
+COL064-8
+COL064-9
+COL064-1
+COL064-1
+COL065-1
+COL066-1
+COL066-2
+COL066-3
+COL067-1
+COL068-1
+COL069-1
+COL070-1
+COL071-1
+COL073-1
+COL075-2
+COL083-1
+COL084-1
+COL085-1
+COL086-1
+COL087-1
+GRP001-2
+GRP001-4
+GRP002-2
+GRP002-3
+GRP002-4
+GRP010-4
+GRP011-4
+GRP012-4
+GRP014-1
+GRP022-2
+GRP023-2
+GRP024-5
+GRP114-1
+GRP115-1
+GRP116-1
+GRP117-1
+GRP118-1
+GRP119-1
+GRP120-1
+GRP121-1
+GRP122-1
+GRP136-1
+GRP137-1
+GRP138-1
+GRP139-1
+GRP140-1
+GRP141-1
+GRP142-1
+GRP143-1
+GRP144-1
+GRP145-1
+GRP146-1
+GRP147-1
+GRP148-1
+GRP149-1
+GRP150-1
+GRP151-1
+GRP152-1
+GRP153-1
+GRP154-1
+GRP155-1
+GRP156-1
+GRP157-1
+GRP158-1
+GRP159-1
+GRP160-1
+GRP161-1
+GRP162-1
+GRP163-1
+GRP164-1
+GRP164-2
+GRP165-1
+GRP165-2
+GRP166-1
+GRP166-2
+GRP166-3
+GRP166-4
+GRP167-1
+GRP167-2
+GRP167-3
+GRP167-4
+GRP167-5
+GRP168-1
+GRP168-2
+GRP169-1
+GRP169-2
+GRP170-1
+GRP170-2
+GRP170-3
+GRP170-4
+GRP171-1
+GRP171-2
+GRP172-1
+GRP172-2
+GRP173-1
+GRP174-1
+GRP175-1
+GRP175-2
+GRP175-3
+GRP175-4
+GRP176-1
+GRP176-2
+GRP177-1
+GRP177-2
+GRP178-1
+GRP178-2
+GRP179-1
+GRP179-2
+GRP179-3
+GRP180-1
+GRP180-2
+GRP181-1
+GRP181-2
+GRP181-3
+GRP181-4
+GRP182-1
+GRP182-2
+GRP182-3
+GRP182-4
+GRP183-1
+GRP183-2
+GRP183-3
+GRP183-4
+GRP184-1
+GRP184-2
+GRP184-3
+GRP184-4
+GRP185-1
+GRP185-2
+GRP185-3
+GRP185-4
+GRP186-1
+GRP186-2
+GRP186-3
+GRP186-4
+GRP187-1
+GRP188-1
+GRP188-2
+GRP189-1
+GRP189-2
+GRP190-1
+GRP190-2
+GRP191-1
+GRP191-2
+GRP192-1
+GRP193-1
+GRP193-2
+GRP195-1
+GRP196-1
+GRP200-1
+GRP201-1
+GRP202-1
+GRP203-1
+GRP204-1
+GRP205-1
+GRP206-1
+GRP207-1
+GRP393-2
+GRP394-3
+GRP399-1
+GRP403-1
+GRP404-1
+GRP405-1
+GRP406-1
+GRP407-1
+GRP408-1
+GRP409-1
+GRP410-1
+GRP411-1
+GRP412-1
+GRP413-1
+GRP414-1
+GRP415-1
+GRP416-1
+GRP417-1
+GRP418-1
+GRP419-1
+GRP420-1
+GRP421-1
+GRP422-1
+GRP423-1
+GRP424-1
+GRP425-1
+GRP426-1
+GRP427-1
+GRP428-1
+GRP429-1
+GRP430-1
+GRP431-1
+GRP432-1
+GRP433-1
+GRP434-1
+GRP435-1
+GRP436-1
+GRP437-1
+GRP438-1
+GRP439-1
+GRP440-1
+GRP441-1
+GRP442-1
+GRP443-1
+GRP444-1
+GRP445-1
+GRP446-1
+GRP447-1
+GRP448-1
+GRP449-1
+GRP450-1
+GRP451-1
+GRP452-1
+GRP453-1
+GRP454-1
+GRP455-1
+GRP456-1
+GRP457-1
+GRP458-1
+GRP459-1
+GRP460-1
+GRP461-1
+GRP462-1
+GRP463-1
+GRP464-1
+GRP465-1
+GRP466-1
+GRP467-1
+GRP468-1
+GRP469-1
+GRP470-1
+GRP471-1
+GRP472-1
+GRP473-1
+GRP474-1
+GRP475-1
+GRP476-1
+GRP477-1
+GRP478-1
+GRP479-1
+GRP480-1
+GRP481-1
+GRP482-1
+GRP483-1
+GRP484-1
+GRP485-1
+GRP486-1
+GRP487-1
+GRP488-1
+GRP489-1
+GRP490-1
+GRP491-1
+GRP492-1
+GRP493-1
+GRP494-1
+GRP495-1
+GRP496-1
+GRP497-1
+GRP498-1
+GRP499-1
+GRP500-1
+GRP501-1
+GRP502-1
+GRP503-1
+GRP504-1
+GRP505-1
+GRP506-1
+GRP507-1
+GRP508-1
+GRP509-1
+GRP510-1
+GRP511-1
+GRP512-1
+GRP513-1
+GRP514-1
+GRP515-1
+GRP516-1
+GRP517-1
+GRP518-1
+GRP519-1
+GRP520-1
+GRP521-1
+GRP522-1
+GRP523-1
+GRP524-1
+GRP525-1
+GRP526-1
+GRP527-1
+GRP528-1
+GRP529-1
+GRP530-1
+GRP531-1
+GRP532-1
+GRP533-1
+GRP534-1
+GRP535-1
+GRP536-1
+GRP537-1
+GRP538-1
+GRP539-1
+GRP540-1
+GRP541-1
+GRP542-1
+GRP543-1
+GRP544-1
+GRP545-1
+GRP546-1
+GRP547-1
+GRP548-1
+GRP549-1
+GRP550-1
+GRP551-1
+GRP552-1
+GRP553-1
+GRP554-1
+GRP555-1
+GRP556-1
+GRP557-1
+GRP558-1
+GRP559-1
+GRP560-1
+GRP561-1
+GRP562-1
+GRP563-1
+GRP564-1
+GRP565-1
+GRP566-1
+GRP567-1
+GRP568-1
+GRP569-1
+GRP570-1
+GRP571-1
+GRP572-1
+GRP573-1
+GRP574-1
+GRP575-1
+GRP576-1
+GRP577-1
+GRP578-1
+GRP579-1
+GRP580-1
+GRP581-1
+GRP582-1
+GRP583-1
+GRP584-1
+GRP585-1
+GRP586-1
+GRP587-1
+GRP588-1
+GRP589-1
+GRP590-1
+GRP591-1
+GRP592-1
+GRP593-1
+GRP594-1
+GRP595-1
+GRP596-1
+GRP597-1
+GRP598-1
+GRP599-1
+GRP600-1
+GRP601-1
+GRP602-1
+GRP603-1
+GRP604-1
+GRP605-1
+GRP606-1
+GRP607-1
+GRP608-1
+GRP609-1
+GRP610-1
+GRP611-1
+GRP612-1
+GRP613-1
+GRP614-1
+GRP615-1
+GRP616-1
+HWC004-1
+HWC004-2
+LAT006-1
+LAT007-1
+LAT008-1
+LAT009-1
+LAT010-1
+LAT011-1
+LAT012-1
+LAT013-1
+LAT014-1
+LAT016-1
+LAT017-1
+LAT018-1
+LAT019-1
+LAT020-1
+LAT021-1
+LAT022-1
+LAT023-1
+LAT024-1
+LAT025-1
+LAT026-1
+LAT027-1
+LAT028-1
+LAT031-1
+LAT032-1
+LAT033-1
+LAT034-1
+LAT038-1
+LAT039-1
+LAT039-2
+LAT040-1
+LAT042-1
+LAT043-1
+LAT044-1
+LAT045-1
+LAT046-1
+LAT047-1
+LAT048-1
+LAT049-1
+LAT050-1
+LAT051-1
+LAT052-1
+LAT053-1
+LAT054-1
+LAT055-2
+LAT059-1
+LAT060-1
+LAT061-1
+LAT062-1
+LAT063-1
+LAT070-1
+LAT071-1
+LAT072-1
+LAT073-1
+LAT074-1
+LAT075-1
+LAT076-1
+LAT077-1
+LAT078-1
+LAT079-1
+LAT080-1
+LAT081-1
+LAT082-1
+LAT083-1
+LAT084-1
+LAT085-1
+LAT086-1
+LAT087-1
+LAT088-1
+LAT089-1
+LAT090-1
+LAT091-1
+LAT092-1
+LAT093-1
+LAT094-1
+LAT095-1
+LAT096-1
+LAT097-1
+LAT098-1
+LAT099-1
+LAT100-1
+LAT101-1
+LAT102-1
+LAT103-1
+LAT104-1
+LAT105-1
+LAT106-1
+LAT107-1
+LAT108-1
+LAT109-1
+LAT110-1
+LAT111-1
+LAT112-1
+LAT113-1
+LAT114-1
+LAT115-1
+LAT116-1
+LAT117-1
+LAT118-1
+LAT119-1
+LAT120-1
+LAT121-1
+LAT122-1
+LAT123-1
+LAT124-1
+LAT125-1
+LAT126-1
+LAT127-1
+LAT128-1
+LAT129-1
+LAT130-1
+LAT131-1
+LAT132-1
+LAT133-1
+LAT134-1
+LAT135-1
+LAT136-1
+LAT137-1
+LAT138-1
+LAT139-1
+LAT140-1
+LAT141-1
+LAT142-1
+LAT143-1
+LAT144-1
+LAT145-1
+LAT146-1
+LAT147-1
+LAT148-1
+LAT149-1
+LAT150-1
+LAT151-1
+LAT152-1
+LAT153-1
+LAT154-1
+LAT155-1
+LAT156-1
+LAT157-1
+LAT158-1
+LAT159-1
+LAT160-1
+LAT161-1
+LAT162-1
+LAT163-1
+LAT164-1
+LAT165-1
+LAT166-1
+LAT167-1
+LAT168-1
+LAT169-1
+LAT170-1
+LAT171-1
+LAT172-1
+LAT173-1
+LAT174-1
+LAT175-1
+LAT176-1
+LAT177-1
+LCL109-2
+LCL109-6
+LCL110-2
+LCL111-2
+LCL112-2
+LCL113-2
+LCL114-2
+LCL115-2
+LCL116-2
+LCL132-1
+LCL133-1
+LCL134-1
+LCL135-1
+LCL136-1
+LCL137-1
+LCL138-1
+LCL139-1
+LCL140-1
+LCL141-1
+LCL153-1
+LCL154-1
+LCL155-1
+LCL156-1
+LCL157-1
+LCL158-1
+LCL159-1
+LCL160-1
+LCL161-1
+LCL162-1
+LCL163-1
+LCL164-1
+LCL165-1
+LCL407-1
+LCL407-2
+LCL409-1
+LCL410-1
+LDA001-1
+LDA002-1
+LDA007-3
+RNG007-4
+RNG008-3
+RNG008-4
+RNG008-7
+RNG009-5
+RNG009-7
+RNG010-5
+RNG010-6
+RNG010-7
+RNG011-5
+RNG012-6
+RNG013-6
+RNG014-6
+RNG015-6
+RNG016-6
+RNG017-6
+RNG018-6
+RNG019-6
+RNG019-7
+RNG020-6
+RNG020-7
+RNG021-6
+RNG021-7
+RNG023-6
+RNG023-7
+RNG024-6
+RNG024-7
+RNG025-4
+RNG025-5
+RNG025-6
+RNG025-7
+RNG025-8
+RNG025-9
+RNG026-6
+RNG026-7
+RNG027-5
+RNG027-7
+RNG027-8
+RNG027-9
+RNG028-5
+RNG028-7
+RNG028-8
+RNG028-9
+RNG029-5
+RNG029-6
+RNG029-7
+RNG030-6
+RNG030-7
+RNG031-6
+RNG031-7
+RNG032-6
+RNG032-7
+RNG033-6
+RNG033-7
+RNG033-8
+RNG033-9
+RNG035-7
+RNG036-7
+RNG042-2
+RNG042-3
+RNG043-1
+ROB001-1
+ROB002-1
+ROB003-1
+ROB004-1
+ROB005-1
+ROB006-1
+ROB006-2
+ROB007-1
+ROB007-2
+ROB008-1
+ROB009-1
+ROB010-1
+ROB013-1
+ROB020-1
+ROB020-2
+ROB022-1
+ROB023-1
+ROB024-1
+ROB026-1
+ROB027-1
+ROB028-1
+ROB030-1
+ROB031-1
+ROB032-1
+SYN080-1
+SYN083-1
+SYN305-1
+SYN552-1
-- 
2.39.2