-------------------------------------------------------------------------------- Execute format string : ./dctp-10.21p Problems list file : nne0-problems Output file : nne0-output Summary file : nne0-summary Time limit : 300 s Memory limit : 500 MB -------------------------------------------------------------------------------- Rating Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug [0.00] ALG002-1 theorem 0.1 0 [0.00] CAT007-3 theorem 0.1 0 [0.00] COM002-2 theorem 0.1 0 [0.00] COM003-2 theorem 0.1 0 [0.00] FLD006-1 theorem 0.5 0 [0.00] FLD006-3 theorem 0.1 0 [0.00] FLD010-1 theorem 11.2 37 [0.00] FLD010-3 theorem 0.1 0 [0.00] FLD018-3 theorem 0.1 0 [0.00] FLD019-3 theorem 0.1 0 [0.00] FLD020-3 theorem 0.1 0 [0.00] FLD021-3 theorem 0.1 0 [0.00] FLD033-3 theorem 0.1 0 [0.00] FLD034-3 theorem 0.1 0 [0.00] FLD039-1 theorem 0.1 0 [0.00] FLD039-3 theorem 0.1 0 [0.00] FLD055-1 theorem 0.1 0 [0.00] FLD056-1 theorem 0.1 0 [0.00] FLD056-3 theorem 0.1 0 [0.00] FLD058-1 theorem 0.1 0 [0.00] FLD071-3 theorem 0.1 0 [0.00] FLD071-4 theorem 0.1 0 [0.00] GRA001-1 theorem 0.1 0 [0.00] GRP123-1.003 theorem 0.1 0 [0.00] GRP123-2.003 theorem 0.1 0 [0.00] GRP123-3.003 theorem 0.1 0 [0.00] GRP123-4.003 theorem 0.1 0 [0.00] GRP123-6.003 theorem 0.1 0 [0.00] GRP123-7.003 theorem 0.1 0 [0.00] GRP123-8.003 theorem 0.1 0 [0.00] GRP123-9.003 theorem 0.1 0 [0.00] GRP124-1.004 theorem 0.1 0 [0.00] GRP124-2.004 theorem 0.1 0 [0.00] GRP124-3.004 theorem 0.1 0 [0.00] GRP124-4.004 theorem 0.1 0 [0.00] GRP124-6.004 theorem 0.1 0 [0.00] GRP124-7.004 theorem 0.1 0 [0.00] GRP124-8.004 theorem 0.1 0 [0.00] GRP124-9.004 theorem 0.1 0 [0.00] GRP125-1.003 theorem 0.1 0 [0.00] GRP125-2.005 theorem 0.1 0 [0.00] GRP125-3.005 theorem 0.2 0 [0.00] GRP125-4.003 theorem 0.1 0 [0.00] GRP126-1.004 theorem 0.1 0 [0.00] GRP126-2.004 theorem 0.1 0 [0.00] GRP126-3.004 theorem 0.1 0 [0.00] GRP126-4.004 theorem 0.1 0 [0.00] GRP127-1.004 theorem 0.1 0 [0.00] GRP127-2.006 theorem 0.1 0 [0.00] GRP127-3.004 theorem 0.1 0 [0.00] GRP127-4.004 theorem 0.1 0 [0.00] GRP128-1.003 theorem 0.1 0 [0.00] GRP128-4.003 theorem 0.1 0 [0.00] GRP129-1.003 theorem 0.1 0 [0.00] GRP129-2.004 theorem 0.1 0 [0.00] GRP129-3.004 theorem 0.2 0 [0.00] GRP129-4.004 theorem 0.3 0 [0.00] GRP130-1.003 theorem 0.1 0 [0.00] GRP130-2.003 theorem 0.1 0 [0.00] GRP130-3.003 theorem 0.1 0 [0.00] GRP130-4.003 theorem 0.1 0 [0.00] GRP131-1.002 theorem 0.1 0 [0.00] GRP131-2.002 theorem 0.1 0 [0.00] GRP132-1.002 theorem 0.1 0 [0.00] GRP132-2.002 theorem 0.1 0 [0.00] GRP133-1.003 theorem 0.1 0 [0.00] GRP133-2.003 theorem 0.1 0 [0.00] GRP134-1.003 theorem 0.1 0 [0.00] GRP134-2.003 theorem 0.1 0 [0.00] GRP135-1.002 theorem 0.1 0 [0.00] GRP135-2.002 theorem 0.1 0 [0.00] HWV003-3 theorem 0.1 0 [0.00] HWV005-1 theorem 0.1 0 [0.00] HWV005-2 theorem 0.1 0 [0.00] HWV006-1 theorem 0.3 0 [0.00] HWV006-2 theorem 0.3 0 [0.00] HWV007-1 theorem 0.3 0 [0.00] HWV007-2 theorem 0.2 0 [0.00] KRS001-1 theorem 0.1 0 [0.00] KRS002-1 theorem 0.1 0 [0.00] KRS003-1 theorem 0.1 0 [0.00] KRS010-1 theorem 0.1 0 [0.00] KRS012-1 theorem 0.1 0 [0.00] KRS013-1 theorem 0.1 0 [0.00] KRS015-1 theorem 0.1 0 [0.00] KRS017-1 theorem 0.1 0 [0.00] LCL181-2 theorem 0.1 0 [0.00] LCL230-2 theorem 0.1 0 [0.00] MGT004-1 theorem 0.2 0 [0.00] MGT007-1 theorem 0.3 0 [0.00] MGT016-1 theorem 0.1 0 [0.00] MGT018-1 theorem 0.1 0 [0.00] MGT022-1 theorem 0.1 0 [0.00] MGT022-2 theorem 0.1 0 [0.00] MGT028-1 theorem 0.1 0 [0.00] MGT030-1 theorem 0.1 0 [0.00] MGT036-1 theorem 0.1 0 [0.00] MGT036-2 theorem 0.1 0 [0.00] MGT041-2 theorem 0.1 0 [0.00] MSC001-1 theorem 0.3 0 [0.00] MSC002-1 theorem 0.1 0 [0.00] MSC002-2 theorem 0.1 0 [0.00] MSC003-1 theorem 0.1 0 [0.00] MSC004-1 theorem 0.1 0 [0.00] MSC006-1 theorem 0.1 0 [0.00] MSC008-1.002 theorem 0.1 0 [0.00] MSC008-2.002 theorem 0.1 0 [0.00] NLP114-1 non_thm 0.1 0 [0.00] NLP115-1 non_thm 0.1 0 [0.00] NLP116-1 non_thm 0.1 0 [0.00] NLP117-1 theorem 0.1 0 [0.00] NLP118-1 non_thm 0.1 0 [0.00] NLP119-1 non_thm 0.1 0 [0.00] NLP120-1 non_thm 0.1 0 [0.00] NLP121-1 non_thm 0.1 0 [0.00] NLP122-1 theorem 0.1 0 [0.00] NLP123-1 non_thm 0.1 0 [0.00] NUM014-1 theorem 0.1 0 [0.00] NUM015-1 theorem 0.1 0 [0.00] NUM016-1 theorem 0.1 0 [0.00] NUM016-2 theorem 0.1 0 [0.00] NUM021-1 theorem 0.2 0 [0.00] NUM022-1 theorem 0.1 0 [0.00] NUM025-2 theorem 0.1 0 [0.00] NUM027-1 theorem 0.7 0 [0.00] NUM285-1 non_thm 0.1 0 [0.00] PLA002-1 theorem 0.1 0 [0.00] PLA002-2 theorem 0.1 0 [0.00] PUZ001-1 theorem 0.1 0 [0.00] PUZ001-3 non_thm 0.1 0 [0.00] PUZ002-1 theorem 0.1 0 [0.00] PUZ004-1 theorem 0.1 0 [0.00] PUZ005-1 theorem 0.1 0 [0.00] PUZ009-1 theorem 0.1 0 [0.00] PUZ012-1 theorem 0.1 0 [0.00] PUZ013-1 theorem 0.1 0 [0.00] PUZ014-1 theorem 0.1 0 [0.00] PUZ015-2.006 theorem 0.4 0 [0.00] PUZ016-2.004 non_thm 0.1 0 [0.00] PUZ016-2.005 theorem 0.1 0 [0.00] PUZ019-1 theorem 0.1 0 [0.00] PUZ021-1 theorem 0.7 0 [0.00] PUZ023-1 theorem 0.1 0 [0.00] PUZ024-1 theorem 0.1 0 [0.00] PUZ025-1 theorem 0.1 0 [0.00] PUZ026-1 theorem 0.1 0 [0.00] PUZ027-1 theorem 0.1 0 [0.00] PUZ028-1 non_thm 0.1 0 [0.00] PUZ028-2 non_thm 0.1 0 [0.00] PUZ028-3 non_thm 0.4 0 [0.00] PUZ028-4 non_thm 0.3 0 [0.00] PUZ028-5 theorem 0.1 0 [0.00] PUZ029-1 theorem 0.1 0 [0.00] PUZ030-1 theorem 0.1 0 [0.00] PUZ030-2 theorem 0.1 0 [0.00] PUZ031-1 theorem 0.1 0 [0.00] PUZ032-1 theorem 0.1 0 [0.00] PUZ033-1 theorem 0.1 0 [0.00] PUZ035-1 theorem 0.1 0 [0.00] PUZ035-2 theorem 0.1 0 [0.00] PUZ035-5 theorem 0.1 0 [0.00] PUZ035-6 theorem 0.1 0 [0.00] SET001-1 theorem 0.1 0 [0.00] SET002-1 theorem 0.1 0 [0.00] SET003-1 theorem 0.1 0 [0.00] SET004-1 theorem 0.1 0 [0.00] SET006-1 theorem 0.1 0 [0.00] SET008-1 theorem 0.1 0 [0.00] SET009-1 theorem 0.1 0 [0.00] SET011-1 theorem 0.1 0 [0.00] SET043-5 theorem 0.1 0 [0.00] SET044-5 theorem 0.1 0 [0.00] SET045-5 theorem 0.1 0 [0.00] SET046-5 theorem 0.1 0 [0.00] SET047-5 theorem 0.1 0 [0.00] SET055-7 theorem 0.1 0 [0.00] SET786-1 theorem 0.1 0 [0.00] SWV001-1 theorem 0.1 0 [0.00] SWV009-1 theorem 0.1 0 [0.00] SYN001-1.005 theorem 0.1 0 [0.00] SYN006-1 theorem 0.1 0 [0.00] SYN008-1 theorem 0.1 0 [0.00] SYN009-1 theorem 0.1 0 [0.00] SYN009-2 theorem 0.1 0 [0.00] SYN009-3 theorem 0.1 0 [0.00] SYN009-4 theorem 0.1 0 [0.00] SYN011-1 theorem 0.1 0 [0.00] SYN012-1 theorem 0.1 0 [0.00] SYN014-2 theorem 0.1 0 [0.00] SYN028-1 theorem 0.1 0 [0.00] SYN029-1 theorem 0.1 0 [0.00] SYN030-1 theorem 0.1 0 [0.00] SYN031-1 theorem 0.1 0 [0.00] SYN032-1 theorem 0.1 0 [0.00] SYN034-1 theorem 0.1 0 [0.00] SYN038-1 theorem 0.1 0 [0.00] SYN039-1 theorem 0.1 0 [0.00] SYN044-1 theorem 0.1 0 [0.00] SYN045-1 theorem 0.1 0 [0.00] SYN047-1 theorem 0.1 0 [0.00] SYN051-1 theorem 0.1 0 [0.00] SYN052-1 theorem 0.1 0 [0.00] SYN053-1 theorem 0.1 0 [0.00] SYN054-1 theorem 0.1 0 [0.00] SYN055-1 theorem 0.1 0 [0.00] SYN056-1 non_thm 0.1 0 [0.00] SYN059-1 non_thm 0.1 0 [0.00] SYN060-1 theorem 0.1 0 [0.00] SYN061-1 theorem 0.1 0 [0.00] SYN063-1 theorem 0.1 0 [0.00] SYN066-1 theorem 0.1 0 [0.00] SYN069-1 theorem 0.1 0 [0.00] SYN070-1 theorem 0.1 0 [0.00] SYN081-1 theorem 0.1 0 [0.00] SYN082-1 theorem 0.1 0 [0.00] SYN084-2 theorem 0.1 0 [0.00] SYN091-1.003 non_thm 0.1 0 [0.00] SYN092-1.003 non_thm 0.1 0 [0.00] SYN093-1.002 theorem 0.1 0 [0.00] SYN094-1.005 theorem 0.1 0 [0.00] SYN097-1.002 theorem 0.1 0 [0.00] SYN098-1.002 theorem 0.1 0 [0.00] SYN099-1.003 theorem 0.1 0 [0.00] SYN100-1.005 theorem 0.1 0 [0.00] SYN315-1 theorem 0.1 0 [0.00] SYN317-1 non_thm 0.1 0 [0.00] SYN319-1 theorem 0.1 0 [0.00] SYN321-1 theorem 0.1 0 [0.00] SYN323-1 theorem 0.1 0 [0.00] SYN325-1 theorem 0.1 0 [0.00] SYN326-1 theorem 0.1 0 [0.00] SYN327-1 theorem 0.1 0 [0.00] SYN328-1 theorem 0.1 0 [0.00] SYN331-1 theorem 0.1 0 [0.00] SYN332-1 theorem 0.1 0 [0.00] SYN334-1 theorem 0.1 0 [0.00] SYN343-1 theorem 0.1 0 [0.00] SYN345-1 theorem 0.1 0 [0.00] SYN347-1 theorem 0.1 0 [0.00] SYN349-1 theorem 0.1 0 [0.00] SYN350-1 theorem 0.1 0 [0.00] SYN352-1 theorem 0.1 0 [0.00] SYN354-1 theorem 0.1 0 [0.00] SYN430-1 non_thm 0.1 0 [0.00] SYN431-1 non_thm 0.1 0 [0.00] SYN432-1 non_thm 0.1 0 [0.00] SYN433-1 non_thm 0.3 0 [0.00] SYN445-1 theorem 2.6 6 [0.00] SYN446-1 non_thm 1.4 0 [0.00] SYN463-1 non_thm 2.0 0 [0.00] SYN478-1 theorem 36.8 6 [0.00] SYN484-1 theorem 2.4 6 [0.00] SYN490-1 non_thm 0.1 0 [0.00] SYN491-1 non_thm 0.1 0 [0.00] SYN492-1 non_thm 0.1 0 [0.00] SYN493-1 non_thm 0.1 0 [0.00] SYN494-1 non_thm 0.1 0 [0.00] SYN495-1 non_thm 0.1 0 [0.00] SYN496-1 non_thm 0.1 0 [0.00] SYN497-1 non_thm 0.1 0 [0.00] SYN501-1 theorem 14.2 6 [0.00] SYN504-1 theorem 8.5 6 [0.00] SYN505-1 theorem 17.4 6 [0.00] SYN510-1 theorem 12.3 6 [0.00] SYN515-1 non_thm 0.1 0 [0.00] SYN516-1 non_thm 0.1 0 [0.00] SYN517-1 non_thm 0.1 0 [0.00] SYN521-1 non_thm 0.1 0 [0.00] SYN522-1 non_thm 0.1 0 [0.00] SYN523-1 non_thm 0.1 0 [0.00] SYN524-1 non_thm 0.1 0 [0.00] SYN525-1 non_thm 0.1 0 [0.00] SYN526-1 non_thm 0.1 0 [0.00] SYN527-1 non_thm 0.1 0 [0.00] SYN528-1 non_thm 0.1 0 [0.00] SYN529-1 non_thm 0.2 0 [0.00] SYN530-1 non_thm 0.1 0 [0.00] SYN531-1 non_thm 0.1 0 [0.00] SYN532-1 non_thm 0.1 0 [0.00] SYN533-1 non_thm 0.1 0 [0.00] SYN534-1 non_thm 0.1 0 [0.00] SYN535-1 non_thm 0.1 0 [0.00] SYN536-1 non_thm 0.1 0 [0.00] SYN537-1 non_thm 0.1 0 [0.00] SYN554-1 theorem 0.1 0 [0.00] SYN560-1 theorem 115.4 53 [0.00] SYN567-1 theorem 0.1 0 [0.00] SYN568-1 theorem 0.1 0 [0.00] SYN571-1 theorem 0.1 0 [0.00] SYN573-1 theorem 0.1 0 [0.00] SYN574-1 theorem 0.1 0 [0.00] SYN575-1 theorem 0.1 0 [0.00] SYN578-1 theorem 0.1 0 [0.00] SYN579-1 theorem 0.1 0 [0.00] SYN580-1 theorem 0.1 0 [0.00] SYN581-1 theorem 0.1 0 [0.00] SYN582-1 theorem 0.1 0 [0.00] SYN583-1 theorem 0.3 0 [0.00] SYN585-1 theorem 8.9 45 [0.00] SYN586-1 theorem 0.1 0 [0.00] SYN587-1 theorem 0.1 0 [0.00] SYN591-1 theorem 0.1 0 [0.00] SYN592-1 theorem 0.1 0 [0.00] SYN593-1 theorem 0.1 0 [0.00] SYN594-1 theorem 0.1 0 [0.00] SYN605-1 theorem 11.1 27 [0.00] SYN608-1 theorem 11.1 21 [0.00] SYN613-1 theorem 0.1 0 [0.00] SYN619-1 theorem 0.1 0 [0.00] SYN621-1 theorem 0.1 0 [0.00] SYN622-1 theorem 0.1 0 [0.00] SYN623-1 theorem 0.1 0 [0.00] SYN624-1 theorem 0.1 0 [0.00] SYN626-1 theorem 0.1 0 [0.00] SYN627-1 theorem 0.1 0 [0.00] SYN656-1 theorem 0.2 0 [0.00] SYN660-1 theorem 0.1 0 [0.00] SYN661-1 theorem 0.1 0 [0.00] SYN662-1 theorem 0.1 0 [0.00] SYN663-1 theorem 0.1 0 [0.00] SYN664-1 theorem 0.1 0 [0.00] SYN665-1 theorem 0.1 0 [0.00] SYN666-1 theorem 0.1 0 [0.00] SYN667-1 theorem 0.1 0 [0.00] SYN668-1 theorem 0.1 0 [0.00] SYN669-1 theorem 0.1 0 [0.00] SYN670-1 theorem 0.1 0 [0.00] SYN671-1 theorem 0.1 0 [0.00] SYN672-1 theorem 0.1 0 [0.00] SYN673-1 theorem 3.1 12 [0.00] SYN674-1 theorem 0.1 0 [0.00] SYN675-1 theorem 0.1 0 [0.00] SYN676-1 theorem 0.1 0 [0.00] SYN677-1 theorem 0.1 0 [0.00] SYN678-1 theorem 0.1 0 [0.00] SYN679-1 theorem 0.1 0 [0.00] SYN680-1 theorem 0.1 0 [0.00] SYN681-1 theorem 0.1 0 [0.00] SYN682-1 theorem 0.1 0 [0.00] SYN683-1 theorem 0.2 0 [0.00] SYN684-1 theorem 0.1 0 [0.00] SYN685-1 theorem 0.1 0 [0.00] SYN686-1 theorem 0.1 0 [0.00] SYN710-1 theorem 0.1 0 [0.00] SYN713-1 theorem 0.1 0 [0.00] SYN717-1 theorem 0.1 0 [0.00] SYN718-1 theorem 4.7 0 [0.00] SYN724-1 theorem 0.1 0 [0.00] SYN726-1 theorem 0.1 0 [0.00] SYN728-1 theorem 0.1 0 [0.00] SYN811-1 non_thm 23.9 12 [0.00] SYN823-1 non_thm 1.3 0 [0.00] SYN824-1 non_thm 16.0 16 [0.00] SYN827-1 non_thm 2.2 7 [0.00] SYN867-1 non_thm 0.1 0 [0.00] SYN868-1 non_thm 0.1 0 [0.00] SYN870-1 non_thm 0.2 0 [0.00] SYN872-1 non_thm 0.6 0 [0.00] SYN888-1 non_thm 1.4 0 [0.00] SYN902-1 non_thm 1.6 7 [0.00] TOP001-2 theorem 11.8 16 [0.00] TOP002-2 theorem 0.1 0 [0.00] TOP004-1 theorem 0.1 0 [0.00] TOP004-2 theorem 0.1 0 [0.11] PUZ010-1 theorem 0.9 0 [0.11] PUZ017-1 theorem 30.6 6 [0.11] PUZ018-1 theorem 0.1 0 [0.11] PUZ028-6 theorem 0.4 0 [0.11] SYN452-1 theorem 9.3 6 [0.11] SYN459-1 theorem 3.7 6 [0.11] SYN461-1 theorem 37.6 7 [0.11] SYN462-1 theorem 39.5 6 [0.11] SYN471-1 theorem 9.1 6 [0.11] SYN475-1 theorem 6.1 6 [0.11] SYN479-1 theorem 20.4 6 [0.11] SYN482-1 theorem 118.8 6 [0.11] SYN483-1 theorem 7.0 6 [0.11] SYN486-1 theorem 7.2 6 [0.11] SYN500-1 theorem 26.1 6 [0.11] SYN502-1 theorem 9.0 6 [0.11] SYN506-1 theorem 2.3 6 [0.11] SYN508-1 theorem 10.7 6 [0.11] SYN509-1 theorem 4.0 6 [0.11] SYN512-1 theorem 4.9 6 [0.11] SYN836-1 theorem 2.3 7 [0.11] SYN869-1 theorem 0.2 0 [0.11] SYN871-1 theorem 0.3 0 [0.11] SYN873-1 theorem 0.3 0 [0.11] SYN874-1 theorem 0.3 0 [0.11] SYN875-1 theorem 0.3 0 [0.11] SYN876-1 theorem 0.4 0 [0.11] SYN877-1 theorem 0.4 0 [0.11] SYN878-1 theorem 0.5 0 [0.11] SYN879-1 theorem 0.5 0 [0.11] SYN880-1 theorem 1.0 0 [0.11] SYN881-1 theorem 0.7 0 [0.11] SYN882-1 theorem 1.1 0 [0.11] SYN883-1 theorem 1.2 6 [0.11] SYN884-1 theorem 1.3 0 [0.11] SYN889-1 theorem 0.6 0 [0.11] SYN890-1 theorem 0.6 0 [0.11] SYN891-1 theorem 0.6 0 [0.11] SYN892-1 theorem 0.6 0 [0.11] SYN893-1 theorem 0.8 0 [0.11] SYN894-1 theorem 0.9 0 [0.11] SYN895-1 theorem 1.3 6 [0.14] HWV034-1 non_thm 0.1 0 [0.14] KRS005-1 non_thm 0.1 0 [0.14] KRS006-1 non_thm 0.1 0 [0.14] KRS007-1 non_thm 0.1 0 [0.14] KRS008-1 non_thm 0.1 0 [0.14] KRS009-1 non_thm 0.1 0 [0.14] KRS011-1 non_thm 0.1 0 [0.14] KRS014-1 non_thm 0.1 0 [0.14] KRS016-1 non_thm 0.1 0 [0.14] MSC009-1 non_thm 0.1 0 [0.14] NLP043-1 non_thm 0.1 0 [0.14] NLP044-1 non_thm 0.1 0 [0.14] NLP045-1 non_thm 0.1 0 [0.14] NLP046-1 non_thm 0.1 0 [0.14] NLP047-1 non_thm 0.1 0 [0.14] NLP048-1 non_thm 0.1 0 [0.14] NLP066-1 non_thm 0.1 0 [0.14] NLP067-1 non_thm 0.1 0 [0.14] NLP068-1 non_thm 0.1 0 [0.14] NLP095-1 non_thm 0.1 0 [0.14] NLP096-1 non_thm 0.1 0 [0.14] NLP097-1 non_thm 0.1 0 [0.14] NLP098-1 non_thm 0.1 0 [0.14] NLP099-1 non_thm 0.1 0 [0.14] NLP100-1 non_thm 0.1 0 [0.14] NLP101-1 non_thm 0.1 0 [0.14] NLP102-1 non_thm 0.1 0 [0.14] NLP103-1 non_thm 0.1 0 [0.14] NLP130-1 non_thm 0.1 0 [0.14] NLP131-1 non_thm 0.1 0 [0.14] NLP132-1 non_thm 0.1 0 [0.14] NLP133-1 non_thm 0.1 0 [0.14] NLP134-1 non_thm 0.1 0 [0.14] NLP135-1 non_thm 0.1 0 [0.14] NLP136-1 non_thm 0.1 0 [0.14] NLP137-1 non_thm 0.1 0 [0.14] NLP138-1 non_thm 0.1 0 [0.14] NLP139-1 non_thm 0.1 0 [0.14] NLP221-1 non_thm 0.1 0 [0.14] NLP222-1 non_thm 0.1 0 [0.14] NLP223-1 non_thm 0.1 0 [0.14] NLP230-1 non_thm 0.2 0 [0.14] NLP231-1 non_thm 0.1 0 [0.14] NLP232-1 non_thm 0.1 0 [0.14] NLP233-1 non_thm 0.2 0 [0.14] NLP234-1 non_thm 0.1 0 [0.14] NLP235-1 non_thm 0.1 0 [0.14] NLP236-1 non_thm 0.1 0 [0.14] NLP237-1 non_thm 0.1 0 [0.14] NLP238-1 non_thm 0.1 0 [0.14] NLP239-1 non_thm 0.1 0 [0.14] PUZ044-1 non_thm 0.1 0 [0.14] PUZ045-1 non_thm 0.1 0 [0.14] SET777-1 non_thm 0.1 0 [0.14] SET778-1 non_thm 0.1 0 [0.14] SET779-1 non_thm 0.1 0 [0.14] SET780-1 non_thm 0.1 0 [0.14] SYN036-2 non_thm 85.1 15 [0.14] SYN084-1 non_thm 0.1 0 [0.14] SYN304-1 non_thm 0.1 0 [0.14] SYN306-1 non_thm 0.1 0 [0.14] SYN308-1 non_thm 0.1 0 [0.14] SYN309-1 non_thm 0.1 0 [0.14] SYN320-1 non_thm 0.1 0 [0.14] SYN344-1 non_thm 0.1 0 [0.14] SYN348-1 non_thm 0.1 0 [0.14] SYN735-1 non_thm 0.1 0 [0.14] SYN738-1 non_thm 0.1 0 [0.14] SYN740-1 non_thm 14.2 15 [0.14] SYN743-1 non_thm 0.1 0 [0.14] SYN744-1 non_thm 0.1 0 [0.14] SYN756-1 non_thm 0.1 0 [0.14] SYN772-1 non_thm 0.1 0 [0.17] FLD001-3 theorem 0.1 0 [0.17] FLD002-3 theorem 0.4 0 [0.17] FLD005-3 theorem 4.5 28 [0.17] FLD007-3 theorem 11.4 55 [0.17] FLD008-4 theorem 14.4 22 [0.17] FLD009-3 theorem 11.7 22 [0.17] FLD010-5 theorem 3.2 22 [0.17] FLD011-3 timeout 301.3 55 [0.17] FLD012-4 timeout 301.3 55 [0.17] FLD013-3 theorem 0.2 0 [0.17] FLD013-4 theorem 0.1 0 [0.17] FLD013-5 theorem 0.1 0 [0.17] FLD014-3 theorem 0.3 0 [0.17] FLD015-3 theorem 0.7 0 [0.17] FLD016-3 theorem 1.2 0 [0.17] FLD016-5 theorem 15.5 37 [0.17] FLD017-3 theorem 0.1 0 [0.17] FLD021-1 theorem 0.1 0 [0.17] FLD022-3 theorem 12.3 22 [0.17] FLD023-3 theorem 0.1 0 [0.17] FLD024-3 theorem 0.1 0 [0.17] FLD025-3 theorem 0.1 0 [0.17] FLD025-4 theorem 0.1 0 [0.17] FLD025-5 theorem 0.1 0 [0.17] FLD026-3 theorem 88.0 37 [0.17] FLD027-3 theorem 1.0 0 [0.17] FLD028-3 theorem 2.4 10 [0.17] FLD029-3 theorem 145.4 47 [0.17] FLD030-1 theorem 0.1 0 [0.17] FLD030-2 theorem 0.1 0 [0.17] FLD030-3 theorem 0.1 0 [0.17] FLD030-4 theorem 0.1 0 [0.17] FLD031-3 theorem 0.1 0 [0.17] FLD031-5 theorem 0.2 0 [0.17] FLD032-3 theorem 0.1 0 [0.17] FLD034-1 theorem 0.1 0 [0.17] FLD035-3 theorem 1.9 6 [0.17] FLD036-3 theorem 3.8 10 [0.17] FLD037-1 theorem 0.3 0 [0.17] FLD037-3 theorem 0.1 0 [0.17] FLD038-3 theorem 0.1 0 [0.17] FLD040-3 theorem 0.7 0 [0.17] FLD040-5 theorem 1.2 0 [0.17] FLD041-3 theorem 20.2 47 [0.17] FLD041-4 theorem 221.1 18 [0.17] FLD043-3 theorem 0.1 0 [0.17] FLD049-4 theorem 15.8 13 [0.17] FLD050-4 theorem 17.3 28 [0.17] FLD055-3 theorem 0.1 0 [0.17] FLD058-3 theorem 0.1 0 [0.17] FLD059-1 theorem 0.1 0 [0.17] FLD059-3 theorem 0.1 0 [0.17] FLD059-4 theorem 0.1 0 [0.17] FLD060-3 theorem 45.6 36 [0.17] FLD060-4 theorem 5.1 16 [0.17] FLD061-4 theorem 10.3 22 [0.17] FLD063-3 timeout 301.3 28 [0.17] FLD064-3 theorem 11.2 36 [0.17] FLD065-3 theorem 0.5 0 [0.17] FLD066-3 theorem 1.2 0 [0.17] FLD067-3 theorem 11.1 29 [0.17] FLD067-4 theorem 0.1 0 [0.17] FLD068-3 timeout 301.3 45 [0.17] FLD068-4 theorem 0.1 0 [0.17] FLD069-3 theorem 0.1 0 [0.17] FLD070-1 theorem 0.1 0 [0.17] FLD070-3 theorem 0.1 0 [0.17] FLD070-4 theorem 0.1 0 [0.17] FLD071-1 theorem 0.1 0 [0.17] GRP123-3.004 non_thm 0.2 0 [0.17] GRP123-8.004 non_thm 0.2 0 [0.17] GRP123-9.004 non_thm 0.1 0 [0.17] GRP125-1.004 non_thm 0.1 0 [0.17] GRP125-2.004 non_thm 0.1 0 [0.17] GRP125-3.004 non_thm 0.1 0 [0.17] GRP127-2.005 non_thm 0.1 0 [0.17] GRP128-1.004 non_thm 0.5 0 [0.17] GRP128-2.004 non_thm 0.1 0 [0.17] GRP128-3.004 non_thm 0.5 0 [0.17] GRP130-3.004 non_thm 0.4 0 [0.17] GRP133-2.004 non_thm 0.1 0 [0.17] HWV008-1.001 theorem 0.3 0 [0.17] HWV008-1.002 theorem 0.3 0 [0.17] HWV008-2.001 theorem 0.2 0 [0.17] HWV008-2.002 theorem 0.2 0 [0.17] NLP079-1 theorem 0.1 0 [0.17] NLP080-1 theorem 0.1 0 [0.17] NLP081-1 theorem 0.1 0 [0.17] NLP094-1 theorem 0.1 0 [0.17] PUZ035-3 theorem 0.1 0 [0.17] PUZ035-4 theorem 0.1 0 [0.17] SET005-1 theorem 0.1 0 [0.17] SET007-1 theorem 0.1 0 [0.17] SET014-2 theorem 14.3 36 [0.17] SET055-6 theorem 0.1 0 [0.17] SYN002-1.007.008 theorem 0.1 0 [0.17] SYN015-2 theorem 0.1 0 [0.17] SYN036-3 theorem 0.1 0 [0.17] SYN037-1 theorem 0.1 0 [0.17] SYN037-2 theorem 0.1 0 [0.17] SYN313-1.001.002 theorem 0.1 0 [0.17] SYN419-1 non_thm 0.7 0 [0.17] SYN420-1 non_thm 0.6 0 [0.17] SYN425-1 non_thm 1.2 0 [0.17] SYN434-1 non_thm 5.6 6 [0.17] SYN435-1 non_thm 0.3 0 [0.17] SYN437-1 non_thm 30.4 7 [0.17] SYN438-1 non_thm 3.5 6 [0.17] SYN449-1 non_thm 36.9 6 [0.17] SYN456-1 non_thm 41.3 6 [0.17] SYN538-1 non_thm 0.1 0 [0.17] SYN539-1 non_thm 0.2 0 [0.17] SYN540-1 non_thm 0.1 0 [0.17] SYN541-1 non_thm 0.1 0 [0.17] SYN545-1 non_thm 0.5 0 [0.17] SYN606-1 theorem 11.1 0 [0.17] SYN607-1 theorem 11.1 27 [0.17] SYN620-1 theorem 0.1 0 [0.17] SYN625-1 theorem 14.2 21 [0.17] SYN630-1 theorem 0.1 0 [0.17] SYN633-1 theorem 0.1 0 [0.17] SYN634-1 theorem 0.1 0 [0.17] SYN635-1 theorem 0.1 0 [0.17] SYN636-1 theorem 0.1 0 [0.17] SYN641-1 theorem 0.2 0 [0.17] SYN642-1 theorem 0.2 0 [0.17] SYN643-1 theorem 0.2 0 [0.17] SYN648-1 theorem 16.3 9 [0.17] SYN659-1 theorem 0.1 0 [0.17] SYN692-1 theorem 0.3 0 [0.17] SYN693-1 theorem 0.3 0 [0.17] SYN695-1 theorem 0.2 0 [0.17] SYN697-1 theorem 2.1 0 [0.17] SYN699-1 theorem 3.7 12 [0.17] SYN701-1 theorem 2.1 9 [0.17] SYN714-1 theorem 0.1 0 [0.17] SYN815-1 non_thm 23.1 27 [0.17] SYN816-1 non_thm 20.6 28 [0.17] SYN817-1 non_thm 25.5 16 [0.17] SYN825-1 non_thm 24.2 44 [0.17] SYN826-1 non_thm 27.3 10 [0.17] SYN828-1 non_thm 9.7 21 [0.17] SYN835-1 non_thm 2.6 7 [0.17] TOP005-2 theorem 0.2 0 [0.22] GRP128-2.006 theorem 0.3 0 [0.22] GRP128-3.005 theorem 1.0 0 [0.22] SYN442-1 theorem 42.4 6 [0.22] SYN443-1 theorem 46.6 6 [0.22] SYN444-1 theorem 21.1 6 [0.22] SYN448-1 theorem 8.1 6 [0.22] SYN450-1 theorem 3.9 6 [0.22] SYN451-1 theorem 7.0 7 [0.22] SYN454-1 theorem 8.0 6 [0.22] SYN455-1 theorem 11.5 6 [0.22] SYN458-1 theorem 16.8 0 [0.22] SYN460-1 theorem 70.6 6 [0.22] SYN465-1 theorem 23.7 7 [0.22] SYN466-1 theorem 14.6 6 [0.22] SYN467-1 theorem 58.6 6 [0.22] SYN469-1 theorem 15.9 6 [0.22] SYN472-1 theorem 41.1 6 [0.22] SYN477-1 theorem 43.6 6 [0.22] SYN480-1 theorem 106.8 6 [0.22] SYN485-1 theorem 28.6 6 [0.22] SYN488-1 theorem 15.1 6 [0.22] SYN489-1 theorem 70.2 6 [0.22] SYN499-1 theorem 17.1 7 [0.22] SYN507-1 theorem 22.3 10 [0.22] SYN813-1 theorem 12.0 8 [0.22] SYN833-1 theorem 3.3 7 [0.22] SYN834-1 theorem 3.2 7 [0.22] SYN843-1 theorem 5.1 6 [0.22] SYN849-1 theorem 13.9 10 [0.22] SYN856-1 theorem 5.8 8 [0.22] SYN857-1 theorem 7.3 8 [0.22] SYN859-1 theorem 4.2 0 [0.22] SYN886-1 theorem 1.3 7 [0.22] SYN887-1 theorem 1.4 0 [0.22] SYN896-1 theorem 1.2 0 [0.22] SYN898-1 theorem 3.2 9 [0.22] SYN899-1 theorem 3.5 7 [0.22] SYN900-1 theorem 2.7 7 [0.22] SYN901-1 theorem 5.5 0 [0.29] HWV034-2 non_thm 0.1 0 [0.29] HWV035-1 non_thm 0.1 0 [0.29] HWV036-1 non_thm 0.1 0 [0.29] NLP059-1 non_thm 0.1 0 [0.29] NLP064-1 non_thm 0.1 0 [0.29] NLP065-1 non_thm 0.1 0 [0.29] SYN316-1 timeout 300.3 26 [0.29] SYN324-1 timeout 300.3 26 [0.29] SYN330-1 timeout 301.3 28 [0.29] SYN335-1 timeout 301.3 27 [0.29] SYN351-1 timeout 301.3 72 [0.29] SYN734-1 non_thm 115.4 101 [0.29] SYN742-1 non_thm 14.2 15 [0.29] SYN748-1 non_thm 0.1 0 [0.29] SYN749-1 non_thm 14.1 9 [0.29] SYN754-1 non_thm 83.4 76 [0.29] SYN757-1 non_thm 0.1 0 [0.29] SYN760-1 non_thm 0.5 0 [0.29] SYN774-1 non_thm 0.1 0 [0.29] SYN785-1 non_thm 14.2 16 [0.29] SYN797-1 non_thm 0.1 0 [0.29] SYN798-1 non_thm 14.2 10 [0.33] ANA002-1 timeout 301.3 45 [0.33] ANA002-2 theorem 12.2 21 [0.33] ANA002-3 timeout 301.2 36 [0.33] ANA002-4 theorem 12.4 21 [0.33] ANA003-4 timeout 302.3 52 [0.33] FLD003-1 theorem 16.4 10 [0.33] FLD005-1 timeout 301.3 38 [0.33] FLD009-1 timeout 301.2 13 [0.33] FLD013-1 theorem 0.1 0 [0.33] FLD013-2 theorem 0.1 0 [0.33] FLD015-1 timeout 301.3 37 [0.33] FLD017-1 theorem 0.1 0 [0.33] FLD018-1 theorem 16.3 10 [0.33] FLD019-1 theorem 11.3 22 [0.33] FLD023-1 theorem 0.2 0 [0.33] FLD024-1 timeout 301.2 36 [0.33] FLD025-1 theorem 0.1 0 [0.33] FLD025-2 theorem 0.1 0 [0.33] FLD031-1 theorem 142.3 22 [0.33] FLD032-1 theorem 0.3 0 [0.33] FLD043-5 theorem 9.5 37 [0.33] FLD047-4 timeout 301.4 48 [0.33] FLD049-3 timeout 301.3 97 [0.33] FLD054-4 timeout 301.2 17 [0.33] FLD059-2 theorem 0.1 0 [0.33] FLD060-1 theorem 0.1 0 [0.33] FLD060-2 theorem 0.3 0 [0.33] FLD061-1 theorem 0.1 0 [0.33] FLD061-2 theorem 0.3 0 [0.33] FLD061-3 theorem 15.9 10 [0.33] FLD062-3 theorem 51.0 22 [0.33] FLD064-1 theorem 76.3 98 [0.33] FLD065-1 theorem 70.8 17 [0.33] FLD067-1 theorem 0.2 0 [0.33] FLD067-2 theorem 74.7 0 [0.33] FLD068-2 timeout 301.3 29 [0.33] FLD069-1 theorem 0.1 0 [0.33] FLD070-2 theorem 0.6 0 [0.33] FLD071-2 theorem 0.1 0 [0.33] GRP039-6 theorem 3.9 8 [0.33] GRP123-4.004 non_thm 0.1 0 [0.33] GRP125-4.004 non_thm 0.1 0 [0.33] GRP126-2.005 non_thm 0.1 0 [0.33] GRP127-3.005 non_thm 0.4 0 [0.33] GRP128-4.004 non_thm 0.1 0 [0.33] GRP130-2.005 non_thm 0.2 0 [0.33] GRP130-4.004 non_thm 0.2 0 [0.33] MSC007-1.008 theorem 1.9 0 [0.33] PUZ018-2 non_thm 0.1 0 [0.33] PUZ035-7 theorem 0.1 0 [0.33] SET010-1 theorem 0.1 0 [0.33] SET012-1 theorem 137.5 61 [0.33] SET012-2 theorem 15.6 21 [0.33] SET013-1 timeout 301.2 16 [0.33] SET015-1 timeout 301.3 28 [0.33] SYN036-1 theorem 1.3 0 [0.33] SYN036-4 theorem 0.1 0 [0.33] SYN353-1 timeout 300.2 15 [0.33] SYN418-1 non_thm 1.5 0 [0.33] SYN421-1 non_thm 1.2 6 [0.33] SYN422-1 non_thm 1.2 0 [0.33] SYN423-1 non_thm 1.3 0 [0.33] SYN424-1 non_thm 3.0 6 [0.33] SYN426-1 non_thm 1.8 0 [0.33] SYN427-1 non_thm 5.9 16 [0.33] SYN428-1 non_thm 1.8 0 [0.33] SYN429-1 non_thm 1.5 0 [0.33] SYN436-1 theorem 20.1 7 [0.33] SYN441-1 non_thm 31.6 8 [0.33] SYN453-1 non_thm 35.5 6 [0.33] SYN464-1 non_thm 0.5 0 [0.33] SYN468-1 theorem 13.4 6 [0.33] SYN470-1 theorem 22.0 6 [0.33] SYN474-1 theorem 11.5 6 [0.33] SYN476-1 theorem 73.3 6 [0.33] SYN481-1 theorem 42.3 6 [0.33] SYN487-1 theorem 7.7 6 [0.33] SYN498-1 theorem 8.6 6 [0.33] SYN503-1 theorem 14.4 6 [0.33] SYN511-1 theorem 44.0 6 [0.33] SYN513-1 non_thm 0.5 0 [0.33] SYN518-1 non_thm 1.4 0 [0.33] SYN542-1 non_thm 1.2 0 [0.33] SYN543-1 non_thm 30.5 6 [0.33] SYN544-1 non_thm 0.5 0 [0.33] SYN546-1 non_thm 4.1 21 [0.33] SYN547-1 non_thm 0.9 0 [0.33] SYN576-1 theorem 0.4 0 [0.33] SYN595-1 theorem 0.1 0 [0.33] SYN604-1 theorem 4.2 20 [0.33] SYN610-1 theorem 11.2 21 [0.33] SYN611-1 theorem 11.1 12 [0.33] SYN612-1 theorem 11.2 21 [0.33] SYN645-1 theorem 0.2 0 [0.33] SYN657-1 theorem 0.1 0 [0.33] SYN658-1 theorem 0.1 0 [0.33] SYN687-1 theorem 15.6 16 [0.33] SYN694-1 theorem 0.2 0 [0.33] SYN696-1 theorem 0.2 0 [0.33] SYN698-1 theorem 0.2 0 [0.33] SYN700-1 theorem 0.2 0 [0.33] SYN755-1 theorem 0.2 0 [0.33] SYN759-1 theorem 0.3 0 [0.33] SYN762-1 theorem 1.0 0 [0.33] SYN784-1 theorem 2.5 6 [0.33] SYN796-1 theorem 1.9 0 [0.33] SYN812-1 non_thm 75.3 45 [0.33] SYN814-1 timeout 300.6 10 [0.33] SYN819-1 theorem 9.6 8 [0.33] SYN820-1 theorem 9.5 0 [0.33] SYN829-1 non_thm 42.4 53 [0.33] SYN831-1 non_thm 43.6 53 [0.33] SYN832-1 non_thm 36.2 10 [0.33] SYN837-1 theorem 12.0 10 [0.33] SYN838-1 non_thm 12.5 0 [0.33] SYN841-1 non_thm 55.2 62 [0.33] SYN844-1 theorem 4.1 8 [0.33] SYN845-1 theorem 5.0 6 [0.33] SYN847-1 theorem 14.7 10 [0.33] SYN848-1 theorem 16.1 10 [0.33] SYN851-1 non_thm 13.5 28 [0.33] SYN858-1 theorem 4.0 10 [0.33] SYN860-1 theorem 4.5 12 [0.33] SYN863-1 non_thm 16.3 28 [0.33] SYN864-1 non_thm 14.9 10 [0.33] SYN897-1 theorem 3.4 12 [0.43] HWV035-2 non_thm 0.1 0 [0.43] HWV036-2 non_thm 0.1 0 [0.43] NLP026-1 non_thm 0.1 0 [0.43] NLP031-1 non_thm 0.1 0 [0.43] SYN736-1 non_thm 82.4 42 [0.43] SYN737-1 non_thm 11.1 16 [0.43] SYN739-1 non_thm 11.1 6 [0.43] SYN745-1 non_thm 83.3 93 [0.43] SYN752-1 non_thm 0.1 0 [0.43] SYN768-1 non_thm 115.2 12 [0.43] SYN794-1 non_thm 14.2 17 [0.43] SYN804-1 non_thm 0.1 0 [0.43] TOP003-2 non_thm 0.1 0 [0.44] SYN447-1 theorem 129.9 7 [0.44] SYN457-1 theorem 46.9 6 [0.44] SYN473-1 theorem 26.1 6 [0.44] SYN846-1 theorem 16.4 12 [0.44] SYN862-1 theorem 16.1 28 [0.44] SYN885-1 theorem 32.8 0 [0.50] ANA004-4 timeout 302.4 234 [0.50] ANA004-5 timeout 301.3 45 [0.50] COM003-1 theorem 15.8 8 [0.50] FLD004-1 theorem 1.6 0 [0.50] FLD007-1 timeout 301.3 45 [0.50] FLD016-1 timeout 301.2 21 [0.50] FLD020-1 timeout 301.3 54 [0.50] FLD022-1 timeout 301.3 45 [0.50] FLD033-1 timeout 301.3 62 [0.50] FLD050-3 theorem 63.5 16 [0.50] FLD052-4 timeout 301.2 29 [0.50] FLD057-3 timeout 301.2 16 [0.50] FLD063-1 timeout 301.3 22 [0.50] FLD066-1 timeout 301.2 8 [0.50] FLD068-1 timeout 301.3 21 [0.50] GRP123-1.005 non_thm 0.3 0 [0.50] GRP123-2.005 non_thm 0.3 0 [0.50] GRP123-6.005 non_thm 0.1 0 [0.50] GRP123-7.005 non_thm 0.1 0 [0.50] GRP124-1.005 non_thm 0.2 0 [0.50] GRP124-2.005 non_thm 0.1 0 [0.50] GRP124-3.005 non_thm 2.3 6 [0.50] GRP124-4.005 non_thm 0.2 0 [0.50] GRP124-6.005 non_thm 0.1 0 [0.50] GRP124-7.005 non_thm 0.2 0 [0.50] GRP124-8.005 non_thm 1.6 0 [0.50] GRP124-9.005 non_thm 0.2 0 [0.50] GRP126-1.005 non_thm 0.1 0 [0.50] GRP126-3.005 non_thm 0.4 0 [0.50] GRP126-4.005 non_thm 0.1 0 [0.50] GRP127-1.005 non_thm 0.1 0 [0.50] GRP127-4.005 non_thm 0.1 0 [0.50] GRP129-1.005 non_thm 5.8 6 [0.50] GRP129-2.005 non_thm 0.1 0 [0.50] GRP129-3.005 non_thm 11.3 6 [0.50] GRP129-4.005 non_thm 0.8 0 [0.50] GRP130-1.005 non_thm 2.2 6 [0.50] GRP131-1.005 non_thm 0.2 0 [0.50] GRP131-2.005 non_thm 0.3 0 [0.50] GRP132-2.005 non_thm 0.3 0 [0.50] GRP133-1.004 non_thm 0.1 0 [0.50] GRP134-1.005 non_thm 0.1 0 [0.50] GRP134-2.005 non_thm 0.1 0 [0.50] GRP135-1.005 non_thm 6.9 6 [0.50] GRP135-2.005 non_thm 0.2 0 [0.50] SET013-2 theorem 21.6 13 [0.50] SET015-2 theorem 36.5 45 [0.50] SYN067-1 theorem 3.6 6 [0.50] SYN307-1 non_thm 0.1 0 [0.50] SYN514-1 non_thm 4.7 12 [0.50] SYN520-1 non_thm 1.2 0 [0.50] SYN609-1 theorem 11.2 27 [0.50] SYN644-1 theorem 14.9 21 [0.50] SYN690-1 theorem 0.5 0 [0.50] SYN758-1 theorem 0.7 0 [0.50] SYN802-1 timeout 300.4 13 [0.50] SYN830-1 non_thm 47.3 53 [0.50] SYN839-1 non_thm 55.2 62 [0.50] SYN840-1 non_thm 54.2 62 [0.50] SYN842-1 non_thm 65.3 62 [0.50] SYN852-1 non_thm 72.6 16 [0.50] SYN853-1 non_thm 68.9 62 [0.50] SYN854-1 non_thm 70.8 62 [0.50] SYN855-1 non_thm 64.0 61 [0.56] SYN439-1 theorem 170.7 6 [0.56] SYN440-1 theorem 95.6 6 [0.56] SYN850-1 theorem 14.8 28 [0.56] SYN861-1 theorem 15.4 27 [0.56] SYN865-1 theorem 16.7 28 [0.56] SYN866-1 theorem 16.6 28 [0.57] NLP032-1 non_thm 84.0 45 [0.57] NLP033-1 non_thm 0.4 0 [0.57] NLP061-1 non_thm 0.1 0 [0.57] NLP062-1 non_thm 0.1 0 [0.57] NLP063-1 non_thm 9.5 0 [0.57] NLP160-1 non_thm 0.1 0 [0.57] NLP161-1 non_thm 0.1 0 [0.57] NLP162-1 non_thm 0.1 0 [0.57] NLP163-1 non_thm 0.1 0 [0.57] NLP164-1 non_thm 0.2 0 [0.57] NLP165-1 non_thm 0.2 0 [0.57] NLP166-1 non_thm 0.2 0 [0.57] NLP167-1 non_thm 0.1 0 [0.57] NLP168-1 non_thm 0.1 0 [0.57] NLP169-1 non_thm 0.1 0 [0.57] NLP190-1 non_thm 0.1 0 [0.57] NLP191-1 non_thm 0.1 0 [0.57] NLP192-1 non_thm 0.1 0 [0.57] NLP193-1 non_thm 0.1 0 [0.57] NLP194-1 non_thm 0.1 0 [0.57] NLP195-1 non_thm 0.1 0 [0.57] NLP196-1 non_thm 0.1 0 [0.57] NLP197-1 non_thm 0.1 0 [0.57] NLP198-1 non_thm 0.1 0 [0.57] NLP199-1 non_thm 0.1 0 [0.57] SYN741-1 timeout 301.4 26 [0.57] SYN746-1 non_thm 255.3 10 [0.57] SYN747-1 timeout 300.1 7 [0.57] SYN750-1 timeout 301.4 94 [0.57] SYN751-1 timeout 301.4 101 [0.57] SYN753-1 timeout 301.3 26 [0.57] SYN761-1 timeout 300.2 12 [0.57] SYN763-1 timeout 301.2 68 [0.57] SYN766-1 timeout 301.2 16 [0.57] SYN769-1 non_thm 11.1 6 [0.57] SYN775-1 timeout 300.2 16 [0.57] SYN780-1 non_thm 0.1 0 [0.57] SYN786-1 non_thm 0.1 0 [0.57] SYN787-1 non_thm 0.1 0 [0.57] SYN790-1 timeout 301.3 27 [0.57] SYN791-1 non_thm 0.1 0 [0.57] SYN800-1 timeout 300.1 0 [0.57] SYN801-1 timeout 300.4 13 [0.57] SYN903-1 non_thm 0.8 0 [0.57] SYN904-1 non_thm 2.7 9 [0.57] SYN905-1 non_thm 5.7 20 [0.57] SYN907-1 non_thm 3.5 8 [0.57] SYN908-1 non_thm 28.4 35 [0.57] SYN909-1 non_thm 2.6 10 [0.57] SYN910-1 non_thm 10.9 13 [0.57] SYN912-1 non_thm 33.1 44 [0.57] TOP010-1 timeout 301.3 28 [0.57] TOP011-1 non_thm 14.2 28 [0.57] TOP014-1 timeout 301.2 21 [0.57] TOP016-1 timeout 301.2 13 [0.67] COM005-1 timeout 300.2 10 [0.67] FLD008-3 timeout 301.2 46 [0.67] FLD027-1 timeout 301.3 21 [0.67] FLD038-1 timeout 301.3 53 [0.67] FLD040-1 timeout 300.3 45 [0.67] FLD048-4 timeout 301.3 88 [0.67] FLD051-4 timeout 308.4 74 [0.67] FLD086-3 timeout 301.2 38 [0.67] FLD090-3 timeout 301.2 13 [0.67] GRP132-1.005 non_thm 2.2 6 [0.67] PUZ034-1.004 theorem 117.2 37 [0.67] SYN067-2 theorem 13.2 6 [0.67] SYN067-3 theorem 2.4 6 [0.67] SYN519-1 non_thm 141.9 12 [0.67] SYN650-1 theorem 8.1 16 [0.67] SYN818-1 non_thm 150.3 53 [0.67] SYN821-1 non_thm 29.7 28 [0.71] NLP027-1 non_thm 0.1 0 [0.71] NLP028-1 non_thm 0.1 0 [0.71] NLP029-1 non_thm 0.1 0 [0.71] NLP030-1 non_thm 0.1 0 [0.71] NLP034-1 timeout 301.2 10 [0.71] NLP035-1 timeout 301.2 12 [0.71] NLP060-1 non_thm 4.3 6 [0.71] NUM288-1 non_thm 0.1 0 [0.71] SET781-1 timeout 301.3 60 [0.71] SYN764-1 timeout 300.2 15 [0.71] SYN770-1 non_thm 115.1 6 [0.71] SYN777-1 non_thm 0.1 0 [0.71] SYN778-1 non_thm 0.1 0 [0.71] SYN781-1 non_thm 0.1 0 [0.71] SYN783-1 non_thm 0.1 0 [0.71] SYN793-1 non_thm 0.1 0 [0.71] SYN799-1 timeout 300.1 0 [0.71] SYN808-1 non_thm 0.1 0 [0.71] SYN810-1 non_thm 0.1 0 [0.71] SYN906-1 timeout 301.4 21 [0.71] SYN913-1 timeout 301.4 20 [0.71] TOP001-1 non_thm 14.2 21 [0.71] TOP002-1 timeout 301.4 63 [0.71] TOP003-1 timeout 301.4 45 [0.71] TOP006-1 non_thm 14.2 37 [0.71] TOP015-1 timeout 301.2 13 [0.71] TOP018-1 timeout 301.5 36 [0.71] TOP019-1 timeout 301.4 27 [0.83] FLD012-3 timeout 301.3 55 [0.83] FLD014-1 timeout 301.2 45 [0.83] FLD028-1 timeout 301.3 46 [0.83] FLD035-1 timeout 301.4 70 [0.83] FLD036-1 timeout 301.3 53 [0.83] FLD041-1 timeout 301.3 28 [0.83] FLD044-4 timeout 301.2 16 [0.83] FLD045-4 timeout 301.1 0 [0.83] FLD062-1 timeout 301.3 27 [0.83] FLD072-3 timeout 301.2 21 [0.83] FLD072-4 timeout 301.2 22 [0.83] FLD074-3 timeout 301.2 16 [0.83] FLD087-3 timeout 301.2 37 [0.83] FLD088-3 timeout 301.2 36 [0.83] FLD089-3 timeout 301.2 23 [0.83] FLD097-4 timeout 301.3 17 [0.83] SYN314-1.002.001 timeout 301.3 20 [0.83] SYN822-1 non_thm 34.2 28 [0.86] GRP025-3 timeout 301.2 16 [0.86] GRP026-3 timeout 301.2 13 [0.86] GRP027-2 timeout 301.2 13 [0.86] PUZ034-1.003 timeout 301.4 45 [0.86] SYN765-1 timeout 300.2 15 [0.86] SYN767-1 timeout 301.2 15 [0.86] SYN771-1 non_thm 115.1 6 [0.86] SYN773-1 non_thm 115.2 27 [0.86] SYN776-1 non_thm 255.2 12 [0.86] SYN779-1 timeout 301.4 21 [0.86] SYN782-1 timeout 301.4 28 [0.86] SYN788-1 timeout 301.3 21 [0.86] SYN789-1 timeout 300.3 16 [0.86] SYN792-1 timeout 300.3 16 [0.86] SYN795-1 timeout 300.2 16 [0.86] SYN803-1 timeout 301.4 27 [0.86] SYN805-1 timeout 301.4 21 [0.86] SYN806-1 timeout 301.4 21 [0.86] SYN807-1 non_thm 0.1 0 [0.86] SYN809-1 timeout 301.4 21 [0.86] SYN911-1 timeout 301.6 43 [0.86] TOP005-1 timeout 301.4 55 [0.86] TOP007-1 timeout 301.3 45 [0.86] TOP008-1 timeout 301.3 28 [0.86] TOP009-1 timeout 301.3 36 [0.86] TOP012-1 timeout 301.2 28 [0.86] TOP013-1 timeout 301.2 21 [0.86] TOP017-1 timeout 301.2 0 [1.00] ANA001-1 timeout 301.3 45 [1.00] ANA005-4 timeout 301.2 61 [1.00] ANA005-5 timeout 301.3 36 [1.00] COM006-1 timeout 301.2 13 [1.00] FLD008-1 timeout 301.2 38 [1.00] FLD008-2 timeout 301.2 55 [1.00] FLD011-1 timeout 301.3 28 [1.00] FLD012-1 timeout 301.3 45 [1.00] FLD012-2 timeout 301.3 54 [1.00] FLD026-1 timeout 301.2 46 [1.00] FLD029-1 timeout 301.3 28 [1.00] FLD041-2 timeout 301.3 39 [1.00] FLD043-1 timeout 301.2 28 [1.00] FLD044-1 timeout 301.2 38 [1.00] FLD044-2 timeout 301.2 45 [1.00] FLD044-3 timeout 301.2 38 [1.00] FLD045-1 timeout 301.1 22 [1.00] FLD045-2 timeout 301.2 17 [1.00] FLD045-3 timeout 301.1 0 [1.00] FLD046-1 timeout 301.4 28 [1.00] FLD046-3 timeout 301.4 55 [1.00] FLD047-1 timeout 301.4 38 [1.00] FLD047-2 timeout 301.4 53 [1.00] FLD047-3 timeout 301.4 114 [1.00] FLD048-1 timeout 301.4 38 [1.00] FLD048-2 timeout 301.4 81 [1.00] FLD048-3 timeout 301.4 133 [1.00] FLD049-1 timeout 301.3 29 [1.00] FLD049-2 timeout 301.3 46 [1.00] FLD050-1 timeout 301.2 21 [1.00] FLD050-2 timeout 301.3 47 [1.00] FLD051-1 timeout 301.4 36 [1.00] FLD051-2 timeout 301.4 81 [1.00] FLD051-3 timeout 301.4 141 [1.00] FLD052-1 timeout 301.2 36 [1.00] FLD052-2 timeout 301.2 44 [1.00] FLD052-3 timeout 301.2 37 [1.00] FLD053-1 timeout 301.2 16 [1.00] FLD053-2 timeout 301.2 63 [1.00] FLD053-3 timeout 301.2 17 [1.00] FLD053-4 timeout 301.2 29 [1.00] FLD054-1 timeout 301.2 22 [1.00] FLD054-2 timeout 301.2 22 [1.00] FLD054-3 timeout 301.2 22 [1.00] FLD057-1 timeout 301.1 13 [1.00] FLD072-1 timeout 301.3 36 [1.00] FLD072-2 timeout 301.3 28 [1.00] FLD073-1 timeout 301.2 22 [1.00] FLD073-2 timeout 301.2 22 [1.00] FLD073-3 timeout 301.2 16 [1.00] FLD073-4 timeout 301.2 37 [1.00] FLD074-1 timeout 301.2 28 [1.00] FLD074-2 timeout 301.2 37 [1.00] FLD074-4 timeout 301.2 16 [1.00] FLD075-1 timeout 301.2 8 [1.00] FLD075-2 timeout 301.1 17 [1.00] FLD075-3 timeout 301.2 12 [1.00] FLD075-4 timeout 301.2 8 [1.00] FLD076-1 timeout 301.1 0 [1.00] FLD076-2 timeout 301.4 36 [1.00] FLD076-3 timeout 301.4 38 [1.00] FLD076-4 timeout 301.4 46 [1.00] FLD077-1 timeout 301.4 54 [1.00] FLD077-2 timeout 301.4 53 [1.00] FLD077-3 timeout 301.4 38 [1.00] FLD077-4 timeout 301.3 55 [1.00] FLD078-1 timeout 301.4 46 [1.00] FLD078-2 timeout 301.3 45 [1.00] FLD078-3 timeout 301.3 63 [1.00] FLD078-4 timeout 301.3 57 [1.00] FLD079-1 timeout 301.3 28 [1.00] FLD079-2 timeout 301.3 21 [1.00] FLD079-3 timeout 301.3 45 [1.00] FLD079-4 timeout 301.3 28 [1.00] FLD080-1 timeout 301.2 17 [1.00] FLD080-2 timeout 301.2 17 [1.00] FLD080-3 timeout 301.2 21 [1.00] FLD080-4 timeout 301.2 46 [1.00] FLD081-1 timeout 301.2 21 [1.00] FLD081-2 timeout 301.2 16 [1.00] FLD081-3 timeout 301.2 16 [1.00] FLD081-4 timeout 301.2 10 [1.00] FLD082-1 timeout 301.2 0 [1.00] FLD082-3 timeout 301.1 0 [1.00] FLD083-1 timeout 301.4 45 [1.00] FLD083-3 timeout 301.4 45 [1.00] FLD084-1 timeout 301.4 22 [1.00] FLD084-3 timeout 301.4 46 [1.00] FLD085-1 timeout 301.4 21 [1.00] FLD085-3 timeout 304.4 55 [1.00] FLD086-1 timeout 305.4 13 [1.00] FLD087-1 timeout 301.2 28 [1.00] FLD088-1 timeout 301.2 28 [1.00] FLD089-1 timeout 301.2 22 [1.00] FLD090-1 timeout 301.2 8 [1.00] FLD091-1 timeout 301.1 8 [1.00] FLD091-3 timeout 301.2 0 [1.00] FLD092-1 timeout 301.4 37 [1.00] FLD092-3 timeout 301.8 46 [1.00] FLD093-1 timeout 301.4 28 [1.00] FLD093-3 timeout 301.3 88 [1.00] FLD094-1 timeout 301.4 37 [1.00] FLD094-3 timeout 301.3 57 [1.00] FLD095-1 timeout 301.4 45 [1.00] FLD095-2 timeout 301.4 56 [1.00] FLD095-3 timeout 301.3 28 [1.00] FLD095-4 timeout 301.3 63 [1.00] FLD096-1 timeout 301.3 38 [1.00] FLD096-2 timeout 301.3 48 [1.00] FLD096-3 timeout 301.3 22 [1.00] FLD096-4 timeout 301.3 37 [1.00] FLD097-1 timeout 301.3 48 [1.00] FLD097-2 timeout 301.3 28 [1.00] FLD097-3 timeout 301.3 28 [1.00] FLD098-1 timeout 301.3 44 [1.00] FLD098-2 timeout 301.3 54 [1.00] FLD098-3 timeout 301.3 22 [1.00] FLD098-4 timeout 301.3 13 [1.00] FLD099-1 timeout 301.2 36 [1.00] FLD099-2 timeout 301.2 17 [1.00] FLD099-3 timeout 301.3 46 [1.00] FLD099-4 timeout 301.2 10 [1.00] FLD100-1 timeout 301.2 16 [1.00] FLD100-2 timeout 301.2 28 [1.00] FLD100-3 timeout 301.2 13 [1.00] FLD100-4 timeout 301.2 13 [1.00] MSC008-1.010 timeout 300.3 13