-------------------------------------------------------------------------------- Execute format string : ./dctp-10.21p Problems list file : hne-problems Output file : hne-output Summary file : hne-summary Time limit : 300 s Memory limit : 500 MB -------------------------------------------------------------------------------- Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug ANA003-2 timeout 302.3 44 ANA004-2 timeout 301.2 27 ANA005-2 timeout 301.2 27 COM001-1 theorem 0.1 0 COM002-1 theorem 0.1 0 GEO001-4 timeout 301.2 35 GEO002-4 theorem 0.1 0 GEO079-1 theorem 0.1 0 GRP001-5 theorem 0.1 0 GRP003-1 theorem 0.1 0 GRP003-2 theorem 0.1 0 GRP004-1 theorem 0.1 0 GRP004-2 theorem 7.0 16 GRP005-1 theorem 0.1 0 GRP006-1 theorem 0.1 0 GRP028-1 theorem 0.1 0 GRP028-3 theorem 0.1 0 GRP028-4 theorem 0.1 0 GRP029-2 theorem 0.1 0 GRP031-2 theorem 0.1 0 GRP033-3 theorem 0.1 0 GRP034-4 theorem 0.1 0 GRP041-2 theorem 0.1 0 GRP042-2 theorem 0.1 0 GRP043-2 theorem 0.1 0 GRP044-2 theorem 0.1 0 GRP045-2 theorem 0.1 0 GRP046-2 theorem 0.1 0 GRP047-2 theorem 0.2 0 GRP048-2 theorem 77.6 86 GRP394-2 non_thm 0.1 0 KRS004-1 theorem 0.1 0 LAT005-1 theorem 0.4 0 LAT005-2 theorem 0.2 0 LCL001-1 timeout 301.3 21 LCL002-1 timeout 301.3 16 LCL003-1 timeout 301.3 16 LCL004-1 theorem 102.2 12 LCL005-1 timeout 301.3 16 LCL006-1 theorem 11.4 12 LCL007-1 theorem 0.1 0 LCL008-1 theorem 0.1 0 LCL009-1 theorem 10.5 12 LCL010-1 theorem 0.1 0 LCL011-1 theorem 1.6 0 LCL012-1 timeout 301.3 21 LCL013-1 theorem 0.1 0 LCL014-1 theorem 73.0 21 LCL015-1 theorem 92.3 8 LCL016-1 timeout 301.3 21 LCL017-1 timeout 301.3 12 LCL018-1 theorem 99.7 12 LCL019-1 timeout 301.4 21 LCL020-1 timeout 301.4 16 LCL021-1 timeout 301.4 16 LCL022-1 theorem 0.1 0 LCL023-1 theorem 10.3 12 LCL024-1 timeout 301.3 16 LCL025-1 theorem 58.2 35 LCL026-1 theorem 16.3 16 LCL027-1 theorem 0.1 0 LCL028-1 timeout 301.2 16 LCL029-1 theorem 0.1 0 LCL030-1 timeout 301.2 16 LCL031-1 timeout 301.2 12 LCL032-1 timeout 308.2 10 LCL033-1 theorem 0.1 0 LCL034-1 theorem 23.3 12 LCL035-1 theorem 0.1 0 LCL036-1 theorem 10.4 10 LCL037-1 timeout 301.2 10 LCL038-1 timeout 301.1 8 LCL039-1 theorem 31.3 10 LCL040-1 theorem 10.4 10 LCL041-1 theorem 0.1 0 LCL042-1 theorem 219.9 35 LCL043-1 theorem 0.1 0 LCL044-1 theorem 0.1 0 LCL045-1 theorem 1.4 8 LCL046-1 theorem 0.1 0 LCL047-1 theorem 1.2 0 LCL048-1 theorem 1.0 0 LCL049-1 theorem 6.2 10 LCL050-1 theorem 47.7 27 LCL051-1 theorem 43.5 27 LCL052-1 theorem 24.6 21 LCL053-1 theorem 23.6 20 LCL054-1 timeout 301.2 10 LCL055-1 theorem 26.6 10 LCL056-1 theorem 14.9 12 LCL057-1 theorem 27.4 21 LCL058-1 timeout 301.4 35 LCL059-1 theorem 52.5 35 LCL060-1 timeout 301.2 9 LCL061-1 timeout 301.1 8 LCL062-1 timeout 301.1 0 LCL063-1 timeout 301.4 35 LCL064-1 theorem 77.6 43 LCL064-2 theorem 12.3 10 LCL065-1 theorem 10.3 10 LCL066-1 theorem 0.2 0 LCL067-1 theorem 91.5 16 LCL068-1 theorem 0.4 0 LCL069-1 theorem 0.1 0 LCL070-1 theorem 91.6 44 LCL071-1 theorem 2.2 9 LCL072-1 theorem 0.1 0 LCL073-1 timeout 301.2 8 LCL074-1 timeout 301.1 8 LCL075-1 theorem 0.3 0 LCL076-1 theorem 0.2 0 LCL076-2 theorem 0.1 0 LCL076-3 theorem 10.4 15 LCL077-1 theorem 0.1 0 LCL077-2 theorem 0.4 0 LCL078-1 timeout 301.4 44 LCL079-1 theorem 0.1 0 LCL080-1 theorem 10.4 10 LCL080-2 theorem 2.6 8 LCL081-1 theorem 0.1 0 LCL082-1 theorem 0.1 0 LCL083-1 theorem 0.6 0 LCL083-2 theorem 0.1 0 LCL084-2 timeout 301.3 16 LCL084-3 timeout 301.3 16 LCL085-1 timeout 301.3 12 LCL086-1 theorem 0.1 0 LCL087-1 theorem 0.1 0 LCL088-1 theorem 0.1 0 LCL089-1 theorem 0.3 0 LCL090-1 theorem 0.5 0 LCL091-1 theorem 0.3 0 LCL092-1 theorem 1.3 0 LCL093-1 theorem 40.4 16 LCL094-1 theorem 0.5 0 LCL095-1 theorem 2.3 7 LCL096-1 theorem 46.7 43 LCL097-1 theorem 9.7 9 LCL098-1 theorem 0.1 0 LCL099-1 timeout 301.4 35 LCL100-1 timeout 301.3 35 LCL101-1 theorem 0.1 0 LCL102-1 theorem 10.5 10 LCL103-1 timeout 301.3 35 LCL104-1 theorem 0.1 0 LCL105-1 timeout 301.3 20 LCL106-1 theorem 0.1 0 LCL107-1 theorem 0.1 0 LCL108-1 theorem 1.7 0 LCL109-1 timeout 301.3 35 LCL110-1 theorem 0.1 0 LCL111-1 theorem 10.3 12 LCL112-1 theorem 0.1 0 LCL113-1 theorem 11.2 12 LCL114-1 theorem 117.1 8 LCL115-1 theorem 2.1 0 LCL116-1 timeout 301.2 8 LCL117-1 theorem 0.1 0 LCL118-1 theorem 0.3 0 LCL119-1 timeout 301.1 0 LCL120-1 theorem 0.6 0 LCL121-1 theorem 94.0 43 LCL122-1 timeout 301.3 20 LCL123-1 theorem 4.9 8 LCL124-1 timeout 301.2 12 LCL125-1 timeout 301.2 12 LCL126-1 theorem 0.1 0 LCL127-1 timeout 301.2 9 LCL128-1 theorem 10.9 9 LCL129-1 theorem 244.4 0 LCL130-1 theorem 0.1 0 LCL131-1 theorem 10.5 9 LCL166-1 timeout 301.3 16 LCL167-1 timeout 301.3 16 LCL168-1 timeout 301.3 16 LCL169-1 theorem 0.1 0 LCL170-1 theorem 0.1 0 LCL171-1 theorem 0.1 0 LCL172-1 theorem 0.1 0 LCL173-1 theorem 0.1 0 LCL174-1 theorem 0.1 0 LCL175-1 theorem 0.1 0 LCL176-1 theorem 0.1 0 LCL177-1 theorem 0.1 0 LCL178-1 theorem 0.1 0 LCL179-1 timeout 301.3 37 LCL180-1 timeout 301.3 37 LCL181-1 timeout 301.3 38 LCL182-1 theorem 0.5 0 LCL183-1 timeout 301.3 37 LCL184-1 timeout 301.3 28 LCL185-1 theorem 0.1 0 LCL186-1 theorem 0.1 0 LCL187-1 theorem 0.1 0 LCL188-1 theorem 0.1 0 LCL189-1 theorem 0.1 0 LCL190-1 theorem 0.1 0 LCL191-1 theorem 68.9 37 LCL192-1 theorem 0.1 0 LCL193-1 theorem 0.1 0 LCL194-1 theorem 0.5 0 LCL195-1 theorem 10.4 12 LCL196-1 theorem 15.2 10 LCL197-1 theorem 0.1 0 LCL198-1 theorem 14.8 16 LCL199-1 theorem 0.1 0 LCL200-1 theorem 0.1 0 LCL201-1 theorem 1.9 0 LCL202-1 theorem 10.3 13 LCL203-1 theorem 1.8 0 LCL204-1 theorem 1.7 0 LCL205-1 theorem 10.4 10 LCL206-1 theorem 1.3 0 LCL207-1 theorem 1.1 0 LCL208-1 theorem 10.4 8 LCL209-1 timeout 301.3 55 LCL210-1 theorem 10.4 10 LCL211-1 theorem 0.1 0 LCL212-1 theorem 11.3 12 LCL213-1 theorem 10.4 8 LCL214-1 theorem 10.3 8 LCL215-1 theorem 10.4 8 LCL216-1 theorem 0.1 0 LCL217-1 theorem 0.2 0 LCL218-1 theorem 0.2 0 LCL219-1 timeout 301.5 46 LCL220-1 timeout 301.4 55 LCL221-1 theorem 11.2 10 LCL222-1 theorem 11.2 10 LCL223-1 timeout 301.2 37 LCL224-1 theorem 261.3 37 LCL225-1 timeout 301.2 10 LCL226-1 theorem 0.1 0 LCL227-1 timeout 301.2 8 LCL228-1 timeout 301.2 8 LCL229-1 timeout 301.2 0 LCL230-1 theorem 11.1 0 LCL231-1 theorem 18.5 22 LCL234-1 theorem 67.0 37 LCL235-1 timeout 301.3 28 LCL236-1 theorem 0.1 0 LCL237-1 theorem 66.9 28 LCL238-1 theorem 0.3 0 LCL239-1 timeout 301.2 16 LCL240-1 timeout 301.2 13 LCL241-1 timeout 301.2 13 LCL242-1 timeout 301.2 10 LCL243-1 timeout 301.2 10 LCL244-1 timeout 301.2 10 LCL245-1 timeout 301.2 8 LCL246-1 timeout 301.2 10 LCL247-1 timeout 301.2 0 LCL248-1 timeout 301.4 55 LCL249-1 timeout 301.4 55 LCL250-1 theorem 86.4 55 LCL251-1 timeout 301.3 37 LCL252-1 timeout 303.3 28 LCL253-1 timeout 301.4 55 LCL254-1 timeout 301.4 46 LCL255-1 timeout 301.4 45 LCL256-1 theorem 24.4 20 LCL257-1 theorem 0.1 0 LCL355-1 theorem 0.1 0 LCL356-1 theorem 0.4 0 LCL357-1 theorem 0.1 0 LCL358-1 theorem 0.6 0 LCL359-1 theorem 0.6 0 LCL360-1 theorem 0.1 0 LCL361-1 theorem 0.1 0 LCL362-1 theorem 0.1 0 LCL363-1 theorem 0.1 0 LCL364-1 theorem 5.2 9 LCL365-1 theorem 41.0 10 LCL366-1 theorem 0.1 0 LCL367-1 theorem 0.9 0 LCL368-1 timeout 301.3 27 LCL369-1 theorem 47.9 21 LCL370-1 theorem 151.4 27 LCL371-1 theorem 151.5 10 LCL372-1 timeout 301.3 27 LCL373-1 timeout 301.3 27 LCL374-1 timeout 301.3 27 LCL375-1 timeout 301.3 27 LCL376-1 timeout 301.3 27 LCL377-1 timeout 301.3 27 LCL378-1 theorem 6.7 10 LCL379-1 theorem 20.0 16 LCL380-1 theorem 29.9 0 LCL381-1 theorem 39.0 27 LCL382-1 timeout 301.3 35 LCL383-1 timeout 301.3 35 LCL384-1 theorem 105.7 35 LCL385-1 timeout 301.1 0 LCL386-1 timeout 301.4 35 LCL387-1 timeout 301.4 35 LCL388-1 timeout 301.4 35 LCL389-1 timeout 301.3 35 LCL390-1 timeout 301.3 35 LCL391-1 timeout 301.4 27 LCL392-1 timeout 301.4 35 LCL393-1 timeout 301.4 35 LCL394-1 timeout 301.3 35 LCL395-1 timeout 301.3 35 LCL396-1 theorem 37.5 27 LCL397-1 theorem 0.1 0 LCL398-1 theorem 0.1 0 LCL399-1 theorem 10.4 7 LCL400-1 theorem 27.4 21 LCL401-1 theorem 46.3 21 LCL402-1 theorem 29.9 21 LCL403-1 timeout 301.2 10 LCL404-1 timeout 301.2 10 LCL405-1 theorem 24.9 9 LCL411-1 non_thm 0.1 0 LCL414-1 theorem 0.1 0 LCL415-1 timeout 83.5 67 LCL416-1 theorem 174.0 9 LCL417-1 timeout 301.2 10 LCL418-1 timeout 301.2 12 LCL419-1 timeout 301.2 21 LCL420-1 timeout 301.2 21 LCL421-1 timeout 301.2 16 LCL422-1 timeout 301.2 10 LCL423-1 timeout 301.2 7 LCL424-1 timeout 301.2 7 LCL425-1 timeout 301.2 12 LCL426-1 timeout 301.2 10 LCL427-1 timeout 301.2 8 LCL428-1 theorem 0.1 0 MGT001-1 theorem 0.1 0 MGT002-1 theorem 0.1 0 MGT003-1 theorem 0.1 0 MGT006-1 theorem 0.1 0 MGT008-1 theorem 0.1 0 MGT009-1 theorem 0.1 0 MGT010-1 theorem 0.1 0 MGT015-1 theorem 0.1 0 MGT017-1 theorem 0.1 0 MGT032-2 theorem 0.1 0 MGT036-3 theorem 0.1 0 MSC005-1 theorem 0.1 0 NLP001-1 theorem 0.1 0 NLP104-1 non_thm 0.1 0 NLP105-1 non_thm 0.1 0 NLP106-1 non_thm 0.1 0 NLP107-1 non_thm 0.1 0 NLP108-1 non_thm 0.1 0 NLP109-1 non_thm 0.1 0 NLP110-1 non_thm 0.1 0 NLP111-1 non_thm 0.1 0 NLP112-1 non_thm 0.1 0 NLP113-1 non_thm 0.1 0 NUM001-1 theorem 0.1 0 NUM002-1 theorem 0.1 0 NUM003-1 theorem 0.1 0 NUM004-1 theorem 0.1 0 NUM017-1 theorem 29.1 53 NUM019-1 theorem 0.1 0 NUM020-1 theorem 0.1 0 NUM023-1 theorem 0.1 0 NUM024-1 theorem 0.2 0 NUM025-1 theorem 0.1 0 NUM026-1 timeout 301.3 28 NUM283-1.005 theorem 0.3 0 NUM284-1.014 theorem 68.8 21 NUM286-1 non_thm 0.1 0 NUM286-2 non_thm 0.1 0 NUM287-1 non_thm 0.1 0 PLA001-1 theorem 0.1 0 PLA003-1 theorem 0.1 0 PLA004-1 theorem 0.1 0 PLA004-2 theorem 0.1 0 PLA005-1 theorem 0.1 0 PLA005-2 theorem 0.1 0 PLA006-1 theorem 0.1 0 PLA007-1 theorem 0.1 0 PLA008-1 theorem 2.0 13 PLA009-1 theorem 0.1 0 PLA009-2 theorem 0.1 0 PLA010-1 theorem 3.4 17 PLA011-1 theorem 0.1 0 PLA011-2 theorem 0.1 0 PLA012-1 theorem 2.2 16 PLA013-1 theorem 0.1 0 PLA014-1 theorem 0.1 0 PLA014-2 theorem 0.1 0 PLA015-1 theorem 5.9 21 PLA016-1 theorem 0.1 0 PLA017-1 theorem 0.1 0 PLA018-1 theorem 3.1 21 PLA019-1 theorem 0.1 0 PLA020-1 theorem 0.1 0 PLA021-1 theorem 0.1 0 PLA022-1 theorem 0.1 0 PLA022-2 theorem 0.1 0 PLA023-1 theorem 2.2 16 PLA029-1 non_thm 0.1 0 PLA030-1 non_thm 0.1 0 PUZ003-1 theorem 0.1 0 PUZ008-1 theorem 0.1 0 PUZ008-2 theorem 0.1 0 PUZ008-3 theorem 0.1 0 PUZ011-1 theorem 0.1 0 PUZ015-3 timeout 301.4 99 PUZ022-1 theorem 0.1 0 PUZ036-1.005 theorem 0.1 0 PUZ037-1 theorem 0.1 0 PUZ037-2 theorem 1.0 0 PUZ037-3 timeout 301.7 91 PUZ038-1 theorem 0.1 0 PUZ039-1 theorem 11.4 38 PUZ040-1 theorem 10.2 55 PUZ041-1 timeout 302.4 46 PUZ042-1 theorem 12.1 46 PUZ046-1 non_thm 0.1 0 PUZ047-1 theorem 0.1 0 PUZ048-1 non_thm 0.7 0 PUZ049-1 non_thm 10.8 46 PUZ050-1 timeout 302.3 209 PUZ051-1 timeout 302.4 183 PUZ052-1 timeout 301.2 91 PUZ053-1 timeout 301.7 90 PUZ054-1 non_thm 10.1 53 RNG001-2 theorem 66.8 27 RNG001-3 theorem 1.1 0 RNG001-5 theorem 66.4 16 RNG004-3 timeout 301.4 138 RNG005-2 theorem 0.1 0 RNG006-2 theorem 0.1 0 RNG037-2 theorem 0.1 0 RNG038-2 theorem 0.1 0 RNG039-2 theorem 10.3 37 ROB025-1 timeout 301.3 67 SWV010-1 non_thm 0.1 0 SWV011-1 theorem 0.1 0 SWV012-1 non_thm 0.1 0 SWV013-1 non_thm 0.1 0 SWV014-1 timeout 302.4 135 SWV015-1 non_thm 0.1 0 SWV016-1 timeout 302.4 161 SWV017-1 non_thm 0.1 0 SWV018-1 timeout 302.4 152 SYN003-1.006 theorem 0.1 0 SYN004-1.007 theorem 0.1 0 SYN005-1.010 theorem 0.1 0 SYN010-1.005.005 theorem 0.1 0 SYN033-1 theorem 0.1 0 SYN035-1 theorem 0.1 0 SYN040-1 theorem 0.1 0 SYN041-1 theorem 0.1 0 SYN046-1 theorem 0.1 0 SYN048-1 theorem 0.1 0 SYN049-1 theorem 0.1 0 SYN050-1 theorem 0.1 0 SYN057-1 theorem 0.1 0 SYN058-1 theorem 0.1 0 SYN062-1 theorem 0.1 0 SYN063-2 theorem 0.1 0 SYN064-1 theorem 0.1 0 SYN065-1 theorem 0.1 0 SYN068-1 theorem 0.1 0 SYN079-1 theorem 0.1 0 SYN085-1.010 theorem 0.1 0 SYN086-1.003 non_thm 0.1 0 SYN087-1.003 non_thm 0.1 0 SYN088-1.010 theorem 0.1 0 SYN089-1.002 theorem 0.1 0 SYN090-1.008 theorem 0.1 0 SYN095-1.002 theorem 0.1 0 SYN096-1.008 theorem 0.1 0 SYN101-1.002.002 theorem 0.1 0 SYN102-1.007.007 theorem 0.2 0 SYN103-1 theorem 0.2 0 SYN104-1 theorem 0.2 0 SYN105-1 theorem 0.3 0 SYN106-1 theorem 0.3 0 SYN107-1 theorem 0.6 0 SYN108-1 theorem 0.6 0 SYN109-1 theorem 0.6 0 SYN110-1 theorem 0.6 0 SYN111-1 theorem 0.6 0 SYN112-1 theorem 0.6 0 SYN113-1 theorem 0.6 0 SYN114-1 theorem 0.6 0 SYN115-1 theorem 0.6 0 SYN116-1 theorem 0.6 0 SYN117-1 theorem 0.6 0 SYN118-1 theorem 0.2 0 SYN119-1 theorem 0.2 0 SYN120-1 theorem 0.6 0 SYN121-1 theorem 0.6 0 SYN122-1 theorem 0.6 0 SYN123-1 theorem 0.7 0 SYN124-1 theorem 0.6 0 SYN125-1 theorem 0.6 0 SYN126-1 theorem 0.6 0 SYN127-1 theorem 0.6 0 SYN128-1 theorem 0.7 0 SYN129-1 theorem 0.6 0 SYN130-1 theorem 0.2 0 SYN131-1 theorem 0.2 0 SYN132-1 theorem 0.2 0 SYN133-1 theorem 0.2 0 SYN134-1 theorem 0.3 0 SYN135-1 theorem 0.6 0 SYN136-1 theorem 0.7 0 SYN137-1 theorem 0.7 0 SYN138-1 theorem 0.7 0 SYN139-1 theorem 0.7 0 SYN140-1 theorem 0.7 0 SYN141-1 theorem 0.6 0 SYN142-1 theorem 0.7 0 SYN143-1 theorem 0.7 0 SYN144-1 theorem 0.6 0 SYN145-1 theorem 0.2 0 SYN146-1 theorem 0.2 0 SYN147-1 theorem 0.2 0 SYN148-1 theorem 0.6 0 SYN149-1 theorem 0.6 0 SYN150-1 theorem 0.6 0 SYN151-1 theorem 0.6 0 SYN152-1 theorem 0.3 0 SYN153-1 theorem 0.6 0 SYN154-1 theorem 0.6 0 SYN155-1 theorem 0.6 0 SYN156-1 theorem 0.6 0 SYN157-1 theorem 0.7 0 SYN158-1 theorem 0.7 0 SYN159-1 theorem 0.7 0 SYN160-1 theorem 0.7 0 SYN161-1 theorem 0.6 0 SYN162-1 theorem 0.7 0 SYN163-1 theorem 0.7 0 SYN164-1 theorem 0.2 0 SYN165-1 theorem 0.2 0 SYN166-1 theorem 0.6 0 SYN167-1 theorem 0.6 0 SYN168-1 theorem 0.7 0 SYN169-1 theorem 0.6 0 SYN170-1 theorem 0.6 0 SYN171-1 theorem 0.7 0 SYN172-1 theorem 0.2 0 SYN173-1 theorem 0.6 0 SYN174-1 theorem 0.6 0 SYN175-1 theorem 0.6 0 SYN176-1 theorem 0.6 0 SYN177-1 theorem 0.6 0 SYN178-1 theorem 0.6 0 SYN179-1 theorem 0.7 0 SYN180-1 theorem 0.6 0 SYN181-1 theorem 0.7 0 SYN182-1 theorem 0.6 0 SYN183-1 theorem 0.6 0 SYN184-1 theorem 0.2 0 SYN185-1 theorem 0.2 0 SYN186-1 theorem 0.5 0 SYN187-1 theorem 0.6 0 SYN188-1 theorem 0.6 0 SYN189-1 theorem 0.3 0 SYN190-1 theorem 0.7 0 SYN191-1 theorem 0.7 0 SYN192-1 theorem 0.6 0 SYN193-1 theorem 0.6 0 SYN194-1 theorem 0.6 0 SYN195-1 theorem 0.6 0 SYN196-1 theorem 0.6 0 SYN197-1 theorem 0.2 0 SYN198-1 theorem 0.3 0 SYN199-1 theorem 0.6 0 SYN200-1 theorem 0.3 0 SYN201-1 theorem 0.6 0 SYN202-1 theorem 0.6 0 SYN203-1 theorem 0.6 0 SYN204-1 theorem 0.7 0 SYN205-1 theorem 0.7 0 SYN206-1 theorem 0.6 0 SYN207-1 theorem 0.6 0 SYN208-1 theorem 0.6 0 SYN209-1 theorem 0.6 0 SYN210-1 theorem 0.6 0 SYN211-1 theorem 0.6 0 SYN212-1 theorem 0.6 0 SYN213-1 theorem 0.7 0 SYN214-1 theorem 0.7 0 SYN215-1 theorem 0.7 0 SYN216-1 theorem 0.6 0 SYN217-1 theorem 0.6 0 SYN218-1 theorem 0.6 0 SYN219-1 theorem 0.5 0 SYN220-1 theorem 0.6 0 SYN221-1 theorem 0.6 0 SYN222-1 theorem 0.6 0 SYN223-1 theorem 0.6 0 SYN224-1 theorem 0.6 0 SYN225-1 theorem 0.6 0 SYN226-1 theorem 0.6 0 SYN227-1 theorem 0.6 0 SYN228-1 theorem 0.6 0 SYN229-1 theorem 0.6 0 SYN230-1 theorem 0.7 0 SYN231-1 theorem 0.6 0 SYN232-1 theorem 0.6 0 SYN233-1 theorem 0.6 0 SYN234-1 theorem 0.6 0 SYN235-1 theorem 0.6 0 SYN236-1 theorem 0.6 0 SYN237-1 theorem 0.2 0 SYN238-1 theorem 0.6 0 SYN239-1 theorem 0.2 0 SYN240-1 theorem 0.2 0 SYN241-1 theorem 0.2 0 SYN242-1 theorem 0.2 0 SYN243-1 theorem 0.6 0 SYN244-1 theorem 0.2 0 SYN245-1 theorem 0.2 0 SYN246-1 theorem 0.6 0 SYN247-1 theorem 0.6 0 SYN248-1 theorem 0.6 0 SYN249-1 theorem 0.6 0 SYN250-1 theorem 0.6 0 SYN251-1 theorem 0.6 0 SYN252-1 theorem 0.7 0 SYN253-1 theorem 0.7 0 SYN254-1 theorem 0.7 0 SYN255-1 theorem 0.2 0 SYN256-1 theorem 0.6 0 SYN257-1 theorem 0.2 0 SYN258-1 theorem 0.6 0 SYN259-1 theorem 0.6 0 SYN260-1 theorem 0.6 0 SYN261-1 theorem 0.6 0 SYN262-1 theorem 0.6 0 SYN263-1 theorem 0.6 0 SYN264-1 theorem 0.6 0 SYN265-1 theorem 0.6 0 SYN266-1 theorem 0.7 0 SYN267-1 theorem 0.6 0 SYN268-1 theorem 0.6 0 SYN269-1 theorem 0.7 0 SYN270-1 theorem 0.7 0 SYN271-1 theorem 0.7 0 SYN272-1 theorem 0.7 0 SYN273-1 theorem 0.7 0 SYN274-1 theorem 0.2 0 SYN275-1 theorem 0.2 0 SYN276-1 theorem 0.2 0 SYN277-1 theorem 0.2 0 SYN278-1 theorem 0.1 0 SYN279-1 theorem 0.6 0 SYN280-1 theorem 0.2 0 SYN281-1 theorem 0.1 0 SYN282-1 theorem 0.2 0 SYN283-1 theorem 0.6 0 SYN284-1 theorem 0.6 0 SYN285-1 theorem 0.7 0 SYN286-1 theorem 0.6 0 SYN287-1 theorem 0.2 0 SYN288-1 theorem 0.2 0 SYN289-1 theorem 0.7 0 SYN290-1 theorem 0.6 0 SYN291-1 theorem 0.2 0 SYN292-1 theorem 0.6 0 SYN293-1 theorem 0.6 0 SYN294-1 theorem 0.6 0 SYN295-1 theorem 0.2 0 SYN296-1 theorem 0.6 0 SYN297-1 theorem 0.2 0 SYN298-1 theorem 0.7 0 SYN299-1 theorem 0.6 0 SYN300-1 theorem 0.6 0 SYN301-1 theorem 0.6 0 SYN302-1.003 non_thm 0.1 0 SYN303-1 non_thm 10.1 12 SYN310-1 theorem 0.1 0 SYN311-1 theorem 0.1 0 SYN312-1 theorem 0.1 0 SYN318-1 theorem 0.1 0 SYN322-1 non_thm 0.1 0 SYN329-1 non_thm 0.1 0 SYN333-1 theorem 0.1 0 SYN336-1 theorem 0.1 0 SYN337-1 non_thm 0.1 0 SYN338-1 theorem 0.1 0 SYN339-1 theorem 0.1 0 SYN340-1 theorem 0.1 0 SYN341-1 theorem 0.1 0 SYN342-1 non_thm 0.1 0 SYN346-1 theorem 0.1 0 SYN553-1 theorem 0.1 0 SYN555-1 theorem 0.1 0 SYN556-1 theorem 0.1 0 SYN557-1 theorem 0.7 0 SYN558-1 theorem 0.1 0 SYN559-1 theorem 0.1 0 SYN561-1 theorem 0.1 0 SYN562-1 theorem 0.1 0 SYN563-1 theorem 0.5 0 SYN564-1 theorem 1.2 0 SYN565-1 theorem 2.0 10 SYN566-1 theorem 0.1 0 SYN569-1 theorem 0.1 0 SYN570-1 theorem 0.1 0 SYN572-1 theorem 10.7 16 SYN577-1 theorem 0.1 0 SYN584-1 theorem 0.1 0 SYN588-1 theorem 0.1 0 SYN589-1 theorem 0.1 0 SYN590-1 theorem 0.3 0 SYN596-1 theorem 0.1 0 SYN597-1 theorem 0.1 0 SYN598-1 theorem 0.1 0 SYN599-1 theorem 0.1 0 SYN600-1 theorem 0.1 0 SYN601-1 theorem 0.1 0 SYN602-1 theorem 0.1 0 SYN603-1 theorem 20.6 53 SYN614-1 theorem 85.2 27 SYN615-1 theorem 216.7 63 SYN616-1 theorem 0.1 0 SYN617-1 theorem 64.6 20 SYN618-1 theorem 0.1 0 SYN628-1 theorem 0.1 0 SYN629-1 theorem 0.1 0 SYN631-1 theorem 5.2 21 SYN632-1 theorem 0.1 0 SYN637-1 theorem 0.1 0 SYN638-1 theorem 0.1 0 SYN639-1 theorem 0.3 0 SYN640-1 theorem 0.3 0 SYN646-1 theorem 0.3 0 SYN647-1 theorem 0.3 0 SYN649-1 theorem 2.4 8 SYN651-1 theorem 0.1 0 SYN652-1 theorem 0.1 0 SYN653-1 theorem 0.2 0 SYN654-1 theorem 0.2 0 SYN655-1 theorem 0.2 0 SYN688-1 theorem 0.1 0 SYN689-1 theorem 0.1 0 SYN691-1 theorem 0.9 0 SYN702-1 theorem 0.2 0 SYN703-1 theorem 2.5 10 SYN704-1 theorem 0.3 0 SYN705-1 theorem 4.7 12 SYN706-1 theorem 0.2 0 SYN707-1 theorem 2.0 0 SYN708-1 theorem 2.0 0 SYN709-1 theorem 3.3 16 SYN711-1 theorem 0.1 0 SYN712-1 theorem 0.3 0 SYN715-1 theorem 10.1 20 SYN716-1 theorem 0.2 0 SYN719-1 theorem 0.1 0 SYN720-1 non_thm 0.6 0 SYN721-1 theorem 0.1 0 SYN727-1 theorem 0.1 0 SYN729-1 theorem 0.1 0 SYN731-1 theorem 0.1 0