-------------------------------------------------------------------------------- Execute format string : ./vampire.7.0 --mode casc-j2 -t 300 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 12.2 36 ANA004-2 timeout 300.0 280 ANA005-2 timeout 300.0 281 COM001-1 theorem 0.0 20 COM002-1 theorem 0.0 20 GEO001-4 timeout 300.0 277 GEO002-4 theorem 0.0 20 GEO079-1 theorem 0.0 20 GRP001-5 theorem 0.0 20 GRP003-1 theorem 0.1 20 GRP003-2 theorem 6.1 36 GRP004-1 theorem 0.0 20 GRP004-2 theorem 0.2 20 GRP005-1 theorem 0.0 20 GRP006-1 theorem 0.0 20 GRP028-1 theorem 0.0 20 GRP028-3 theorem 0.0 20 GRP028-4 theorem 0.0 20 GRP029-2 theorem 5.6 36 GRP031-2 theorem 0.1 20 GRP033-3 theorem 0.0 20 GRP034-4 theorem 0.0 20 GRP041-2 theorem 0.0 20 GRP042-2 theorem 0.0 20 GRP043-2 theorem 0.1 20 GRP044-2 theorem 1.0 20 GRP045-2 theorem 16.1 68 GRP046-2 theorem 0.6 20 GRP047-2 theorem 19.8 84 GRP048-2 theorem 47.9 100 GRP394-2 timeout 300.0 100 KRS004-1 theorem 0.0 20 LAT005-1 timeout 300.0 148 LAT005-2 theorem 282.0 116 LCL001-1 theorem 157.6 100 LCL002-1 theorem 39.4 148 LCL003-1 theorem 38.4 148 LCL004-1 theorem 1.2 20 LCL005-1 theorem 39.7 148 LCL006-1 theorem 5.1 20 LCL007-1 theorem 0.0 4 LCL008-1 theorem 0.0 20 LCL009-1 theorem 0.6 20 LCL010-1 theorem 4.0 20 LCL011-1 theorem 1.1 20 LCL012-1 theorem 21.5 36 LCL013-1 theorem 0.0 20 LCL014-1 theorem 19.9 20 LCL015-1 theorem 20.0 36 LCL016-1 theorem 25.3 36 LCL017-1 theorem 33.9 20 LCL018-1 theorem 21.8 20 LCL019-1 theorem 29.7 20 LCL020-1 theorem 52.8 20 LCL021-1 theorem 43.0 20 LCL022-1 theorem 0.0 20 LCL023-1 theorem 0.3 20 LCL024-1 theorem 18.4 20 LCL025-1 theorem 13.4 36 LCL026-1 theorem 16.2 52 LCL027-1 theorem 0.0 20 LCL028-1 theorem 49.8 52 LCL029-1 theorem 0.2 20 LCL030-1 theorem 68.3 52 LCL031-1 theorem 19.3 36 LCL032-1 timeout 300.0 277 LCL033-1 theorem 0.0 20 LCL034-1 theorem 2.2 20 LCL035-1 theorem 0.0 20 LCL036-1 theorem 0.6 20 LCL037-1 timeout 300.0 277 LCL038-1 theorem 84.9 52 LCL039-1 theorem 1.1 20 LCL040-1 theorem 4.8 36 LCL041-1 theorem 0.0 20 LCL042-1 theorem 0.4 20 LCL043-1 theorem 0.0 20 LCL044-1 theorem 0.0 20 LCL045-1 theorem 0.4 20 LCL046-1 theorem 0.0 20 LCL047-1 theorem 9.4 52 LCL048-1 theorem 10.7 52 LCL049-1 theorem 13.9 52 LCL050-1 theorem 16.1 52 LCL051-1 theorem 57.2 100 LCL052-1 theorem 13.0 52 LCL053-1 theorem 12.7 52 LCL054-1 theorem 169.7 116 LCL055-1 theorem 15.1 52 LCL056-1 theorem 11.3 52 LCL057-1 theorem 12.0 52 LCL058-1 theorem 41.7 100 LCL059-1 theorem 25.4 84 LCL060-1 theorem 42.2 100 LCL061-1 theorem 177.6 100 LCL062-1 theorem 171.8 116 LCL063-1 timeout 300.0 277 LCL064-1 theorem 16.5 52 LCL064-2 theorem 4.7 20 LCL065-1 theorem 0.5 20 LCL066-1 theorem 0.2 20 LCL067-1 theorem 23.7 52 LCL068-1 theorem 15.7 52 LCL069-1 theorem 0.7 20 LCL070-1 theorem 47.3 84 LCL071-1 theorem 26.9 68 LCL072-1 theorem 11.6 52 LCL073-1 timeout 300.0 277 LCL074-1 timeout 300.0 277 LCL075-1 theorem 1.0 36 LCL076-1 theorem 0.0 20 LCL076-2 theorem 0.0 20 LCL076-3 theorem 0.1 20 LCL077-1 theorem 0.0 20 LCL077-2 theorem 0.1 20 LCL078-1 timeout 300.0 197 LCL079-1 theorem 0.0 20 LCL080-1 theorem 7.9 20 LCL080-2 theorem 8.1 36 LCL081-1 theorem 0.0 20 LCL082-1 theorem 0.0 20 LCL083-1 theorem 0.5 20 LCL083-2 theorem 0.1 20 LCL084-2 theorem 89.8 52 LCL084-3 theorem 85.0 36 LCL085-1 theorem 70.9 52 LCL086-1 theorem 0.1 20 LCL087-1 theorem 0.0 20 LCL088-1 theorem 0.1 20 LCL089-1 theorem 2.2 36 LCL090-1 theorem 0.1 20 LCL091-1 theorem 0.1 20 LCL092-1 theorem 0.4 20 LCL093-1 theorem 9.7 52 LCL094-1 theorem 0.3 20 LCL095-1 theorem 0.8 20 LCL096-1 theorem 0.3 20 LCL097-1 theorem 0.1 20 LCL098-1 theorem 0.2 20 LCL099-1 theorem 31.5 36 LCL100-1 theorem 229.2 53 LCL101-1 theorem 3.3 36 LCL102-1 theorem 9.2 36 LCL103-1 theorem 23.9 36 LCL104-1 theorem 2.0 20 LCL105-1 timeout 300.0 228 LCL106-1 theorem 0.0 20 LCL107-1 theorem 0.0 20 LCL108-1 theorem 0.6 20 LCL109-1 timeout 300.0 277 LCL110-1 theorem 0.1 20 LCL111-1 theorem 19.3 52 LCL112-1 theorem 0.2 20 LCL113-1 theorem 4.3 20 LCL114-1 theorem 15.6 52 LCL115-1 theorem 7.4 36 LCL116-1 theorem 28.2 52 LCL117-1 theorem 0.0 20 LCL118-1 theorem 8.2 20 LCL119-1 theorem 21.9 20 LCL120-1 theorem 3.6 20 LCL121-1 theorem 20.0 36 LCL122-1 theorem 225.3 53 LCL123-1 theorem 115.7 52 LCL124-1 theorem 223.5 53 LCL125-1 theorem 119.0 52 LCL126-1 theorem 0.1 20 LCL127-1 theorem 69.1 52 LCL128-1 theorem 34.8 36 LCL129-1 theorem 71.9 52 LCL130-1 theorem 0.0 20 LCL131-1 theorem 7.9 36 LCL166-1 theorem 23.7 20 LCL167-1 theorem 28.9 20 LCL168-1 timeout 300.0 277 LCL169-1 theorem 0.0 20 LCL170-1 theorem 0.0 20 LCL171-1 theorem 0.0 20 LCL172-1 theorem 0.0 20 LCL173-1 theorem 0.0 20 LCL174-1 theorem 0.0 20 LCL175-1 theorem 0.0 4 LCL176-1 theorem 0.0 20 LCL177-1 theorem 0.0 20 LCL178-1 theorem 0.0 20 LCL179-1 timeout 300.0 277 LCL180-1 timeout 300.0 277 LCL181-1 timeout 300.0 277 LCL182-1 theorem 8.6 84 LCL183-1 timeout 300.0 277 LCL184-1 timeout 300.0 277 LCL185-1 theorem 0.0 20 LCL186-1 theorem 0.0 20 LCL187-1 theorem 0.0 20 LCL188-1 theorem 0.0 20 LCL189-1 theorem 0.0 20 LCL190-1 theorem 0.0 20 LCL191-1 theorem 64.6 100 LCL192-1 theorem 0.0 20 LCL193-1 theorem 0.0 20 LCL194-1 theorem 0.4 20 LCL195-1 theorem 33.2 116 LCL196-1 theorem 7.0 68 LCL197-1 theorem 0.0 20 LCL198-1 theorem 9.9 84 LCL199-1 theorem 0.1 20 LCL200-1 theorem 0.0 20 LCL201-1 theorem 2.3 52 LCL202-1 theorem 0.1 20 LCL203-1 theorem 0.0 20 LCL204-1 theorem 2.2 52 LCL205-1 theorem 0.1 20 LCL206-1 theorem 0.1 20 LCL207-1 theorem 0.3 20 LCL208-1 theorem 7.0 68 LCL209-1 timeout 300.0 277 LCL210-1 theorem 7.4 84 LCL211-1 theorem 5.9 68 LCL212-1 theorem 30.8 116 LCL213-1 theorem 2.2 36 LCL214-1 theorem 3.4 52 LCL215-1 theorem 28.3 116 LCL216-1 theorem 2.6 52 LCL217-1 theorem 1.8 36 LCL218-1 theorem 16.3 100 LCL219-1 timeout 300.0 277 LCL220-1 timeout 300.0 277 LCL221-1 theorem 86.6 228 LCL222-1 theorem 85.3 228 LCL223-1 theorem 8.1 84 LCL224-1 theorem 8.2 84 LCL225-1 theorem 10.8 100 LCL226-1 theorem 0.0 20 LCL227-1 theorem 11.6 100 LCL228-1 timeout 300.0 277 LCL229-1 timeout 300.0 277 LCL230-1 theorem 4.2 52 LCL231-1 theorem 4.5 68 LCL234-1 theorem 1.3 36 LCL235-1 timeout 300.0 277 LCL236-1 theorem 0.0 20 LCL237-1 theorem 1.3 36 LCL238-1 theorem 0.2 20 LCL239-1 timeout 300.0 277 LCL240-1 timeout 300.0 277 LCL241-1 timeout 300.0 277 LCL242-1 timeout 300.0 277 LCL243-1 timeout 300.0 277 LCL244-1 timeout 300.0 277 LCL245-1 timeout 300.0 277 LCL246-1 timeout 300.0 277 LCL247-1 timeout 300.0 277 LCL248-1 timeout 300.0 277 LCL249-1 theorem 33.6 116 LCL250-1 theorem 33.6 116 LCL251-1 timeout 300.0 277 LCL252-1 timeout 300.0 277 LCL253-1 theorem 252.8 277 LCL254-1 timeout 300.0 277 LCL255-1 timeout 300.0 277 LCL256-1 theorem 10.6 52 LCL257-1 theorem 0.8 20 LCL355-1 theorem 0.0 20 LCL356-1 theorem 0.0 20 LCL357-1 theorem 0.0 20 LCL358-1 theorem 0.1 20 LCL359-1 theorem 0.1 20 LCL360-1 theorem 0.0 20 LCL361-1 theorem 0.0 20 LCL362-1 theorem 0.0 20 LCL363-1 theorem 0.0 20 LCL364-1 theorem 0.1 20 LCL365-1 theorem 0.1 20 LCL366-1 theorem 0.0 20 LCL367-1 theorem 9.5 52 LCL368-1 theorem 17.5 52 LCL369-1 theorem 56.2 116 LCL370-1 theorem 30.5 100 LCL371-1 theorem 31.0 100 LCL372-1 theorem 31.5 100 LCL373-1 theorem 42.8 100 LCL374-1 theorem 38.2 116 LCL375-1 theorem 173.5 100 LCL376-1 theorem 30.1 100 LCL377-1 timeout 300.0 277 LCL378-1 theorem 13.1 52 LCL379-1 theorem 11.9 52 LCL380-1 theorem 14.0 52 LCL381-1 theorem 15.0 52 LCL382-1 theorem 30.5 100 LCL383-1 theorem 30.3 100 LCL384-1 theorem 10.0 52 LCL385-1 theorem 55.7 100 LCL386-1 theorem 32.3 100 LCL387-1 theorem 33.8 84 LCL388-1 theorem 37.9 100 LCL389-1 theorem 38.5 100 LCL390-1 theorem 42.0 100 LCL391-1 theorem 222.0 116 LCL392-1 theorem 42.6 100 LCL393-1 theorem 170.1 116 LCL394-1 theorem 180.8 100 LCL395-1 theorem 208.6 100 LCL396-1 theorem 13.9 52 LCL397-1 theorem 0.0 20 LCL398-1 theorem 0.0 20 LCL399-1 theorem 3.8 36 LCL400-1 theorem 13.2 52 LCL401-1 theorem 13.9 52 LCL402-1 theorem 13.6 52 LCL403-1 theorem 66.4 100 LCL404-1 theorem 34.8 100 LCL405-1 theorem 12.4 52 LCL411-1 timeout 300.0 277 LCL414-1 theorem 0.0 20 LCL415-1 non_thm 0.0 4 LCL416-1 theorem 0.7 20 LCL417-1 timeout 300.0 277 LCL418-1 timeout 300.0 180 LCL419-1 timeout 300.0 277 LCL420-1 timeout 300.0 277 LCL421-1 timeout 300.0 277 LCL422-1 timeout 300.0 277 LCL423-1 timeout 300.0 100 LCL424-1 timeout 300.0 180 LCL425-1 timeout 300.0 277 LCL426-1 timeout 300.0 277 LCL427-1 timeout 300.0 245 LCL428-1 theorem 0.0 20 MGT001-1 theorem 0.0 20 MGT002-1 theorem 0.0 20 MGT003-1 theorem 0.0 20 MGT006-1 theorem 0.0 20 MGT008-1 theorem 0.0 20 MGT009-1 theorem 0.0 20 MGT010-1 theorem 0.0 20 MGT015-1 theorem 0.0 20 MGT017-1 theorem 0.0 20 MGT032-2 theorem 0.0 20 MGT036-3 theorem 0.0 20 MSC005-1 theorem 0.0 20 NLP001-1 theorem 0.0 20 NLP104-1 non_thm 0.0 20 NLP105-1 non_thm 0.0 20 NLP106-1 non_thm 0.0 20 NLP107-1 non_thm 0.0 20 NLP108-1 non_thm 0.0 20 NLP109-1 non_thm 0.0 20 NLP110-1 non_thm 0.0 20 NLP111-1 non_thm 0.0 20 NLP112-1 non_thm 0.0 20 NLP113-1 non_thm 0.0 20 NUM001-1 theorem 2.3 20 NUM002-1 theorem 3.5 36 NUM003-1 theorem 0.6 20 NUM004-1 theorem 3.8 36 NUM017-1 theorem 62.8 116 NUM019-1 theorem 0.0 20 NUM020-1 theorem 0.0 20 NUM023-1 theorem 0.0 20 NUM024-1 theorem 0.0 20 NUM025-1 theorem 0.0 20 NUM026-1 timeout 300.0 148 NUM283-1.005 theorem 3.3 52 NUM284-1.014 theorem 62.4 86 NUM286-1 non_thm 0.0 4 NUM286-2 timeout 300.0 68 NUM287-1 timeout 73.3 276 PLA001-1 theorem 41.7 164 PLA003-1 theorem 0.0 20 PLA004-1 theorem 0.0 20 PLA004-2 theorem 0.0 20 PLA005-1 theorem 0.0 20 PLA005-2 theorem 0.0 20 PLA006-1 theorem 0.0 20 PLA007-1 theorem 0.0 20 PLA008-1 theorem 0.1 20 PLA009-1 theorem 0.0 20 PLA009-2 theorem 0.0 20 PLA010-1 theorem 0.1 20 PLA011-1 theorem 0.0 20 PLA011-2 theorem 0.0 20 PLA012-1 theorem 0.0 20 PLA013-1 theorem 0.0 20 PLA014-1 theorem 0.0 20 PLA014-2 theorem 0.0 20 PLA015-1 theorem 0.1 20 PLA016-1 theorem 0.0 20 PLA017-1 theorem 0.0 20 PLA018-1 theorem 0.1 20 PLA019-1 theorem 0.0 20 PLA020-1 theorem 0.0 20 PLA021-1 theorem 0.0 20 PLA022-1 theorem 0.0 20 PLA022-2 theorem 0.0 20 PLA023-1 theorem 0.0 20 PLA029-1 non_thm 0.0 20 PLA030-1 non_thm 0.0 20 PUZ003-1 theorem 0.0 20 PUZ008-1 theorem 0.0 20 PUZ008-2 theorem 0.0 20 PUZ008-3 theorem 0.2 20 PUZ011-1 theorem 0.0 20 PUZ015-3 timeout 300.0 276 PUZ022-1 theorem 0.0 20 PUZ036-1.005 theorem 0.0 20 PUZ037-1 theorem 0.0 20 PUZ037-2 theorem 0.1 20 PUZ037-3 theorem 2.0 116 PUZ038-1 theorem 0.1 20 PUZ039-1 theorem 61.2 100 PUZ040-1 theorem 61.1 116 PUZ041-1 timeout 300.0 277 PUZ042-1 theorem 61.1 100 PUZ046-1 timeout 300.0 133 PUZ047-1 theorem 0.0 20 PUZ048-1 timeout 300.0 277 PUZ049-1 timeout 300.0 277 PUZ050-1 theorem 83.3 229 PUZ051-1 timeout 300.0 277 PUZ052-1 timeout 300.0 276 PUZ053-1 timeout 300.0 276 PUZ054-1 non_thm 0.0 20 RNG001-2 theorem 291.4 100 RNG001-3 theorem 70.2 36 RNG001-5 theorem 2.8 20 RNG004-3 theorem 68.7 100 RNG005-2 theorem 24.0 68 RNG006-2 theorem 75.2 100 RNG037-2 theorem 24.1 52 RNG038-2 theorem 0.0 20 RNG039-2 theorem 16.5 52 ROB025-1 timeout 300.0 278 SWV010-1 non_thm 0.0 20 SWV011-1 theorem 0.0 20 SWV012-1 timeout 247.7 276 SWV013-1 non_thm 122.2 164 SWV014-1 theorem 0.0 20 SWV015-1 non_thm 0.1 20 SWV016-1 non_thm 0.0 20 SWV017-1 non_thm 179.4 276 SWV018-1 non_thm 267.8 372 SYN003-1.006 theorem 0.0 20 SYN004-1.007 theorem 0.0 20 SYN005-1.010 theorem 0.0 20 SYN010-1.005.005 theorem 0.0 20 SYN033-1 theorem 0.0 20 SYN035-1 theorem 0.0 20 SYN040-1 theorem 0.0 20 SYN041-1 theorem 0.0 20 SYN046-1 theorem 0.0 20 SYN048-1 theorem 0.0 20 SYN049-1 theorem 0.0 20 SYN050-1 theorem 0.0 20 SYN057-1 theorem 0.0 20 SYN058-1 theorem 0.0 20 SYN062-1 theorem 0.0 4 SYN063-2 theorem 0.0 20 SYN064-1 theorem 0.0 4 SYN065-1 theorem 0.0 20 SYN068-1 theorem 0.0 20 SYN079-1 theorem 0.0 20 SYN085-1.010 theorem 0.0 20 SYN086-1.003 non_thm 0.0 20 SYN087-1.003 non_thm 0.0 20 SYN088-1.010 theorem 0.0 20 SYN089-1.002 theorem 0.0 20 SYN090-1.008 theorem 0.0 20 SYN095-1.002 theorem 0.0 20 SYN096-1.008 theorem 0.0 20 SYN101-1.002.002 theorem 0.0 20 SYN102-1.007.007 theorem 0.1 20 SYN103-1 theorem 0.1 20 SYN104-1 theorem 0.1 20 SYN105-1 theorem 0.1 20 SYN106-1 theorem 0.1 20 SYN107-1 theorem 0.1 20 SYN108-1 theorem 0.1 20 SYN109-1 theorem 0.2 20 SYN110-1 theorem 0.2 20 SYN111-1 theorem 0.2 20 SYN112-1 theorem 0.1 20 SYN113-1 theorem 0.2 20 SYN114-1 theorem 0.1 20 SYN115-1 theorem 0.2 20 SYN116-1 theorem 0.1 20 SYN117-1 theorem 0.2 20 SYN118-1 theorem 0.1 20 SYN119-1 theorem 0.1 20 SYN120-1 theorem 0.1 20 SYN121-1 theorem 0.2 20 SYN122-1 theorem 0.2 20 SYN123-1 theorem 0.2 20 SYN124-1 theorem 0.1 20 SYN125-1 theorem 0.2 20 SYN126-1 theorem 0.1 20 SYN127-1 theorem 0.1 20 SYN128-1 theorem 0.1 20 SYN129-1 theorem 0.1 20 SYN130-1 theorem 0.1 20 SYN131-1 theorem 0.1 20 SYN132-1 theorem 0.1 20 SYN133-1 theorem 0.1 20 SYN134-1 theorem 0.1 20 SYN135-1 theorem 0.1 20 SYN136-1 theorem 0.1 20 SYN137-1 theorem 0.2 20 SYN138-1 theorem 0.2 20 SYN139-1 theorem 0.4 20 SYN140-1 theorem 0.4 20 SYN141-1 theorem 0.2 20 SYN142-1 theorem 0.4 20 SYN143-1 theorem 0.4 20 SYN144-1 theorem 0.2 20 SYN145-1 theorem 0.1 20 SYN146-1 theorem 0.1 20 SYN147-1 theorem 0.1 20 SYN148-1 theorem 0.3 20 SYN149-1 theorem 0.1 20 SYN150-1 theorem 0.1 20 SYN151-1 theorem 0.1 20 SYN152-1 theorem 0.1 20 SYN153-1 theorem 0.1 20 SYN154-1 theorem 0.1 20 SYN155-1 theorem 0.2 20 SYN156-1 theorem 0.3 20 SYN157-1 theorem 0.1 20 SYN158-1 theorem 0.2 20 SYN159-1 theorem 0.4 20 SYN160-1 theorem 0.2 20 SYN161-1 theorem 0.1 20 SYN162-1 theorem 0.1 20 SYN163-1 theorem 0.3 20 SYN164-1 theorem 0.1 20 SYN165-1 theorem 0.1 20 SYN166-1 theorem 0.2 20 SYN167-1 theorem 0.1 20 SYN168-1 theorem 0.1 20 SYN169-1 theorem 0.1 20 SYN170-1 theorem 0.1 20 SYN171-1 theorem 0.4 20 SYN172-1 theorem 0.1 20 SYN173-1 theorem 0.2 20 SYN174-1 theorem 0.2 20 SYN175-1 theorem 0.1 20 SYN176-1 theorem 0.2 20 SYN177-1 theorem 0.2 20 SYN178-1 theorem 0.4 20 SYN179-1 theorem 0.2 20 SYN180-1 theorem 0.4 20 SYN181-1 theorem 0.3 20 SYN182-1 theorem 0.1 20 SYN183-1 theorem 0.1 20 SYN184-1 theorem 0.1 20 SYN185-1 theorem 0.1 20 SYN186-1 theorem 0.1 20 SYN187-1 theorem 0.1 20 SYN188-1 theorem 0.1 20 SYN189-1 theorem 0.1 20 SYN190-1 theorem 0.4 20 SYN191-1 theorem 0.3 20 SYN192-1 theorem 0.2 20 SYN193-1 theorem 0.2 20 SYN194-1 theorem 0.2 20 SYN195-1 theorem 0.2 20 SYN196-1 theorem 0.1 20 SYN197-1 theorem 0.1 20 SYN198-1 theorem 0.1 20 SYN199-1 theorem 0.1 20 SYN200-1 theorem 0.1 20 SYN201-1 theorem 0.1 20 SYN202-1 theorem 0.4 20 SYN203-1 theorem 0.2 20 SYN204-1 theorem 0.4 20 SYN205-1 theorem 0.4 20 SYN206-1 theorem 0.3 20 SYN207-1 theorem 0.3 20 SYN208-1 theorem 0.2 20 SYN209-1 theorem 0.1 20 SYN210-1 theorem 0.1 20 SYN211-1 theorem 0.1 20 SYN212-1 theorem 0.1 20 SYN213-1 theorem 0.2 20 SYN214-1 theorem 0.2 20 SYN215-1 theorem 0.2 20 SYN216-1 theorem 0.2 20 SYN217-1 theorem 0.2 20 SYN218-1 theorem 0.2 20 SYN219-1 theorem 0.2 20 SYN220-1 theorem 0.1 20 SYN221-1 theorem 0.1 20 SYN222-1 theorem 0.1 20 SYN223-1 theorem 0.1 20 SYN224-1 theorem 0.1 20 SYN225-1 theorem 0.2 20 SYN226-1 theorem 0.1 20 SYN227-1 theorem 0.2 20 SYN228-1 theorem 0.2 20 SYN229-1 theorem 0.1 20 SYN230-1 theorem 0.1 20 SYN231-1 theorem 0.1 20 SYN232-1 theorem 0.1 20 SYN233-1 theorem 0.1 20 SYN234-1 theorem 0.2 20 SYN235-1 theorem 0.2 20 SYN236-1 theorem 0.1 20 SYN237-1 theorem 0.1 20 SYN238-1 theorem 0.1 20 SYN239-1 theorem 0.1 20 SYN240-1 theorem 0.1 20 SYN241-1 theorem 0.1 20 SYN242-1 theorem 0.1 20 SYN243-1 theorem 0.1 20 SYN244-1 theorem 0.1 20 SYN245-1 theorem 0.1 20 SYN246-1 theorem 0.1 20 SYN247-1 theorem 0.1 20 SYN248-1 theorem 0.2 20 SYN249-1 theorem 0.2 20 SYN250-1 theorem 0.3 20 SYN251-1 theorem 0.1 20 SYN252-1 theorem 0.4 20 SYN253-1 theorem 0.4 20 SYN254-1 theorem 0.4 20 SYN255-1 theorem 0.1 20 SYN256-1 theorem 0.1 20 SYN257-1 theorem 0.1 20 SYN258-1 theorem 0.1 20 SYN259-1 theorem 0.1 20 SYN260-1 theorem 0.1 20 SYN261-1 theorem 0.1 20 SYN262-1 theorem 0.1 20 SYN263-1 theorem 0.1 20 SYN264-1 theorem 0.2 20 SYN265-1 theorem 0.1 20 SYN266-1 theorem 0.2 20 SYN267-1 theorem 0.1 20 SYN268-1 theorem 0.1 20 SYN269-1 theorem 0.3 20 SYN270-1 theorem 0.3 20 SYN271-1 theorem 0.4 20 SYN272-1 theorem 0.2 20 SYN273-1 theorem 0.2 20 SYN274-1 theorem 0.1 20 SYN275-1 theorem 0.1 20 SYN276-1 theorem 0.1 20 SYN277-1 theorem 0.1 20 SYN278-1 theorem 0.1 20 SYN279-1 theorem 0.2 20 SYN280-1 theorem 0.1 20 SYN281-1 theorem 0.1 20 SYN282-1 theorem 0.1 20 SYN283-1 theorem 0.2 20 SYN284-1 theorem 0.2 20 SYN285-1 theorem 0.3 20 SYN286-1 theorem 0.2 20 SYN287-1 theorem 0.1 20 SYN288-1 theorem 0.1 20 SYN289-1 theorem 0.2 20 SYN290-1 theorem 0.1 20 SYN291-1 theorem 0.1 20 SYN292-1 theorem 0.1 20 SYN293-1 theorem 0.1 20 SYN294-1 theorem 0.1 20 SYN295-1 theorem 0.1 20 SYN296-1 theorem 0.2 20 SYN297-1 theorem 0.1 20 SYN298-1 theorem 0.2 20 SYN299-1 theorem 0.3 20 SYN300-1 theorem 0.3 20 SYN301-1 theorem 0.1 20 SYN302-1.003 non_thm 0.0 20 SYN303-1 non_thm 0.0 4 SYN310-1 theorem 0.0 20 SYN311-1 theorem 0.0 20 SYN312-1 theorem 3.5 36 SYN318-1 theorem 0.0 20 SYN322-1 non_thm 0.0 4 SYN329-1 non_thm 0.0 4 SYN333-1 theorem 0.0 20 SYN336-1 theorem 0.0 20 SYN337-1 non_thm 0.0 4 SYN338-1 theorem 0.0 20 SYN339-1 theorem 0.0 20 SYN340-1 theorem 0.0 20 SYN341-1 theorem 0.0 20 SYN342-1 non_thm 0.0 20 SYN346-1 theorem 0.0 20 SYN553-1 theorem 0.1 20 SYN555-1 theorem 0.2 20 SYN556-1 theorem 0.3 20 SYN557-1 theorem 18.9 36 SYN558-1 theorem 18.5 36 SYN559-1 theorem 0.6 20 SYN561-1 theorem 0.6 20 SYN562-1 theorem 0.0 20 SYN563-1 theorem 6.8 36 SYN564-1 theorem 4.6 36 SYN565-1 theorem 9.4 52 SYN566-1 theorem 8.1 36 SYN569-1 theorem 2.7 20 SYN570-1 theorem 0.1 20 SYN572-1 theorem 64.7 68 SYN577-1 theorem 3.5 36 SYN584-1 theorem 1.8 20 SYN588-1 theorem 0.0 20 SYN589-1 theorem 0.0 20 SYN590-1 theorem 0.1 20 SYN596-1 theorem 0.1 20 SYN597-1 theorem 209.3 164 SYN598-1 theorem 62.7 116 SYN599-1 theorem 209.4 180 SYN600-1 theorem 5.9 36 SYN601-1 theorem 127.2 164 SYN602-1 theorem 7.5 52 SYN603-1 theorem 7.9 52 SYN614-1 theorem 209.5 196 SYN615-1 theorem 209.6 148 SYN616-1 theorem 0.8 20 SYN617-1 theorem 209.7 116 SYN618-1 theorem 0.1 20 SYN628-1 theorem 209.3 132 SYN629-1 theorem 209.2 116 SYN631-1 theorem 12.5 84 SYN632-1 theorem 1.1 36 SYN637-1 theorem 3.5 36 SYN638-1 theorem 3.6 36 SYN639-1 theorem 67.6 116 SYN640-1 theorem 67.6 116 SYN646-1 theorem 0.5 20 SYN647-1 theorem 0.6 20 SYN649-1 theorem 11.3 116 SYN651-1 theorem 12.3 132 SYN652-1 theorem 0.9 20 SYN653-1 theorem 15.0 70 SYN654-1 theorem 13.8 54 SYN655-1 theorem 13.8 54 SYN688-1 theorem 20.2 116 SYN689-1 theorem 20.5 116 SYN691-1 theorem 0.1 20 SYN702-1 theorem 0.1 20 SYN703-1 theorem 0.1 20 SYN704-1 theorem 0.3 20 SYN705-1 theorem 0.1 20 SYN706-1 theorem 0.0 20 SYN707-1 theorem 28.9 148 SYN708-1 theorem 29.1 148 SYN709-1 theorem 2.0 20 SYN711-1 theorem 0.1 20 SYN712-1 theorem 0.2 20 SYN715-1 theorem 0.3 20 SYN716-1 theorem 0.2 20 SYN719-1 theorem 0.1 20 SYN720-1 non_thm 0.5 20 SYN721-1 theorem 0.0 20 SYN727-1 theorem 0.0 20 SYN729-1 theorem 0.0 20 SYN731-1 theorem 0.0 20