-------------------------------------------------------------------------------- Execute format string : ./darwin --iterative-deepening TermWeight Problems list file : hne_weight-problems Output file : hne_weight-output Summary file : hne_weight-summary Time limit : 300 s Memory limit : 400 MB -------------------------------------------------------------------------------- Rating Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. [0.00] COM001-1 theorem 0.0 4 1 10 0 7 0 0 0 3 10 13 0 [0.00] COM002-1 theorem 0.0 4 1 30 0 15 0 0 0 3 30 56 0 [0.00] GEO002-4 theorem 0.0 4 1 15 0 3 0 5 0 2 15 41 0 [0.00] GEO079-1 theorem 0.0 4 1 3 0 2 0 0 0 5 3 3 0 [0.00] GRP001-5 theorem 0.0 4 1 8 0 5 0 0 0 4 8 94 0 [0.00] GRP003-1 theorem 0.0 4 1 5 0 3 0 0 0 4 5 29 0 [0.00] GRP003-2 theorem 0.0 4 1 11 0 4 0 0 0 3 11 74 0 [0.00] GRP004-1 theorem 0.0 4 1 5 0 3 0 0 0 4 5 29 0 [0.00] GRP004-2 theorem 0.0 4 1 10 0 4 0 0 0 3 10 49 0 [0.00] GRP005-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 19 0 [0.00] GRP006-1 theorem 0.0 4 1 7 0 6 0 0 0 2 7 20 0 [0.00] GRP028-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 4 0 [0.00] GRP028-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 6 0 [0.00] GRP028-4 theorem 0.0 4 1 3 0 3 0 0 0 2 3 5 0 [0.00] GRP029-2 theorem 0.0 4 1 11 0 5 0 0 0 3 11 102 0 [0.00] GRP031-2 theorem 0.0 4 1 10 0 4 0 0 0 3 10 56 0 [0.00] GRP033-3 theorem 0.0 4 1 8 0 7 0 0 0 2 8 38 0 [0.00] GRP034-4 theorem 0.0 4 1 7 0 6 0 0 0 2 7 21 0 [0.00] GRP041-2 theorem 0.0 4 1 3 0 3 0 0 0 2 3 8 0 [0.00] GRP042-2 theorem 0.0 2 1 7 0 5 0 0 0 4 7 46 0 [0.00] GRP043-2 theorem 0.0 4 1 13 0 6 0 0 0 4 13 96 0 [0.00] GRP044-2 theorem 0.1 4 1 8 0 6 0 0 0 4 8 46 0 [0.00] GRP045-2 theorem 0.1 2 1 29 0 6 0 0 0 4 29 444 0 [0.00] GRP046-2 theorem 0.0 4 1 20 0 5 0 0 0 4 20 285 0 [0.00] GRP047-2 theorem 0.0 4 1 19 0 5 0 0 0 4 19 279 0 [0.00] GRP048-2 theorem 3.8 4 1 145 0 5 0 4 0 5 145 17104 0 [0.00] KRS004-1 theorem 0.0 4 1 2 0 1 0 0 0 2 2 2 0 [0.00] LAT005-2 theorem 0.3 4 1 146 0 21 0 0 0 4 146 5862 0 [0.00] LCL006-1 theorem 0.5 4 1 195 0 3 0 0 0 6 195 12637 0 [0.00] LCL007-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 3 0 [0.00] LCL008-1 theorem 0.0 4 1 8 0 2 0 1 0 8 8 38 0 [0.00] LCL009-1 theorem 0.1 4 1 57 0 2 0 6 0 8 57 2141 0 [0.00] LCL010-1 theorem 0.0 4 1 17 0 2 0 0 0 8 17 236 0 [0.00] LCL011-1 theorem 0.0 4 1 29 0 2 0 0 0 8 29 519 0 [0.00] LCL013-1 theorem 0.0 4 1 3 0 2 0 0 0 10 3 4 0 [0.00] LCL022-1 theorem 0.0 4 1 26 0 2 0 3 0 8 26 445 0 [0.00] LCL023-1 theorem 0.1 4 1 57 0 2 0 6 0 8 57 2141 0 [0.00] LCL025-1 theorem 0.5 4 1 193 0 4 0 16 0 7 193 18432 0 [0.00] LCL027-1 theorem 0.2 4 1 101 0 4 0 16 0 7 101 5765 0 [0.00] LCL029-1 theorem 0.4 4 1 34 0 5 0 0 0 8 34 764 0 [0.00] LCL033-1 theorem 0.0 4 1 11 0 2 0 2 0 9 11 59 0 [0.00] LCL035-1 theorem 0.0 4 1 8 0 2 0 1 0 9 8 37 0 [0.00] LCL041-1 theorem 0.0 4 1 13 0 6 0 0 0 6 13 90 0 [0.00] LCL043-1 theorem 0.0 4 1 11 0 6 0 0 0 6 11 71 0 [0.00] LCL044-1 theorem 0.1 4 1 65 0 6 0 0 0 6 65 1282 0 [0.00] LCL045-1 theorem 35.6 6 1 370 0 6 0 0 0 8 370 44668 0 [0.00] LCL046-1 theorem 0.0 4 1 5 0 4 0 0 0 6 5 11 0 [0.00] LCL047-1 theorem 0.1 2 1 44 0 4 0 5 0 8 44 617 0 [0.00] LCL064-1 theorem 0.6 4 1 212 0 4 0 11 0 7 212 19257 0 [0.00] LCL064-2 theorem 0.3 4 1 137 0 3 0 11 0 7 137 10928 0 [0.00] LCL065-1 theorem 1.0 4 1 298 0 4 0 11 0 7 298 32752 0 [0.00] LCL066-1 theorem 0.2 4 1 123 0 4 0 11 0 7 123 7846 0 [0.00] LCL069-1 theorem 6.1 4 1 40 0 4 0 1 0 9 40 710 0 [0.00] LCL075-1 theorem 0.0 4 1 45 0 2 0 3 0 9 45 1402 0 [0.00] LCL076-1 theorem 0.6 4 1 219 0 4 0 11 0 7 219 20190 0 [0.00] LCL076-2 theorem 0.0 4 1 4 0 4 0 0 0 2 4 5 0 [0.00] LCL076-3 theorem 0.0 2 1 37 0 4 0 3 0 6 37 881 0 [0.00] LCL077-1 theorem 0.6 4 1 214 0 4 0 11 0 7 214 19592 0 [0.00] LCL077-2 theorem 0.0 4 1 29 0 4 0 3 0 6 29 583 0 [0.00] LCL079-1 theorem 0.0 4 1 13 0 6 0 0 0 6 13 72 0 [0.00] LCL081-1 theorem 0.0 4 1 26 0 2 0 11 0 9 26 328 0 [0.00] LCL082-1 theorem 0.0 2 1 31 0 2 0 16 0 9 31 429 0 [0.00] LCL083-1 theorem 0.1 4 1 79 0 2 0 33 0 9 79 2691 0 [0.00] LCL083-2 theorem 0.1 4 1 33 0 3 0 3 0 9 33 804 0 [0.00] LCL086-1 theorem 0.0 4 1 25 0 2 0 7 0 10 25 387 0 [0.00] LCL087-1 theorem 0.0 4 1 12 0 2 0 2 0 10 12 96 0 [0.00] LCL088-1 theorem 0.1 4 1 50 0 2 0 15 0 10 50 1493 0 [0.00] LCL089-1 theorem 0.0 4 1 46 0 2 0 15 0 10 46 1249 0 [0.00] LCL090-1 theorem 0.0 4 1 47 0 2 0 22 0 10 47 735 0 [0.00] LCL091-1 theorem 0.1 4 1 54 0 2 0 24 0 10 54 1049 0 [0.00] LCL094-1 theorem 0.1 4 1 58 0 2 0 15 0 10 58 2038 0 [0.00] LCL096-1 theorem 1.2 4 1 299 0 4 0 1 0 8 299 30658 0 [0.00] LCL097-1 theorem 4.6 5 1 263 0 3 0 1 0 10 263 37777 0 [0.00] LCL098-1 theorem 0.7 4 1 222 0 2 0 0 0 14 222 1417 0 [0.00] LCL101-1 theorem 0.0 4 1 17 0 3 0 2 0 12 17 128 0 [0.00] LCL102-1 theorem 0.3 4 1 131 0 4 0 2 0 8 131 8761 0 [0.00] LCL104-1 theorem 0.0 4 1 13 0 3 0 0 0 8 13 67 0 [0.00] LCL106-1 theorem 0.0 4 1 9 0 3 0 0 0 12 9 15 0 [0.00] LCL107-1 theorem 0.0 4 1 6 0 2 0 0 0 16 6 16 0 [0.00] LCL108-1 theorem 0.2 3 1 76 0 2 0 1 0 16 76 3492 0 [0.00] LCL110-1 theorem 0.3 4 1 93 0 5 0 0 0 7 93 4139 0 [0.00] LCL111-1 theorem 6.1 4 1 69 0 5 0 2 0 8 69 1905 0 [0.00] LCL112-1 theorem 0.3 4 1 96 0 5 0 0 0 7 96 4235 0 [0.00] LCL117-1 theorem 0.0 4 1 4 0 2 0 0 0 8 4 7 0 [0.00] LCL118-1 theorem 0.0 4 1 10 0 2 0 0 0 8 10 50 0 [0.00] LCL120-1 theorem 0.0 4 1 30 0 2 0 0 0 8 30 413 0 [0.00] LCL123-1 theorem 154.6 51 1 1628 0 2 0 5 0 14 1628 1954124 0 [0.00] LCL126-1 theorem 0.0 4 1 8 0 3 0 1 0 8 8 27 0 [0.00] LCL130-1 timeout 300.0 109 [0.00] LCL169-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 [0.00] LCL170-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 6 0 [0.00] LCL171-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 [0.00] LCL172-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 [0.00] LCL173-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 [0.00] LCL174-1 theorem 9.1 10 1 76 0 6 0 0 0 9 76 386 0 [0.00] LCL175-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 6 0 [0.00] LCL176-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 13 0 [0.00] LCL177-1 theorem 0.0 4 1 10 0 6 0 0 0 4 10 18 0 [0.00] LCL178-1 theorem 0.0 4 1 10 0 6 0 0 0 4 10 18 0 [0.00] LCL182-1 theorem 0.8 4 1 363 0 6 0 0 0 8 363 1543 0 [0.00] LCL185-1 theorem 0.0 4 1 12 0 6 0 0 0 5 12 31 0 [0.00] LCL186-1 theorem 0.0 4 1 12 0 6 0 0 0 5 12 31 0 [0.00] LCL187-1 theorem 0.0 4 1 13 0 6 0 0 0 5 13 38 0 [0.00] LCL188-1 theorem 0.0 4 1 10 0 6 0 0 0 4 10 18 0 [0.00] LCL189-1 theorem 0.0 2 1 10 0 6 0 0 0 4 10 18 0 [0.00] LCL190-1 theorem 0.0 4 1 12 0 6 0 0 0 5 12 33 0 [0.00] LCL192-1 theorem 0.1 4 1 118 0 6 0 0 0 7 118 483 0 [0.00] LCL193-1 theorem 0.1 4 1 81 0 6 0 0 0 7 81 338 0 [0.00] LCL194-1 theorem 9.5 10 1 1170 0 6 0 0 0 9 1170 4843 0 [0.00] LCL196-1 theorem 0.3 4 1 756 0 6 0 0 0 7 756 2360 0 [0.00] LCL197-1 theorem 0.0 4 1 78 0 6 0 0 0 6 78 261 0 [0.00] LCL198-1 theorem 0.3 4 1 756 0 6 0 0 0 7 756 2360 0 [0.00] LCL199-1 theorem 0.1 4 1 278 0 6 0 0 0 7 278 996 0 [0.00] LCL200-1 theorem 0.0 4 1 125 0 6 0 0 0 6 125 390 0 [0.00] LCL201-1 theorem 1.1 4 1 1227 0 6 0 0 0 8 1227 4456 0 [0.00] LCL202-1 theorem 0.3 4 1 781 0 6 0 0 0 7 781 2439 0 [0.00] LCL203-1 theorem 0.3 4 1 781 0 6 0 0 0 7 781 2439 0 [0.00] LCL204-1 theorem 1.0 4 1 1227 0 6 0 0 0 8 1227 4456 0 [0.00] LCL205-1 theorem 0.3 4 1 781 0 6 0 0 0 7 781 2439 0 [0.00] LCL206-1 theorem 0.3 4 1 781 0 6 0 0 0 7 781 2439 0 [0.00] LCL207-1 theorem 0.2 4 1 616 0 6 0 0 0 7 616 1948 0 [0.00] LCL208-1 theorem 0.8 4 1 524 0 6 0 0 0 8 524 2103 0 [0.00] LCL210-1 theorem 0.9 4 1 666 0 6 0 0 0 8 666 2586 0 [0.00] LCL211-1 theorem 0.7 4 1 228 0 6 0 0 0 8 228 1059 0 [0.00] LCL212-1 theorem 1.1 4 1 1242 0 6 0 0 0 8 1242 4506 0 [0.00] LCL213-1 theorem 0.9 4 1 946 0 6 0 0 0 8 946 3528 0 [0.00] LCL214-1 theorem 1.0 4 1 946 0 6 0 0 0 8 946 3528 0 [0.00] LCL215-1 theorem 1.1 4 1 1242 0 6 0 0 0 8 1242 4506 0 [0.00] LCL216-1 theorem 0.7 4 1 228 0 6 0 0 0 8 228 1061 0 [0.00] LCL217-1 theorem 0.7 4 1 228 0 6 0 0 0 8 228 1061 0 [0.00] LCL224-1 theorem 171.9 50 1 11264 0 6 0 0 0 10 11264 42332 0 [0.00] LCL226-1 theorem 9.1 10 1 76 0 6 0 0 0 9 76 386 0 [0.00] LCL236-1 theorem 0.0 4 1 10 0 6 0 0 0 4 10 18 0 [0.00] LCL238-1 theorem 0.1 4 1 180 0 6 0 0 0 7 180 700 0 [0.00] LCL257-1 theorem 0.1 4 1 61 0 2 0 6 0 8 61 2557 0 [0.00] LCL355-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 4 0 [0.00] LCL356-1 theorem 0.1 4 1 10 0 4 0 0 0 8 10 46 0 [0.00] LCL357-1 theorem 0.1 4 1 10 0 4 0 0 0 8 10 46 0 [0.00] LCL358-1 theorem 0.1 4 1 14 0 4 0 0 0 8 14 80 0 [0.00] LCL359-1 theorem 0.1 4 1 14 0 4 0 0 0 8 14 71 0 [0.00] LCL360-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 4 0 [0.00] LCL361-1 theorem 0.1 4 1 13 0 4 0 0 0 8 13 64 0 [0.00] LCL362-1 theorem 0.0 4 1 20 0 4 0 1 0 7 20 129 0 [0.00] LCL363-1 theorem 0.0 4 1 20 0 4 0 1 0 7 20 129 0 [0.00] LCL364-1 theorem 0.2 4 1 89 0 4 0 12 0 8 89 2922 0 [0.00] LCL365-1 theorem 0.3 3 1 129 0 4 0 16 0 8 129 5506 0 [0.00] LCL366-1 theorem 0.0 2 1 8 0 4 0 0 0 6 8 26 0 [0.00] LCL367-1 theorem 0.1 4 1 44 0 4 0 5 0 8 44 617 0 [0.00] LCL384-1 theorem 0.4 4 1 163 0 4 0 17 0 8 163 8541 0 [0.00] LCL397-1 theorem 0.0 4 1 18 0 4 0 1 0 7 18 85 0 [0.00] LCL398-1 theorem 0.0 4 1 6 0 4 0 0 0 6 6 14 0 [0.00] LCL399-1 theorem 0.2 4 1 117 0 4 0 15 0 8 117 4695 0 [0.00] LCL414-1 theorem 0.0 4 1 5 0 4 0 0 0 4 5 7 0 [0.00] LCL428-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 5 0 [0.00] MGT001-1 theorem 0.0 4 1 19 0 10 0 0 0 7 19 22 0 [0.00] MGT002-1 theorem 0.0 4 1 12 0 7 0 0 0 7 12 17 0 [0.00] MGT003-1 theorem 0.0 4 1 12 0 7 0 0 0 7 12 17 0 [0.00] MGT006-1 theorem 0.0 4 1 13 0 8 2 0 0 7 13 13 0 [0.00] MGT008-1 theorem 0.0 2 1 15 0 12 0 0 0 7 15 16 0 [0.00] MGT009-1 theorem 0.0 4 1 15 0 12 0 0 0 7 15 16 0 [0.00] MGT010-1 theorem 0.0 4 1 18 0 13 2 0 0 7 18 18 0 [0.00] MGT015-1 theorem 0.0 4 1 17 0 13 0 0 0 7 17 18 0 [0.00] MGT017-1 theorem 0.0 4 1 17 0 13 0 0 0 7 17 18 0 [0.00] MGT032-2 theorem 0.0 4 1 7 0 2 0 0 0 11 7 7 0 [0.00] MGT036-3 theorem 0.0 4 1 6 0 4 0 0 0 5 6 7 0 [0.00] MSC005-1 theorem 0.0 4 1 50 0 3 0 0 0 9 50 103 0 [0.00] NLP001-1 theorem 0.0 2 2 28 1 48 5 0 0 3 19 32 30 [0.00] NLP104-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 [0.00] NLP105-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 [0.00] NLP106-1 non_thm 0.0 4 0 14 0 2 0 0 0 3 14 14 0 [0.00] NLP107-1 non_thm 0.0 4 0 26 0 3 0 0 0 3 26 26 0 [0.00] NLP108-1 non_thm 0.0 2 0 49 0 10 0 0 0 3 49 51 0 [0.00] NLP109-1 non_thm 0.0 2 0 26 0 3 0 0 0 3 26 26 0 [0.00] NLP110-1 non_thm 0.0 4 0 37 0 9 0 0 0 3 37 39 0 [0.00] NLP111-1 non_thm 0.0 4 0 49 0 10 0 0 0 3 49 51 0 [0.00] NLP112-1 non_thm 0.0 4 0 49 0 10 0 0 0 3 49 51 0 [0.00] NLP113-1 non_thm 0.0 2 0 13 0 2 0 0 0 3 13 13 0 [0.00] NUM001-1 theorem 0.0 4 1 29 0 8 0 0 0 5 29 521 0 [0.00] NUM002-1 theorem 0.0 4 1 23 0 8 0 0 0 5 23 353 0 [0.00] NUM003-1 theorem 0.0 2 1 31 0 8 0 0 0 5 31 572 0 [0.00] NUM004-1 theorem 0.0 4 1 21 0 8 0 0 0 5 21 289 0 [0.00] NUM019-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 10 0 [0.00] NUM020-1 theorem 0.0 4 1 13 0 8 0 0 0 5 13 54 0 [0.00] NUM023-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 11 0 [0.00] NUM024-1 timeout 300.0 18 [0.00] NUM025-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 12 0 [0.00] PLA001-1 theorem 2.1 6 1 3335 0 12 0 0 0 24 3335 4775 0 [0.00] PLA003-1 theorem 0.0 4 1 8 0 4 2 3 0 11 8 15 0 [0.00] PLA006-1 theorem 0.0 4 1 64 0 20 0 0 0 7 64 117 0 [0.00] PLA017-1 theorem 0.0 4 1 93 0 20 0 0 0 7 93 117 0 [0.00] PLA020-1 theorem 0.0 4 1 18 0 18 0 0 0 2 18 20 0 [0.00] PLA022-1 theorem 27.9 6 1 3153 0 20 0 0 0 12 3153 5472 0 [0.00] PLA022-2 theorem 28.7 7 1 3153 0 20 0 0 0 12 3153 5472 0 [0.00] PLA029-1 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 [0.00] PLA030-1 timeout 300.0 18 [0.00] PUZ003-1 theorem 0.0 4 1 14 0 6 0 0 0 3 14 27 0 [0.00] PUZ008-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 6 0 [0.00] PUZ008-3 theorem 0.0 4 1 27 0 4 0 0 0 18 27 47 0 [0.00] PUZ011-1 theorem 0.0 4 1 18 0 18 0 0 0 2 18 26 0 [0.00] PUZ022-1 theorem 0.0 4 1 34 0 31 0 0 0 3 34 53 0 [0.00] PUZ038-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 2 0 [0.00] PUZ047-1 theorem 0.0 4 1 36 0 2 0 0 0 12 36 73 0 [0.00] PUZ054-1 non_thm 0.0 4 0 75 0 2 0 0 0 21 75 180 0 [0.00] RNG001-3 theorem 0.5 4 1 15 0 4 0 0 0 6 15 357 0 [0.00] RNG001-5 theorem 32.7 4 1 109 0 8 0 17 0 5 109 31518 0 [0.00] RNG005-2 theorem 0.0 4 1 11 0 11 0 0 0 2 11 36 0 [0.00] RNG006-2 timeout 300.0 8 [0.00] RNG037-2 theorem 0.0 4 1 15 0 9 0 0 0 3 15 194 0 [0.00] RNG038-2 theorem 1.2 4 1 69 0 9 0 0 0 4 69 14251 0 [0.00] RNG039-2 theorem 1.4 4 1 64 0 50 0 2 0 3 64 5095 0 [0.00] SWV010-1 non_thm 0.0 4 0 8 0 5 0 0 0 24 8 8 0 [0.00] SWV011-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 2 0 [0.00] SYN003-1.006 theorem 0.0 4 1 18 0 22 18 0 0 2 18 23 0 [0.00] SYN004-1.007 theorem 0.0 4 1 14 0 14 14 0 0 2 14 14 0 [0.00] SYN005-1.010 theorem 0.0 4 1 10 0 10 0 0 0 2 10 10 0 [0.00] SYN010-1.005.005 theorem 0.0 4 1 26 0 26 26 0 0 2 26 27 0 [0.00] SYN033-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 4 0 [0.00] SYN035-1 theorem 0.0 2 1 2 0 2 6 0 0 2 2 2 0 [0.00] SYN040-1 theorem 0.0 2 1 2 0 3 2 0 0 2 2 3 0 [0.00] SYN041-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 4 0 [0.00] SYN046-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 3 0 [0.00] SYN048-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 2 0 [0.00] SYN049-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 3 0 [0.00] SYN050-1 theorem 0.0 4 1 3 0 3 1 0 0 2 3 4 0 [0.00] SYN057-1 theorem 0.0 4 1 7 0 4 0 0 0 2 7 8 0 [0.00] SYN058-1 theorem 0.0 4 1 5 0 8 1 0 0 2 5 6 0 [0.00] SYN062-1 theorem 0.0 2 1 5 0 3 0 0 0 2 5 6 0 [0.00] SYN063-2 theorem 0.0 4 1 2 0 2 2 0 0 2 2 3 0 [0.00] SYN064-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 2 0 [0.00] SYN065-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 3 0 [0.00] SYN068-1 theorem 0.0 4 1 6 0 1 0 0 0 4 6 7 0 [0.00] SYN079-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 3 0 [0.00] SYN085-1.010 theorem 0.0 4 1 11 0 11 11 0 0 2 11 12 0 [0.00] SYN086-1.003 non_thm 0.0 4 0 1 0 1 1 0 0 2 1 1 0 [0.00] SYN087-1.003 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 [0.00] SYN088-1.010 theorem 0.0 4 1 21 0 21 0 0 0 2 21 21 0 [0.00] SYN089-1.002 theorem 0.0 4 1 5 0 9 5 0 0 2 5 9 0 [0.00] SYN090-1.008 theorem 0.0 2 1 34 0 64 58 0 0 2 34 62 0 [0.00] SYN095-1.002 theorem 0.0 4 1 4 0 6 1 0 0 2 4 7 0 [0.00] SYN096-1.008 theorem 0.0 4 1 34 0 4 0 0 0 2 34 64 0 [0.00] SYN101-1.002.002 theorem 0.0 4 1 17 0 5 0 0 0 3 17 29 0 [0.00] SYN102-1.007.007 theorem 0.6 4 1 3854 0 14 2 0 0 8 3854 7182 0 [0.00] SYN103-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN104-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN105-1 theorem 0.0 4 1 22 0 29 31 0 0 2 22 64 0 [0.00] SYN106-1 theorem 0.0 4 1 17 0 24 30 0 0 2 17 60 0 [0.00] SYN107-1 theorem 0.0 4 1 47 0 97 55 1 0 2 47 118 0 [0.00] SYN108-1 theorem 0.0 4 1 46 0 97 54 1 0 2 46 117 0 [0.00] SYN109-1 theorem 0.1 4 1 78 0 125 82 3 0 3 78 266 0 [0.00] SYN110-1 theorem 0.1 4 1 134 0 125 86 24 0 4 134 1159 0 [0.00] SYN111-1 theorem 0.2 4 1 138 0 126 86 24 0 4 138 1213 0 [0.00] SYN112-1 theorem 0.0 4 1 48 0 96 57 1 0 2 48 120 0 [0.00] SYN113-1 theorem 0.0 2 1 56 0 123 78 2 0 2 56 149 0 [0.00] SYN114-1 theorem 0.0 4 1 56 0 123 78 2 0 2 56 148 0 [0.00] SYN115-1 theorem 0.1 4 1 194 0 226 146 24 0 3 194 1059 0 [0.00] SYN116-1 theorem 0.0 4 1 92 0 218 126 3 0 2 92 241 0 [0.00] SYN117-1 theorem 0.0 4 1 92 0 217 125 3 0 2 92 241 0 [0.00] SYN118-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN119-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN120-1 theorem 0.0 2 1 17 0 25 30 0 0 2 17 59 0 [0.00] SYN121-1 theorem 0.0 4 1 66 0 157 96 3 0 2 66 187 0 [0.00] SYN122-1 theorem 0.0 4 1 66 0 156 96 3 0 2 66 187 0 [0.00] SYN123-1 theorem 0.0 4 1 41 0 57 41 0 0 2 41 84 0 [0.00] SYN124-1 theorem 0.0 4 1 60 0 128 85 3 0 2 60 154 0 [0.00] SYN125-1 theorem 0.2 4 1 164 0 155 97 37 0 4 164 1734 0 [0.00] SYN126-1 theorem 0.0 4 1 77 0 192 114 3 0 2 77 210 0 [0.00] SYN127-1 theorem 0.1 4 1 77 0 192 114 3 0 2 77 210 0 [0.00] SYN128-1 theorem 0.0 4 1 88 0 217 125 3 0 2 88 233 0 [0.00] SYN129-1 theorem 0.0 4 1 88 0 217 125 3 0 2 88 233 0 [0.00] SYN130-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN131-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN132-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 54 0 [0.00] SYN133-1 theorem 0.0 4 1 5 0 4 9 0 0 2 5 39 0 [0.00] SYN134-1 theorem 0.0 4 1 39 0 40 41 0 0 2 39 73 0 [0.00] SYN135-1 theorem 0.0 4 1 60 0 129 85 3 0 2 60 151 0 [0.00] SYN136-1 theorem 0.0 4 1 60 0 128 85 3 0 2 60 151 0 [0.00] SYN137-1 theorem 0.0 4 1 81 0 207 117 3 0 2 81 213 0 [0.00] SYN138-1 theorem 0.2 3 1 229 0 165 116 59 0 4 229 2396 0 [0.00] SYN139-1 theorem 0.3 4 1 512 0 237 156 163 0 4 512 5041 0 [0.00] SYN140-1 theorem 0.3 3 1 512 0 237 156 163 0 4 512 5041 0 [0.00] SYN141-1 theorem 0.1 4 1 246 0 247 150 33 0 3 246 1110 0 [0.00] SYN142-1 theorem 0.3 4 1 594 0 259 163 189 0 4 594 5525 0 [0.00] SYN143-1 theorem 0.3 3 1 594 0 259 163 189 0 4 594 5525 0 [0.00] SYN144-1 theorem 0.1 4 1 249 0 249 150 33 0 3 249 1139 0 [0.00] SYN145-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN146-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 39 0 [0.00] SYN147-1 theorem 0.0 4 1 6 0 8 13 0 0 2 6 42 0 [0.00] SYN148-1 theorem 0.1 3 1 52 0 59 44 1 0 3 52 152 0 [0.00] SYN149-1 theorem 0.0 4 1 12 0 20 30 0 0 2 12 54 0 [0.00] SYN150-1 theorem 0.0 4 1 44 0 77 49 1 0 2 44 111 0 [0.00] SYN151-1 theorem 0.0 4 1 45 0 95 52 1 0 2 45 113 0 [0.00] SYN152-1 theorem 0.0 4 1 45 0 96 53 1 0 2 45 113 0 [0.00] SYN153-1 theorem 0.0 4 1 61 0 131 85 3 0 2 61 159 0 [0.00] SYN154-1 theorem 0.0 4 1 61 0 131 85 3 0 2 61 159 0 [0.00] SYN155-1 theorem 0.1 4 1 246 0 247 150 33 0 3 246 1100 0 [0.00] SYN156-1 theorem 0.1 4 1 255 0 251 152 34 0 3 255 1247 0 [0.00] SYN157-1 theorem 0.0 2 1 87 0 215 124 3 0 2 87 225 0 [0.00] SYN158-1 theorem 0.0 4 1 87 0 215 123 3 0 2 87 225 0 [0.00] SYN159-1 theorem 0.1 4 1 255 0 251 151 34 0 3 255 1239 0 [0.00] SYN160-1 theorem 0.0 4 1 87 0 215 123 3 0 2 87 225 0 [0.00] SYN161-1 theorem 0.0 2 1 87 0 215 123 3 0 2 87 225 0 [0.00] SYN162-1 theorem 0.0 4 1 87 0 215 123 3 0 2 87 225 0 [0.00] SYN164-1 theorem 0.0 4 1 7 0 10 16 0 0 2 7 49 0 [0.00] SYN165-1 theorem 0.0 4 1 5 0 6 10 0 0 2 5 39 0 [0.00] SYN166-1 theorem 0.1 4 1 100 0 158 95 11 0 3 100 396 0 [0.00] SYN167-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 54 0 [0.00] SYN168-1 theorem 0.0 4 1 56 0 123 79 2 0 2 56 147 0 [0.00] SYN169-1 theorem 0.0 4 1 56 0 123 79 2 0 2 56 147 0 [0.00] SYN170-1 theorem 0.0 4 1 73 0 175 104 3 0 2 73 200 0 [0.00] SYN171-1 theorem 0.3 4 1 503 0 237 154 163 0 4 503 5019 0 [0.00] SYN172-1 theorem 0.0 2 1 6 0 7 12 0 0 2 6 49 0 [0.00] SYN173-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN174-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN175-1 theorem 0.0 4 1 39 0 41 41 0 0 2 39 74 0 [0.00] SYN176-1 theorem 0.0 4 1 66 0 156 94 3 0 2 66 184 0 [0.00] SYN177-1 theorem 0.1 4 1 94 0 154 93 9 0 3 94 354 0 [0.00] SYN178-1 theorem 0.0 4 1 67 0 156 96 3 0 2 67 187 0 [0.00] SYN179-1 theorem 0.1 4 1 132 0 205 124 17 0 3 132 562 0 [0.00] SYN180-1 theorem 0.0 4 1 75 0 191 107 3 0 2 75 206 0 [0.00] SYN181-1 theorem 0.0 4 1 75 0 191 107 3 0 2 75 206 0 [0.00] SYN182-1 theorem 0.0 4 1 86 0 209 122 3 0 2 86 224 0 [0.00] SYN183-1 theorem 0.0 4 1 86 0 209 122 3 0 2 86 224 0 [0.00] SYN184-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN185-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN186-1 theorem 0.0 4 1 47 0 97 55 1 0 2 47 119 0 [0.00] SYN187-1 theorem 0.0 4 1 47 0 98 55 1 0 2 47 119 0 [0.00] SYN188-1 theorem 0.0 4 1 47 0 97 55 1 0 2 47 119 0 [0.00] SYN189-1 theorem 0.0 2 1 54 0 121 61 1 0 2 54 142 0 [0.00] SYN190-1 theorem 0.1 4 1 148 0 214 134 19 0 3 148 714 0 [0.00] SYN191-1 theorem 0.1 4 1 133 0 212 124 17 0 3 133 562 0 [0.00] SYN192-1 theorem 0.1 4 1 130 0 206 124 17 0 3 130 547 0 [0.00] SYN193-1 theorem 0.1 3 1 130 0 205 124 17 0 3 130 547 0 [0.00] SYN194-1 theorem 0.1 4 1 176 0 225 142 24 0 3 176 878 0 [0.00] SYN195-1 theorem 0.0 2 1 92 0 217 125 3 0 2 92 239 0 [0.00] SYN196-1 theorem 0.0 4 1 53 0 118 60 1 0 2 53 140 0 [0.00] SYN197-1 theorem 0.0 4 1 8 0 15 20 0 0 2 8 50 0 [0.00] SYN198-1 theorem 0.0 4 1 53 0 119 60 1 0 2 53 140 0 [0.00] SYN199-1 theorem 0.0 4 1 53 0 118 60 1 0 2 53 140 0 [0.00] SYN200-1 theorem 0.0 4 1 53 0 117 60 1 0 2 53 140 0 [0.00] SYN201-1 theorem 0.0 4 1 63 0 153 86 3 0 2 63 172 0 [0.00] SYN202-1 theorem 0.0 4 1 68 0 157 98 3 0 2 68 191 0 [0.00] SYN203-1 theorem 0.0 4 1 71 0 156 102 3 0 2 71 194 0 [0.00] SYN204-1 theorem 0.2 4 1 312 0 218 143 94 0 4 312 3225 0 [0.00] SYN205-1 theorem 0.2 4 1 312 0 218 143 94 0 4 312 3225 0 [0.00] SYN206-1 theorem 0.0 4 1 71 0 156 102 3 0 2 71 194 0 [0.00] SYN207-1 theorem 0.2 4 1 311 0 218 143 94 0 4 311 3207 0 [0.00] SYN208-1 theorem 0.0 2 1 72 0 158 103 3 0 2 72 197 0 [0.00] SYN209-1 theorem 0.1 4 1 128 0 197 123 17 0 3 128 536 0 [0.00] SYN210-1 theorem 0.1 4 1 128 0 197 123 17 0 3 128 536 0 [0.00] SYN211-1 theorem 0.0 4 1 77 0 192 114 3 0 2 77 209 0 [0.00] SYN212-1 theorem 0.1 4 1 128 0 198 123 17 0 3 128 536 0 [0.00] SYN213-1 theorem 0.1 3 1 173 0 225 139 24 0 3 173 858 0 [0.00] SYN214-1 theorem 0.1 4 1 173 0 225 139 24 0 3 173 858 0 [0.00] SYN215-1 theorem 0.1 4 1 173 0 225 139 24 0 3 173 858 0 [0.00] SYN216-1 theorem 0.0 4 1 53 0 118 60 1 0 2 53 134 0 [0.00] SYN217-1 theorem 0.0 4 1 55 0 120 76 2 0 2 55 147 0 [0.00] SYN218-1 theorem 0.0 2 1 53 0 119 61 1 0 2 53 134 0 [0.00] SYN219-1 theorem 0.0 4 1 66 0 158 96 3 0 2 66 187 0 [0.00] SYN220-1 theorem 0.0 4 1 59 0 124 81 2 0 2 59 149 0 [0.00] SYN221-1 theorem 0.0 4 1 60 0 128 87 3 0 2 60 154 0 [0.00] SYN222-1 theorem 0.0 4 1 60 0 128 86 3 0 2 60 154 0 [0.00] SYN223-1 theorem 0.0 4 1 60 0 129 85 3 0 2 60 154 0 [0.00] SYN224-1 theorem 0.0 4 1 60 0 128 85 3 0 2 60 154 0 [0.00] SYN225-1 theorem 0.0 2 1 61 0 131 85 3 0 2 61 162 0 [0.00] SYN226-1 theorem 0.0 4 1 59 0 124 81 2 0 2 59 149 0 [0.00] SYN227-1 theorem 0.2 4 1 163 0 155 97 37 0 4 163 1719 0 [0.00] SYN228-1 theorem 0.1 4 1 92 0 154 93 9 0 3 92 341 0 [0.00] SYN229-1 theorem 0.0 4 1 60 0 128 86 3 0 2 60 154 0 [0.00] SYN230-1 theorem 0.0 4 1 60 0 128 86 3 0 2 60 154 0 [0.00] SYN231-1 theorem 0.0 4 1 60 0 128 87 3 0 2 60 154 0 [0.00] SYN232-1 theorem 0.0 4 1 60 0 128 86 3 0 2 60 154 0 [0.00] SYN233-1 theorem 0.0 4 1 60 0 128 85 3 0 2 60 154 0 [0.00] SYN234-1 theorem 0.0 4 1 61 0 130 85 3 0 2 61 162 0 [0.00] SYN235-1 theorem 0.1 4 1 93 0 153 93 9 0 3 93 351 0 [0.00] SYN236-1 theorem 0.0 4 1 60 0 128 85 3 0 2 60 154 0 [0.00] SYN237-1 theorem 0.0 4 1 6 0 8 13 0 0 2 6 46 0 [0.00] SYN238-1 theorem 0.0 4 1 4 0 4 6 0 0 2 4 39 0 [0.00] SYN239-1 theorem 0.0 4 1 4 0 5 9 0 0 2 4 39 0 [0.00] SYN240-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 54 0 [0.00] SYN241-1 theorem 0.0 2 1 12 0 19 30 0 0 2 12 54 0 [0.00] SYN242-1 theorem 0.0 4 1 27 0 33 35 0 0 2 27 70 0 [0.00] SYN243-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN244-1 theorem 0.0 4 1 4 0 4 9 0 0 2 4 39 0 [0.00] SYN245-1 theorem 0.0 4 1 12 0 18 31 0 0 2 12 54 0 [0.00] SYN246-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN247-1 theorem 0.0 4 1 6 0 10 12 0 0 2 6 46 0 [0.00] SYN248-1 theorem 0.0 4 1 37 0 39 39 0 0 2 37 70 0 [0.00] SYN249-1 theorem 0.0 2 1 36 0 40 38 0 0 2 36 70 0 [0.00] SYN250-1 theorem 0.1 4 1 102 0 118 66 16 0 4 102 1029 0 [0.00] SYN251-1 theorem 0.0 4 1 30 0 36 34 0 0 2 30 70 0 [0.00] SYN252-1 theorem 0.3 4 1 512 0 237 156 163 0 4 512 5041 0 [0.00] SYN253-1 theorem 0.3 4 1 512 0 238 156 163 0 4 512 5041 0 [0.00] SYN254-1 theorem 0.3 4 1 512 0 237 156 163 0 4 512 5041 0 [0.00] SYN255-1 theorem 0.0 4 1 45 0 95 53 1 0 2 45 113 0 [0.00] SYN256-1 theorem 0.0 4 1 45 0 95 53 1 0 2 45 113 0 [0.00] SYN257-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 54 0 [0.00] SYN258-1 theorem 0.0 4 1 7 0 11 16 0 0 2 7 49 0 [0.00] SYN259-1 theorem 0.0 4 1 7 0 11 16 0 0 2 7 49 0 [0.00] SYN260-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 54 0 [0.00] SYN261-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 54 0 [0.00] SYN262-1 theorem 0.0 4 1 44 0 77 50 1 0 2 44 111 0 [0.00] SYN263-1 theorem 0.1 4 1 70 0 119 64 2 0 3 70 233 0 [0.00] SYN264-1 theorem 0.1 4 1 74 0 75 53 9 0 4 74 856 0 [0.00] SYN265-1 theorem 0.0 4 1 60 0 128 84 3 0 2 60 149 0 [0.00] SYN266-1 theorem 0.1 4 1 139 0 214 131 19 0 3 139 586 0 [0.00] SYN267-1 theorem 0.0 4 1 73 0 176 103 3 0 2 73 200 0 [0.00] SYN268-1 theorem 0.0 2 1 73 0 175 103 3 0 2 73 200 0 [0.00] SYN269-1 theorem 0.3 4 1 500 0 237 154 163 0 4 500 5012 0 [0.00] SYN270-1 theorem 0.1 4 1 197 0 227 145 24 0 3 197 1075 0 [0.00] SYN271-1 theorem 0.3 4 1 503 0 237 154 163 0 4 503 5019 0 [0.00] SYN272-1 theorem 0.0 4 1 95 0 217 125 3 0 2 95 244 0 [0.00] SYN273-1 theorem 0.0 4 1 94 0 217 125 3 0 2 94 243 0 [0.00] SYN274-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN275-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN276-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 54 0 [0.00] SYN277-1 theorem 0.0 4 1 6 0 10 11 0 0 2 6 40 0 [0.00] SYN278-1 theorem 0.0 4 1 4 0 5 9 0 0 2 4 39 0 [0.00] SYN279-1 theorem 0.0 4 1 13 0 19 29 0 0 2 13 55 0 [0.00] SYN280-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 39 0 [0.00] SYN281-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 54 0 [0.00] SYN282-1 theorem 0.0 2 1 6 0 9 12 0 0 2 6 40 0 [0.00] SYN283-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN284-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN285-1 theorem 0.1 4 1 71 0 120 64 2 0 3 71 235 0 [0.00] SYN286-1 theorem 0.0 4 1 17 0 23 30 0 0 2 17 59 0 [0.00] SYN287-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 39 0 [0.00] SYN288-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN289-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN290-1 theorem 0.0 4 1 6 0 10 10 0 0 2 6 40 0 [0.00] SYN291-1 theorem 0.0 2 1 6 0 10 12 0 0 2 6 40 0 [0.00] SYN292-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN293-1 theorem 0.0 4 1 35 0 39 37 0 0 2 35 70 0 [0.00] SYN294-1 theorem 0.0 4 1 35 0 39 38 0 0 2 35 70 0 [0.00] SYN295-1 theorem 0.0 4 1 27 0 34 35 0 0 2 27 70 0 [0.00] SYN296-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 70 0 [0.00] SYN297-1 theorem 0.0 4 1 27 0 34 34 0 0 2 27 70 0 [0.00] SYN298-1 theorem 0.0 2 1 71 0 156 102 3 0 2 71 194 0 [0.00] SYN299-1 theorem 0.0 4 1 71 0 156 102 3 0 2 71 194 0 [0.00] SYN300-1 theorem 0.0 4 1 71 0 156 102 3 0 2 71 194 0 [0.00] SYN301-1 theorem 0.1 4 1 128 0 197 123 17 0 3 128 536 0 [0.00] SYN302-1.003 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 [0.00] SYN310-1 theorem 0.0 4 1 42 0 2 0 0 0 9 42 111 0 [0.00] SYN311-1 theorem 23.6 52 1 15433 0 2 0 0 0 12 15433 56334 0 [0.00] SYN312-1 theorem 47.8 9 1 6785 0 3 0 0 0 8 6785 115379 0 [0.00] SYN318-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 4 0 [0.00] SYN322-1 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 [0.00] SYN329-1 non_thm 0.0 4 0 3 0 4 0 0 0 2 3 4 0 [0.00] SYN333-1 theorem 0.0 4 1 2 0 2 6 0 0 2 2 2 0 [0.00] SYN336-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 5 0 [0.00] SYN337-1 non_thm 0.0 4 0 4 0 5 0 0 0 2 4 5 0 [0.00] SYN338-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 3 0 [0.00] SYN339-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 2 0 [0.00] SYN340-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 [0.00] SYN341-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 2 0 [0.00] SYN342-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 [0.00] SYN346-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 [0.00] SYN553-1 theorem 0.0 4 1 16 0 7 0 0 0 5 16 71 0 [0.00] SYN555-1 theorem 0.0 4 1 8 0 6 0 0 0 7 8 21 0 [0.00] SYN557-1 timeout 300.0 83 [0.00] SYN558-1 theorem 0.0 4 1 16 0 6 0 0 0 5 16 81 0 [0.00] SYN559-1 theorem 0.0 2 1 26 0 6 0 0 0 8 26 120 0 [0.00] SYN561-1 theorem 0.1 4 1 76 0 6 0 0 0 9 76 556 0 [0.00] SYN562-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 9 0 [0.00] SYN563-1 theorem 0.0 4 1 44 0 6 0 0 0 7 44 350 0 [0.00] SYN564-1 theorem 0.0 4 1 34 0 7 0 0 0 6 34 161 0 [0.00] SYN565-1 theorem 0.0 4 1 35 0 7 0 0 0 6 35 166 0 [0.00] SYN566-1 theorem 0.0 4 1 21 0 8 0 0 0 6 21 70 0 [0.00] SYN569-1 timeout 300.0 17 [0.00] SYN570-1 theorem 0.0 4 1 16 0 10 0 0 0 6 16 50 0 [0.00] SYN572-1 theorem 0.4 4 1 157 0 9 0 0 0 9 157 2453 0 [0.00] SYN577-1 theorem 0.1 4 1 52 0 12 0 0 0 8 52 248 0 [0.00] SYN584-1 theorem 0.0 4 1 10 0 9 0 0 0 19 10 28 0 [0.00] SYN588-1 theorem 0.0 2 1 12 0 12 0 0 0 2 12 14 0 [0.00] SYN589-1 theorem 0.0 4 1 12 0 12 0 0 0 2 12 14 0 [0.00] SYN590-1 theorem 0.0 4 1 74 0 8 0 0 0 8 74 261 0 [0.00] SYN596-1 theorem 0.0 2 1 12 0 11 0 0 0 21 12 33 0 [0.00] SYN597-1 theorem 0.1 4 1 214 0 11 0 0 0 9 214 1181 0 [0.00] SYN601-1 theorem 0.1 4 1 241 0 12 0 0 0 9 241 1303 0 [0.00] SYN602-1 timeout 300.0 18 [0.00] SYN603-1 timeout 300.0 18 [0.00] SYN616-1 theorem 0.3 4 1 155 0 13 0 0 0 7 155 802 0 [0.00] SYN618-1 theorem 0.0 4 1 34 0 16 0 0 0 7 34 114 0 [0.00] SYN628-1 theorem 0.1 4 1 111 0 15 0 0 0 7 111 557 0 [0.00] SYN629-1 theorem 0.1 2 1 111 0 15 0 0 0 7 111 557 0 [0.00] SYN632-1 theorem 0.0 4 1 26 0 12 0 1 0 21 26 88 0 [0.00] SYN637-1 theorem 0.0 4 1 25 0 14 0 0 0 23 25 111 0 [0.00] SYN638-1 theorem 0.0 4 1 25 0 14 0 0 0 23 25 111 0 [0.00] SYN651-1 theorem 0.0 4 1 21 0 15 0 0 0 19 21 58 0 [0.00] SYN652-1 theorem 0.0 4 1 27 0 20 0 0 0 7 27 74 0 [0.00] SYN688-1 theorem 0.0 4 1 42 0 28 0 0 0 7 42 98 0 [0.00] SYN689-1 theorem 0.0 4 1 42 0 28 0 0 0 7 42 98 0 [0.00] SYN691-1 theorem 0.0 4 1 32 0 24 0 0 0 29 32 104 0 [0.00] SYN702-1 theorem 0.1 4 1 34 0 28 0 0 0 35 34 106 0 [0.00] SYN703-1 theorem 0.1 4 1 37 0 29 0 0 0 35 37 115 0 [0.00] SYN705-1 theorem 0.1 4 1 37 0 29 0 0 0 35 37 115 0 [0.00] SYN706-1 theorem 0.1 4 1 52 0 31 0 1 0 16 52 178 0 [0.00] SYN709-1 theorem 0.1 4 1 44 0 35 0 0 0 17 44 132 0 [0.00] SYN712-1 theorem 0.1 4 1 44 0 36 0 0 0 41 44 137 0 [0.00] SYN715-1 theorem 0.1 4 1 44 0 36 0 0 0 41 44 139 0 [0.00] SYN716-1 theorem 0.1 4 1 43 0 36 0 0 0 41 43 134 0 [0.00] SYN719-1 theorem 0.0 2 1 49 0 46 0 0 0 7 49 127 0 [0.00] SYN720-1 non_thm 0.3 4 0 638 0 264 171 221 0 4 638 6975 0 [0.00] SYN721-1 theorem 0.0 2 1 3 0 1 0 0 0 3 3 3 0 [0.00] SYN727-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 3 0 [0.00] SYN729-1 theorem 0.0 4 1 30 0 1 0 0 0 6 30 89 0 [0.00] SYN731-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 [0.11] PUZ008-2 theorem 0.0 4 1 13 0 28 13 0 0 12 13 16 0 [0.11] SYN163-1 theorem 0.1 4 1 255 0 251 151 34 0 3 255 1239 0 [0.14] NUM286-1 timeout 300.0 17 [0.14] PUZ046-1 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 [0.14] SWV013-1 timeout 300.0 4 [0.14] SWV015-1 timeout 300.0 4 [0.14] SWV017-1 timeout 300.0 4 [0.14] SYN303-1 non_thm 0.0 4 0 2 0 2 0 0 0 3 2 5 0 [0.17] LCL004-1 theorem 61.3 24 1 3555 0 2 0 1903 0 16 3555 864402 0 [0.17] LCL012-1 theorem 280.9 116 1 3161 0 2 0 0 0 10 3161 3920164 0 [0.17] LCL014-1 theorem 1.7 4 1 349 0 2 0 29 0 8 349 43597 0 [0.17] LCL015-1 timeout 300.0 117 [0.17] LCL016-1 timeout 300.0 87 [0.17] LCL018-1 theorem 4.6 11 1 340 0 2 0 0 0 14 340 61658 0 [0.17] LCL026-1 theorem 1.5 4 1 359 0 4 0 17 0 7 359 50295 0 [0.17] LCL030-1 theorem 3.9 5 1 454 0 5 0 22 0 8 454 87545 0 [0.17] LCL031-1 theorem 4.1 5 1 462 0 5 0 22 0 8 462 90028 0 [0.17] LCL034-1 theorem 0.9 4 1 245 0 2 0 18 0 10 245 31542 0 [0.17] LCL036-1 theorem 0.1 4 1 53 0 2 0 3 0 10 53 1769 0 [0.17] LCL039-1 theorem 6.4 5 1 968 0 6 0 34 0 7 968 208960 0 [0.17] LCL042-1 theorem 34.4 6 1 157 0 6 0 0 0 8 157 8646 0 [0.17] LCL048-1 theorem 0.1 4 1 42 0 4 0 5 0 8 42 531 0 [0.17] LCL049-1 theorem 0.4 4 1 164 0 4 0 17 0 8 164 8657 0 [0.17] LCL050-1 theorem 0.4 4 1 165 0 4 0 17 0 8 165 8793 0 [0.17] LCL051-1 theorem 0.4 4 1 168 0 4 0 17 0 8 168 9323 0 [0.17] LCL052-1 theorem 0.4 4 1 164 0 4 0 17 0 8 164 8700 0 [0.17] LCL053-1 theorem 0.5 4 1 176 0 4 0 19 0 8 176 10122 0 [0.17] LCL055-1 theorem 0.2 2 1 74 0 4 0 8 0 8 74 2259 0 [0.17] LCL056-1 theorem 0.2 4 1 75 0 4 0 8 0 8 75 2352 0 [0.17] LCL057-1 theorem 0.4 4 1 157 0 4 0 17 0 8 157 7948 0 [0.17] LCL058-1 theorem 2.9 6 1 486 0 4 0 28 0 8 486 62051 0 [0.17] LCL059-1 theorem 0.4 4 1 156 0 4 0 17 0 8 156 7843 0 [0.17] LCL060-1 theorem 1.4 4 1 331 0 4 0 22 0 8 331 30648 0 [0.17] LCL067-1 theorem 6.2 4 1 74 0 4 0 1 0 9 74 2095 0 [0.17] LCL068-1 theorem 15.7 11 1 1085 0 4 0 83 0 9 1085 179790 0 [0.17] LCL070-1 theorem 6.6 4 1 59 0 4 0 0 0 9 59 1548 0 [0.17] LCL071-1 theorem 22.6 15 1 1341 0 4 0 93 0 9 1341 293649 0 [0.17] LCL072-1 theorem 6.2 4 1 37 0 4 0 0 0 9 37 637 0 [0.17] LCL080-1 theorem 1.0 4 1 178 0 4 0 2 0 8 178 17397 0 [0.17] LCL080-2 theorem 1.1 4 1 190 0 5 0 2 0 8 190 19311 0 [0.17] LCL092-1 theorem 0.6 4 1 156 0 2 0 48 0 10 156 11515 0 [0.17] LCL093-1 theorem 0.9 4 1 193 0 2 0 48 0 10 193 18915 0 [0.17] LCL095-1 theorem 0.6 4 1 164 0 2 0 48 0 10 164 13004 0 [0.17] LCL103-1 theorem 12.8 7 1 599 0 3 0 2 0 10 599 195216 0 [0.17] LCL113-1 theorem 12.8 8 1 791 0 5 0 36 0 8 791 134020 0 [0.17] LCL114-1 theorem 18.1 11 1 1113 0 5 0 63 0 8 1113 217203 0 [0.17] LCL115-1 theorem 0.5 4 1 200 0 5 0 2 0 7 200 13705 0 [0.17] LCL116-1 theorem 18.1 12 1 1113 0 5 0 63 0 8 1113 217203 0 [0.17] LCL121-1 theorem 167.0 55 1 1686 0 2 0 5 0 14 1686 2078584 0 [0.17] LCL127-1 timeout 300.0 94 [0.17] LCL128-1 timeout 300.0 93 [0.17] LCL129-1 theorem 53.6 18 1 1680 0 2 0 3 0 10 1680 984347 0 [0.17] LCL131-1 theorem 2.5 6 1 258 0 2 0 1 0 12 258 41029 0 [0.17] LCL191-1 theorem 2.5 5 1 4217 0 6 0 0 0 8 4217 12737 0 [0.17] LCL195-1 theorem 10.0 10 1 1839 0 6 0 0 0 9 1839 7448 0 [0.17] LCL218-1 theorem 19.9 13 1 13699 0 6 0 0 0 9 13699 42615 0 [0.17] LCL225-1 theorem 168.5 52 1 11264 0 6 0 0 0 10 11264 42332 0 [0.17] LCL230-1 theorem 204.9 52 1 34068 0 6 0 0 0 10 34068 113679 0 [0.17] LCL231-1 theorem 203.7 52 1 34068 0 6 0 0 0 10 34068 113679 0 [0.17] LCL234-1 theorem 1.7 4 1 2837 0 6 0 0 0 8 2837 9054 0 [0.17] LCL237-1 theorem 1.8 4 1 2838 0 6 0 0 0 8 2838 9059 0 [0.17] LCL250-1 theorem 12.4 10 1 5491 0 6 0 0 0 9 5491 19347 0 [0.17] LCL256-1 theorem 0.3 4 1 136 0 4 0 16 0 8 136 6132 0 [0.17] LCL368-1 theorem 0.4 4 1 168 0 4 0 17 0 8 168 9178 0 [0.17] LCL370-1 theorem 2.6 5 1 461 0 4 0 27 0 8 461 56874 0 [0.17] LCL371-1 theorem 2.6 6 1 461 0 4 0 27 0 8 461 56874 0 [0.17] LCL372-1 theorem 2.7 6 1 466 0 4 0 27 0 8 466 57660 0 [0.17] LCL373-1 theorem 1.4 5 1 331 0 4 0 22 0 8 331 30648 0 [0.17] LCL374-1 theorem 20.1 14 1 1378 0 4 0 51 0 8 1378 360978 0 [0.17] LCL378-1 theorem 0.2 4 1 75 0 4 0 8 0 8 75 2291 0 [0.17] LCL379-1 theorem 0.4 4 1 164 0 4 0 17 0 8 164 8700 0 [0.17] LCL380-1 theorem 0.2 4 1 76 0 4 0 9 0 8 76 2384 0 [0.17] LCL381-1 theorem 0.2 4 1 79 0 4 0 9 0 8 79 2610 0 [0.17] LCL382-1 theorem 2.9 6 1 485 0 4 0 28 0 8 485 61940 0 [0.17] LCL383-1 theorem 15.9 13 1 1212 0 4 0 49 0 8 1212 285770 0 [0.17] LCL385-1 theorem 8.9 10 1 911 0 4 0 49 0 8 911 174709 0 [0.17] LCL386-1 theorem 0.4 4 1 163 0 4 0 17 0 8 163 8592 0 [0.17] LCL387-1 theorem 0.4 4 1 171 0 4 0 17 0 8 171 9614 0 [0.17] LCL388-1 theorem 3.0 6 1 492 0 4 0 28 0 8 492 62871 0 [0.17] LCL389-1 theorem 9.1 10 1 912 0 4 0 49 0 8 912 174952 0 [0.17] LCL390-1 theorem 2.7 6 1 466 0 4 0 27 0 8 466 57660 0 [0.17] LCL396-1 theorem 0.2 4 1 79 0 4 0 9 0 8 79 2610 0 [0.17] LCL400-1 theorem 0.4 4 1 171 0 4 0 17 0 8 171 9660 0 [0.17] LCL401-1 theorem 0.4 4 1 171 0 4 0 17 0 8 171 9660 0 [0.17] LCL402-1 theorem 0.4 4 1 171 0 4 0 17 0 8 171 9660 0 [0.17] LCL405-1 theorem 0.4 4 1 177 0 4 0 19 0 8 177 10233 0 [0.17] LCL416-1 theorem 8.0 4 1 727 0 2 0 1 0 16 727 103883 0 [0.17] NUM017-1 timeout 300.0 15 [0.17] NUM283-1.005 theorem 19.7 6 1 605 0 4 0 0 0 153 605 610 0 [0.17] NUM284-1.014 theorem 40.0 6 1 249 0 4 0 0 0 468 249 249 0 [0.17] PLA004-1 timeout 300.0 18 [0.17] PLA004-2 timeout 300.0 18 [0.17] PLA005-1 timeout 300.0 18 [0.17] PLA005-2 timeout 300.0 18 [0.17] PLA009-1 timeout 300.0 18 [0.17] PLA009-2 timeout 300.0 18 [0.17] PLA011-1 timeout 300.0 18 [0.17] PLA011-2 timeout 300.0 18 [0.17] PLA013-1 timeout 300.0 18 [0.17] PLA014-1 timeout 300.0 18 [0.17] PLA014-2 timeout 300.0 18 [0.17] PLA021-1 timeout 300.0 18 [0.17] SWV014-1 timeout 300.0 4 [0.17] SYN556-1 timeout 300.0 5 [0.17] SYN598-1 timeout 300.0 31 [0.17] SYN599-1 timeout 300.0 31 [0.17] SYN631-1 timeout 300.0 20 [0.17] SYN639-1 theorem 49.1 11 1 4199 0 20 0 0 0 14 4199 20374 0 [0.17] SYN640-1 theorem 48.9 11 1 4199 0 20 0 0 0 14 4199 20374 0 [0.17] SYN646-1 theorem 56.8 11 1 4487 0 22 0 0 0 14 4487 21704 0 [0.17] SYN647-1 theorem 57.4 11 1 4487 0 22 0 0 0 14 4487 21704 0 [0.17] SYN649-1 timeout 300.0 14 [0.17] SYN654-1 timeout 300.0 4 [0.17] SYN655-1 timeout 300.0 4 [0.17] SYN704-1 timeout 300.0 78 [0.17] SYN707-1 timeout 300.0 15 [0.17] SYN708-1 timeout 300.0 15 [0.22] LAT005-1 theorem 0.4 4 1 150 0 17 0 0 0 4 150 7301 0 [0.22] PUZ036-1.005 theorem 0.2 4 1 605 0 2 0 0 0 21 605 1812 0 [0.22] PUZ037-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 2 0 [0.22] PUZ037-2 theorem 0.5 10 1 118 0 2 0 0 0 55 118 2100 0 [0.29] GRP394-2 timeout 300.0 11 [0.29] SWV016-1 timeout 300.0 4 [0.29] SWV018-1 timeout 300.0 4 [0.33] LCL003-1 theorem 78.2 33 1 4583 0 2 0 3896 0 16 4583 1107271 0 [0.33] LCL017-1 timeout 300.0 110 [0.33] LCL019-1 theorem 60.8 21 1 2122 0 2 0 0 0 10 2122 1128248 0 [0.33] LCL024-1 theorem 25.0 8 1 1602 0 2 0 0 0 10 1602 553046 0 [0.33] LCL028-1 theorem 14.1 7 1 771 0 4 0 84 0 8 771 181822 0 [0.33] LCL038-1 theorem 132.2 28 1 2289 0 2 0 171 0 10 2289 2635004 0 [0.33] LCL040-1 theorem 1.2 3 1 354 0 6 0 42 0 7 354 38943 0 [0.33] LCL054-1 theorem 3.6 6 1 545 0 4 0 28 0 8 545 75122 0 [0.33] LCL085-1 theorem 21.2 5 1 905 0 2 0 112 0 10 905 482648 0 [0.33] LCL099-1 theorem 182.2 32 1 2918 0 3 0 2 0 10 2918 2645615 0 [0.33] LCL122-1 timeout 300.0 103 [0.33] LCL221-1 theorem 174.6 50 1 14855 0 6 0 0 0 10 14855 54474 0 [0.33] LCL222-1 theorem 173.8 52 1 14611 0 6 0 0 0 10 14611 53372 0 [0.33] LCL223-1 theorem 178.6 50 1 17887 0 6 0 0 0 10 17887 63997 0 [0.33] LCL227-1 timeout 300.0 58 [0.33] LCL369-1 theorem 0.4 4 1 168 0 4 0 17 0 8 168 9323 0 [0.33] LCL391-1 theorem 47.4 25 1 2207 0 4 0 64 0 8 2207 791080 0 [0.33] LCL392-1 theorem 2.8 6 1 469 0 4 0 28 0 8 469 58935 0 [0.33] LCL403-1 theorem 2.9 6 1 492 0 4 0 28 0 8 492 62871 0 [0.33] LCL404-1 theorem 8.9 10 1 912 0 4 0 49 0 8 912 174952 0 [0.33] PLA007-1 timeout 300.0 18 [0.33] PLA008-1 timeout 300.0 18 [0.33] PLA010-1 timeout 300.0 18 [0.33] PLA012-1 timeout 300.0 18 [0.33] PLA015-1 timeout 300.0 18 [0.33] PLA016-1 timeout 300.0 18 [0.33] PLA018-1 timeout 300.0 18 [0.33] PLA019-1 timeout 300.0 18 [0.33] PLA023-1 timeout 300.0 18 [0.33] PUZ039-1 theorem 3.8 16 1 4587 0 2 0 0 0 81 4587 13152 0 [0.33] PUZ040-1 theorem 0.9 6 1 1078 0 2 0 0 0 81 1078 3181 0 [0.33] PUZ042-1 theorem 0.3 4 1 416 0 2 0 0 0 81 416 1242 0 [0.33] RNG001-2 timeout 300.0 18 [0.33] RNG004-3 timeout 300.0 9 [0.33] SYN600-1 timeout 300.0 22 [0.33] SYN653-1 timeout 300.0 4 [0.33] SYN711-1 timeout 300.0 21 [0.43] LCL411-1 timeout 300.0 58 [0.43] LCL415-1 crash 111.1 97 [0.43] NUM286-2 timeout 300.0 79 [0.43] PUZ049-1 non_thm 1.4 7 0 1897 0 2 0 0 0 74 1897 5126 0 [0.43] SWV012-1 timeout 300.0 4 [0.44] PUZ037-3 memory 119.0 399 [0.50] LCL002-1 theorem 94.5 40 1 5371 0 2 0 4314 0 16 5371 1332425 0 [0.50] LCL020-1 timeout 300.0 49 [0.50] LCL021-1 timeout 300.0 30 [0.50] LCL032-1 theorem 251.7 41 1 3579 0 2 0 120 0 10 3579 5364254 0 [0.50] LCL061-1 theorem 3.8 6 1 556 0 4 0 29 0 8 556 78421 0 [0.50] LCL084-2 theorem 129.9 28 1 2229 0 3 0 137 0 10 2229 2585320 0 [0.50] LCL100-1 theorem 152.2 32 1 2725 0 3 0 0 0 10 2725 2331515 0 [0.50] LCL119-1 timeout 300.0 27 [0.50] LCL124-1 timeout 300.0 95 [0.50] LCL166-1 timeout 300.0 30 [0.50] LCL167-1 timeout 300.0 49 [0.50] LCL253-1 timeout 300.0 56 [0.50] LCL375-1 theorem 19.7 14 1 1354 0 4 0 51 0 8 1354 353162 0 [0.50] LCL376-1 theorem 9.1 10 1 919 0 4 0 49 0 8 919 177212 0 [0.50] LCL393-1 theorem 9.5 10 1 935 0 4 0 49 0 8 935 180418 0 [0.50] SYN614-1 timeout 300.0 49 [0.50] SYN617-1 timeout 300.0 48 [0.57] NUM287-1 timeout 300.0 20 [0.67] ANA003-2 timeout 300.0 12 [0.67] LCL005-1 theorem 115.1 57 1 5846 0 2 0 4464 0 16 5846 1537472 0 [0.67] LCL062-1 theorem 17.4 13 1 1270 0 4 0 49 0 8 1270 313054 0 [0.67] LCL084-3 theorem 129.3 28 1 2237 0 4 0 152 0 10 2237 2578165 0 [0.67] LCL105-1 theorem 206.1 28 1 3413 0 4 0 143 0 10 3413 3037112 0 [0.67] LCL249-1 timeout 300.0 58 [0.67] LCL394-1 theorem 38.4 22 1 1919 0 4 0 54 0 8 1919 649319 0 [0.67] LCL395-1 theorem 50.1 25 1 2264 0 4 0 64 0 8 2264 819554 0 [0.67] SYN615-1 timeout 300.0 39 [0.71] PUZ048-1 memory 207.2 399 [0.83] LCL001-1 timeout 300.0 58 [0.83] LCL063-1 timeout 300.0 70 [0.83] LCL125-1 theorem 181.4 26 1 3206 0 3 0 113 0 10 3206 2793829 0 [0.83] LCL377-1 theorem 3.7 6 1 551 0 4 0 29 0 8 551 77175 0 [0.86] LCL078-1 timeout 300.0 58 [0.86] LCL168-1 timeout 300.0 8 [0.86] LCL179-1 timeout 300.0 56 [0.86] LCL180-1 timeout 300.0 57 [0.86] LCL181-1 timeout 300.0 57 [0.86] LCL183-1 timeout 300.0 57 [0.86] LCL184-1 timeout 300.0 58 [0.86] LCL209-1 timeout 300.0 58 [0.86] LCL219-1 timeout 300.0 56 [0.86] LCL220-1 timeout 300.0 56 [0.86] LCL235-1 timeout 300.0 56 [0.86] LCL239-1 timeout 300.0 58 [0.86] LCL240-1 timeout 300.0 57 [0.86] LCL241-1 timeout 300.0 57 [0.86] LCL242-1 timeout 300.0 58 [0.86] LCL244-1 timeout 300.0 56 [0.86] LCL245-1 timeout 300.0 58 [0.86] LCL246-1 timeout 300.0 58 [0.86] LCL247-1 timeout 300.0 57 [0.86] LCL248-1 timeout 300.0 56 [0.86] LCL252-1 timeout 300.0 58 [0.86] LCL255-1 timeout 300.0 57 [0.86] PUZ015-3 timeout 300.0 287 [1.00] ANA004-2 timeout 300.0 12 [1.00] ANA005-2 timeout 300.0 12 [1.00] GEO001-4 timeout 300.0 10 [1.00] LCL037-1 theorem 288.4 49 1 3814 0 2 0 133 0 10 3814 6120105 0 [1.00] LCL073-1 timeout 300.0 10 [1.00] LCL074-1 timeout 300.0 10 [1.00] LCL109-1 timeout 300.0 33 [1.00] LCL228-1 timeout 300.0 59 [1.00] LCL229-1 timeout 300.0 56 [1.00] LCL243-1 timeout 300.0 56 [1.00] LCL251-1 timeout 300.0 58 [1.00] LCL254-1 timeout 300.0 56 [1.00] LCL417-1 timeout 300.0 31 [1.00] LCL418-1 timeout 300.0 23 [1.00] LCL419-1 timeout 300.0 33 [1.00] LCL420-1 timeout 300.0 33 [1.00] LCL421-1 timeout 300.0 33 [1.00] LCL422-1 timeout 300.0 33 [1.00] LCL423-1 timeout 300.0 68 [1.00] LCL424-1 timeout 300.0 11 [1.00] LCL425-1 timeout 300.0 106 [1.00] LCL426-1 timeout 300.0 15 [1.00] LCL427-1 timeout 300.0 48 [1.00] NUM026-1 timeout 300.0 28 [1.00] PUZ041-1 memory 216.2 399 [1.00] PUZ050-1 theorem 80.7 200 1 73260 0 2 0 0 0 81 73260 194762 0 [1.00] PUZ051-1 memory 217.7 399 [1.00] PUZ052-1 memory 117.7 399 [1.00] PUZ053-1 memory 119.3 399 [1.00] ROB025-1 timeout 300.0 86