From 19f17706f835cff0e0cc0e6c65b9cb65d64a53a4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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