X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Ftests%2FTPTP%2Felenco_unsatisfiable.txt;fp=matita%2Ftests%2FTPTP%2Felenco_unsatisfiable.txt;h=e70ebb599fd335c957f536dfcacb459e70b3b949;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/tests/TPTP/elenco_unsatisfiable.txt b/matita/tests/TPTP/elenco_unsatisfiable.txt
new file mode 100644
index 000000000..e70ebb599
--- /dev/null
+++ b/matita/tests/TPTP/elenco_unsatisfiable.txt
@@ -0,0 +1,698 @@
+ALG005-1.p
+ALG006-1.p
+ALG007-1.p
+BOO001-1.p
+BOO002-1.p
+BOO002-2.p
+BOO003-2.p
+BOO003-4.p
+BOO004-2.p
+BOO004-4.p
+BOO005-2.p
+BOO005-4.p
+BOO006-2.p
+BOO006-4.p
+BOO007-2.p
+BOO007-4.p
+BOO008-2.p
+BOO008-4.p
+BOO009-2.p
+BOO009-4.p
+BOO010-2.p
+BOO010-4.p
+BOO011-2.p
+BOO011-4.p
+BOO012-2.p
+BOO012-4.p
+BOO013-2.p
+BOO013-4.p
+BOO014-2.p
+BOO014-4.p
+BOO015-2.p
+BOO015-4.p
+BOO016-2.p
+BOO017-2.p
+BOO018-4.p
+BOO021-1.p
+BOO022-1.p
+BOO023-1.p
+BOO024-1.p
+BOO025-1.p
+BOO026-1.p
+BOO028-1.p
+BOO029-1.p
+BOO031-1.p
+BOO034-1.p
+BOO067-1.p
+BOO068-1.p
+BOO069-1.p
+BOO070-1.p
+BOO071-1.p
+BOO072-1.p
+BOO073-1.p
+BOO074-1.p
+BOO075-1.p
+BOO076-1.p
+COL001-1.p
+COL001-2.p
+COL002-1.p
+COL002-4.p
+COL002-5.p
+COL003-1.p
+COL004-1.p
+COL004-3.p
+COL006-1.p
+COL006-5.p
+COL006-6.p
+COL006-7.p
+COL007-1.p
+COL008-1.p
+COL009-1.p
+COL010-1.p
+COL011-1.p
+COL012-1.p
+COL013-1.p
+COL014-1.p
+COL015-1.p
+COL016-1.p
+COL017-1.p
+COL018-1.p
+COL019-1.p
+COL020-1.p
+COL021-1.p
+COL022-1.p
+COL023-1.p
+COL024-1.p
+COL025-1.p
+COL026-1.p
+COL027-1.p
+COL029-1.p
+COL030-1.p
+COL031-1.p
+COL032-1.p
+COL033-1.p
+COL034-1.p
+COL035-1.p
+COL036-1.p
+COL037-1.p
+COL038-1.p
+COL039-1.p
+COL041-1.p
+COL042-1.p
+COL042-6.p
+COL042-7.p
+COL042-8.p
+COL042-9.p
+COL043-1.p
+COL043-3.p
+COL044-1.p
+COL044-6.p
+COL044-7.p
+COL044-8.p
+COL044-9.p
+COL045-1.p
+COL046-1.p
+COL048-1.p
+COL049-1.p
+COL050-1.p
+COL051-1.p
+COL052-1.p
+COL053-1.p
+COL056-1.p
+COL057-1.p
+COL058-1.p
+COL058-2.p
+COL058-3.p
+COL059-1.p
+COL060-1.p
+COL060-2.p
+COL060-3.p
+COL061-1.p
+COL061-2.p
+COL061-3.p
+COL062-1.p
+COL062-2.p
+COL062-3.p
+COL063-1.p
+COL063-2.p
+COL063-3.p
+COL063-4.p
+COL063-5.p
+COL063-6.p
+COL064-1.p
+COL064-2.p
+COL064-3.p
+COL064-4.p
+COL064-5.p
+COL064-6.p
+COL064-7.p
+COL064-8.p
+COL064-9.p
+COL065-1.p
+COL066-1.p
+COL066-2.p
+COL066-3.p
+COL070-1.p
+COL075-2.p
+COL083-1.p
+COL084-1.p
+COL085-1.p
+COL086-1.p
+GRP001-2.p
+GRP001-4.p
+GRP002-2.p
+GRP002-3.p
+GRP002-4.p
+GRP010-4.p
+GRP011-4.p
+GRP012-4.p
+GRP014-1.p
+GRP022-2.p
+GRP023-2.p
+GRP024-5.p
+GRP114-1.p
+GRP115-1.p
+GRP116-1.p
+GRP117-1.p
+GRP118-1.p
+GRP119-1.p
+GRP120-1.p
+GRP121-1.p
+GRP122-1.p
+GRP136-1.p
+GRP137-1.p
+GRP138-1.p
+GRP139-1.p
+GRP140-1.p
+GRP141-1.p
+GRP142-1.p
+GRP143-1.p
+GRP144-1.p
+GRP145-1.p
+GRP146-1.p
+GRP147-1.p
+GRP148-1.p
+GRP149-1.p
+GRP150-1.p
+GRP151-1.p
+GRP152-1.p
+GRP153-1.p
+GRP154-1.p
+GRP155-1.p
+GRP156-1.p
+GRP157-1.p
+GRP158-1.p
+GRP159-1.p
+GRP160-1.p
+GRP161-1.p
+GRP162-1.p
+GRP163-1.p
+GRP164-1.p
+GRP164-2.p
+GRP165-1.p
+GRP165-2.p
+GRP166-1.p
+GRP166-2.p
+GRP166-3.p
+GRP166-4.p
+GRP167-1.p
+GRP167-2.p
+GRP167-3.p
+GRP167-4.p
+GRP167-5.p
+GRP168-1.p
+GRP168-2.p
+GRP169-1.p
+GRP169-2.p
+GRP170-1.p
+GRP170-2.p
+GRP170-3.p
+GRP170-4.p
+GRP171-1.p
+GRP171-2.p
+GRP172-1.p
+GRP172-2.p
+GRP173-1.p
+GRP174-1.p
+GRP175-1.p
+GRP175-2.p
+GRP175-3.p
+GRP175-4.p
+GRP176-1.p
+GRP176-2.p
+GRP177-2.p
+GRP178-1.p
+GRP178-2.p
+GRP179-1.p
+GRP179-2.p
+GRP179-3.p
+GRP180-1.p
+GRP180-2.p
+GRP181-1.p
+GRP181-2.p
+GRP181-3.p
+GRP181-4.p
+GRP182-1.p
+GRP182-2.p
+GRP182-3.p
+GRP182-4.p
+GRP183-1.p
+GRP183-2.p
+GRP183-3.p
+GRP183-4.p
+GRP184-1.p
+GRP184-2.p
+GRP184-3.p
+GRP184-4.p
+GRP185-1.p
+GRP185-2.p
+GRP185-3.p
+GRP185-4.p
+GRP186-1.p
+GRP186-2.p
+GRP186-3.p
+GRP186-4.p
+GRP187-1.p
+GRP188-1.p
+GRP188-2.p
+GRP189-1.p
+GRP189-2.p
+GRP190-1.p
+GRP190-2.p
+GRP191-1.p
+GRP191-2.p
+GRP192-1.p
+GRP193-1.p
+GRP193-2.p
+GRP195-1.p
+GRP196-1.p
+GRP200-1.p
+GRP201-1.p
+GRP202-1.p
+GRP203-1.p
+GRP205-1.p
+GRP206-1.p
+GRP403-1.p
+GRP404-1.p
+GRP405-1.p
+GRP406-1.p
+GRP407-1.p
+GRP408-1.p
+GRP409-1.p
+GRP410-1.p
+GRP411-1.p
+GRP412-1.p
+GRP413-1.p
+GRP414-1.p
+GRP415-1.p
+GRP416-1.p
+GRP417-1.p
+GRP418-1.p
+GRP419-1.p
+GRP420-1.p
+GRP421-1.p
+GRP422-1.p
+GRP423-1.p
+GRP424-1.p
+GRP425-1.p
+GRP426-1.p
+GRP427-1.p
+GRP428-1.p
+GRP429-1.p
+GRP430-1.p
+GRP431-1.p
+GRP432-1.p
+GRP433-1.p
+GRP434-1.p
+GRP435-1.p
+GRP436-1.p
+GRP437-1.p
+GRP438-1.p
+GRP439-1.p
+GRP440-1.p
+GRP441-1.p
+GRP442-1.p
+GRP443-1.p
+GRP444-1.p
+GRP445-1.p
+GRP446-1.p
+GRP447-1.p
+GRP448-1.p
+GRP449-1.p
+GRP450-1.p
+GRP451-1.p
+GRP452-1.p
+GRP453-1.p
+GRP454-1.p
+GRP455-1.p
+GRP456-1.p
+GRP457-1.p
+GRP458-1.p
+GRP459-1.p
+GRP460-1.p
+GRP461-1.p
+GRP462-1.p
+GRP463-1.p
+GRP464-1.p
+GRP465-1.p
+GRP466-1.p
+GRP467-1.p
+GRP468-1.p
+GRP469-1.p
+GRP470-1.p
+GRP471-1.p
+GRP472-1.p
+GRP473-1.p
+GRP474-1.p
+GRP475-1.p
+GRP476-1.p
+GRP477-1.p
+GRP478-1.p
+GRP479-1.p
+GRP480-1.p
+GRP481-1.p
+GRP482-1.p
+GRP483-1.p
+GRP484-1.p
+GRP485-1.p
+GRP486-1.p
+GRP487-1.p
+GRP488-1.p
+GRP489-1.p
+GRP490-1.p
+GRP491-1.p
+GRP492-1.p
+GRP493-1.p
+GRP494-1.p
+GRP495-1.p
+GRP496-1.p
+GRP497-1.p
+GRP498-1.p
+GRP499-1.p
+GRP500-1.p
+GRP501-1.p
+GRP502-1.p
+GRP503-1.p
+GRP504-1.p
+GRP505-1.p
+GRP506-1.p
+GRP507-1.p
+GRP508-1.p
+GRP509-1.p
+GRP510-1.p
+GRP511-1.p
+GRP512-1.p
+GRP513-1.p
+GRP514-1.p
+GRP515-1.p
+GRP516-1.p
+GRP517-1.p
+GRP518-1.p
+GRP519-1.p
+GRP520-1.p
+GRP521-1.p
+GRP522-1.p
+GRP523-1.p
+GRP524-1.p
+GRP525-1.p
+GRP526-1.p
+GRP527-1.p
+GRP528-1.p
+GRP529-1.p
+GRP530-1.p
+GRP531-1.p
+GRP532-1.p
+GRP533-1.p
+GRP534-1.p
+GRP535-1.p
+GRP536-1.p
+GRP537-1.p
+GRP538-1.p
+GRP539-1.p
+GRP540-1.p
+GRP541-1.p
+GRP542-1.p
+GRP543-1.p
+GRP544-1.p
+GRP545-1.p
+GRP546-1.p
+GRP547-1.p
+GRP548-1.p
+GRP549-1.p
+GRP550-1.p
+GRP551-1.p
+GRP552-1.p
+GRP553-1.p
+GRP554-1.p
+GRP555-1.p
+GRP556-1.p
+GRP557-1.p
+GRP558-1.p
+GRP559-1.p
+GRP560-1.p
+GRP561-1.p
+GRP562-1.p
+GRP563-1.p
+GRP564-1.p
+GRP565-1.p
+GRP566-1.p
+GRP567-1.p
+GRP568-1.p
+GRP569-1.p
+GRP570-1.p
+GRP571-1.p
+GRP572-1.p
+GRP573-1.p
+GRP574-1.p
+GRP575-1.p
+GRP576-1.p
+GRP577-1.p
+GRP578-1.p
+GRP579-1.p
+GRP580-1.p
+GRP581-1.p
+GRP582-1.p
+GRP583-1.p
+GRP584-1.p
+GRP585-1.p
+GRP586-1.p
+GRP587-1.p
+GRP588-1.p
+GRP589-1.p
+GRP590-1.p
+GRP591-1.p
+GRP592-1.p
+GRP593-1.p
+GRP594-1.p
+GRP595-1.p
+GRP596-1.p
+GRP597-1.p
+GRP598-1.p
+GRP599-1.p
+GRP600-1.p
+GRP601-1.p
+GRP602-1.p
+GRP603-1.p
+GRP604-1.p
+GRP605-1.p
+GRP606-1.p
+GRP607-1.p
+GRP608-1.p
+GRP609-1.p
+GRP610-1.p
+GRP611-1.p
+GRP612-1.p
+GRP613-1.p
+GRP614-1.p
+GRP615-1.p
+GRP616-1.p
+LAT006-1.p
+LAT007-1.p
+LAT008-1.p
+LAT009-1.p
+LAT010-1.p
+LAT011-1.p
+LAT012-1.p
+LAT013-1.p
+LAT014-1.p
+LAT017-1.p
+LAT018-1.p
+LAT019-1.p
+LAT020-1.p
+LAT021-1.p
+LAT022-1.p
+LAT023-1.p
+LAT026-1.p
+LAT027-1.p
+LAT028-1.p
+LAT031-1.p
+LAT032-1.p
+LAT033-1.p
+LAT034-1.p
+LAT038-1.p
+LAT039-1.p
+LAT039-2.p
+LAT040-1.p
+LAT042-1.p
+LAT043-1.p
+LAT044-1.p
+LAT045-1.p
+LAT070-1.p
+LAT072-1.p
+LAT074-1.p
+LAT075-1.p
+LAT076-1.p
+LAT077-1.p
+LAT078-1.p
+LAT079-1.p
+LAT080-1.p
+LAT081-1.p
+LAT082-1.p
+LAT083-1.p
+LAT084-1.p
+LAT085-1.p
+LAT086-1.p
+LAT087-1.p
+LAT088-1.p
+LAT089-1.p
+LAT090-1.p
+LAT091-1.p
+LAT092-1.p
+LAT093-1.p
+LAT094-1.p
+LAT095-1.p
+LAT096-1.p
+LAT097-1.p
+LAT138-1.p
+LAT139-1.p
+LAT140-1.p
+LAT141-1.p
+LAT142-1.p
+LAT143-1.p
+LAT144-1.p
+LAT145-1.p
+LAT146-1.p
+LAT147-1.p
+LAT148-1.p
+LAT149-1.p
+LAT150-1.p
+LAT151-1.p
+LAT152-1.p
+LAT153-1.p
+LAT154-1.p
+LAT155-1.p
+LAT156-1.p
+LAT157-1.p
+LAT158-1.p
+LAT159-1.p
+LAT160-1.p
+LAT161-1.p
+LAT162-1.p
+LAT163-1.p
+LAT164-1.p
+LAT165-1.p
+LAT166-1.p
+LAT167-1.p
+LAT168-1.p
+LAT169-1.p
+LAT170-1.p
+LAT171-1.p
+LAT172-1.p
+LAT173-1.p
+LAT174-1.p
+LAT175-1.p
+LAT176-1.p
+LAT177-1.p
+LCL109-2.p
+LCL109-6.p
+LCL110-2.p
+LCL111-2.p
+LCL112-2.p
+LCL113-2.p
+LCL114-2.p
+LCL115-2.p
+LCL116-2.p
+LCL132-1.p
+LCL133-1.p
+LCL134-1.p
+LCL135-1.p
+LCL138-1.p
+LCL139-1.p
+LCL140-1.p
+LCL141-1.p
+LCL153-1.p
+LCL154-1.p
+LCL155-1.p
+LCL156-1.p
+LCL157-1.p
+LCL158-1.p
+LCL159-1.p
+LCL160-1.p
+LCL161-1.p
+LCL162-1.p
+LCL163-1.p
+LCL164-1.p
+LDA001-1.p
+LDA002-1.p
+LDA007-3.p
+RNG007-4.p
+RNG008-3.p
+RNG008-4.p
+RNG008-7.p
+RNG009-5.p
+RNG009-7.p
+RNG011-5.p
+RNG012-6.p
+RNG013-6.p
+RNG014-6.p
+RNG015-6.p
+RNG016-6.p
+RNG017-6.p
+RNG018-6.p
+RNG019-6.p
+RNG019-7.p
+RNG020-6.p
+RNG020-7.p
+RNG021-6.p
+RNG021-7.p
+RNG023-6.p
+RNG023-7.p
+RNG024-6.p
+RNG024-7.p
+RNG025-4.p
+RNG025-5.p
+RNG025-6.p
+RNG025-7.p
+RNG026-6.p
+RNG026-7.p
+RNG027-5.p
+RNG027-7.p
+RNG027-8.p
+RNG027-9.p
+RNG028-5.p
+RNG028-7.p
+RNG028-8.p
+RNG028-9.p
+RNG029-5.p
+RNG029-6.p
+RNG029-7.p
+RNG035-7.p
+ROB001-1.p
+ROB002-1.p
+ROB003-1.p
+ROB004-1.p
+ROB005-1.p
+ROB006-1.p
+ROB006-2.p
+ROB008-1.p
+ROB009-1.p
+ROB010-1.p
+ROB013-1.p
+ROB022-1.p
+ROB023-1.p
+ROB026-1.p
+ROB030-1.p
+ROB031-1.p
+ROB032-1.p
+SYN080-1.p
+SYN083-1.p