-------------------------------------------------------------------------------- Execute format string : ./darwin --restart Reluctant Problems list file : hne_reluctant-problems Output file : hne_reluctant-output Summary file : hne_reluctant-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 2 10 13 0 [0.00] COM002-1 theorem 0.0 4 1 30 0 15 0 0 0 2 30 56 0 [0.00] GEO002-4 theorem 0.0 4 1 15 0 3 0 5 0 2 15 252 0 [0.00] GEO079-1 theorem 0.0 4 1 3 0 2 0 0 0 2 3 4 0 [0.00] GRP001-5 theorem 0.0 4 1 8 0 5 0 0 0 2 8 94 0 [0.00] GRP003-1 theorem 0.0 4 1 5 0 3 0 0 0 3 5 36 0 [0.00] GRP003-2 theorem 0.2 4 1 11 0 4 0 0 0 3 11 365 0 [0.00] GRP004-1 theorem 0.0 4 1 5 0 3 0 0 0 3 5 36 0 [0.00] GRP004-2 theorem 0.2 4 1 10 0 4 0 0 0 3 10 183 0 [0.00] GRP005-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 79 0 [0.00] GRP006-1 theorem 0.0 4 1 7 0 6 0 0 0 2 7 82 0 [0.00] GRP028-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 7 0 [0.00] GRP028-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 38 0 [0.00] GRP028-4 theorem 0.0 4 1 3 0 3 0 0 0 2 3 11 0 [0.00] GRP029-2 theorem 0.3 4 1 11 0 5 0 0 0 3 11 423 0 [0.00] GRP031-2 theorem 0.2 4 1 10 0 4 0 0 0 3 10 220 0 [0.00] GRP033-3 theorem 0.0 4 1 8 0 7 0 0 0 2 8 208 0 [0.00] GRP034-4 theorem 0.0 4 1 7 0 6 0 0 0 2 7 102 0 [0.00] GRP041-2 theorem 0.0 4 1 3 0 3 0 0 0 2 3 22 0 [0.00] GRP042-2 theorem 0.0 4 1 15 0 5 0 0 0 2 15 715 0 [0.00] GRP043-2 theorem 0.1 4 1 24 0 6 0 0 0 2 24 2048 0 [0.00] GRP044-2 theorem 0.0 4 1 16 0 6 0 0 0 2 16 724 0 [0.00] GRP045-2 theorem 0.1 4 1 24 0 6 0 0 0 2 24 2423 0 [0.00] GRP046-2 theorem 0.0 4 1 20 0 5 0 0 0 2 20 1672 0 [0.00] GRP047-2 theorem 0.0 4 1 18 0 5 0 0 0 2 18 1338 0 [0.00] GRP048-2 theorem 37.0 71 1 169 0 5 0 0 0 3 169 665897 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 2 146 5862 0 [0.00] LCL006-1 theorem 1.8 6 1 248 0 3 0 0 0 5 248 40262 0 [0.00] LCL007-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 7 0 [0.00] LCL008-1 theorem 0.0 4 1 8 0 2 0 1 0 5 8 40 0 [0.00] LCL009-1 theorem 0.9 4 1 184 0 2 0 2 0 5 184 22315 0 [0.00] LCL010-1 theorem 0.0 4 1 33 0 2 0 0 0 5 33 749 0 [0.00] LCL011-1 theorem 0.1 4 1 47 0 2 0 0 0 5 47 1412 0 [0.00] LCL013-1 theorem 0.0 4 1 3 0 2 0 0 0 8 3 6 0 [0.00] LCL022-1 theorem 0.0 4 1 44 0 2 0 2 0 5 44 1129 0 [0.00] LCL023-1 theorem 0.3 4 1 115 0 2 0 2 0 5 115 8617 0 [0.00] LCL025-1 theorem 1.3 5 1 257 0 4 0 3 0 5 257 40968 0 [0.00] LCL027-1 theorem 0.1 4 1 64 0 4 0 2 0 5 64 2885 0 [0.00] LCL029-1 theorem 0.3 4 1 120 0 5 0 1 0 5 120 11545 0 [0.00] LCL033-1 theorem 0.0 4 1 11 0 2 0 2 0 5 11 77 0 [0.00] LCL035-1 theorem 0.0 4 1 8 0 2 0 0 0 5 8 49 0 [0.00] LCL041-1 theorem 0.0 4 1 26 0 6 0 0 0 4 26 424 0 [0.00] LCL043-1 theorem 0.0 4 1 23 0 6 0 0 0 4 23 365 0 [0.00] LCL044-1 theorem 0.1 4 1 74 0 6 0 0 0 5 74 3469 0 [0.00] LCL045-1 theorem 12.7 24 1 742 0 6 0 16 0 5 742 240294 0 [0.00] LCL046-1 theorem 0.0 4 1 5 0 4 0 0 0 5 5 15 0 [0.00] LCL047-1 theorem 0.1 4 1 56 0 4 0 4 0 5 56 2097 0 [0.00] LCL064-1 theorem 2.8 7 1 455 0 4 0 8 0 5 455 80173 0 [0.00] LCL064-2 theorem 0.4 4 1 131 0 3 0 1 0 5 131 13637 0 [0.00] LCL065-1 theorem 0.1 4 1 90 0 4 0 1 0 5 90 4894 0 [0.00] LCL066-1 theorem 0.1 4 1 79 0 4 0 1 0 5 79 3946 0 [0.00] LCL069-1 theorem 1.4 4 1 368 0 4 0 7 0 5 368 41791 0 [0.00] LCL075-1 theorem 0.1 4 1 56 0 2 0 2 0 6 56 2538 0 [0.00] LCL076-1 theorem 0.1 4 1 73 0 4 0 1 0 5 73 3372 0 [0.00] LCL076-2 theorem 0.0 4 1 4 0 4 0 0 0 2 4 9 0 [0.00] LCL076-3 theorem 0.0 4 1 27 0 4 0 1 0 4 27 800 0 [0.00] LCL077-1 theorem 0.1 4 1 72 0 4 0 1 0 5 72 3336 0 [0.00] LCL077-2 theorem 0.0 4 1 25 0 4 0 1 0 4 25 634 0 [0.00] LCL079-1 theorem 0.0 4 1 14 0 6 0 1 0 3 14 99 0 [0.00] LCL081-1 theorem 0.0 4 1 21 0 2 0 6 0 5 21 281 0 [0.00] LCL082-1 theorem 0.0 4 1 24 0 2 0 10 0 5 24 349 0 [0.00] LCL083-1 theorem 0.1 4 1 89 0 2 0 41 0 6 89 4061 0 [0.00] LCL083-2 theorem 0.1 4 1 40 0 3 0 0 0 6 40 1437 0 [0.00] LCL086-1 theorem 0.0 4 1 23 0 2 0 5 0 6 23 369 0 [0.00] LCL087-1 theorem 0.0 4 1 12 0 2 0 2 0 6 12 113 0 [0.00] LCL088-1 theorem 0.1 4 1 50 0 2 0 8 0 6 50 1891 0 [0.00] LCL089-1 theorem 0.1 4 1 61 0 2 0 8 0 6 61 2832 0 [0.00] LCL090-1 theorem 0.0 4 1 32 0 2 0 8 0 6 32 709 0 [0.00] LCL091-1 theorem 0.0 4 1 36 0 2 0 8 0 6 36 905 0 [0.00] LCL094-1 theorem 0.2 4 1 92 0 2 0 8 0 6 92 6784 0 [0.00] LCL096-1 theorem 10.8 13 1 538 0 4 0 1 0 5 538 220910 0 [0.00] LCL097-1 theorem 2.4 6 1 278 0 3 0 1 0 5 278 57483 0 [0.00] LCL098-1 theorem 4.4 13 1 191 0 2 0 0 0 7 191 35912 0 [0.00] LCL101-1 theorem 0.0 4 1 14 0 3 0 1 0 5 14 111 0 [0.00] LCL102-1 theorem 0.5 4 1 139 0 4 0 1 0 5 139 14091 0 [0.00] LCL104-1 theorem 0.0 4 1 16 0 3 0 0 0 5 16 150 0 [0.00] LCL106-1 theorem 0.0 4 1 9 0 3 0 0 0 7 9 32 0 [0.00] LCL107-1 theorem 0.0 4 1 17 0 2 0 0 0 8 17 138 0 [0.00] LCL108-1 theorem 0.0 4 1 11 0 2 0 0 0 8 11 57 0 [0.00] LCL110-1 theorem 0.2 4 1 111 0 5 0 0 0 5 111 7739 0 [0.00] LCL111-1 theorem 1.0 4 1 269 0 5 0 3 0 5 269 33781 0 [0.00] LCL112-1 theorem 0.2 4 1 112 0 5 0 0 0 5 112 7790 0 [0.00] LCL117-1 theorem 0.0 4 1 4 0 2 0 0 0 5 4 8 0 [0.00] LCL118-1 theorem 0.2 4 1 93 0 2 0 3 0 6 93 5456 0 [0.00] LCL120-1 theorem 0.1 4 1 74 0 2 0 0 0 6 74 2839 0 [0.00] LCL123-1 theorem 22.3 27 1 556 0 2 0 3 0 7 556 214642 0 [0.00] LCL126-1 theorem 0.0 4 1 8 0 3 0 1 0 5 8 40 0 [0.00] LCL130-1 timeout 299.0 173 [0.00] LCL169-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 11 0 [0.00] LCL170-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 10 0 [0.00] LCL171-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 11 0 [0.00] LCL172-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 11 0 [0.00] LCL173-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 11 0 [0.00] LCL174-1 theorem 0.3 4 1 805 0 6 0 0 0 5 805 4335 0 [0.00] LCL175-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 9 0 [0.00] LCL176-1 theorem 0.0 4 1 8 0 6 0 0 0 4 8 24 0 [0.00] LCL177-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 37 0 [0.00] LCL178-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 37 0 [0.00] LCL182-1 theorem 0.2 4 1 587 0 6 0 0 0 5 587 3259 0 [0.00] LCL185-1 theorem 0.0 4 1 19 0 6 0 0 0 4 19 100 0 [0.00] LCL186-1 theorem 0.0 4 1 19 0 6 0 0 0 4 19 100 0 [0.00] LCL187-1 theorem 0.0 4 1 20 0 6 0 0 0 4 20 113 0 [0.00] LCL188-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 37 0 [0.00] LCL189-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 37 0 [0.00] LCL190-1 theorem 0.0 4 1 19 0 6 0 0 0 4 19 104 0 [0.00] LCL192-1 theorem 0.1 4 1 271 0 6 0 0 0 5 271 1552 0 [0.00] LCL193-1 theorem 0.1 4 1 247 0 6 0 0 0 5 247 1401 0 [0.00] LCL194-1 theorem 4.0 7 1 4728 0 6 0 0 0 6 4728 26136 0 [0.00] LCL196-1 theorem 0.2 4 1 669 0 6 0 0 0 5 669 3677 0 [0.00] LCL197-1 theorem 0.1 4 1 85 0 6 0 0 0 5 85 508 0 [0.00] LCL198-1 theorem 0.2 4 1 669 0 6 0 0 0 5 669 3677 0 [0.00] LCL199-1 theorem 0.1 4 1 297 0 6 0 0 0 5 297 1733 0 [0.00] LCL200-1 theorem 0.1 4 1 134 0 6 0 0 0 5 134 821 0 [0.00] LCL201-1 theorem 1.4 4 1 1415 0 6 0 0 0 6 1415 8247 0 [0.00] LCL202-1 theorem 1.0 4 1 643 0 6 0 0 0 6 643 4095 0 [0.00] LCL203-1 theorem 1.0 4 1 643 0 6 0 0 0 6 643 4095 0 [0.00] LCL204-1 theorem 1.4 4 1 1415 0 6 0 0 0 6 1415 8247 0 [0.00] LCL205-1 theorem 1.1 4 1 643 0 6 0 0 0 6 643 4095 0 [0.00] LCL206-1 theorem 1.0 4 1 643 0 6 0 0 0 6 643 4095 0 [0.00] LCL207-1 theorem 0.9 4 1 486 0 6 0 0 0 6 486 2989 0 [0.00] LCL208-1 theorem 0.2 4 1 589 0 6 0 0 0 5 589 3266 0 [0.00] LCL210-1 theorem 0.2 4 1 591 0 6 0 0 0 5 591 3281 0 [0.00] LCL211-1 theorem 0.2 4 1 586 0 6 0 0 0 5 586 3250 0 [0.00] LCL212-1 theorem 1.6 4 1 1626 0 6 0 0 0 6 1626 9469 0 [0.00] LCL213-1 theorem 1.4 4 1 1400 0 6 0 0 0 6 1400 8113 0 [0.00] LCL214-1 theorem 1.4 5 1 1400 0 6 0 0 0 6 1400 8113 0 [0.00] LCL215-1 theorem 1.5 4 1 1626 0 6 0 0 0 6 1626 9469 0 [0.00] LCL216-1 theorem 0.2 4 1 586 0 6 0 0 0 5 586 3254 0 [0.00] LCL217-1 theorem 0.2 4 1 586 0 6 0 0 0 5 586 3254 0 [0.00] LCL224-1 theorem 31.4 25 1 21624 0 6 0 0 0 6 21624 116526 0 [0.00] LCL226-1 theorem 0.3 4 1 805 0 6 0 0 0 5 805 4335 0 [0.00] LCL236-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 37 0 [0.00] LCL238-1 theorem 0.1 4 1 296 0 6 0 0 0 5 296 1725 0 [0.00] LCL257-1 theorem 0.0 4 1 38 0 2 0 2 0 5 38 840 0 [0.00] LCL355-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 10 0 [0.00] LCL356-1 theorem 0.0 4 1 13 0 4 0 1 0 5 13 106 0 [0.00] LCL357-1 theorem 0.0 4 1 13 0 4 0 1 0 5 13 106 0 [0.00] LCL358-1 theorem 0.0 4 1 18 0 4 0 2 0 5 18 190 0 [0.00] LCL359-1 theorem 0.0 4 1 18 0 4 0 2 0 5 18 175 0 [0.00] LCL360-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 10 0 [0.00] LCL361-1 theorem 0.0 4 1 17 0 4 0 2 0 5 17 152 0 [0.00] LCL362-1 theorem 0.0 4 1 24 0 4 0 2 0 5 24 332 0 [0.00] LCL363-1 theorem 0.0 4 1 24 0 4 0 2 0 5 24 332 0 [0.00] LCL364-1 theorem 0.0 4 1 53 0 4 0 2 0 5 53 1892 0 [0.00] LCL365-1 theorem 0.1 4 1 86 0 4 0 6 0 5 86 4963 0 [0.00] LCL366-1 theorem 0.0 4 1 8 0 4 0 0 0 5 8 38 0 [0.00] LCL367-1 theorem 0.0 4 1 56 0 4 0 4 0 5 56 2097 0 [0.00] LCL384-1 theorem 0.4 4 1 148 0 4 0 10 0 5 148 13496 0 [0.00] LCL397-1 theorem 0.0 4 1 24 0 4 0 2 0 5 24 332 0 [0.00] LCL398-1 theorem 0.0 4 1 6 0 4 0 0 0 5 6 18 0 [0.00] LCL399-1 theorem 0.0 4 1 40 0 4 0 2 0 5 40 1083 0 [0.00] LCL414-1 theorem 0.0 4 1 5 0 4 0 0 0 3 5 13 0 [0.00] LCL428-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 14 0 [0.00] MGT001-1 theorem 0.0 4 1 19 0 10 0 0 0 2 19 22 0 [0.00] MGT002-1 theorem 0.0 4 1 12 0 7 0 0 0 2 12 17 0 [0.00] MGT003-1 theorem 0.0 4 1 12 0 7 0 0 0 2 12 17 0 [0.00] MGT006-1 theorem 0.0 4 1 13 0 8 2 0 0 2 13 13 0 [0.00] MGT008-1 theorem 0.0 4 1 15 0 12 0 0 0 2 15 16 0 [0.00] MGT009-1 theorem 0.0 4 1 15 0 12 0 0 0 2 15 16 0 [0.00] MGT010-1 theorem 0.0 4 1 18 0 13 2 0 0 2 18 18 0 [0.00] MGT015-1 theorem 0.0 4 1 17 0 13 0 0 0 2 17 18 0 [0.00] MGT017-1 theorem 0.0 4 1 17 0 13 0 0 0 2 17 18 0 [0.00] MGT032-2 theorem 0.0 4 1 7 0 2 0 0 0 4 7 7 0 [0.00] MGT036-3 theorem 0.0 4 1 6 0 4 0 0 0 2 6 7 0 [0.00] MSC005-1 theorem 0.1 4 1 50 0 3 0 0 0 4 50 2336 0 [0.00] NLP001-1 theorem 0.0 4 2 28 1 48 5 0 0 2 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 2 14 14 0 [0.00] NLP107-1 non_thm 0.0 4 0 26 0 3 0 0 0 2 26 26 0 [0.00] NLP108-1 non_thm 0.0 4 0 49 0 10 0 0 0 2 49 51 0 [0.00] NLP109-1 non_thm 0.0 4 0 26 0 3 0 0 0 2 26 26 0 [0.00] NLP110-1 non_thm 0.0 4 0 37 0 9 0 0 0 2 37 39 0 [0.00] NLP111-1 non_thm 0.0 4 0 49 0 10 0 0 0 2 49 51 0 [0.00] NLP112-1 non_thm 0.0 4 0 49 0 10 0 0 0 2 49 51 0 [0.00] NLP113-1 non_thm 0.0 4 0 13 0 2 0 0 0 2 13 13 0 [0.00] NUM001-1 theorem 0.1 4 1 38 0 8 0 0 0 3 38 3843 0 [0.00] NUM002-1 theorem 0.1 4 1 34 0 8 0 0 0 3 34 3201 0 [0.00] NUM003-1 theorem 0.1 4 1 40 0 8 0 0 0 3 40 4248 0 [0.00] NUM004-1 theorem 0.1 4 1 33 0 8 0 0 0 3 33 3036 0 [0.00] NUM019-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 14 0 [0.00] NUM020-1 theorem 0.0 4 1 12 0 8 0 0 0 3 12 69 0 [0.00] NUM023-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 21 0 [0.00] NUM024-1 theorem 19.8 43 1 1892 0 8 0 44 0 4 1892 344415 0 [0.00] NUM025-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 17 0 [0.00] PLA001-1 theorem 2.7 8 1 3066 0 12 0 0 0 10 3066 12232 0 [0.00] PLA003-1 theorem 0.0 4 1 8 0 4 2 3 0 2 8 15 0 [0.00] PLA006-1 theorem 0.0 4 1 64 0 20 0 0 0 3 64 1864 0 [0.00] PLA017-1 theorem 0.0 4 1 93 0 20 0 0 0 3 93 2511 0 [0.00] PLA020-1 theorem 0.0 4 1 18 0 18 0 0 0 2 18 93 0 [0.00] PLA022-1 timeout 299.0 396 [0.00] PLA022-2 timeout 299.0 392 [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 299.0 391 [0.00] PUZ003-1 theorem 0.0 4 1 14 0 6 0 0 0 2 14 27 0 [0.00] PUZ008-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 46 0 [0.00] PUZ008-3 theorem 0.0 4 1 27 0 4 0 0 0 6 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 2 34 53 0 [0.00] PUZ038-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 4 0 [0.00] PUZ047-1 theorem 0.0 4 1 36 0 2 0 0 0 7 36 74 0 [0.00] PUZ054-1 non_thm 0.0 4 0 75 0 2 0 0 0 15 75 180 0 [0.00] RNG001-3 theorem 0.0 4 1 18 0 4 0 1 0 2 18 690 0 [0.00] RNG001-5 theorem 2.0 8 1 66 0 8 0 3 0 2 66 77990 0 [0.00] RNG005-2 theorem 0.0 4 1 11 0 11 0 0 0 2 11 803 0 [0.00] RNG006-2 theorem 175.7 257 1 209 0 13 0 9 0 2 209 4161376 0 [0.00] RNG037-2 theorem 0.1 4 1 15 0 9 0 0 0 2 15 1589 0 [0.00] RNG038-2 theorem 3.7 12 1 69 0 9 0 0 0 2 69 137142 0 [0.00] RNG039-2 theorem 2.7 10 1 64 0 50 0 7 0 2 64 73141 0 [0.00] SWV010-1 non_thm 0.0 4 0 8 0 5 0 0 0 6 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 7 0 [0.00] SYN035-1 theorem 0.0 4 1 2 0 2 6 0 0 2 2 2 0 [0.00] SYN040-1 theorem 0.0 4 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 4 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 5 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 4 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 4 0 [0.00] SYN068-1 theorem 0.0 4 1 6 0 1 0 0 0 2 6 7 0 [0.00] SYN079-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 4 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 4 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 1045 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 4 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 2 17 29 0 [0.00] SYN102-1.007.007 theorem 0.6 4 1 3854 0 14 2 0 0 2 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 208 0 [0.00] SYN106-1 theorem 0.0 4 1 17 0 24 30 0 0 2 17 166 0 [0.00] SYN107-1 theorem 0.0 4 1 37 0 116 51 0 0 2 37 370 0 [0.00] SYN108-1 theorem 0.0 4 1 37 0 117 51 0 0 2 37 370 0 [0.00] SYN109-1 theorem 0.0 4 1 129 0 234 134 1 0 2 129 900 0 [0.00] SYN110-1 theorem 0.1 4 1 252 0 255 159 6 0 2 252 2060 0 [0.00] SYN111-1 theorem 0.1 4 1 234 0 255 155 6 0 2 234 1917 0 [0.00] SYN112-1 theorem 0.0 4 1 37 0 115 52 0 0 2 37 370 0 [0.00] SYN113-1 theorem 0.0 4 1 60 0 218 89 0 0 2 60 493 0 [0.00] SYN114-1 theorem 0.0 4 1 39 0 119 60 0 0 2 39 388 0 [0.00] SYN115-1 theorem 0.1 4 1 208 0 252 155 4 0 2 208 1846 0 [0.00] SYN116-1 theorem 0.0 4 1 93 0 231 127 1 0 2 93 707 0 [0.00] SYN117-1 theorem 0.1 4 1 93 0 231 126 1 0 2 93 707 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 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN120-1 theorem 0.0 4 1 17 0 25 30 0 0 2 17 165 0 [0.00] SYN121-1 theorem 0.0 4 1 70 0 225 109 1 0 2 70 549 0 [0.00] SYN122-1 theorem 0.0 4 1 70 0 225 109 1 0 2 70 549 0 [0.00] SYN123-1 theorem 0.0 4 1 34 0 57 35 0 0 2 34 326 0 [0.00] SYN124-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 [0.00] SYN125-1 theorem 0.1 4 1 274 0 256 162 6 0 2 274 2213 0 [0.00] SYN126-1 theorem 0.0 4 1 47 0 189 78 0 0 2 47 435 0 [0.00] SYN127-1 theorem 0.0 4 1 47 0 189 78 0 0 2 47 435 0 [0.00] SYN128-1 theorem 0.0 4 1 57 0 218 87 0 0 2 57 470 0 [0.00] SYN129-1 theorem 0.0 4 1 56 0 218 86 0 0 2 56 463 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 135 0 [0.00] SYN133-1 theorem 0.0 4 1 5 0 4 9 0 0 2 5 52 0 [0.00] SYN134-1 theorem 0.0 4 1 59 0 219 89 0 0 2 59 486 0 [0.00] SYN135-1 theorem 0.0 4 1 40 0 124 64 0 0 2 40 391 0 [0.00] SYN136-1 theorem 0.0 4 1 40 0 123 64 0 0 2 40 391 0 [0.00] SYN137-1 theorem 0.0 4 1 85 0 231 122 1 0 2 85 662 0 [0.00] SYN138-1 theorem 0.1 4 1 237 0 254 156 6 0 2 237 1951 0 [0.00] SYN139-1 theorem 0.1 4 1 295 0 257 164 6 0 2 295 2366 0 [0.00] SYN140-1 theorem 0.1 4 1 295 0 257 164 6 0 2 295 2366 0 [0.00] SYN141-1 theorem 0.1 4 1 209 0 253 154 4 0 2 209 1858 0 [0.00] SYN142-1 theorem 0.1 4 1 296 0 259 167 6 0 2 296 2374 0 [0.00] SYN143-1 theorem 0.1 4 1 296 0 259 167 6 0 2 296 2374 0 [0.00] SYN144-1 theorem 0.1 4 1 227 0 254 154 4 0 2 227 1887 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 44 0 [0.00] SYN147-1 theorem 0.0 4 1 6 0 8 13 0 0 2 6 60 0 [0.00] SYN148-1 theorem 0.1 4 1 133 0 234 135 1 0 2 133 954 0 [0.00] SYN149-1 theorem 0.0 4 1 12 0 20 30 0 0 2 12 135 0 [0.00] SYN150-1 theorem 0.0 4 1 36 0 94 45 0 0 2 36 358 0 [0.00] SYN151-1 theorem 0.0 4 1 36 0 94 45 0 0 2 36 358 0 [0.00] SYN152-1 theorem 0.0 4 1 36 0 95 46 0 0 2 36 358 0 [0.00] SYN153-1 theorem 0.0 4 1 41 0 143 65 0 0 2 41 397 0 [0.00] SYN154-1 theorem 0.0 4 1 41 0 143 65 0 0 2 41 397 0 [0.00] SYN155-1 theorem 0.1 4 1 188 0 245 147 3 0 2 188 1578 0 [0.00] SYN156-1 theorem 0.1 4 1 203 0 252 152 4 0 2 203 1839 0 [0.00] SYN157-1 theorem 0.0 4 1 51 0 206 83 0 0 2 51 443 0 [0.00] SYN158-1 theorem 0.0 4 1 51 0 206 82 0 0 2 51 443 0 [0.00] SYN159-1 theorem 0.1 4 1 189 0 248 147 3 0 2 189 1609 0 [0.00] SYN160-1 theorem 0.0 4 1 51 0 206 82 0 0 2 51 443 0 [0.00] SYN161-1 theorem 0.0 4 1 51 0 206 82 0 0 2 51 443 0 [0.00] SYN162-1 theorem 0.0 4 1 51 0 206 82 0 0 2 51 443 0 [0.00] SYN164-1 theorem 0.0 4 1 7 0 10 16 0 0 2 7 78 0 [0.00] SYN165-1 theorem 0.0 4 1 5 0 6 10 0 0 2 5 48 0 [0.00] SYN166-1 theorem 0.1 4 1 141 0 236 137 2 0 2 141 1037 0 [0.00] SYN167-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 [0.00] SYN168-1 theorem 0.0 4 1 39 0 119 61 0 0 2 39 387 0 [0.00] SYN169-1 theorem 0.0 4 1 39 0 119 61 0 0 2 39 387 0 [0.00] SYN170-1 theorem 0.0 4 1 43 0 164 67 0 0 2 43 424 0 [0.00] SYN171-1 theorem 0.1 4 1 386 0 264 170 6 0 2 386 2976 0 [0.00] SYN172-1 theorem 0.0 4 1 6 0 7 12 0 0 2 6 71 0 [0.00] SYN173-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN174-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN175-1 theorem 0.0 4 1 35 0 77 38 0 0 2 35 347 0 [0.00] SYN176-1 theorem 0.0 4 1 70 0 225 107 1 0 2 70 547 0 [0.00] SYN177-1 theorem 0.1 4 1 148 0 240 138 3 0 2 148 1157 0 [0.00] SYN178-1 theorem 0.1 4 1 77 0 229 114 1 0 2 77 604 0 [0.00] SYN179-1 theorem 0.0 4 1 164 0 242 145 3 0 2 164 1272 0 [0.00] SYN180-1 theorem 0.1 4 1 78 0 229 115 1 0 2 78 608 0 [0.00] SYN181-1 theorem 0.0 4 1 75 0 229 113 1 0 2 75 583 0 [0.00] SYN182-1 theorem 0.0 4 1 49 0 198 80 0 0 2 49 438 0 [0.00] SYN183-1 theorem 0.0 4 1 49 0 198 80 0 0 2 49 438 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 4 1 1 0 1 0 0 0 2 1 39 0 [0.00] SYN186-1 theorem 0.0 4 1 37 0 116 51 0 0 2 37 371 0 [0.00] SYN187-1 theorem 0.0 4 1 37 0 117 51 0 0 2 37 371 0 [0.00] SYN188-1 theorem 0.0 4 1 37 0 116 51 0 0 2 37 371 0 [0.00] SYN189-1 theorem 0.0 4 1 38 0 119 52 0 0 2 38 377 0 [0.00] SYN190-1 theorem 0.1 4 1 177 0 244 147 3 0 2 177 1476 0 [0.00] SYN191-1 theorem 0.0 4 1 155 0 239 138 3 0 2 155 1240 0 [0.00] SYN192-1 theorem 0.1 4 1 161 0 239 141 3 0 2 161 1265 0 [0.00] SYN193-1 theorem 0.1 4 1 161 0 239 141 3 0 2 161 1265 0 [0.00] SYN194-1 theorem 0.0 4 1 119 0 233 134 1 0 2 119 808 0 [0.00] SYN195-1 theorem 0.0 4 1 93 0 231 126 1 0 2 93 701 0 [0.00] SYN196-1 theorem 0.0 4 1 68 0 221 92 0 0 2 68 522 0 [0.00] SYN197-1 theorem 0.0 4 1 8 0 15 20 0 0 2 8 80 0 [0.00] SYN198-1 theorem 0.0 4 1 68 0 222 92 0 0 2 68 522 0 [0.00] SYN199-1 theorem 0.0 4 1 68 0 221 92 0 0 2 68 522 0 [0.00] SYN200-1 theorem 0.1 4 1 68 0 220 92 0 0 2 68 522 0 [0.00] SYN201-1 theorem 0.0 4 1 68 0 220 92 0 0 2 68 511 0 [0.00] SYN202-1 theorem 0.0 4 1 78 0 229 116 1 0 2 78 612 0 [0.00] SYN203-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 [0.00] SYN204-1 theorem 0.1 4 1 294 0 257 163 6 0 2 294 2354 0 [0.00] SYN205-1 theorem 0.1 4 1 294 0 257 163 6 0 2 294 2354 0 [0.00] SYN206-1 theorem 0.1 4 1 81 0 229 120 1 0 2 81 638 0 [0.00] SYN207-1 theorem 0.1 4 1 288 0 257 163 6 0 2 288 2301 0 [0.00] SYN208-1 theorem 0.0 4 1 82 0 231 121 1 0 2 82 645 0 [0.00] SYN209-1 theorem 0.1 4 1 122 0 233 134 1 0 2 122 815 0 [0.00] SYN210-1 theorem 0.0 4 1 118 0 233 133 1 0 2 118 794 0 [0.00] SYN211-1 theorem 0.0 4 1 59 0 218 88 0 0 2 59 483 0 [0.00] SYN212-1 theorem 0.0 4 1 114 0 233 130 1 0 2 114 779 0 [0.00] SYN213-1 theorem 0.1 4 1 162 0 240 142 3 0 2 162 1271 0 [0.00] SYN214-1 theorem 0.1 4 1 162 0 240 142 3 0 2 162 1271 0 [0.00] SYN215-1 theorem 0.0 4 1 162 0 240 142 3 0 2 162 1271 0 [0.00] SYN216-1 theorem 0.0 4 1 68 0 220 92 0 0 2 68 516 0 [0.00] SYN217-1 theorem 0.0 4 1 69 0 222 101 1 0 2 69 541 0 [0.00] SYN218-1 theorem 0.0 4 1 68 0 222 93 0 0 2 68 516 0 [0.00] SYN219-1 theorem 0.0 4 1 70 0 226 109 1 0 2 70 549 0 [0.00] SYN220-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 [0.00] SYN221-1 theorem 0.0 4 1 41 0 142 67 0 0 2 41 396 0 [0.00] SYN222-1 theorem 0.0 4 1 41 0 142 66 0 0 2 41 396 0 [0.00] SYN223-1 theorem 0.0 4 1 41 0 143 65 0 0 2 41 396 0 [0.00] SYN224-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 [0.00] SYN225-1 theorem 0.0 4 1 74 0 230 113 1 0 2 74 582 0 [0.00] SYN226-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 [0.00] SYN227-1 theorem 0.1 4 1 272 0 256 162 6 0 2 272 2196 0 [0.00] SYN228-1 theorem 0.1 4 1 128 0 235 134 1 0 2 128 881 0 [0.00] SYN229-1 theorem 0.0 4 1 41 0 142 66 0 0 2 41 396 0 [0.00] SYN230-1 theorem 0.0 4 1 41 0 142 66 0 0 2 41 396 0 [0.00] SYN231-1 theorem 0.0 4 1 41 0 142 67 0 0 2 41 396 0 [0.00] SYN232-1 theorem 0.0 4 1 41 0 142 66 0 0 2 41 396 0 [0.00] SYN233-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 [0.00] SYN234-1 theorem 0.0 4 1 74 0 229 113 1 0 2 74 582 0 [0.00] SYN235-1 theorem 0.0 4 1 130 0 234 134 1 0 2 130 931 0 [0.00] SYN236-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 [0.00] SYN237-1 theorem 0.0 4 1 6 0 8 13 0 0 2 6 66 0 [0.00] SYN238-1 theorem 0.0 4 1 4 0 4 6 0 0 2 4 43 0 [0.00] SYN239-1 theorem 0.0 4 1 4 0 5 9 0 0 2 4 45 0 [0.00] SYN240-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 135 0 [0.00] SYN241-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 135 0 [0.00] SYN242-1 theorem 0.0 4 1 27 0 33 35 0 0 2 27 269 0 [0.00] SYN243-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN244-1 theorem 0.0 4 1 4 0 4 9 0 0 2 4 45 0 [0.00] SYN245-1 theorem 0.0 4 1 12 0 18 31 0 0 2 12 135 0 [0.00] SYN246-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN247-1 theorem 0.0 4 1 6 0 10 12 0 0 2 6 66 0 [0.00] SYN248-1 theorem 0.0 4 1 57 0 218 87 0 0 2 57 468 0 [0.00] SYN249-1 theorem 0.0 4 1 56 0 218 86 0 0 2 56 461 0 [0.00] SYN250-1 theorem 0.1 4 1 257 0 254 161 6 0 2 257 2097 0 [0.00] SYN251-1 theorem 0.0 4 1 30 0 36 34 0 0 2 30 297 0 [0.00] SYN252-1 theorem 0.1 4 1 295 0 257 164 6 0 2 295 2366 0 [0.00] SYN253-1 theorem 0.1 4 1 295 0 258 164 6 0 2 295 2366 0 [0.00] SYN254-1 theorem 0.1 4 1 295 0 257 164 6 0 2 295 2366 0 [0.00] SYN255-1 theorem 0.0 4 1 36 0 94 46 0 0 2 36 358 0 [0.00] SYN256-1 theorem 0.0 4 1 36 0 94 46 0 0 2 36 358 0 [0.00] SYN257-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 [0.00] SYN258-1 theorem 0.0 4 1 7 0 11 16 0 0 2 7 77 0 [0.00] SYN259-1 theorem 0.0 4 1 7 0 11 16 0 0 2 7 77 0 [0.00] SYN260-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 [0.00] SYN261-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 135 0 [0.00] SYN262-1 theorem 0.0 4 1 61 0 219 89 0 0 2 61 500 0 [0.00] SYN263-1 theorem 0.0 4 1 140 0 236 136 1 0 2 140 1015 0 [0.00] SYN264-1 theorem 0.1 4 1 247 0 254 158 6 0 2 247 2028 0 [0.00] SYN265-1 theorem 0.0 4 1 40 0 123 64 0 0 2 40 390 0 [0.00] SYN266-1 theorem 0.1 4 1 170 0 243 146 3 0 2 170 1333 0 [0.00] SYN267-1 theorem 0.0 4 1 43 0 165 66 0 0 2 43 424 0 [0.00] SYN268-1 theorem 0.0 4 1 43 0 164 66 0 0 2 43 424 0 [0.00] SYN269-1 theorem 0.1 4 1 384 0 264 170 6 0 2 384 2958 0 [0.00] SYN270-1 theorem 0.1 4 1 173 0 244 147 3 0 2 173 1386 0 [0.00] SYN271-1 theorem 0.1 4 1 386 0 264 170 6 0 2 386 2976 0 [0.00] SYN272-1 theorem 0.0 4 1 97 0 233 128 1 0 2 97 736 0 [0.00] SYN273-1 theorem 0.0 4 1 96 0 233 128 1 0 2 96 723 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 135 0 [0.00] SYN277-1 theorem 0.0 4 1 6 0 10 11 0 0 2 6 53 0 [0.00] SYN278-1 theorem 0.0 4 1 4 0 5 9 0 0 2 4 47 0 [0.00] SYN279-1 theorem 0.0 4 1 13 0 19 29 0 0 2 13 136 0 [0.00] SYN280-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 47 0 [0.00] SYN281-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 [0.00] SYN282-1 theorem 0.0 4 1 6 0 9 12 0 0 2 6 53 0 [0.00] SYN283-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN284-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN285-1 theorem 0.1 4 1 144 0 238 138 3 0 2 144 1096 0 [0.00] SYN286-1 theorem 0.0 4 1 17 0 23 30 0 0 2 17 160 0 [0.00] SYN287-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 47 0 [0.00] SYN288-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN289-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN290-1 theorem 0.0 4 1 6 0 10 10 0 0 2 6 53 0 [0.00] SYN291-1 theorem 0.0 4 1 6 0 10 12 0 0 2 6 53 0 [0.00] SYN292-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN293-1 theorem 0.0 4 1 55 0 218 85 0 0 2 55 455 0 [0.00] SYN294-1 theorem 0.0 4 1 55 0 218 86 0 0 2 55 455 0 [0.00] SYN295-1 theorem 0.0 4 1 27 0 34 35 0 0 2 27 269 0 [0.00] SYN296-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 [0.00] SYN297-1 theorem 0.0 4 1 27 0 34 34 0 0 2 27 269 0 [0.00] SYN298-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 [0.00] SYN299-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 [0.00] SYN300-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 [0.00] SYN301-1 theorem 0.1 4 1 110 0 233 130 1 0 2 110 759 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 14 0 2 0 0 0 3 14 34 0 [0.00] SYN311-1 theorem 3.6 14 1 15758 0 2 0 0 0 3 15758 63027 0 [0.00] SYN312-1 theorem 38.1 12 1 6733 0 3 0 0 0 3 6733 147238 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 4 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 4 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 14 0 7 0 0 0 3 14 196 0 [0.00] SYN555-1 theorem 0.0 4 1 8 0 6 0 0 0 2 8 40 0 [0.00] SYN557-1 timeout 299.0 237 [0.00] SYN558-1 theorem 0.0 4 1 16 0 6 0 0 0 2 16 97 0 [0.00] SYN559-1 theorem 0.1 4 1 40 0 6 0 0 0 3 40 4367 0 [0.00] SYN561-1 theorem 1.5 9 1 76 0 6 0 0 0 4 76 16512 0 [0.00] SYN562-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 30 0 [0.00] SYN563-1 theorem 0.0 4 1 42 0 6 0 0 0 3 42 326 0 [0.00] SYN564-1 theorem 0.1 4 1 38 0 7 0 0 0 4 38 1577 0 [0.00] SYN565-1 theorem 0.1 4 1 56 0 7 0 0 0 4 56 3566 0 [0.00] SYN566-1 theorem 0.0 4 1 16 0 8 0 0 0 3 16 56 0 [0.00] SYN569-1 theorem 0.0 4 1 36 0 7 0 0 0 3 36 1558 0 [0.00] SYN570-1 theorem 0.0 4 1 16 0 10 0 0 0 3 16 57 0 [0.00] SYN572-1 theorem 1.5 5 1 141 0 9 0 0 0 5 141 12319 0 [0.00] SYN577-1 theorem 0.5 5 1 80 0 12 0 0 0 3 80 17155 0 [0.00] SYN584-1 theorem 0.0 4 1 10 0 9 0 0 0 8 10 39 0 [0.00] SYN588-1 theorem 0.0 4 1 12 0 12 0 0 0 2 12 73 0 [0.00] SYN589-1 theorem 0.0 4 1 12 0 12 0 0 0 2 12 73 0 [0.00] SYN590-1 theorem 0.0 4 1 57 0 8 0 0 0 4 57 225 0 [0.00] SYN596-1 theorem 0.0 4 1 12 0 11 0 0 0 5 12 35 0 [0.00] SYN597-1 theorem 0.9 8 1 214 0 11 0 0 0 4 214 15987 0 [0.00] SYN601-1 theorem 1.0 8 1 241 0 12 0 0 0 4 241 17330 0 [0.00] SYN602-1 theorem 1.6 10 1 114 0 7 0 0 0 3 114 49618 0 [0.00] SYN603-1 timeout 299.0 350 [0.00] SYN616-1 theorem 3.3 18 1 155 0 13 0 0 0 3 155 63503 0 [0.00] SYN618-1 theorem 0.0 4 1 32 0 16 0 0 0 3 32 163 0 [0.00] SYN628-1 theorem 1.3 10 1 111 0 15 0 0 0 3 111 27100 0 [0.00] SYN629-1 theorem 1.3 10 1 111 0 15 0 0 0 3 111 27100 0 [0.00] SYN632-1 theorem 0.0 4 1 24 0 12 0 0 0 7 24 115 0 [0.00] SYN637-1 theorem 0.0 4 1 25 0 14 0 0 0 7 25 270 0 [0.00] SYN638-1 theorem 0.0 4 1 25 0 14 0 0 0 7 25 270 0 [0.00] SYN651-1 theorem 0.0 4 1 25 0 15 0 0 0 6 25 79 0 [0.00] SYN652-1 theorem 0.0 4 1 27 0 20 0 0 0 3 27 96 0 [0.00] SYN688-1 theorem 0.0 4 1 41 0 28 0 0 0 3 41 243 0 [0.00] SYN689-1 theorem 0.0 4 1 41 0 28 0 0 0 3 41 243 0 [0.00] SYN691-1 theorem 0.0 4 1 32 0 24 0 0 0 8 32 110 0 [0.00] SYN702-1 theorem 0.0 4 1 34 0 28 0 0 0 9 34 110 0 [0.00] SYN703-1 theorem 0.0 4 1 37 0 29 0 0 0 9 37 119 0 [0.00] SYN705-1 theorem 0.0 4 1 37 0 29 0 0 0 9 37 119 0 [0.00] SYN706-1 theorem 0.0 4 1 56 0 31 0 1 0 6 56 313 0 [0.00] SYN709-1 theorem 0.0 4 1 47 0 35 0 0 0 4 47 152 0 [0.00] SYN712-1 theorem 0.0 4 1 44 0 36 0 0 0 10 44 141 0 [0.00] SYN715-1 theorem 0.0 4 1 44 0 36 0 0 0 10 44 143 0 [0.00] SYN716-1 theorem 0.0 4 1 43 0 36 0 0 0 10 43 138 0 [0.00] SYN719-1 theorem 0.0 4 1 49 0 46 0 0 0 3 49 137 0 [0.00] SYN720-1 non_thm 0.1 4 0 423 0 264 171 6 0 2 423 3107 0 [0.00] SYN721-1 theorem 0.0 4 1 3 0 1 0 0 0 2 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 41 0 1 0 0 0 4 41 161 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 3 13 16 0 [0.11] SYN163-1 theorem 0.1 4 1 189 0 248 147 3 0 2 189 1609 0 [0.14] NUM286-1 timeout 298.9 25 [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 299.0 300 [0.14] SWV015-1 timeout 299.0 286 [0.14] SWV017-1 memory 238.0 399 [0.14] SYN303-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 5 0 [0.17] LCL004-1 theorem 2.0 8 1 305 0 2 0 197 0 8 305 33507 0 [0.17] LCL012-1 theorem 11.8 19 1 477 0 2 0 0 0 7 477 145358 0 [0.17] LCL014-1 theorem 5.3 12 1 340 0 2 0 1 0 7 340 74086 0 [0.17] LCL015-1 theorem 27.4 33 1 617 0 2 0 0 0 8 617 246104 0 [0.17] LCL016-1 theorem 27.3 32 1 692 0 2 0 0 0 8 692 278115 0 [0.17] LCL018-1 theorem 18.6 26 1 530 0 2 0 0 0 9 530 172961 0 [0.17] LCL026-1 theorem 1.7 5 1 282 0 4 0 3 0 5 282 50760 0 [0.17] LCL030-1 theorem 3.0 8 1 323 0 5 0 9 0 5 323 73396 0 [0.17] LCL031-1 theorem 14.0 23 1 590 0 5 0 23 0 5 590 241566 0 [0.17] LCL034-1 theorem 0.7 4 1 182 0 2 0 9 0 7 182 23761 0 [0.17] LCL036-1 theorem 0.1 4 1 74 0 2 0 5 0 7 74 4320 0 [0.17] LCL039-1 theorem 3.6 7 1 684 0 6 0 4 0 5 684 113674 0 [0.17] LCL042-1 theorem 11.5 21 1 719 0 6 0 16 0 5 719 222710 0 [0.17] LCL048-1 theorem 0.1 4 1 55 0 4 0 3 0 5 55 2006 0 [0.17] LCL049-1 theorem 0.1 4 1 88 0 4 0 6 0 5 88 5205 0 [0.17] LCL050-1 theorem 0.1 4 1 89 0 4 0 6 0 5 89 5347 0 [0.17] LCL051-1 theorem 0.2 4 1 93 0 4 0 6 0 5 93 5983 0 [0.17] LCL052-1 theorem 0.2 4 1 100 0 4 0 9 0 5 100 6551 0 [0.17] LCL053-1 theorem 0.2 4 1 101 0 4 0 9 0 5 101 6701 0 [0.17] LCL055-1 theorem 0.2 4 1 94 0 4 0 7 0 5 94 6029 0 [0.17] LCL056-1 theorem 0.2 4 1 95 0 4 0 7 0 5 95 6098 0 [0.17] LCL057-1 theorem 0.3 4 1 139 0 4 0 10 0 5 139 11960 0 [0.17] LCL058-1 theorem 9.9 19 1 674 0 4 0 14 0 5 674 197697 0 [0.17] LCL059-1 theorem 0.3 4 1 136 0 4 0 10 0 5 136 11633 0 [0.17] LCL060-1 theorem 17.2 29 1 824 0 4 0 17 0 5 824 294458 0 [0.17] LCL067-1 theorem 87.4 103 1 2025 0 4 0 101 0 5 2025 1143123 0 [0.17] LCL068-1 theorem 2.0 5 1 419 0 4 0 9 0 5 419 58290 0 [0.17] LCL070-1 theorem 1.9 5 1 404 0 4 0 7 0 5 404 54339 0 [0.17] LCL071-1 theorem 2.8 7 1 447 0 4 0 7 0 5 447 72754 0 [0.17] LCL072-1 theorem 1.6 5 1 381 0 4 0 7 0 5 381 45161 0 [0.17] LCL080-1 theorem 0.4 4 1 123 0 4 0 2 0 5 123 12569 0 [0.17] LCL080-2 theorem 0.4 4 1 123 0 5 0 2 0 5 123 12570 0 [0.17] LCL092-1 theorem 0.2 4 1 83 0 2 0 12 0 6 83 5090 0 [0.17] LCL093-1 theorem 2.5 6 1 278 0 2 0 12 0 6 278 62673 0 [0.17] LCL095-1 theorem 0.1 4 1 70 0 2 0 12 0 6 70 3550 0 [0.17] LCL103-1 theorem 6.1 11 1 358 0 3 0 0 0 6 358 92038 0 [0.17] LCL113-1 theorem 5.0 12 1 476 0 5 0 4 0 5 476 108208 0 [0.17] LCL114-1 theorem 16.6 30 1 781 0 5 0 14 0 5 781 279231 0 [0.17] LCL115-1 theorem 0.6 4 1 206 0 5 0 2 0 5 206 22319 0 [0.17] LCL116-1 theorem 16.9 29 1 783 0 5 0 14 0 5 783 280779 0 [0.17] LCL121-1 theorem 5.1 11 1 318 0 2 0 3 0 7 318 69600 0 [0.17] LCL127-1 theorem 143.9 111 1 1107 0 2 0 5 0 7 1107 920083 0 [0.17] LCL128-1 theorem 0.6 4 1 126 0 2 0 1 0 7 126 11312 0 [0.17] LCL129-1 theorem 107.0 56 1 479 0 2 0 2 0 6 479 158052 0 [0.17] LCL131-1 theorem 0.6 4 1 150 0 2 0 1 0 5 150 16860 0 [0.17] LCL191-1 theorem 3.4 7 1 4171 0 6 0 0 0 6 4171 23289 0 [0.17] LCL195-1 theorem 4.5 8 1 5123 0 6 0 0 0 6 5123 28495 0 [0.17] LCL218-1 timeout 299.0 98 [0.17] LCL225-1 theorem 31.5 25 1 21624 0 6 0 0 0 6 21624 116526 0 [0.17] LCL230-1 timeout 299.0 99 [0.17] LCL231-1 timeout 299.0 97 [0.17] LCL234-1 theorem 2.3 5 1 2604 0 6 0 0 0 6 2604 15109 0 [0.17] LCL237-1 theorem 2.3 5 1 2605 0 6 0 0 0 6 2605 15118 0 [0.17] LCL250-1 theorem 5.9 9 1 6332 0 6 0 0 0 6 6332 35419 0 [0.17] LCL256-1 theorem 0.2 4 1 96 0 4 0 7 0 5 96 6237 0 [0.17] LCL368-1 theorem 0.2 4 1 107 0 4 0 9 0 5 107 7306 0 [0.17] LCL370-1 theorem 0.7 4 1 192 0 4 0 10 0 5 192 20275 0 [0.17] LCL371-1 theorem 0.6 4 1 192 0 4 0 10 0 5 192 20275 0 [0.17] LCL372-1 theorem 0.7 4 1 201 0 4 0 10 0 5 201 21611 0 [0.17] LCL373-1 theorem 0.9 5 1 231 0 4 0 11 0 5 231 26519 0 [0.17] LCL374-1 theorem 149.4 161 1 1933 0 4 0 23 0 5 1933 1490150 0 [0.17] LCL378-1 theorem 0.2 4 1 93 0 4 0 6 0 5 93 5983 0 [0.17] LCL379-1 theorem 0.3 4 1 136 0 4 0 10 0 5 136 11707 0 [0.17] LCL380-1 theorem 0.2 4 1 94 0 4 0 7 0 5 94 6029 0 [0.17] LCL381-1 theorem 0.2 4 1 96 0 4 0 7 0 5 96 6237 0 [0.17] LCL382-1 theorem 4.7 11 1 450 0 4 0 12 0 5 450 103836 0 [0.17] LCL383-1 theorem 6.5 15 1 527 0 4 0 12 0 5 527 131927 0 [0.17] LCL385-1 theorem 4.8 12 1 450 0 4 0 12 0 5 450 103836 0 [0.17] LCL386-1 theorem 0.8 4 1 215 0 4 0 10 0 5 215 24276 0 [0.17] LCL387-1 theorem 1.0 5 1 240 0 4 0 12 0 5 240 28748 0 [0.17] LCL388-1 theorem 10.0 19 1 676 0 4 0 14 0 5 676 198407 0 [0.17] LCL389-1 theorem 4.8 12 1 452 0 4 0 12 0 5 452 104910 0 [0.17] LCL390-1 theorem 17.3 31 1 823 0 4 0 17 0 5 823 294109 0 [0.17] LCL396-1 theorem 0.3 4 1 140 0 4 0 10 0 5 140 12055 0 [0.17] LCL400-1 theorem 0.2 4 1 117 0 4 0 9 0 5 117 8788 0 [0.17] LCL401-1 theorem 0.8 5 1 222 0 4 0 10 0 5 222 25365 0 [0.17] LCL402-1 theorem 0.3 4 1 136 0 4 0 10 0 5 136 11707 0 [0.17] LCL405-1 theorem 0.3 4 1 139 0 4 0 10 0 5 139 11966 0 [0.17] LCL416-1 theorem 16.5 21 1 507 0 2 0 1 0 10 507 127926 0 [0.17] NUM017-1 timeout 299.0 291 [0.17] NUM283-1.005 theorem 25.6 8 1 601 0 4 0 0 0 121 601 678 0 [0.17] NUM284-1.014 theorem 171.5 12 1 249 0 4 0 0 0 378 249 251 0 [0.17] PLA004-1 timeout 299.0 390 [0.17] PLA004-2 timeout 299.0 390 [0.17] PLA005-1 timeout 299.0 397 [0.17] PLA005-2 timeout 299.0 390 [0.17] PLA009-1 memory 292.9 399 [0.17] PLA009-2 timeout 299.0 387 [0.17] PLA011-1 timeout 299.0 388 [0.17] PLA011-2 timeout 299.0 395 [0.17] PLA013-1 timeout 299.0 388 [0.17] PLA014-1 timeout 299.0 387 [0.17] PLA014-2 timeout 299.0 389 [0.17] PLA021-1 timeout 299.0 387 [0.17] SWV014-1 timeout 299.0 324 [0.17] SYN556-1 timeout 299.0 331 [0.17] SYN598-1 timeout 299.0 326 [0.17] SYN599-1 timeout 299.0 318 [0.17] SYN631-1 timeout 299.0 305 [0.17] SYN639-1 timeout 299.0 112 [0.17] SYN640-1 timeout 299.0 107 [0.17] SYN646-1 timeout 299.0 140 [0.17] SYN647-1 timeout 299.0 148 [0.17] SYN649-1 timeout 299.0 179 [0.17] SYN654-1 timeout 299.0 71 [0.17] SYN655-1 timeout 299.0 72 [0.17] SYN704-1 timeout 299.0 112 [0.17] SYN707-1 timeout 299.0 329 [0.17] SYN708-1 timeout 299.0 331 [0.22] LAT005-1 theorem 0.4 4 1 150 0 17 0 0 0 2 150 7301 0 [0.22] PUZ036-1.005 theorem 0.2 4 1 605 0 2 0 0 0 2 605 1812 0 [0.22] PUZ037-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 20 0 [0.22] PUZ037-2 theorem 0.5 4 1 118 0 2 0 0 0 2 118 2100 0 [0.29] GRP394-2 timeout 299.0 351 [0.29] SWV016-1 timeout 299.0 281 [0.29] SWV018-1 memory 245.6 399 [0.33] LCL003-1 theorem 90.6 41 1 2442 0 2 0 406 0 8 2442 2018442 0 [0.33] LCL017-1 theorem 27.9 38 1 627 0 2 0 0 0 9 627 240493 0 [0.33] LCL019-1 timeout 299.0 175 [0.33] LCL024-1 theorem 225.4 136 1 1628 0 2 0 0 0 8 1628 1521134 0 [0.33] LCL028-1 theorem 19.0 30 1 740 0 4 0 66 0 5 740 326174 0 [0.33] LCL038-1 theorem 245.0 140 1 2051 0 2 0 134 0 7 2051 3034718 0 [0.33] LCL040-1 theorem 3.8 10 1 481 0 6 0 51 0 5 481 91205 0 [0.33] LCL054-1 theorem 12.9 23 1 746 0 4 0 15 0 5 746 239168 0 [0.33] LCL085-1 theorem 20.3 6 1 750 0 2 0 98 0 7 750 352388 0 [0.33] LCL099-1 timeout 299.0 128 [0.33] LCL122-1 theorem 70.6 58 1 894 0 2 0 3 0 7 894 540873 0 [0.33] LCL221-1 theorem 27.4 24 1 19817 0 6 0 0 0 6 19817 106777 0 [0.33] LCL222-1 theorem 29.8 25 1 21122 0 6 0 0 0 6 21122 112797 0 [0.33] LCL223-1 theorem 34.9 26 1 23044 0 6 0 0 0 6 23044 123999 0 [0.33] LCL227-1 timeout 299.0 99 [0.33] LCL369-1 theorem 0.2 4 1 107 0 4 0 9 0 5 107 7401 0 [0.33] LCL391-1 theorem 70.5 90 1 1452 0 4 0 18 0 5 1452 869079 0 [0.33] LCL392-1 theorem 17.4 31 1 824 0 4 0 17 0 5 824 294458 0 [0.33] LCL403-1 theorem 10.1 19 1 676 0 4 0 14 0 5 676 198407 0 [0.33] LCL404-1 theorem 4.8 12 1 452 0 4 0 12 0 5 452 104910 0 [0.33] PLA007-1 memory 292.3 399 [0.33] PLA008-1 timeout 299.0 388 [0.33] PLA010-1 timeout 299.0 389 [0.33] PLA012-1 timeout 299.0 391 [0.33] PLA015-1 timeout 299.0 387 [0.33] PLA016-1 timeout 299.0 391 [0.33] PLA018-1 timeout 299.0 395 [0.33] PLA019-1 timeout 299.0 395 [0.33] PLA023-1 timeout 299.0 389 [0.33] PUZ039-1 theorem 8.8 30 1 10655 0 2 0 0 0 6 10655 28569 0 [0.33] PUZ040-1 theorem 0.1 4 1 67 0 2 0 0 0 6 67 194 0 [0.33] PUZ042-1 theorem 62.4 141 1 63506 0 2 0 0 0 6 63506 173714 0 [0.33] RNG001-2 theorem 48.2 100 1 163 0 7 0 18 0 2 163 1387441 0 [0.33] RNG004-3 timeout 299.0 381 [0.33] SYN600-1 timeout 299.0 329 [0.33] SYN653-1 timeout 298.9 70 [0.33] SYN711-1 timeout 299.0 344 [0.43] LCL411-1 timeout 299.0 98 [0.43] LCL415-1 crash 64.0 97 [0.43] NUM286-2 timeout 299.0 303 [0.43] PUZ049-1 non_thm 1.4 7 0 1897 0 2 0 0 0 6 1897 5126 0 [0.43] SWV012-1 timeout 299.0 307 [0.44] PUZ037-3 memory 115.4 398 [0.50] LCL002-1 theorem 91.7 41 1 2482 0 2 0 411 0 8 2482 2063446 0 [0.50] LCL020-1 timeout 299.0 94 [0.50] LCL021-1 theorem 108.5 82 1 1166 0 2 0 0 0 10 1166 756143 0 [0.50] LCL032-1 timeout 299.0 147 [0.50] LCL061-1 theorem 128.7 146 1 1764 0 4 0 20 0 5 1764 1294457 0 [0.50] LCL084-2 theorem 216.7 126 1 1900 0 3 0 57 0 7 1900 2768236 0 [0.50] LCL100-1 timeout 299.0 150 [0.50] LCL119-1 timeout 299.0 140 [0.50] LCL124-1 timeout 299.0 172 [0.50] LCL166-1 theorem 55.0 52 1 901 0 2 0 0 0 10 901 410916 0 [0.50] LCL167-1 timeout 299.0 93 [0.50] LCL253-1 timeout 299.0 98 [0.50] LCL375-1 theorem 124.3 143 1 1761 0 4 0 19 0 5 1761 1289158 0 [0.50] LCL376-1 theorem 22.2 33 1 915 0 4 0 17 0 5 915 362232 0 [0.50] LCL393-1 theorem 78.7 95 1 1524 0 4 0 18 0 5 1524 958395 0 [0.50] SYN614-1 timeout 299.0 324 [0.50] SYN617-1 timeout 299.0 236 [0.57] NUM287-1 timeout 299.0 41 [0.67] ANA003-2 timeout 299.0 389 [0.67] LCL005-1 timeout 299.0 129 [0.67] LCL062-1 theorem 276.4 253 1 2472 0 4 0 30 0 5 2472 2274877 0 [0.67] LCL084-3 theorem 219.1 116 1 1923 0 4 0 48 0 7 1923 2865503 0 [0.67] LCL105-1 timeout 299.0 197 [0.67] LCL249-1 timeout 299.0 97 [0.67] LCL394-1 theorem 143.8 160 1 1853 0 4 0 22 0 5 1853 1393973 0 [0.67] LCL395-1 theorem 196.4 198 1 2150 0 4 0 24 0 5 2150 1815895 0 [0.67] SYN615-1 timeout 299.0 348 [0.71] PUZ048-1 memory 234.6 399 [0.83] LCL001-1 timeout 299.0 242 [0.83] LCL063-1 timeout 299.0 251 [0.83] LCL125-1 timeout 299.0 190 [0.83] LCL377-1 theorem 43.9 61 1 1174 0 4 0 17 0 5 1174 615074 0 [0.86] LCL078-1 timeout 299.0 258 [0.86] LCL168-1 timeout 299.0 113 [0.86] LCL179-1 timeout 299.0 99 [0.86] LCL180-1 timeout 299.0 98 [0.86] LCL181-1 timeout 299.0 99 [0.86] LCL183-1 timeout 299.0 97 [0.86] LCL184-1 timeout 299.0 99 [0.86] LCL209-1 timeout 299.0 99 [0.86] LCL219-1 timeout 299.0 99 [0.86] LCL220-1 timeout 299.0 98 [0.86] LCL235-1 timeout 299.0 97 [0.86] LCL239-1 timeout 299.0 98 [0.86] LCL240-1 timeout 299.0 100 [0.86] LCL241-1 timeout 299.0 97 [0.86] LCL242-1 timeout 299.0 98 [0.86] LCL244-1 timeout 299.0 98 [0.86] LCL245-1 timeout 299.0 96 [0.86] LCL246-1 timeout 299.0 98 [0.86] LCL247-1 timeout 299.0 99 [0.86] LCL248-1 timeout 299.0 98 [0.86] LCL252-1 timeout 299.0 99 [0.86] LCL255-1 timeout 299.0 99 [0.86] PUZ015-3 timeout 299.0 291 [1.00] ANA004-2 timeout 299.0 382 [1.00] ANA005-2 timeout 299.0 382 [1.00] GEO001-4 timeout 299.0 110 [1.00] LCL037-1 timeout 299.0 149 [1.00] LCL073-1 timeout 299.0 90 [1.00] LCL074-1 timeout 299.0 88 [1.00] LCL109-1 timeout 299.0 255 [1.00] LCL228-1 timeout 299.0 98 [1.00] LCL229-1 timeout 299.0 98 [1.00] LCL243-1 timeout 299.0 96 [1.00] LCL251-1 timeout 299.0 98 [1.00] LCL254-1 timeout 299.0 98 [1.00] LCL417-1 timeout 299.0 124 [1.00] LCL418-1 timeout 299.0 193 [1.00] LCL419-1 timeout 299.0 253 [1.00] LCL420-1 timeout 299.0 272 [1.00] LCL421-1 timeout 299.0 268 [1.00] LCL422-1 timeout 299.0 255 [1.00] LCL423-1 timeout 299.0 179 [1.00] LCL424-1 timeout 299.0 92 [1.00] LCL425-1 timeout 299.0 275 [1.00] LCL426-1 timeout 299.0 257 [1.00] LCL427-1 timeout 299.0 84 [1.00] NUM026-1 timeout 299.0 148 [1.00] PUZ041-1 memory 255.6 399 [1.00] PUZ050-1 memory 240.5 399 [1.00] PUZ051-1 memory 253.3 399 [1.00] PUZ052-1 memory 113.6 399 [1.00] PUZ053-1 memory 117.8 399 [1.00] ROB025-1 timeout 299.0 167