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