-------------------------------------------------------------------------------- Execute format string : ./dctp.1.31 -negpref -complexity -fullrewrite -alternate -resisol 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 memory 118.9 499 ANA004-2 memory 118.1 499 ANA005-2 memory 117.8 499 COM001-1 theorem 0.0 4 COM002-1 theorem 0.0 6 GEO001-4 timeout 300.0 27 GEO002-4 theorem 0.1 4 GEO079-1 theorem 0.0 6 GRP001-5 theorem 0.0 6 GRP003-1 theorem 0.0 6 GRP003-2 theorem 0.1 6 GRP004-1 theorem 0.1 6 GRP004-2 theorem 0.1 6 GRP005-1 theorem 0.0 0 GRP006-1 theorem 0.0 6 GRP028-1 theorem 0.0 4 GRP028-3 theorem 0.0 4 GRP028-4 theorem 0.0 6 GRP029-2 theorem 0.2 6 GRP031-2 theorem 0.0 4 GRP033-3 theorem 0.0 6 GRP034-4 theorem 0.0 6 GRP041-2 theorem 0.0 6 GRP042-2 theorem 0.0 6 GRP043-2 theorem 0.0 6 GRP044-2 theorem 0.0 6 GRP045-2 theorem 0.0 6 GRP046-2 theorem 0.0 6 GRP047-2 theorem 0.0 6 GRP048-2 theorem 8.2 27 GRP394-2 non_thm 0.0 6 KRS004-1 theorem 0.0 6 LAT005-1 theorem 0.3 8 LAT005-2 theorem 0.4 8 LCL001-1 timeout 300.0 76 LCL002-1 timeout 300.0 27 LCL003-1 timeout 300.0 34 LCL004-1 theorem 189.1 27 LCL005-1 timeout 300.0 35 LCL006-1 timeout 300.0 84 LCL007-1 theorem 0.0 6 LCL008-1 theorem 0.0 6 LCL009-1 theorem 0.0 6 LCL010-1 theorem 0.0 6 LCL011-1 theorem 0.0 4 LCL012-1 timeout 300.0 34 LCL013-1 theorem 0.0 6 LCL014-1 theorem 1.7 9 LCL015-1 timeout 300.0 34 LCL016-1 theorem 186.4 34 LCL017-1 timeout 300.0 34 LCL018-1 timeout 300.0 34 LCL019-1 timeout 300.0 34 LCL020-1 timeout 300.0 26 LCL021-1 timeout 300.0 34 LCL022-1 theorem 0.0 6 LCL023-1 theorem 0.0 6 LCL024-1 timeout 300.0 34 LCL025-1 theorem 61.3 43 LCL026-1 theorem 133.1 51 LCL027-1 theorem 0.0 4 LCL028-1 timeout 300.0 68 LCL029-1 timeout 300.0 50 LCL030-1 timeout 300.0 59 LCL031-1 timeout 300.0 51 LCL032-1 timeout 300.0 43 LCL033-1 theorem 0.0 6 LCL034-1 theorem 0.1 6 LCL035-1 theorem 0.0 6 LCL036-1 theorem 0.0 4 LCL037-1 timeout 300.0 43 LCL038-1 timeout 300.0 50 LCL039-1 timeout 300.0 67 LCL040-1 timeout 300.0 60 LCL041-1 theorem 0.1 4 LCL042-1 timeout 300.0 102 LCL043-1 theorem 0.0 6 LCL044-1 theorem 0.1 4 LCL045-1 theorem 83.4 45 LCL046-1 theorem 0.0 4 LCL047-1 theorem 179.5 34 LCL048-1 timeout 300.0 43 LCL049-1 theorem 1.4 8 LCL050-1 theorem 69.3 26 LCL051-1 timeout 300.0 52 LCL052-1 timeout 300.0 43 LCL053-1 timeout 300.0 43 LCL054-1 timeout 300.0 51 LCL055-1 timeout 300.0 43 LCL056-1 theorem 1.2 7 LCL057-1 theorem 1.0 7 LCL058-1 timeout 300.0 52 LCL059-1 timeout 300.0 51 LCL060-1 timeout 300.0 51 LCL061-1 timeout 300.0 43 LCL062-1 timeout 300.0 59 LCL063-1 timeout 300.0 51 LCL064-1 theorem 9.9 15 LCL064-2 theorem 9.0 15 LCL065-1 theorem 14.3 20 LCL066-1 theorem 0.3 7 LCL067-1 theorem 83.3 44 LCL068-1 theorem 0.1 6 LCL069-1 theorem 0.0 6 LCL070-1 timeout 300.0 52 LCL071-1 timeout 300.0 51 LCL072-1 theorem 0.7 7 LCL073-1 timeout 300.0 21 LCL074-1 timeout 300.0 20 LCL075-1 theorem 0.0 6 LCL076-1 timeout 300.0 50 LCL076-2 theorem 0.0 6 LCL076-3 theorem 0.0 6 LCL077-1 theorem 46.9 34 LCL077-2 theorem 0.0 6 LCL078-1 timeout 300.0 51 LCL079-1 theorem 0.0 6 LCL080-1 timeout 300.0 51 LCL080-2 theorem 0.8 4 LCL081-1 theorem 0.0 6 LCL082-1 theorem 0.0 6 LCL083-1 theorem 0.0 6 LCL083-2 theorem 0.0 6 LCL084-2 timeout 300.0 43 LCL084-3 timeout 300.0 59 LCL085-1 timeout 300.0 42 LCL086-1 theorem 0.0 6 LCL087-1 theorem 0.0 4 LCL088-1 theorem 0.0 0 LCL089-1 theorem 0.0 6 LCL090-1 theorem 0.0 6 LCL091-1 theorem 0.0 6 LCL092-1 theorem 1.4 7 LCL093-1 timeout 300.0 51 LCL094-1 theorem 0.5 6 LCL095-1 theorem 1.0 7 LCL096-1 theorem 55.4 34 LCL097-1 theorem 0.5 7 LCL098-1 theorem 4.0 7 LCL099-1 timeout 300.0 59 LCL100-1 timeout 300.0 51 LCL101-1 theorem 0.0 6 LCL102-1 theorem 1.4 9 LCL103-1 timeout 300.0 58 LCL104-1 theorem 0.1 6 LCL105-1 timeout 300.0 51 LCL106-1 theorem 0.0 6 LCL107-1 theorem 0.0 6 LCL108-1 theorem 0.5 7 LCL109-1 timeout 300.0 68 LCL110-1 theorem 0.0 6 LCL111-1 theorem 1.5 10 LCL112-1 theorem 0.0 4 LCL113-1 timeout 300.0 60 LCL114-1 timeout 300.0 76 LCL115-1 theorem 4.0 12 LCL116-1 timeout 300.0 68 LCL117-1 theorem 0.0 4 LCL118-1 theorem 0.0 6 LCL119-1 timeout 300.0 34 LCL120-1 theorem 0.1 6 LCL121-1 timeout 300.0 50 LCL122-1 timeout 300.0 50 LCL123-1 timeout 300.0 50 LCL124-1 timeout 300.0 50 LCL125-1 timeout 300.0 51 LCL126-1 theorem 0.0 6 LCL127-1 timeout 300.0 42 LCL128-1 timeout 300.0 42 LCL129-1 timeout 300.0 50 LCL130-1 theorem 0.0 4 LCL131-1 timeout 300.0 59 LCL166-1 timeout 300.0 34 LCL167-1 timeout 300.0 26 LCL168-1 timeout 300.0 20 LCL169-1 theorem 0.0 6 LCL170-1 theorem 0.0 0 LCL171-1 theorem 0.0 4 LCL172-1 theorem 0.0 0 LCL173-1 theorem 0.0 4 LCL174-1 theorem 0.0 6 LCL175-1 theorem 0.0 6 LCL176-1 theorem 0.0 4 LCL177-1 theorem 0.0 4 LCL178-1 theorem 0.0 6 LCL179-1 timeout 300.0 159 LCL180-1 timeout 300.0 159 LCL181-1 timeout 300.0 125 LCL182-1 theorem 3.0 17 LCL183-1 timeout 300.0 80 LCL184-1 timeout 300.0 159 LCL185-1 theorem 0.0 6 LCL186-1 theorem 0.0 4 LCL187-1 theorem 0.0 6 LCL188-1 theorem 0.0 6 LCL189-1 theorem 0.0 6 LCL190-1 theorem 0.0 6 LCL191-1 theorem 2.6 13 LCL192-1 theorem 0.0 6 LCL193-1 theorem 0.3 6 LCL194-1 theorem 0.4 6 LCL195-1 theorem 0.4 6 LCL196-1 theorem 0.1 6 LCL197-1 theorem 0.0 6 LCL198-1 theorem 0.1 6 LCL199-1 theorem 0.0 6 LCL200-1 theorem 0.0 6 LCL201-1 theorem 0.3 6 LCL202-1 theorem 0.2 6 LCL203-1 theorem 0.2 6 LCL204-1 theorem 22.6 56 LCL205-1 theorem 0.2 6 LCL206-1 theorem 0.2 6 LCL207-1 theorem 0.0 6 LCL208-1 theorem 0.2 6 LCL209-1 timeout 300.0 159 LCL210-1 theorem 0.2 4 LCL211-1 theorem 0.2 6 LCL212-1 theorem 1.6 10 LCL213-1 theorem 1.6 10 LCL214-1 theorem 0.3 6 LCL215-1 theorem 0.3 6 LCL216-1 theorem 0.2 6 LCL217-1 theorem 1.3 10 LCL218-1 theorem 66.4 63 LCL219-1 timeout 300.0 159 LCL220-1 timeout 300.0 117 LCL221-1 timeout 300.0 97 LCL222-1 timeout 300.0 80 LCL223-1 timeout 300.0 80 LCL224-1 timeout 300.0 81 LCL225-1 theorem 268.3 81 LCL226-1 theorem 0.0 6 LCL227-1 timeout 300.0 89 LCL228-1 timeout 300.0 89 LCL229-1 timeout 300.0 89 LCL230-1 timeout 300.0 80 LCL231-1 timeout 300.0 81 LCL234-1 theorem 0.7 8 LCL235-1 timeout 300.0 80 LCL236-1 theorem 0.0 6 LCL237-1 theorem 0.7 8 LCL238-1 theorem 0.0 6 LCL239-1 timeout 300.0 159 LCL240-1 timeout 300.0 159 LCL241-1 timeout 300.0 159 LCL242-1 timeout 300.0 81 LCL243-1 timeout 300.0 168 LCL244-1 timeout 300.0 89 LCL245-1 timeout 300.0 81 LCL246-1 timeout 300.0 159 LCL247-1 timeout 300.0 100 LCL248-1 timeout 300.0 81 LCL249-1 timeout 300.0 125 LCL250-1 timeout 300.0 125 LCL251-1 timeout 300.0 81 LCL252-1 timeout 300.0 98 LCL253-1 timeout 300.0 151 LCL254-1 timeout 300.0 168 LCL255-1 timeout 300.0 89 LCL256-1 theorem 0.3 4 LCL257-1 theorem 0.0 6 LCL355-1 theorem 0.0 6 LCL356-1 theorem 44.2 20 LCL357-1 theorem 0.0 4 LCL358-1 theorem 167.7 43 LCL359-1 theorem 0.0 6 LCL360-1 theorem 0.0 6 LCL361-1 theorem 0.0 6 LCL362-1 theorem 0.1 6 LCL363-1 theorem 0.4 6 LCL364-1 theorem 4.9 12 LCL365-1 timeout 300.0 51 LCL366-1 theorem 0.0 6 LCL367-1 theorem 0.6 7 LCL368-1 theorem 261.8 51 LCL369-1 timeout 300.0 51 LCL370-1 timeout 300.0 51 LCL371-1 timeout 300.0 51 LCL372-1 timeout 300.0 51 LCL373-1 timeout 300.0 52 LCL374-1 timeout 300.0 51 LCL375-1 timeout 300.0 51 LCL376-1 timeout 300.0 51 LCL377-1 timeout 300.0 43 LCL378-1 timeout 300.0 43 LCL379-1 theorem 0.8 7 LCL380-1 theorem 0.9 7 LCL381-1 theorem 1.1 7 LCL382-1 timeout 300.0 51 LCL383-1 timeout 300.0 51 LCL384-1 timeout 300.0 43 LCL385-1 timeout 300.0 51 LCL386-1 timeout 300.0 51 LCL387-1 timeout 300.0 51 LCL388-1 timeout 300.0 51 LCL389-1 timeout 300.0 51 LCL390-1 timeout 300.0 51 LCL391-1 timeout 300.0 42 LCL392-1 timeout 300.0 51 LCL393-1 timeout 300.0 51 LCL394-1 timeout 300.0 51 LCL395-1 timeout 300.0 51 LCL396-1 theorem 105.3 26 LCL397-1 theorem 0.0 6 LCL398-1 theorem 0.0 6 LCL399-1 theorem 7.4 12 LCL400-1 timeout 300.0 42 LCL401-1 timeout 300.0 34 LCL402-1 timeout 300.0 43 LCL403-1 timeout 300.0 42 LCL404-1 timeout 300.0 43 LCL405-1 theorem 0.3 6 LCL411-1 non_thm 0.0 6 LCL414-1 theorem 0.0 6 LCL415-1 timeout 5.4 42 LCL416-1 theorem 213.9 26 LCL417-1 timeout 300.0 26 LCL418-1 timeout 300.0 42 LCL419-1 timeout 300.0 42 LCL420-1 timeout 300.0 42 LCL421-1 timeout 300.0 42 LCL422-1 timeout 300.0 42 LCL423-1 timeout 300.0 34 LCL424-1 timeout 300.0 21 LCL425-1 timeout 300.0 34 LCL426-1 timeout 300.0 42 LCL427-1 timeout 300.0 43 LCL428-1 theorem 0.0 6 MGT001-1 theorem 0.0 4 MGT002-1 theorem 0.0 6 MGT003-1 theorem 0.0 4 MGT006-1 theorem 0.0 4 MGT008-1 theorem 0.0 4 MGT009-1 theorem 0.0 6 MGT010-1 theorem 0.0 4 MGT015-1 theorem 0.0 4 MGT017-1 theorem 0.0 6 MGT032-2 theorem 0.0 6 MGT036-3 theorem 0.0 6 MSC005-1 theorem 67.5 237 NLP001-1 theorem 0.0 6 NLP104-1 non_thm 0.0 0 NLP105-1 non_thm 0.0 4 NLP106-1 non_thm 0.0 6 NLP107-1 non_thm 0.0 6 NLP108-1 non_thm 0.0 6 NLP109-1 non_thm 0.0 6 NLP110-1 non_thm 0.0 6 NLP111-1 non_thm 0.0 6 NLP112-1 non_thm 0.0 6 NLP113-1 non_thm 0.0 6 NUM001-1 theorem 0.0 6 NUM002-1 theorem 0.3 6 NUM003-1 theorem 0.3 6 NUM004-1 theorem 0.3 6 NUM017-1 theorem 13.1 63 NUM019-1 theorem 0.0 6 NUM020-1 theorem 0.0 6 NUM023-1 theorem 0.0 6 NUM024-1 theorem 0.1 6 NUM025-1 theorem 0.0 4 NUM026-1 timeout 300.0 63 NUM283-1.005 theorem 0.2 8 NUM284-1.014 theorem 4.2 60 NUM286-1 non_thm 0.0 6 NUM286-2 non_thm 0.0 6 NUM287-1 non_thm 0.0 6 PLA001-1 timeout 300.0 101 PLA003-1 theorem 0.0 6 PLA004-1 theorem 0.1 6 PLA004-2 theorem 0.1 4 PLA005-1 theorem 0.9 13 PLA005-2 theorem 1.0 14 PLA006-1 theorem 0.0 6 PLA007-1 theorem 0.1 6 PLA008-1 timeout 300.0 214 PLA009-1 theorem 0.2 4 PLA009-2 theorem 0.2 6 PLA010-1 timeout 300.0 214 PLA011-1 theorem 0.1 6 PLA011-2 theorem 0.1 6 PLA012-1 timeout 300.0 214 PLA013-1 theorem 0.1 6 PLA014-1 theorem 0.1 6 PLA014-2 theorem 0.1 6 PLA015-1 timeout 300.0 214 PLA016-1 theorem 0.4 10 PLA017-1 theorem 0.0 6 PLA018-1 timeout 300.0 214 PLA019-1 theorem 0.1 6 PLA020-1 theorem 0.0 6 PLA021-1 theorem 12.7 47 PLA022-1 theorem 0.0 6 PLA022-2 theorem 0.0 6 PLA023-1 timeout 300.0 214 PLA029-1 non_thm 0.0 6 PLA030-1 non_thm 0.0 6 PUZ003-1 theorem 0.0 6 PUZ008-1 theorem 0.0 6 PUZ008-2 theorem 0.0 6 PUZ008-3 theorem 0.0 6 PUZ011-1 theorem 0.0 6 PUZ015-3 timeout 267.1 480 PUZ022-1 theorem 0.0 6 PUZ036-1.005 theorem 0.0 6 PUZ037-1 theorem 0.0 6 PUZ037-2 theorem 0.9 10 PUZ037-3 timeout 243.3 471 PUZ038-1 theorem 0.0 6 PUZ039-1 theorem 1.3 21 PUZ040-1 theorem 0.0 6 PUZ041-1 timeout 81.6 471 PUZ042-1 theorem 2.0 27 PUZ046-1 non_thm 0.0 6 PUZ047-1 theorem 0.0 6 PUZ048-1 timeout 81.4 471 PUZ049-1 non_thm 0.6 12 PUZ050-1 timeout 81.7 471 PUZ051-1 timeout 81.6 462 PUZ052-1 timeout 242.9 471 PUZ053-1 timeout 242.9 471 PUZ054-1 non_thm 0.0 6 RNG001-2 timeout 300.0 210 RNG001-3 theorem 0.0 4 RNG001-5 timeout 300.0 214 RNG004-3 timeout 300.0 391 RNG005-2 theorem 0.1 6 RNG006-2 theorem 1.3 8 RNG037-2 theorem 0.1 6 RNG038-2 theorem 0.0 6 RNG039-2 theorem 0.1 6 ROB025-1 timeout 300.0 151 SWV010-1 non_thm 0.0 6 SWV011-1 theorem 0.0 6 SWV012-1 non_thm 0.0 6 SWV013-1 non_thm 0.0 6 SWV014-1 memory 190.9 499 SWV015-1 non_thm 0.0 6 SWV016-1 memory 106.2 499 SWV017-1 non_thm 0.0 6 SWV018-1 memory 94.3 499 SYN003-1.006 theorem 0.0 4 SYN004-1.007 theorem 0.0 6 SYN005-1.010 theorem 0.0 6 SYN010-1.005.005 theorem 0.0 6 SYN033-1 theorem 0.0 6 SYN035-1 theorem 0.0 6 SYN040-1 theorem 0.0 6 SYN041-1 theorem 0.0 0 SYN046-1 theorem 0.0 6 SYN048-1 theorem 0.0 6 SYN049-1 theorem 0.0 4 SYN050-1 theorem 0.0 6 SYN057-1 theorem 0.0 6 SYN058-1 theorem 0.0 6 SYN062-1 theorem 0.0 6 SYN063-2 theorem 0.0 6 SYN064-1 theorem 0.0 6 SYN065-1 theorem 0.0 6 SYN068-1 theorem 0.0 6 SYN079-1 theorem 0.0 6 SYN085-1.010 theorem 0.0 6 SYN086-1.003 non_thm 0.0 6 SYN087-1.003 non_thm 0.0 6 SYN088-1.010 theorem 0.0 6 SYN089-1.002 theorem 0.0 6 SYN090-1.008 theorem 0.0 6 SYN095-1.002 theorem 0.0 6 SYN096-1.008 theorem 0.0 6 SYN101-1.002.002 theorem 0.0 6 SYN102-1.007.007 theorem 0.1 6 SYN103-1 theorem 0.1 6 SYN104-1 theorem 0.1 6 SYN105-1 theorem 0.2 6 SYN106-1 theorem 0.2 6 SYN107-1 theorem 0.5 0 SYN108-1 theorem 0.5 6 SYN109-1 theorem 0.5 6 SYN110-1 theorem 0.6 6 SYN111-1 theorem 0.5 6 SYN112-1 theorem 0.5 6 SYN113-1 theorem 0.5 6 SYN114-1 theorem 0.6 6 SYN115-1 theorem 0.5 6 SYN116-1 theorem 0.5 6 SYN117-1 theorem 0.6 6 SYN118-1 theorem 0.1 6 SYN119-1 theorem 0.1 4 SYN120-1 theorem 0.5 6 SYN121-1 theorem 0.5 6 SYN122-1 theorem 0.5 6 SYN123-1 theorem 0.5 6 SYN124-1 theorem 0.5 6 SYN125-1 theorem 0.6 6 SYN126-1 theorem 0.5 6 SYN127-1 theorem 0.6 4 SYN128-1 theorem 0.5 6 SYN129-1 theorem 0.6 6 SYN130-1 theorem 0.1 6 SYN131-1 theorem 0.1 6 SYN132-1 theorem 0.1 6 SYN133-1 theorem 0.1 6 SYN134-1 theorem 0.2 6 SYN135-1 theorem 0.5 6 SYN136-1 theorem 0.5 0 SYN137-1 theorem 0.6 6 SYN138-1 theorem 0.6 4 SYN139-1 theorem 0.6 6 SYN140-1 theorem 0.6 4 SYN141-1 theorem 0.5 6 SYN142-1 theorem 0.6 6 SYN143-1 theorem 0.6 6 SYN144-1 theorem 0.5 4 SYN145-1 theorem 0.1 6 SYN146-1 theorem 0.1 6 SYN147-1 theorem 0.1 6 SYN148-1 theorem 0.6 6 SYN149-1 theorem 0.5 6 SYN150-1 theorem 0.5 6 SYN151-1 theorem 0.5 6 SYN152-1 theorem 0.2 6 SYN153-1 theorem 0.5 6 SYN154-1 theorem 0.5 6 SYN155-1 theorem 0.5 6 SYN156-1 theorem 0.6 6 SYN157-1 theorem 0.6 6 SYN158-1 theorem 0.6 6 SYN159-1 theorem 0.6 6 SYN160-1 theorem 0.5 6 SYN161-1 theorem 0.6 6 SYN162-1 theorem 0.6 6 SYN163-1 theorem 0.6 4 SYN164-1 theorem 0.1 6 SYN165-1 theorem 0.1 6 SYN166-1 theorem 0.6 6 SYN167-1 theorem 0.5 6 SYN168-1 theorem 0.5 6 SYN169-1 theorem 0.5 6 SYN170-1 theorem 0.5 6 SYN171-1 theorem 0.6 6 SYN172-1 theorem 0.1 6 SYN173-1 theorem 0.6 6 SYN174-1 theorem 0.6 6 SYN175-1 theorem 0.5 6 SYN176-1 theorem 0.5 4 SYN177-1 theorem 0.5 6 SYN178-1 theorem 0.6 6 SYN179-1 theorem 0.6 6 SYN180-1 theorem 0.6 6 SYN181-1 theorem 0.6 6 SYN182-1 theorem 0.5 6 SYN183-1 theorem 0.5 6 SYN184-1 theorem 0.1 6 SYN185-1 theorem 0.1 6 SYN186-1 theorem 0.4 6 SYN187-1 theorem 0.5 6 SYN188-1 theorem 0.5 6 SYN189-1 theorem 0.2 6 SYN190-1 theorem 0.6 4 SYN191-1 theorem 0.6 6 SYN192-1 theorem 0.6 6 SYN193-1 theorem 0.6 6 SYN194-1 theorem 0.5 6 SYN195-1 theorem 0.6 6 SYN196-1 theorem 0.5 6 SYN197-1 theorem 0.1 6 SYN198-1 theorem 0.2 6 SYN199-1 theorem 0.5 6 SYN200-1 theorem 0.2 6 SYN201-1 theorem 0.5 6 SYN202-1 theorem 0.6 6 SYN203-1 theorem 0.5 6 SYN204-1 theorem 0.6 6 SYN205-1 theorem 0.6 6 SYN206-1 theorem 0.6 6 SYN207-1 theorem 0.6 6 SYN208-1 theorem 0.5 6 SYN209-1 theorem 0.5 6 SYN210-1 theorem 0.5 6 SYN211-1 theorem 0.5 6 SYN212-1 theorem 0.5 6 SYN213-1 theorem 0.6 6 SYN214-1 theorem 0.6 6 SYN215-1 theorem 0.6 4 SYN216-1 theorem 0.5 6 SYN217-1 theorem 0.5 4 SYN218-1 theorem 0.5 6 SYN219-1 theorem 0.4 6 SYN220-1 theorem 0.6 6 SYN221-1 theorem 0.5 6 SYN222-1 theorem 0.6 6 SYN223-1 theorem 0.5 6 SYN224-1 theorem 0.5 6 SYN225-1 theorem 0.5 4 SYN226-1 theorem 0.5 6 SYN227-1 theorem 0.5 6 SYN228-1 theorem 0.5 6 SYN229-1 theorem 0.5 4 SYN230-1 theorem 0.5 6 SYN231-1 theorem 0.6 6 SYN232-1 theorem 0.5 6 SYN233-1 theorem 0.6 6 SYN234-1 theorem 0.6 6 SYN235-1 theorem 0.6 6 SYN236-1 theorem 0.5 6 SYN237-1 theorem 0.1 6 SYN238-1 theorem 0.5 6 SYN239-1 theorem 0.1 6 SYN240-1 theorem 0.1 6 SYN241-1 theorem 0.1 6 SYN242-1 theorem 0.1 6 SYN243-1 theorem 0.5 6 SYN244-1 theorem 0.1 6 SYN245-1 theorem 0.1 6 SYN246-1 theorem 0.6 6 SYN247-1 theorem 0.5 4 SYN248-1 theorem 0.6 6 SYN249-1 theorem 0.5 6 SYN250-1 theorem 0.6 6 SYN251-1 theorem 0.5 6 SYN252-1 theorem 0.6 4 SYN253-1 theorem 0.6 6 SYN254-1 theorem 0.6 6 SYN255-1 theorem 0.1 4 SYN256-1 theorem 0.5 6 SYN257-1 theorem 0.1 6 SYN258-1 theorem 0.5 6 SYN259-1 theorem 0.6 6 SYN260-1 theorem 0.5 6 SYN261-1 theorem 0.5 6 SYN262-1 theorem 0.5 4 SYN263-1 theorem 0.6 6 SYN264-1 theorem 0.6 6 SYN265-1 theorem 0.5 6 SYN266-1 theorem 0.6 6 SYN267-1 theorem 0.5 6 SYN268-1 theorem 0.5 6 SYN269-1 theorem 0.6 6 SYN270-1 theorem 0.6 6 SYN271-1 theorem 0.6 6 SYN272-1 theorem 0.6 6 SYN273-1 theorem 0.6 6 SYN274-1 theorem 0.1 6 SYN275-1 theorem 0.1 6 SYN276-1 theorem 0.1 6 SYN277-1 theorem 0.1 6 SYN278-1 theorem 0.1 6 SYN279-1 theorem 0.5 6 SYN280-1 theorem 0.0 6 SYN281-1 theorem 0.1 6 SYN282-1 theorem 0.1 6 SYN283-1 theorem 0.5 0 SYN284-1 theorem 0.6 6 SYN285-1 theorem 0.6 6 SYN286-1 theorem 0.5 6 SYN287-1 theorem 0.1 6 SYN288-1 theorem 0.1 6 SYN289-1 theorem 0.5 6 SYN290-1 theorem 0.5 6 SYN291-1 theorem 0.1 6 SYN292-1 theorem 0.5 6 SYN293-1 theorem 0.6 6 SYN294-1 theorem 0.6 6 SYN295-1 theorem 0.1 6 SYN296-1 theorem 0.6 6 SYN297-1 theorem 0.0 6 SYN298-1 theorem 0.5 6 SYN299-1 theorem 0.5 6 SYN300-1 theorem 0.5 6 SYN301-1 theorem 0.5 6 SYN302-1.003 non_thm 0.0 6 SYN303-1 non_thm 0.0 6 SYN310-1 theorem 0.0 6 SYN311-1 theorem 6.7 56 SYN312-1 theorem 4.7 23 SYN318-1 theorem 0.0 6 SYN322-1 non_thm 0.0 0 SYN329-1 non_thm 0.0 4 SYN333-1 theorem 0.0 6 SYN336-1 theorem 0.0 6 SYN337-1 non_thm 0.0 6 SYN338-1 theorem 0.0 6 SYN339-1 theorem 0.0 6 SYN340-1 theorem 0.0 6 SYN341-1 theorem 0.0 6 SYN342-1 non_thm 0.0 6 SYN346-1 theorem 0.0 6 SYN553-1 theorem 0.1 6 SYN555-1 theorem 0.0 6 SYN556-1 timeout 300.0 170 SYN557-1 theorem 0.1 4 SYN558-1 theorem 0.0 4 SYN559-1 theorem 0.0 6 SYN561-1 theorem 0.1 6 SYN562-1 theorem 0.0 6 SYN563-1 theorem 0.0 6 SYN564-1 theorem 0.0 6 SYN565-1 theorem 0.0 6 SYN566-1 theorem 0.0 6 SYN569-1 theorem 0.0 6 SYN570-1 theorem 0.0 4 SYN572-1 theorem 0.5 8 SYN577-1 theorem 0.5 8 SYN584-1 theorem 0.0 4 SYN588-1 theorem 0.0 6 SYN589-1 theorem 0.0 6 SYN590-1 theorem 0.0 4 SYN596-1 theorem 0.0 4 SYN597-1 theorem 2.0 21 SYN598-1 theorem 5.8 6 SYN599-1 theorem 70.3 12 SYN600-1 timeout 300.0 27 SYN601-1 theorem 3.2 28 SYN602-1 theorem 0.1 6 SYN603-1 theorem 142.2 290 SYN614-1 timeout 300.0 36 SYN615-1 timeout 300.0 171 SYN616-1 timeout 300.0 339 SYN617-1 timeout 300.0 35 SYN618-1 theorem 0.0 6 SYN628-1 memory 245.0 498 SYN629-1 memory 265.1 499 SYN631-1 timeout 300.0 85 SYN632-1 theorem 0.0 6 SYN637-1 theorem 0.0 6 SYN638-1 theorem 0.0 6 SYN639-1 timeout 300.0 28 SYN640-1 timeout 300.0 28 SYN646-1 timeout 300.0 36 SYN647-1 timeout 300.0 36 SYN649-1 theorem 0.0 6 SYN651-1 theorem 0.0 6 SYN652-1 theorem 0.0 6 SYN653-1 theorem 0.0 6 SYN654-1 theorem 0.0 6 SYN655-1 theorem 0.0 6 SYN688-1 theorem 0.0 6 SYN689-1 theorem 0.0 6 SYN691-1 theorem 0.0 6 SYN702-1 theorem 0.0 6 SYN703-1 theorem 0.0 6 SYN704-1 theorem 0.1 6 SYN705-1 theorem 0.0 6 SYN706-1 theorem 0.0 6 SYN707-1 timeout 300.0 21 SYN708-1 timeout 300.0 21 SYN709-1 theorem 0.0 6 SYN711-1 theorem 1.0 6 SYN712-1 theorem 0.0 6 SYN715-1 theorem 0.0 6 SYN716-1 theorem 0.0 6 SYN719-1 theorem 0.0 6 SYN720-1 non_thm 0.5 6 SYN721-1 theorem 0.0 6 SYN727-1 theorem 0.0 6 SYN729-1 theorem 0.0 6 SYN731-1 theorem 0.0 6