-------------------------------------------------------------------------------- Execute format string : ./eprover -s --tstp-format -xAuto -tAuto 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 theorem 17.1 77 ANA004-2 memory 174.0 499 ANA005-2 memory 174.7 499 COM001-1 theorem 0.0 4 COM002-1 theorem 0.0 4 GEO001-4 timeout 300.0 69 GEO002-4 theorem 0.0 4 GEO079-1 theorem 0.0 4 GRP001-5 theorem 0.0 4 GRP003-1 theorem 0.0 2 GRP003-2 theorem 2.2 17 GRP004-1 theorem 0.0 2 GRP004-2 theorem 2.1 16 GRP005-1 theorem 0.0 4 GRP006-1 theorem 0.0 2 GRP028-1 theorem 0.0 4 GRP028-3 theorem 0.0 4 GRP028-4 theorem 0.0 4 GRP029-2 theorem 0.7 9 GRP031-2 theorem 0.1 4 GRP033-3 theorem 0.0 4 GRP034-4 theorem 0.0 4 GRP041-2 theorem 0.0 2 GRP042-2 theorem 0.0 4 GRP043-2 theorem 0.0 2 GRP044-2 theorem 0.0 4 GRP045-2 theorem 0.1 4 GRP046-2 theorem 0.0 4 GRP047-2 theorem 2.9 16 GRP048-2 theorem 1.7 14 GRP394-2 memory 81.1 499 KRS004-1 theorem 0.0 4 LAT005-1 theorem 3.4 4 LAT005-2 theorem 2.5 4 LCL001-1 memory 70.6 499 LCL002-1 theorem 17.6 64 LCL003-1 theorem 17.1 64 LCL004-1 theorem 1.0 9 LCL005-1 theorem 55.9 189 LCL006-1 memory 56.5 499 LCL007-1 theorem 0.0 4 LCL008-1 theorem 0.0 2 LCL009-1 theorem 0.0 4 LCL010-1 theorem 0.0 4 LCL011-1 theorem 0.0 4 LCL012-1 theorem 3.2 17 LCL013-1 theorem 0.0 4 LCL014-1 theorem 1.2 9 LCL015-1 theorem 1.1 8 LCL016-1 theorem 0.6 6 LCL017-1 theorem 0.8 6 LCL018-1 theorem 0.5 5 LCL019-1 theorem 1.1 8 LCL020-1 theorem 5.2 30 LCL021-1 theorem 5.0 18 LCL022-1 theorem 0.0 4 LCL023-1 theorem 0.0 4 LCL024-1 theorem 0.5 5 LCL025-1 theorem 0.5 7 LCL026-1 theorem 5.1 43 LCL027-1 theorem 0.0 4 LCL028-1 memory 76.5 499 LCL029-1 theorem 0.3 5 LCL030-1 theorem 5.2 32 LCL031-1 memory 155.7 499 LCL032-1 memory 95.1 499 LCL033-1 theorem 0.0 4 LCL034-1 theorem 1.1 8 LCL035-1 theorem 0.0 4 LCL036-1 theorem 0.7 6 LCL037-1 memory 103.1 499 LCL038-1 theorem 88.1 437 LCL039-1 theorem 0.5 6 LCL040-1 theorem 3.7 27 LCL041-1 theorem 0.1 4 LCL042-1 memory 81.7 499 LCL043-1 theorem 0.0 4 LCL044-1 theorem 0.0 4 LCL045-1 theorem 1.3 13 LCL046-1 theorem 0.0 4 LCL047-1 theorem 8.8 74 LCL048-1 theorem 6.3 56 LCL049-1 theorem 7.3 60 LCL050-1 theorem 5.5 44 LCL051-1 theorem 33.4 225 LCL052-1 theorem 6.7 50 LCL053-1 theorem 7.8 64 LCL054-1 theorem 13.7 94 LCL055-1 theorem 6.6 53 LCL056-1 theorem 6.2 52 LCL057-1 theorem 9.3 76 LCL058-1 theorem 8.2 67 LCL059-1 theorem 5.7 50 LCL060-1 theorem 6.2 49 LCL061-1 theorem 8.0 56 LCL062-1 theorem 11.5 58 LCL063-1 memory 127.8 499 LCL064-1 theorem 1.6 12 LCL064-2 theorem 0.3 5 LCL065-1 theorem 1.6 15 LCL066-1 theorem 0.0 4 LCL067-1 memory 84.0 499 LCL068-1 theorem 0.4 5 LCL069-1 theorem 0.1 3 LCL070-1 theorem 21.4 126 LCL071-1 theorem 1.5 12 LCL072-1 theorem 0.8 7 LCL073-1 memory 225.5 499 LCL074-1 memory 224.2 499 LCL075-1 theorem 0.3 4 LCL076-1 theorem 0.0 4 LCL076-2 theorem 0.0 4 LCL076-3 theorem 0.1 4 LCL077-1 theorem 0.0 4 LCL077-2 theorem 0.0 4 LCL078-1 memory 66.6 499 LCL079-1 theorem 0.0 4 LCL080-1 theorem 1.3 15 LCL080-2 theorem 3.1 22 LCL081-1 theorem 0.0 4 LCL082-1 theorem 0.0 4 LCL083-1 theorem 0.1 4 LCL083-2 theorem 0.4 6 LCL084-2 memory 77.8 499 LCL084-3 memory 70.5 499 LCL085-1 theorem 18.7 79 LCL086-1 theorem 0.0 4 LCL087-1 theorem 0.0 2 LCL088-1 theorem 0.0 2 LCL089-1 theorem 0.1 4 LCL090-1 theorem 0.1 4 LCL091-1 theorem 0.1 4 LCL092-1 theorem 0.1 4 LCL093-1 theorem 1.3 11 LCL094-1 theorem 0.2 4 LCL095-1 theorem 0.4 5 LCL096-1 theorem 0.0 3 LCL097-1 theorem 0.0 4 LCL098-1 theorem 0.0 4 LCL099-1 theorem 2.0 17 LCL100-1 theorem 12.4 79 LCL101-1 theorem 0.0 4 LCL102-1 theorem 0.1 4 LCL103-1 theorem 0.0 4 LCL104-1 theorem 0.0 4 LCL105-1 theorem 1.2 11 LCL106-1 theorem 0.0 4 LCL107-1 theorem 0.1 4 LCL108-1 theorem 0.0 3 LCL109-1 memory 69.8 499 LCL110-1 theorem 0.0 4 LCL111-1 theorem 3.1 28 LCL112-1 theorem 0.0 2 LCL113-1 theorem 0.8 9 LCL114-1 memory 69.3 499 LCL115-1 theorem 0.1 4 LCL116-1 memory 69.3 499 LCL117-1 theorem 0.0 4 LCL118-1 theorem 0.5 6 LCL119-1 theorem 5.0 37 LCL120-1 theorem 0.2 4 LCL121-1 theorem 0.1 4 LCL122-1 theorem 3.1 20 LCL123-1 theorem 0.1 4 LCL124-1 theorem 0.3 5 LCL125-1 theorem 6.8 58 LCL126-1 theorem 0.0 4 LCL127-1 theorem 3.3 20 LCL128-1 theorem 0.4 5 LCL129-1 theorem 10.2 66 LCL130-1 theorem 0.0 4 LCL131-1 theorem 0.1 4 LCL166-1 theorem 0.4 4 LCL167-1 theorem 1.4 10 LCL168-1 memory 251.1 499 LCL169-1 theorem 0.0 4 LCL170-1 theorem 0.0 4 LCL171-1 theorem 0.0 4 LCL172-1 theorem 0.0 2 LCL173-1 theorem 0.0 4 LCL174-1 theorem 0.0 4 LCL175-1 theorem 0.0 4 LCL176-1 theorem 0.0 4 LCL177-1 theorem 0.0 4 LCL178-1 theorem 0.0 4 LCL179-1 timeout 300.0 405 LCL180-1 timeout 300.0 405 LCL181-1 timeout 300.0 246 LCL182-1 theorem 2.6 12 LCL183-1 timeout 300.0 245 LCL184-1 timeout 300.0 405 LCL185-1 theorem 0.0 4 LCL186-1 theorem 0.0 4 LCL187-1 theorem 0.0 4 LCL188-1 theorem 0.0 4 LCL189-1 theorem 0.0 4 LCL190-1 theorem 0.0 4 LCL191-1 theorem 215.8 215 LCL192-1 theorem 4.5 16 LCL193-1 theorem 0.1 4 LCL194-1 theorem 14.1 34 LCL195-1 timeout 300.0 248 LCL196-1 theorem 0.9 8 LCL197-1 theorem 0.1 3 LCL198-1 theorem 0.9 8 LCL199-1 theorem 0.0 4 LCL200-1 theorem 0.0 4 LCL201-1 theorem 0.3 4 LCL202-1 theorem 0.0 4 LCL203-1 theorem 0.0 4 LCL204-1 theorem 0.3 4 LCL205-1 theorem 0.0 3 LCL206-1 theorem 0.0 3 LCL207-1 theorem 0.1 4 LCL208-1 theorem 2.7 12 LCL209-1 timeout 300.0 246 LCL210-1 theorem 2.8 12 LCL211-1 theorem 2.8 12 LCL212-1 theorem 14.3 33 LCL213-1 theorem 12.6 30 LCL214-1 theorem 12.7 30 LCL215-1 theorem 14.3 33 LCL216-1 theorem 12.6 30 LCL217-1 theorem 12.7 28 LCL218-1 theorem 12.6 29 LCL219-1 timeout 300.0 246 LCL220-1 timeout 300.0 245 LCL221-1 timeout 300.0 248 LCL222-1 timeout 300.0 248 LCL223-1 timeout 300.0 248 LCL224-1 theorem 4.3 16 LCL225-1 theorem 4.3 16 LCL226-1 theorem 0.0 4 LCL227-1 theorem 1.5 8 LCL228-1 timeout 300.0 247 LCL229-1 timeout 300.0 254 LCL230-1 theorem 3.1 13 LCL231-1 theorem 3.1 13 LCL234-1 theorem 7.4 22 LCL235-1 timeout 300.0 246 LCL236-1 theorem 0.0 4 LCL237-1 theorem 7.4 22 LCL238-1 theorem 0.1 4 LCL239-1 timeout 300.0 405 LCL240-1 timeout 300.0 405 LCL241-1 timeout 300.0 405 LCL242-1 timeout 300.0 248 LCL243-1 timeout 300.0 245 LCL244-1 timeout 300.0 246 LCL245-1 timeout 300.0 246 LCL246-1 timeout 300.0 405 LCL247-1 timeout 300.0 245 LCL248-1 timeout 300.0 246 LCL249-1 timeout 300.0 245 LCL250-1 theorem 76.3 125 LCL251-1 timeout 300.0 246 LCL252-1 timeout 300.0 246 LCL253-1 timeout 300.0 245 LCL254-1 timeout 300.0 246 LCL255-1 timeout 300.0 249 LCL256-1 theorem 7.3 60 LCL257-1 theorem 0.0 2 LCL355-1 theorem 0.0 4 LCL356-1 theorem 0.0 4 LCL357-1 theorem 0.0 4 LCL358-1 theorem 0.0 4 LCL359-1 theorem 27.3 149 LCL360-1 theorem 0.0 4 LCL361-1 theorem 0.0 4 LCL362-1 theorem 0.0 4 LCL363-1 theorem 0.0 4 LCL364-1 theorem 5.5 46 LCL365-1 theorem 5.1 39 LCL366-1 theorem 0.0 4 LCL367-1 theorem 1.9 19 LCL368-1 theorem 6.4 51 LCL369-1 theorem 22.6 112 LCL370-1 theorem 9.3 73 LCL371-1 theorem 9.0 71 LCL372-1 theorem 7.4 57 LCL373-1 theorem 5.3 42 LCL374-1 theorem 16.4 100 LCL375-1 theorem 18.7 105 LCL376-1 theorem 9.8 68 LCL377-1 theorem 18.8 103 LCL378-1 theorem 6.0 49 LCL379-1 theorem 7.7 63 LCL380-1 theorem 7.9 65 LCL381-1 theorem 8.1 66 LCL382-1 theorem 7.7 63 LCL383-1 theorem 8.3 62 LCL384-1 theorem 5.8 47 LCL385-1 theorem 7.8 64 LCL386-1 theorem 8.0 65 LCL387-1 theorem 7.7 63 LCL388-1 theorem 8.2 67 LCL389-1 theorem 7.8 64 LCL390-1 theorem 5.8 47 LCL391-1 theorem 34.4 252 LCL392-1 theorem 5.9 46 LCL393-1 theorem 17.5 107 LCL394-1 theorem 17.3 92 LCL395-1 theorem 18.5 99 LCL396-1 theorem 7.0 60 LCL397-1 theorem 0.0 4 LCL398-1 theorem 0.0 2 LCL399-1 theorem 0.2 4 LCL400-1 theorem 6.0 49 LCL401-1 theorem 6.4 52 LCL402-1 theorem 6.1 50 LCL403-1 memory 71.4 499 LCL404-1 memory 70.0 499 LCL405-1 theorem 7.6 62 LCL411-1 timeout 300.0 405 LCL414-1 theorem 0.0 4 LCL415-1 non_thm 0.0 4 LCL416-1 theorem 0.2 4 LCL417-1 memory 123.1 499 LCL418-1 memory 105.0 499 LCL419-1 memory 94.2 499 LCL420-1 memory 136.3 499 LCL421-1 memory 101.5 499 LCL422-1 memory 119.1 499 LCL423-1 memory 243.5 499 LCL424-1 memory 186.7 499 LCL425-1 memory 74.5 499 LCL426-1 memory 79.2 499 LCL427-1 memory 125.3 499 LCL428-1 theorem 0.0 4 MGT001-1 theorem 0.0 4 MGT002-1 theorem 0.0 4 MGT003-1 theorem 0.0 2 MGT006-1 theorem 0.0 2 MGT008-1 theorem 0.0 4 MGT009-1 theorem 0.0 4 MGT010-1 theorem 0.0 2 MGT015-1 theorem 0.0 2 MGT017-1 theorem 0.0 4 MGT032-2 theorem 0.0 4 MGT036-3 theorem 0.0 4 MSC005-1 theorem 0.0 4 NLP001-1 theorem 0.0 4 NLP104-1 non_thm 0.0 4 NLP105-1 non_thm 0.0 4 NLP106-1 non_thm 0.0 4 NLP107-1 non_thm 0.0 4 NLP108-1 non_thm 0.0 4 NLP109-1 non_thm 0.0 4 NLP110-1 non_thm 0.0 2 NLP111-1 non_thm 0.0 0 NLP112-1 non_thm 0.0 4 NLP113-1 non_thm 0.0 4 NUM001-1 theorem 0.6 9 NUM002-1 theorem 0.5 8 NUM003-1 theorem 1.3 15 NUM004-1 theorem 0.0 2 NUM017-1 theorem 1.2 10 NUM019-1 theorem 0.0 4 NUM020-1 theorem 0.0 4 NUM023-1 theorem 0.0 4 NUM024-1 theorem 0.0 4 NUM025-1 theorem 0.0 4 NUM026-1 memory 147.8 499 NUM283-1.005 theorem 6.4 7 NUM284-1.014 theorem 0.4 7 NUM286-1 non_thm 0.0 4 NUM286-2 memory 52.4 499 NUM287-1 timeout 300.0 212 PLA001-1 theorem 47.4 12 PLA003-1 theorem 0.0 4 PLA004-1 theorem 0.0 4 PLA004-2 theorem 0.0 4 PLA005-1 theorem 0.0 4 PLA005-2 theorem 0.0 4 PLA006-1 theorem 0.0 4 PLA007-1 theorem 0.0 4 PLA008-1 theorem 0.1 4 PLA009-1 theorem 0.2 4 PLA009-2 theorem 0.2 3 PLA010-1 theorem 0.4 4 PLA011-1 theorem 0.0 4 PLA011-2 theorem 0.0 4 PLA012-1 theorem 0.1 4 PLA013-1 theorem 0.0 4 PLA014-1 theorem 0.0 4 PLA014-2 theorem 0.0 4 PLA015-1 theorem 0.4 4 PLA016-1 theorem 0.0 4 PLA017-1 theorem 0.0 4 PLA018-1 theorem 0.0 3 PLA019-1 theorem 0.0 2 PLA020-1 theorem 0.0 4 PLA021-1 theorem 0.0 4 PLA022-1 theorem 0.0 2 PLA022-2 theorem 0.0 4 PLA023-1 theorem 0.1 4 PLA029-1 non_thm 0.0 4 PLA030-1 non_thm 0.0 2 PUZ003-1 theorem 0.0 4 PUZ008-1 theorem 0.0 4 PUZ008-2 theorem 0.0 4 PUZ008-3 theorem 0.0 4 PUZ011-1 theorem 0.0 4 PUZ015-3 timeout 300.0 91 PUZ022-1 theorem 0.0 4 PUZ036-1.005 theorem 0.0 4 PUZ037-1 theorem 0.0 4 PUZ037-2 theorem 0.7 9 PUZ037-3 theorem 5.9 45 PUZ038-1 theorem 0.0 4 PUZ039-1 theorem 3.5 10 PUZ040-1 theorem 0.0 4 PUZ041-1 timeout 300.0 65 PUZ042-1 theorem 43.4 27 PUZ046-1 non_thm 0.0 4 PUZ047-1 theorem 0.0 4 PUZ048-1 timeout 300.0 65 PUZ049-1 non_thm 2.7 9 PUZ050-1 timeout 300.0 65 PUZ051-1 timeout 300.0 63 PUZ052-1 memory 59.7 499 PUZ053-1 memory 58.6 498 PUZ054-1 non_thm 0.0 4 RNG001-2 memory 65.0 498 RNG001-3 memory 55.8 499 RNG001-5 theorem 13.9 104 RNG004-3 theorem 10.8 41 RNG005-2 theorem 3.0 16 RNG006-2 theorem 10.8 47 RNG037-2 theorem 3.1 17 RNG038-2 theorem 0.0 3 RNG039-2 theorem 0.2 4 ROB025-1 memory 52.7 499 SWV010-1 non_thm 0.0 4 SWV011-1 theorem 0.0 4 SWV012-1 timeout 300.0 125 SWV013-1 non_thm 0.0 4 SWV014-1 theorem 0.0 4 SWV015-1 non_thm 0.0 4 SWV016-1 non_thm 0.1 3 SWV017-1 non_thm 0.0 3 SWV018-1 non_thm 0.1 4 SYN003-1.006 theorem 0.0 2 SYN004-1.007 theorem 0.0 4 SYN005-1.010 theorem 0.0 0 SYN010-1.005.005 theorem 0.0 2 SYN033-1 theorem 0.0 4 SYN035-1 theorem 0.0 4 SYN040-1 theorem 0.0 4 SYN041-1 theorem 0.0 4 SYN046-1 theorem 0.0 2 SYN048-1 theorem 0.0 2 SYN049-1 theorem 0.0 4 SYN050-1 theorem 0.0 4 SYN057-1 theorem 0.0 4 SYN058-1 theorem 0.0 4 SYN062-1 theorem 0.0 4 SYN063-2 theorem 0.0 4 SYN064-1 theorem 0.0 4 SYN065-1 theorem 0.0 4 SYN068-1 theorem 0.0 4 SYN079-1 theorem 0.0 2 SYN085-1.010 theorem 0.0 4 SYN086-1.003 non_thm 0.0 4 SYN087-1.003 non_thm 0.0 4 SYN088-1.010 theorem 0.0 4 SYN089-1.002 theorem 0.0 2 SYN090-1.008 theorem 0.0 2 SYN095-1.002 theorem 0.0 4 SYN096-1.008 theorem 0.0 4 SYN101-1.002.002 theorem 0.0 2 SYN102-1.007.007 theorem 0.0 4 SYN103-1 theorem 0.0 4 SYN104-1 theorem 0.0 4 SYN105-1 theorem 0.0 4 SYN106-1 theorem 0.0 3 SYN107-1 theorem 0.1 4 SYN108-1 theorem 0.1 4 SYN109-1 theorem 0.1 4 SYN110-1 theorem 0.1 3 SYN111-1 theorem 0.1 4 SYN112-1 theorem 0.1 4 SYN113-1 theorem 0.1 4 SYN114-1 theorem 0.1 3 SYN115-1 theorem 0.1 4 SYN116-1 theorem 0.1 4 SYN117-1 theorem 0.1 4 SYN118-1 theorem 0.0 4 SYN119-1 theorem 0.0 4 SYN120-1 theorem 0.0 4 SYN121-1 theorem 0.1 4 SYN122-1 theorem 0.2 3 SYN123-1 theorem 0.1 4 SYN124-1 theorem 0.1 4 SYN125-1 theorem 0.1 4 SYN126-1 theorem 0.1 3 SYN127-1 theorem 0.1 4 SYN128-1 theorem 0.1 4 SYN129-1 theorem 0.1 4 SYN130-1 theorem 0.0 4 SYN131-1 theorem 0.0 4 SYN132-1 theorem 0.0 4 SYN133-1 theorem 0.0 4 SYN134-1 theorem 0.1 4 SYN135-1 theorem 0.1 4 SYN136-1 theorem 0.1 3 SYN137-1 theorem 0.2 4 SYN138-1 theorem 0.2 3 SYN139-1 theorem 0.2 4 SYN140-1 theorem 0.2 4 SYN141-1 theorem 0.1 4 SYN142-1 theorem 0.2 4 SYN143-1 theorem 0.2 4 SYN144-1 theorem 0.1 4 SYN145-1 theorem 0.0 4 SYN146-1 theorem 0.0 4 SYN147-1 theorem 0.0 4 SYN148-1 theorem 0.2 4 SYN149-1 theorem 0.0 4 SYN150-1 theorem 0.1 3 SYN151-1 theorem 0.1 4 SYN152-1 theorem 0.0 4 SYN153-1 theorem 0.1 4 SYN154-1 theorem 0.1 3 SYN155-1 theorem 0.1 4 SYN156-1 theorem 0.2 3 SYN157-1 theorem 0.1 4 SYN158-1 theorem 0.1 3 SYN159-1 theorem 0.3 3 SYN160-1 theorem 0.1 3 SYN161-1 theorem 0.1 4 SYN162-1 theorem 0.1 4 SYN163-1 theorem 0.3 4 SYN164-1 theorem 0.0 4 SYN165-1 theorem 0.0 3 SYN166-1 theorem 0.2 4 SYN167-1 theorem 0.0 4 SYN168-1 theorem 0.1 4 SYN169-1 theorem 0.1 3 SYN170-1 theorem 0.1 4 SYN171-1 theorem 0.2 0 SYN172-1 theorem 0.0 3 SYN173-1 theorem 0.1 4 SYN174-1 theorem 0.1 3 SYN175-1 theorem 0.0 3 SYN176-1 theorem 0.1 4 SYN177-1 theorem 0.1 4 SYN178-1 theorem 0.2 4 SYN179-1 theorem 0.2 4 SYN180-1 theorem 0.2 4 SYN181-1 theorem 0.2 4 SYN182-1 theorem 0.1 4 SYN183-1 theorem 0.1 4 SYN184-1 theorem 0.0 4 SYN185-1 theorem 0.0 4 SYN186-1 theorem 0.1 4 SYN187-1 theorem 0.1 4 SYN188-1 theorem 0.1 4 SYN189-1 theorem 0.1 4 SYN190-1 theorem 0.2 3 SYN191-1 theorem 0.1 4 SYN192-1 theorem 0.1 4 SYN193-1 theorem 0.1 4 SYN194-1 theorem 0.1 4 SYN195-1 theorem 0.1 4 SYN196-1 theorem 0.1 4 SYN197-1 theorem 0.0 3 SYN198-1 theorem 0.1 4 SYN199-1 theorem 0.1 4 SYN200-1 theorem 0.1 4 SYN201-1 theorem 0.1 4 SYN202-1 theorem 0.2 4 SYN203-1 theorem 0.1 3 SYN204-1 theorem 0.2 4 SYN205-1 theorem 0.2 4 SYN206-1 theorem 0.1 4 SYN207-1 theorem 0.1 4 SYN208-1 theorem 0.1 3 SYN209-1 theorem 0.1 4 SYN210-1 theorem 0.1 3 SYN211-1 theorem 0.1 4 SYN212-1 theorem 0.1 3 SYN213-1 theorem 0.1 4 SYN214-1 theorem 0.1 4 SYN215-1 theorem 0.1 4 SYN216-1 theorem 0.1 4 SYN217-1 theorem 0.1 4 SYN218-1 theorem 0.1 4 SYN219-1 theorem 0.1 4 SYN220-1 theorem 0.1 4 SYN221-1 theorem 0.1 4 SYN222-1 theorem 0.1 4 SYN223-1 theorem 0.1 4 SYN224-1 theorem 0.1 4 SYN225-1 theorem 0.1 4 SYN226-1 theorem 0.1 4 SYN227-1 theorem 0.1 4 SYN228-1 theorem 0.1 4 SYN229-1 theorem 0.1 4 SYN230-1 theorem 0.1 4 SYN231-1 theorem 0.1 4 SYN232-1 theorem 0.1 4 SYN233-1 theorem 0.1 4 SYN234-1 theorem 0.1 3 SYN235-1 theorem 0.1 4 SYN236-1 theorem 0.1 3 SYN237-1 theorem 0.0 3 SYN238-1 theorem 0.0 4 SYN239-1 theorem 0.0 4 SYN240-1 theorem 0.0 4 SYN241-1 theorem 0.0 3 SYN242-1 theorem 0.0 4 SYN243-1 theorem 0.1 4 SYN244-1 theorem 0.0 4 SYN245-1 theorem 0.0 3 SYN246-1 theorem 0.1 4 SYN247-1 theorem 0.0 3 SYN248-1 theorem 0.1 4 SYN249-1 theorem 0.1 4 SYN250-1 theorem 0.2 3 SYN251-1 theorem 0.1 3 SYN252-1 theorem 0.2 4 SYN253-1 theorem 0.2 4 SYN254-1 theorem 0.2 4 SYN255-1 theorem 0.1 4 SYN256-1 theorem 0.1 4 SYN257-1 theorem 0.0 4 SYN258-1 theorem 0.0 4 SYN259-1 theorem 0.0 4 SYN260-1 theorem 0.0 4 SYN261-1 theorem 0.0 4 SYN262-1 theorem 0.1 4 SYN263-1 theorem 0.2 4 SYN264-1 theorem 0.1 4 SYN265-1 theorem 0.1 4 SYN266-1 theorem 0.1 3 SYN267-1 theorem 0.1 4 SYN268-1 theorem 0.1 4 SYN269-1 theorem 0.2 4 SYN270-1 theorem 0.1 4 SYN271-1 theorem 0.2 3 SYN272-1 theorem 0.1 4 SYN273-1 theorem 0.1 4 SYN274-1 theorem 0.0 4 SYN275-1 theorem 0.0 4 SYN276-1 theorem 0.0 4 SYN277-1 theorem 0.0 4 SYN278-1 theorem 0.0 3 SYN279-1 theorem 0.1 4 SYN280-1 theorem 0.0 4 SYN281-1 theorem 0.0 4 SYN282-1 theorem 0.0 4 SYN283-1 theorem 0.1 4 SYN284-1 theorem 0.1 4 SYN285-1 theorem 0.1 4 SYN286-1 theorem 0.1 4 SYN287-1 theorem 0.0 4 SYN288-1 theorem 0.0 4 SYN289-1 theorem 0.1 4 SYN290-1 theorem 0.0 4 SYN291-1 theorem 0.0 3 SYN292-1 theorem 0.0 4 SYN293-1 theorem 0.1 3 SYN294-1 theorem 0.1 4 SYN295-1 theorem 0.0 3 SYN296-1 theorem 0.1 4 SYN297-1 theorem 0.0 4 SYN298-1 theorem 0.1 4 SYN299-1 theorem 0.1 4 SYN300-1 theorem 0.1 4 SYN301-1 theorem 0.1 4 SYN302-1.003 non_thm 0.1 4 SYN303-1 non_thm 0.0 4 SYN310-1 theorem 0.0 4 SYN311-1 theorem 0.0 4 SYN312-1 theorem 0.0 4 SYN318-1 theorem 0.0 4 SYN322-1 non_thm 0.0 0 SYN329-1 non_thm 0.0 4 SYN333-1 theorem 0.0 4 SYN336-1 theorem 0.0 4 SYN337-1 non_thm 0.0 4 SYN338-1 theorem 0.0 4 SYN339-1 theorem 0.0 4 SYN340-1 theorem 0.0 2 SYN341-1 theorem 0.0 2 SYN342-1 non_thm 0.0 4 SYN346-1 theorem 0.0 4 SYN553-1 theorem 0.0 4 SYN555-1 theorem 0.0 4 SYN556-1 theorem 5.5 44 SYN557-1 theorem 0.1 4 SYN558-1 theorem 0.0 4 SYN559-1 theorem 0.0 4 SYN561-1 theorem 0.0 4 SYN562-1 theorem 0.0 3 SYN563-1 theorem 1.6 12 SYN564-1 theorem 0.1 4 SYN565-1 theorem 0.1 4 SYN566-1 theorem 0.0 4 SYN569-1 theorem 0.6 6 SYN570-1 theorem 0.0 4 SYN572-1 theorem 2.4 25 SYN577-1 theorem 0.0 4 SYN584-1 theorem 7.9 37 SYN588-1 theorem 0.0 4 SYN589-1 theorem 0.0 4 SYN590-1 theorem 0.2 4 SYN596-1 theorem 0.9 7 SYN597-1 theorem 1.0 5 SYN598-1 theorem 1.0 14 SYN599-1 theorem 17.9 133 SYN600-1 theorem 0.3 6 SYN601-1 theorem 1.6 5 SYN602-1 theorem 3.3 16 SYN603-1 theorem 4.8 23 SYN614-1 theorem 49.1 156 SYN615-1 theorem 9.6 34 SYN616-1 theorem 0.4 4 SYN617-1 memory 103.9 499 SYN618-1 theorem 0.0 4 SYN628-1 theorem 0.5 4 SYN629-1 theorem 0.6 5 SYN631-1 theorem 18.9 211 SYN632-1 theorem 0.1 4 SYN637-1 theorem 0.2 4 SYN638-1 theorem 0.2 4 SYN639-1 theorem 17.4 91 SYN640-1 theorem 17.5 91 SYN646-1 theorem 25.0 138 SYN647-1 theorem 25.0 138 SYN649-1 theorem 0.0 4 SYN651-1 theorem 0.0 4 SYN652-1 theorem 0.2 4 SYN653-1 theorem 31.6 19 SYN654-1 theorem 2.5 6 SYN655-1 theorem 2.0 5 SYN688-1 theorem 0.7 5 SYN689-1 theorem 0.7 5 SYN691-1 theorem 0.2 4 SYN702-1 theorem 0.3 4 SYN703-1 theorem 0.3 4 SYN704-1 theorem 1.0 5 SYN705-1 theorem 0.3 4 SYN706-1 theorem 0.8 4 SYN707-1 theorem 25.2 65 SYN708-1 theorem 25.2 65 SYN709-1 theorem 35.0 101 SYN711-1 theorem 7.0 27 SYN712-1 theorem 0.5 4 SYN715-1 theorem 0.6 4 SYN716-1 theorem 0.7 4 SYN719-1 theorem 11.3 57 SYN720-1 non_thm 0.6 4 SYN721-1 theorem 0.0 4 SYN727-1 theorem 0.0 4 SYN729-1 theorem 0.0 4 SYN731-1 theorem 0.0 4