-------------------------------------------------------------------------------- Execute format string : ./SPASS -PProblem=0 -PGiven=0 -PStatistic=0 -Auto 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 300.0 11 ANA004-2 timeout 300.0 10 ANA005-2 timeout 300.0 10 COM001-1 theorem 0.0 2 COM002-1 theorem 0.0 2 GEO001-4 timeout 300.0 25 GEO002-4 theorem 0.1 2 GEO079-1 theorem 0.0 2 GRP001-5 theorem 0.0 2 GRP003-1 theorem 0.0 2 GRP003-2 theorem 1.4 3 GRP004-1 theorem 0.0 2 GRP004-2 theorem 0.0 2 GRP005-1 theorem 0.0 2 GRP006-1 theorem 0.0 2 GRP028-1 theorem 0.0 2 GRP028-3 theorem 0.0 2 GRP028-4 theorem 0.0 2 GRP029-2 theorem 13.6 4 GRP031-2 theorem 0.1 2 GRP033-3 theorem 0.0 2 GRP034-4 theorem 0.0 2 GRP041-2 theorem 0.0 2 GRP042-2 theorem 0.0 2 GRP043-2 theorem 0.0 2 GRP044-2 theorem 0.0 2 GRP045-2 theorem 13.8 4 GRP046-2 theorem 0.1 2 GRP047-2 theorem 0.1 2 GRP048-2 theorem 61.9 6 GRP394-2 timeout 300.0 10 KRS004-1 theorem 0.0 2 LAT005-1 theorem 2.6 3 LAT005-2 theorem 1.1 3 LCL001-1 timeout 300.0 24 LCL002-1 timeout 300.0 23 LCL003-1 theorem 223.9 20 LCL004-1 theorem 8.4 5 LCL005-1 timeout 300.0 23 LCL006-1 theorem 39.4 7 LCL007-1 theorem 0.0 2 LCL008-1 theorem 0.0 2 LCL009-1 theorem 0.4 3 LCL010-1 theorem 5.9 5 LCL011-1 theorem 16.6 7 LCL012-1 timeout 300.0 12 LCL013-1 theorem 0.0 2 LCL014-1 theorem 18.2 6 LCL015-1 timeout 300.0 20 LCL016-1 timeout 300.0 16 LCL017-1 timeout 300.0 9 LCL018-1 timeout 300.0 8 LCL019-1 timeout 300.0 9 LCL020-1 timeout 300.0 8 LCL021-1 timeout 300.0 7 LCL022-1 theorem 0.0 2 LCL023-1 theorem 0.5 3 LCL024-1 timeout 300.0 9 LCL025-1 timeout 300.0 21 LCL026-1 theorem 235.3 19 LCL027-1 theorem 0.0 2 LCL028-1 timeout 300.0 22 LCL029-1 theorem 4.2 4 LCL030-1 timeout 300.0 16 LCL031-1 timeout 300.0 16 LCL032-1 timeout 300.0 18 LCL033-1 theorem 0.0 2 LCL034-1 theorem 1.2 3 LCL035-1 theorem 0.0 2 LCL036-1 theorem 0.7 3 LCL037-1 timeout 300.0 18 LCL038-1 timeout 300.0 15 LCL039-1 theorem 3.9 6 LCL040-1 timeout 300.0 27 LCL041-1 theorem 0.3 3 LCL042-1 timeout 300.0 25 LCL043-1 theorem 0.1 2 LCL044-1 theorem 1.6 4 LCL045-1 timeout 300.0 25 LCL046-1 theorem 0.0 2 LCL047-1 theorem 1.4 4 LCL048-1 theorem 1.5 4 LCL049-1 theorem 5.8 5 LCL050-1 theorem 6.1 5 LCL051-1 timeout 300.0 29 LCL052-1 theorem 40.1 11 LCL053-1 theorem 40.0 11 LCL054-1 timeout 300.0 29 LCL055-1 theorem 7.9 6 LCL056-1 theorem 7.8 6 LCL057-1 theorem 8.1 6 LCL058-1 timeout 300.0 29 LCL059-1 theorem 73.9 14 LCL060-1 timeout 300.0 29 LCL061-1 timeout 300.0 29 LCL062-1 timeout 300.0 29 LCL063-1 timeout 300.0 28 LCL064-1 theorem 202.8 24 LCL064-2 theorem 3.4 4 LCL065-1 theorem 0.2 3 LCL066-1 theorem 0.1 3 LCL067-1 timeout 300.0 27 LCL068-1 timeout 300.0 26 LCL069-1 theorem 2.6 5 LCL070-1 timeout 300.0 27 LCL071-1 timeout 300.0 27 LCL072-1 theorem 57.8 13 LCL073-1 timeout 300.0 20 LCL074-1 timeout 300.0 20 LCL075-1 theorem 1.0 3 LCL076-1 theorem 0.1 2 LCL076-2 theorem 0.0 2 LCL076-3 theorem 0.3 3 LCL077-1 theorem 0.1 2 LCL077-2 theorem 0.3 3 LCL078-1 timeout 300.0 29 LCL079-1 theorem 0.0 2 LCL080-1 theorem 60.0 8 LCL080-2 theorem 58.4 8 LCL081-1 theorem 0.0 2 LCL082-1 theorem 0.0 2 LCL083-1 theorem 2.2 4 LCL083-2 theorem 2.2 4 LCL084-2 timeout 300.0 13 LCL084-3 timeout 300.0 13 LCL085-1 timeout 300.0 15 LCL086-1 theorem 0.0 2 LCL087-1 theorem 0.0 2 LCL088-1 theorem 0.3 3 LCL089-1 theorem 0.4 3 LCL090-1 theorem 0.2 3 LCL091-1 theorem 0.3 3 LCL092-1 theorem 2.0 4 LCL093-1 timeout 300.0 20 LCL094-1 theorem 36.0 8 LCL095-1 theorem 1.3 3 LCL096-1 theorem 7.8 5 LCL097-1 theorem 0.3 3 LCL098-1 theorem 1.1 5 LCL099-1 timeout 300.0 22 LCL100-1 timeout 300.0 23 LCL101-1 theorem 0.0 2 LCL102-1 theorem 89.1 11 LCL103-1 timeout 300.0 22 LCL104-1 theorem 0.1 2 LCL105-1 timeout 300.0 15 LCL106-1 theorem 0.0 2 LCL107-1 theorem 0.1 3 LCL108-1 theorem 2.2 4 LCL109-1 timeout 300.0 20 LCL110-1 theorem 0.0 2 LCL111-1 theorem 80.8 11 LCL112-1 theorem 0.0 2 LCL113-1 timeout 300.0 20 LCL114-1 timeout 300.0 20 LCL115-1 theorem 1.3 4 LCL116-1 timeout 300.0 20 LCL117-1 theorem 0.0 2 LCL118-1 theorem 1.5 4 LCL119-1 theorem 205.2 8 LCL120-1 theorem 0.0 2 LCL121-1 timeout 300.0 17 LCL122-1 timeout 300.0 17 LCL123-1 timeout 300.0 17 LCL124-1 timeout 300.0 17 LCL125-1 timeout 300.0 12 LCL126-1 theorem 0.0 2 LCL127-1 timeout 300.0 20 LCL128-1 timeout 300.0 18 LCL129-1 timeout 300.0 16 LCL130-1 theorem 0.0 2 LCL131-1 timeout 300.0 16 LCL166-1 timeout 300.0 8 LCL167-1 timeout 300.0 8 LCL168-1 timeout 300.0 7 LCL169-1 theorem 0.0 2 LCL170-1 theorem 0.0 2 LCL171-1 theorem 0.0 2 LCL172-1 theorem 0.0 2 LCL173-1 theorem 0.0 2 LCL174-1 theorem 0.0 2 LCL175-1 theorem 0.0 2 LCL176-1 theorem 0.0 2 LCL177-1 theorem 0.0 2 LCL178-1 theorem 0.0 2 LCL179-1 timeout 300.0 22 LCL180-1 timeout 300.0 22 LCL181-1 timeout 300.0 22 LCL182-1 theorem 56.8 11 LCL183-1 timeout 300.0 22 LCL184-1 timeout 300.0 22 LCL185-1 theorem 0.0 2 LCL186-1 theorem 0.0 2 LCL187-1 theorem 0.1 3 LCL188-1 theorem 0.0 2 LCL189-1 theorem 0.0 2 LCL190-1 theorem 0.0 2 LCL191-1 timeout 300.0 22 LCL192-1 theorem 300.0 22 LCL193-1 theorem 90.8 14 LCL194-1 theorem 37.7 10 LCL195-1 timeout 300.0 22 LCL196-1 theorem 227.7 19 LCL197-1 theorem 0.0 2 LCL198-1 theorem 189.0 18 LCL199-1 theorem 0.1 3 LCL200-1 theorem 0.1 3 LCL201-1 theorem 19.2 8 LCL202-1 theorem 0.1 3 LCL203-1 theorem 0.1 3 LCL204-1 theorem 19.0 8 LCL205-1 theorem 0.1 3 LCL206-1 theorem 0.1 3 LCL207-1 theorem 0.1 3 LCL208-1 theorem 52.3 11 LCL209-1 timeout 300.0 22 LCL210-1 theorem 56.0 11 LCL211-1 theorem 51.7 11 LCL212-1 theorem 65.2 12 LCL213-1 theorem 50.6 11 LCL214-1 theorem 50.7 11 LCL215-1 theorem 65.8 12 LCL216-1 theorem 51.3 11 LCL217-1 theorem 51.1 11 LCL218-1 timeout 300.0 23 LCL219-1 timeout 300.0 22 LCL220-1 timeout 300.0 23 LCL221-1 timeout 300.0 22 LCL222-1 timeout 300.0 22 LCL223-1 timeout 300.0 22 LCL224-1 timeout 300.0 22 LCL225-1 timeout 300.0 22 LCL226-1 theorem 0.0 2 LCL227-1 timeout 300.0 22 LCL228-1 timeout 300.0 22 LCL229-1 timeout 300.0 23 LCL230-1 theorem 21.8 8 LCL231-1 theorem 19.7 8 LCL234-1 timeout 300.0 23 LCL235-1 timeout 300.0 23 LCL236-1 theorem 0.0 2 LCL237-1 timeout 300.0 23 LCL238-1 theorem 0.1 3 LCL239-1 timeout 300.0 22 LCL240-1 timeout 300.0 23 LCL241-1 timeout 300.0 23 LCL242-1 timeout 300.0 22 LCL243-1 timeout 300.0 22 LCL244-1 timeout 300.0 22 LCL245-1 timeout 300.0 22 LCL246-1 timeout 300.0 22 LCL247-1 timeout 300.0 22 LCL248-1 timeout 300.0 22 LCL249-1 timeout 300.0 23 LCL250-1 timeout 300.0 23 LCL251-1 timeout 300.0 22 LCL252-1 timeout 300.0 22 LCL253-1 timeout 300.0 22 LCL254-1 timeout 300.0 22 LCL255-1 timeout 300.0 22 LCL256-1 theorem 8.2 6 LCL257-1 theorem 0.5 3 LCL355-1 theorem 0.0 2 LCL356-1 theorem 0.0 0 LCL357-1 theorem 0.0 2 LCL358-1 theorem 1.9 4 LCL359-1 theorem 0.1 3 LCL360-1 theorem 0.0 2 LCL361-1 theorem 0.0 2 LCL362-1 theorem 0.0 2 LCL363-1 theorem 0.0 2 LCL364-1 theorem 1.4 4 LCL365-1 timeout 300.0 28 LCL366-1 theorem 0.0 4 LCL367-1 theorem 1.4 4 LCL368-1 timeout 300.0 28 LCL369-1 timeout 300.0 28 LCL370-1 timeout 300.0 28 LCL371-1 timeout 300.0 28 LCL372-1 timeout 300.0 28 LCL373-1 timeout 300.0 28 LCL374-1 timeout 300.0 28 LCL375-1 timeout 300.0 28 LCL376-1 timeout 300.0 28 LCL377-1 timeout 300.0 28 LCL378-1 theorem 7.9 6 LCL379-1 theorem 9.7 6 LCL380-1 theorem 8.1 6 LCL381-1 theorem 8.2 6 LCL382-1 timeout 300.0 28 LCL383-1 timeout 300.0 28 LCL384-1 theorem 6.0 5 LCL385-1 timeout 300.0 28 LCL386-1 timeout 300.0 28 LCL387-1 timeout 300.0 28 LCL388-1 timeout 300.0 28 LCL389-1 timeout 300.0 28 LCL390-1 timeout 300.0 28 LCL391-1 timeout 300.0 28 LCL392-1 timeout 300.0 28 LCL393-1 timeout 300.0 27 LCL394-1 timeout 300.0 28 LCL395-1 timeout 300.0 27 LCL396-1 theorem 8.4 6 LCL397-1 theorem 0.0 4 LCL398-1 theorem 0.0 4 LCL399-1 theorem 7.6 6 LCL400-1 theorem 30.0 9 LCL401-1 theorem 36.4 10 LCL402-1 theorem 9.4 6 LCL403-1 timeout 300.0 27 LCL404-1 timeout 300.0 27 LCL405-1 theorem 10.0 6 LCL411-1 timeout 300.0 22 LCL414-1 theorem 0.0 4 LCL415-1 timeout 0.6 4 LCL416-1 theorem 0.5 4 LCL417-1 timeout 300.0 9 LCL418-1 timeout 300.0 37 LCL419-1 timeout 300.0 20 LCL420-1 timeout 300.0 20 LCL421-1 timeout 300.0 20 LCL422-1 timeout 300.0 20 LCL423-1 timeout 300.0 23 LCL424-1 timeout 300.0 20 LCL425-1 timeout 300.0 22 LCL426-1 timeout 300.0 19 LCL427-1 timeout 300.0 70 LCL428-1 theorem 0.0 4 MGT001-1 theorem 0.0 4 MGT002-1 theorem 0.0 4 MGT003-1 theorem 0.0 4 MGT006-1 theorem 0.0 2 MGT008-1 theorem 0.0 2 MGT009-1 theorem 0.0 4 MGT010-1 theorem 0.0 4 MGT015-1 theorem 0.0 4 MGT017-1 theorem 0.0 2 MGT032-2 theorem 0.0 4 MGT036-3 theorem 0.0 2 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 4 NLP111-1 non_thm 0.0 4 NLP112-1 non_thm 0.0 4 NLP113-1 non_thm 0.0 4 NUM001-1 theorem 0.1 4 NUM002-1 theorem 74.9 8 NUM003-1 theorem 38.4 6 NUM004-1 theorem 0.5 4 NUM017-1 timeout 300.0 12 NUM019-1 theorem 0.0 4 NUM020-1 theorem 0.0 4 NUM023-1 theorem 0.0 4 NUM024-1 theorem 0.1 4 NUM025-1 theorem 0.0 4 NUM026-1 timeout 300.0 15 NUM283-1.005 theorem 16.5 5 NUM284-1.014 timeout 300.0 10 NUM286-1 non_thm 0.0 4 NUM286-2 timeout 300.0 12 NUM287-1 timeout 300.0 245 PLA001-1 timeout 300.0 7 PLA003-1 theorem 0.0 4 PLA004-1 theorem 0.0 4 PLA004-2 theorem 0.0 4 PLA005-1 theorem 0.1 4 PLA005-2 theorem 0.1 4 PLA006-1 theorem 0.0 4 PLA007-1 theorem 0.0 4 PLA008-1 theorem 0.8 3 PLA009-1 theorem 0.1 4 PLA009-2 theorem 0.1 4 PLA010-1 theorem 0.7 4 PLA011-1 theorem 0.0 4 PLA011-2 theorem 0.0 4 PLA012-1 theorem 0.2 4 PLA013-1 theorem 0.0 4 PLA014-1 theorem 0.0 2 PLA014-2 theorem 0.0 2 PLA015-1 theorem 0.6 4 PLA016-1 theorem 0.0 4 PLA017-1 theorem 0.0 4 PLA018-1 theorem 0.1 4 PLA019-1 theorem 0.0 4 PLA020-1 theorem 0.0 4 PLA021-1 theorem 0.1 4 PLA022-1 theorem 0.0 4 PLA022-2 theorem 0.0 4 PLA023-1 theorem 0.2 2 PLA029-1 non_thm 0.0 4 PLA030-1 non_thm 0.0 4 PUZ003-1 theorem 0.0 4 PUZ008-1 theorem 0.0 4 PUZ008-2 theorem 0.0 4 PUZ008-3 theorem 0.1 4 PUZ011-1 theorem 0.0 4 PUZ015-3 timeout 300.0 10 PUZ022-1 theorem 0.0 4 PUZ036-1.005 theorem 0.1 4 PUZ037-1 theorem 0.0 4 PUZ037-2 theorem 0.2 4 PUZ037-3 timeout 300.0 30 PUZ038-1 theorem 0.0 4 PUZ039-1 timeout 300.0 15 PUZ040-1 timeout 300.0 15 PUZ041-1 timeout 300.0 17 PUZ042-1 timeout 300.0 15 PUZ046-1 timeout 300.0 15 PUZ047-1 theorem 0.0 4 PUZ048-1 timeout 300.0 15 PUZ049-1 timeout 300.0 17 PUZ050-1 timeout 300.0 15 PUZ051-1 timeout 300.0 17 PUZ052-1 timeout 300.0 30 PUZ053-1 timeout 300.0 30 PUZ054-1 non_thm 0.0 4 RNG001-2 timeout 300.0 9 RNG001-3 timeout 300.0 8 RNG001-5 timeout 300.0 10 RNG004-3 timeout 300.0 11 RNG005-2 theorem 25.9 5 RNG006-2 timeout 300.0 10 RNG037-2 theorem 8.5 4 RNG038-2 theorem 0.0 4 RNG039-2 theorem 2.3 4 ROB025-1 timeout 300.0 8 SWV010-1 non_thm 0.0 4 SWV011-1 theorem 0.0 4 SWV012-1 timeout 300.0 22 SWV013-1 non_thm 0.4 4 SWV014-1 theorem 0.0 4 SWV015-1 non_thm 0.4 3 SWV016-1 non_thm 0.5 4 SWV017-1 non_thm 0.4 4 SWV018-1 non_thm 0.5 3 SYN003-1.006 theorem 0.0 4 SYN004-1.007 theorem 0.0 4 SYN005-1.010 theorem 0.0 4 SYN010-1.005.005 theorem 0.0 4 SYN033-1 theorem 0.0 4 SYN035-1 theorem 0.0 4 SYN040-1 theorem 0.0 0 SYN041-1 theorem 0.0 4 SYN046-1 theorem 0.0 4 SYN048-1 theorem 0.0 4 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 2 SYN079-1 theorem 0.0 4 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 4 SYN090-1.008 theorem 0.0 4 SYN095-1.002 theorem 0.0 4 SYN096-1.008 theorem 0.4 4 SYN101-1.002.002 theorem 0.0 4 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 4 SYN107-1 theorem 0.0 4 SYN108-1 theorem 0.1 4 SYN109-1 theorem 0.1 3 SYN110-1 theorem 0.1 4 SYN111-1 theorem 0.1 4 SYN112-1 theorem 0.1 4 SYN113-1 theorem 0.1 4 SYN114-1 theorem 0.0 4 SYN115-1 theorem 0.1 4 SYN116-1 theorem 0.1 3 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.1 4 SYN123-1 theorem 0.1 4 SYN124-1 theorem 0.0 4 SYN125-1 theorem 0.1 4 SYN126-1 theorem 0.0 4 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.0 4 SYN135-1 theorem 0.1 4 SYN136-1 theorem 0.0 4 SYN137-1 theorem 0.1 4 SYN138-1 theorem 0.2 4 SYN139-1 theorem 0.1 4 SYN140-1 theorem 0.2 3 SYN141-1 theorem 0.1 3 SYN142-1 theorem 0.1 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 2 SYN148-1 theorem 0.1 4 SYN149-1 theorem 0.1 4 SYN150-1 theorem 0.0 4 SYN151-1 theorem 0.1 4 SYN152-1 theorem 0.0 4 SYN153-1 theorem 0.0 2 SYN154-1 theorem 0.0 4 SYN155-1 theorem 0.1 4 SYN156-1 theorem 0.1 4 SYN157-1 theorem 0.1 4 SYN158-1 theorem 0.1 4 SYN159-1 theorem 0.1 4 SYN160-1 theorem 0.1 4 SYN161-1 theorem 0.1 4 SYN162-1 theorem 0.1 3 SYN163-1 theorem 0.1 4 SYN164-1 theorem 0.0 4 SYN165-1 theorem 0.0 4 SYN166-1 theorem 0.1 4 SYN167-1 theorem 0.0 4 SYN168-1 theorem 0.1 4 SYN169-1 theorem 0.0 4 SYN170-1 theorem 0.1 4 SYN171-1 theorem 0.2 3 SYN172-1 theorem 0.0 2 SYN173-1 theorem 0.1 4 SYN174-1 theorem 0.0 2 SYN175-1 theorem 0.1 2 SYN176-1 theorem 0.1 4 SYN177-1 theorem 0.0 4 SYN178-1 theorem 0.1 4 SYN179-1 theorem 0.1 3 SYN180-1 theorem 0.2 3 SYN181-1 theorem 0.1 3 SYN182-1 theorem 0.0 4 SYN183-1 theorem 0.0 4 SYN184-1 theorem 0.0 4 SYN185-1 theorem 0.0 4 SYN186-1 theorem 0.1 4 SYN187-1 theorem 0.0 4 SYN188-1 theorem 0.1 4 SYN189-1 theorem 0.1 4 SYN190-1 theorem 0.2 4 SYN191-1 theorem 0.2 4 SYN192-1 theorem 0.1 4 SYN193-1 theorem 0.1 4 SYN194-1 theorem 0.1 3 SYN195-1 theorem 0.1 3 SYN196-1 theorem 0.1 4 SYN197-1 theorem 0.0 4 SYN198-1 theorem 0.0 4 SYN199-1 theorem 0.0 4 SYN200-1 theorem 0.1 4 SYN201-1 theorem 0.0 4 SYN202-1 theorem 0.1 4 SYN203-1 theorem 0.1 4 SYN204-1 theorem 0.1 4 SYN205-1 theorem 0.1 3 SYN206-1 theorem 0.1 4 SYN207-1 theorem 0.1 4 SYN208-1 theorem 0.0 4 SYN209-1 theorem 0.1 4 SYN210-1 theorem 0.1 3 SYN211-1 theorem 0.1 4 SYN212-1 theorem 0.1 4 SYN213-1 theorem 0.1 4 SYN214-1 theorem 0.1 4 SYN215-1 theorem 0.1 4 SYN216-1 theorem 0.1 3 SYN217-1 theorem 0.0 4 SYN218-1 theorem 0.1 4 SYN219-1 theorem 0.1 4 SYN220-1 theorem 0.0 4 SYN221-1 theorem 0.1 4 SYN222-1 theorem 0.0 4 SYN223-1 theorem 0.1 4 SYN224-1 theorem 0.0 4 SYN225-1 theorem 0.0 4 SYN226-1 theorem 0.1 4 SYN227-1 theorem 0.1 4 SYN228-1 theorem 0.1 4 SYN229-1 theorem 0.0 4 SYN230-1 theorem 0.0 2 SYN231-1 theorem 0.1 4 SYN232-1 theorem 0.0 2 SYN233-1 theorem 0.1 4 SYN234-1 theorem 0.1 3 SYN235-1 theorem 0.1 3 SYN236-1 theorem 0.0 4 SYN237-1 theorem 0.0 4 SYN238-1 theorem 0.0 4 SYN239-1 theorem 0.0 4 SYN240-1 theorem 0.0 4 SYN241-1 theorem 0.0 2 SYN242-1 theorem 0.1 4 SYN243-1 theorem 0.0 2 SYN244-1 theorem 0.0 4 SYN245-1 theorem 0.0 4 SYN246-1 theorem 0.0 2 SYN247-1 theorem 0.0 2 SYN248-1 theorem 0.0 4 SYN249-1 theorem 0.0 2 SYN250-1 theorem 0.2 4 SYN251-1 theorem 0.0 4 SYN252-1 theorem 0.1 4 SYN253-1 theorem 0.1 3 SYN254-1 theorem 0.1 3 SYN255-1 theorem 0.1 4 SYN256-1 theorem 0.0 4 SYN257-1 theorem 0.0 2 SYN258-1 theorem 0.0 4 SYN259-1 theorem 0.0 4 SYN260-1 theorem 0.0 4 SYN261-1 theorem 0.1 2 SYN262-1 theorem 0.0 4 SYN263-1 theorem 0.1 4 SYN264-1 theorem 0.1 4 SYN265-1 theorem 0.1 4 SYN266-1 theorem 0.1 4 SYN267-1 theorem 0.1 2 SYN268-1 theorem 0.0 4 SYN269-1 theorem 0.2 3 SYN270-1 theorem 0.2 4 SYN271-1 theorem 0.2 4 SYN272-1 theorem 0.1 4 SYN273-1 theorem 0.2 4 SYN274-1 theorem 0.0 4 SYN275-1 theorem 0.0 2 SYN276-1 theorem 0.0 4 SYN277-1 theorem 0.0 2 SYN278-1 theorem 0.0 4 SYN279-1 theorem 0.0 4 SYN280-1 theorem 0.0 2 SYN281-1 theorem 0.0 2 SYN282-1 theorem 0.0 4 SYN283-1 theorem 0.1 4 SYN284-1 theorem 0.0 4 SYN285-1 theorem 0.1 4 SYN286-1 theorem 0.0 4 SYN287-1 theorem 0.0 4 SYN288-1 theorem 0.0 2 SYN289-1 theorem 0.1 4 SYN290-1 theorem 0.0 4 SYN291-1 theorem 0.0 4 SYN292-1 theorem 0.0 2 SYN293-1 theorem 0.1 4 SYN294-1 theorem 0.0 2 SYN295-1 theorem 0.0 2 SYN296-1 theorem 0.1 4 SYN297-1 theorem 0.0 4 SYN298-1 theorem 0.1 4 SYN299-1 theorem 0.1 3 SYN300-1 theorem 0.1 4 SYN301-1 theorem 0.1 4 SYN302-1.003 non_thm 0.0 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 2 SYN318-1 theorem 0.0 2 SYN322-1 non_thm 0.0 4 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 0 SYN340-1 theorem 0.0 4 SYN341-1 theorem 0.0 4 SYN342-1 non_thm 0.0 4 SYN346-1 theorem 0.0 4 SYN553-1 theorem 3.3 4 SYN555-1 theorem 0.0 4 SYN556-1 timeout 300.0 7 SYN557-1 theorem 0.0 4 SYN558-1 theorem 1.3 4 SYN559-1 theorem 29.9 4 SYN561-1 theorem 271.4 7 SYN562-1 theorem 0.1 4 SYN563-1 theorem 14.3 4 SYN564-1 timeout 300.0 7 SYN565-1 timeout 300.0 8 SYN566-1 theorem 1.0 4 SYN569-1 theorem 2.4 4 SYN570-1 theorem 14.3 4 SYN572-1 timeout 300.0 8 SYN577-1 timeout 300.0 8 SYN584-1 theorem 114.2 5 SYN588-1 theorem 0.1 4 SYN589-1 theorem 0.1 4 SYN590-1 theorem 0.4 4 SYN596-1 theorem 4.8 3 SYN597-1 theorem 121.7 6 SYN598-1 timeout 300.0 10 SYN599-1 timeout 300.0 10 SYN600-1 theorem 3.6 4 SYN601-1 theorem 140.3 6 SYN602-1 timeout 300.0 8 SYN603-1 timeout 300.0 8 SYN614-1 timeout 300.0 9 SYN615-1 timeout 300.0 8 SYN616-1 timeout 300.0 7 SYN617-1 timeout 300.0 13 SYN618-1 theorem 0.1 4 SYN628-1 timeout 300.0 7 SYN629-1 timeout 300.0 7 SYN631-1 timeout 300.0 11 SYN632-1 theorem 0.5 4 SYN637-1 timeout 300.0 8 SYN638-1 timeout 300.0 8 SYN639-1 theorem 63.6 6 SYN640-1 theorem 63.3 6 SYN646-1 theorem 70.0 6 SYN647-1 theorem 70.0 6 SYN649-1 timeout 300.0 12 SYN651-1 theorem 18.0 5 SYN652-1 theorem 27.1 5 SYN653-1 theorem 9.3 5 SYN654-1 theorem 1.4 4 SYN655-1 theorem 1.4 4 SYN688-1 theorem 75.5 6 SYN689-1 theorem 75.5 6 SYN691-1 theorem 37.6 7 SYN702-1 theorem 4.4 4 SYN703-1 theorem 116.9 10 SYN704-1 theorem 2.7 4 SYN705-1 theorem 4.4 4 SYN706-1 theorem 0.4 4 SYN707-1 theorem 27.4 5 SYN708-1 theorem 27.5 5 SYN709-1 theorem 91.2 7 SYN711-1 theorem 13.3 5 SYN712-1 timeout 300.0 17 SYN715-1 timeout 300.0 17 SYN716-1 theorem 300.0 17 SYN719-1 theorem 15.7 4 SYN720-1 non_thm 0.3 4 SYN721-1 theorem 0.0 4 SYN727-1 theorem 0.0 0 SYN729-1 theorem 0.0 4 SYN731-1 theorem 0.0 0