-------------------------------------------------------------------------------- Execute format string : ../darwin -umx true Problems list file : all-problems Output file : all-output Summary file : all-summary Time limit : 500 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 2 1 9 0 7 0 0 0 2 9 18 0 0 [0.00] COM002-1 theorem 0.0 2 1 26 0 15 0 0 0 2 26 43 0 0 [0.00] GEO002-4 theorem 0.0 2 1 13 0 3 0 3 0 2 13 57 0 0 [0.00] GEO079-1 theorem 0.0 2 1 3 0 2 0 0 0 2 3 6 0 0 [0.00] GRP001-5 theorem 0.0 4 1 7 0 5 0 0 0 2 7 96 0 0 [0.00] GRP003-1 theorem 0.0 4 1 5 0 3 0 0 0 3 5 48 0 0 [0.00] GRP003-2 theorem 0.0 4 1 24 0 4 0 0 0 2 24 860 0 0 [0.00] GRP004-1 theorem 0.0 4 1 11 0 3 0 0 0 2 11 160 0 0 [0.00] GRP004-2 theorem 0.0 4 1 22 0 4 0 0 0 2 22 824 0 0 [0.00] GRP005-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 72 0 0 [0.00] GRP006-1 theorem 0.0 4 1 7 0 6 0 0 0 2 7 74 0 0 [0.00] GRP028-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 5 0 0 [0.00] GRP028-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 9 0 0 [0.00] GRP028-4 theorem 0.0 4 1 3 0 3 0 0 0 2 3 6 0 0 [0.00] GRP029-2 theorem 0.2 4 1 11 0 5 0 0 0 3 11 281 0 0 [0.00] GRP031-2 theorem 0.0 4 1 11 0 4 0 0 0 2 11 176 0 0 [0.00] GRP033-3 theorem 0.0 4 1 8 0 7 0 0 0 2 8 155 0 0 [0.00] GRP034-4 theorem 0.0 4 1 7 0 6 0 0 0 2 7 78 0 0 [0.00] GRP041-2 theorem 0.0 4 1 3 0 3 0 0 0 2 3 20 0 0 [0.00] GRP042-2 theorem 0.0 4 1 6 0 5 0 0 0 2 6 34 0 0 [0.00] GRP043-2 theorem 0.0 4 1 15 0 6 0 0 0 2 15 156 0 0 [0.00] GRP044-2 theorem 0.0 4 1 7 0 6 0 0 0 2 7 62 0 0 [0.00] GRP045-2 theorem 0.0 4 1 17 0 6 0 0 0 2 17 428 0 0 [0.00] GRP046-2 theorem 0.0 4 1 16 0 5 0 0 0 2 16 394 0 0 [0.00] GRP047-2 theorem 0.0 4 1 16 0 5 0 0 0 2 16 425 0 0 [0.00] KRS004-1 theorem 0.0 2 1 2 0 1 0 0 0 2 2 5 0 0 [0.00] LAT005-1 theorem 3.9 6 1 405 0 17 0 14 0 2 405 95285 0 0 [0.00] LAT005-2 theorem 2.8 5 1 403 0 21 0 14 0 2 403 75398 0 0 [0.00] LCL007-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 3 0 0 [0.00] LCL008-1 theorem 0.0 2 1 7 0 2 0 0 0 5 7 38 0 0 [0.00] LCL009-1 theorem 0.0 2 1 23 0 2 0 2 0 5 23 263 0 0 [0.00] LCL010-1 theorem 0.0 2 1 11 0 2 0 0 0 5 11 81 0 0 [0.00] LCL011-1 theorem 0.0 2 1 24 0 2 0 0 0 5 24 292 0 0 [0.00] LCL013-1 theorem 0.0 2 1 3 0 2 0 0 0 6 3 4 0 0 [0.00] LCL022-1 theorem 0.0 2 1 10 0 2 0 2 0 5 10 82 0 0 [0.00] LCL023-1 theorem 0.0 2 1 14 0 2 0 2 0 5 14 109 0 0 [0.00] LCL027-1 theorem 0.0 2 1 32 0 4 0 2 0 4 32 230 0 0 [0.00] LCL033-1 theorem 0.0 2 1 14 0 2 0 2 0 5 14 108 0 0 [0.00] LCL035-1 theorem 0.0 2 1 8 0 2 0 0 0 5 8 48 0 0 [0.00] LCL041-1 theorem 0.0 2 1 47 0 6 0 0 0 4 47 427 0 0 [0.00] LCL043-1 theorem 0.0 2 1 37 0 6 0 0 0 4 37 313 0 0 [0.00] LCL044-1 theorem 0.2 2 1 11 0 6 0 0 0 5 11 87 0 0 [0.00] LCL046-1 theorem 0.0 2 1 5 0 4 0 0 0 5 5 12 0 0 [0.00] LCL075-1 theorem 0.0 2 1 34 0 2 0 2 0 6 34 605 0 0 [0.00] LCL076-2 theorem 0.0 2 1 4 0 4 0 0 0 2 4 5 0 0 [0.00] LCL076-3 theorem 0.0 2 1 35 0 4 0 1 0 4 35 609 0 0 [0.00] LCL077-2 theorem 0.0 2 1 26 0 4 0 1 0 4 26 308 0 0 [0.00] LCL079-1 theorem 0.0 2 1 17 0 6 0 1 0 3 17 76 0 0 [0.00] LCL081-1 theorem 0.0 2 1 37 0 2 0 4 0 5 37 308 0 0 [0.00] LCL082-1 theorem 0.0 2 1 36 0 2 0 7 0 5 36 353 0 0 [0.00] LCL086-1 theorem 0.0 2 1 28 0 2 0 7 0 6 28 443 0 0 [0.00] LCL087-1 theorem 0.0 2 1 12 0 2 0 2 0 6 12 109 0 0 [0.00] LCL088-1 theorem 0.2 2 1 64 0 2 0 9 0 6 64 2130 0 0 [0.00] LCL091-1 theorem 0.1 2 1 47 0 2 0 9 0 6 47 791 0 0 [0.00] LCL096-1 theorem 6.1 3 1 538 0 4 0 1 0 5 538 127303 0 0 [0.00] LCL097-1 theorem 1.4 3 1 278 0 3 0 1 0 5 278 32082 0 0 [0.00] LCL098-1 theorem 0.6 2 1 207 0 2 0 0 0 6 207 531 0 0 [0.00] LCL101-1 theorem 0.0 2 1 14 0 3 0 1 0 5 14 81 0 0 [0.00] LCL102-1 theorem 0.3 2 1 139 0 4 0 1 0 5 139 9651 0 0 [0.00] LCL104-1 theorem 0.0 2 1 16 0 3 0 0 0 5 16 94 0 0 [0.00] LCL106-1 theorem 0.0 2 1 22 0 3 0 0 0 6 22 45 0 0 [0.00] LCL107-1 theorem 0.0 2 1 15 0 2 0 0 0 8 15 114 0 0 [0.00] LCL108-1 theorem 0.0 2 1 11 0 2 0 0 0 8 11 60 0 0 [0.00] LCL110-1 theorem 0.1 2 1 46 0 5 0 0 0 5 46 1016 0 0 [0.00] LCL111-1 theorem 0.1 2 1 61 0 5 0 0 0 5 61 1452 0 0 [0.00] LCL112-1 theorem 0.3 2 1 155 0 5 0 0 0 5 155 6342 0 0 [0.00] LCL117-1 theorem 0.0 2 1 4 0 2 0 0 0 5 4 10 0 0 [0.00] LCL118-1 theorem 0.0 2 1 12 0 2 0 0 0 6 12 81 0 0 [0.00] LCL120-1 theorem 0.1 2 1 40 0 2 0 0 0 6 40 624 0 0 [0.00] LCL126-1 theorem 0.0 2 1 6 0 3 0 0 0 5 6 15 0 0 [0.00] LCL169-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 7 0 0 [0.00] LCL170-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 6 0 0 [0.00] LCL171-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 [0.00] LCL172-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 [0.00] LCL173-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 [0.00] LCL174-1 theorem 0.2 2 1 807 0 6 0 0 0 5 807 2568 0 0 [0.00] LCL175-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 7 0 0 [0.00] LCL176-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 17 0 0 [0.00] LCL177-1 theorem 0.0 2 1 11 0 6 0 0 0 4 11 31 0 0 [0.00] LCL178-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 30 0 0 [0.00] LCL182-1 theorem 0.2 2 1 636 0 6 0 0 0 5 636 2295 0 0 [0.00] LCL185-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 18 0 0 [0.00] LCL186-1 theorem 0.0 2 1 19 0 6 0 0 0 4 19 58 0 0 [0.00] LCL187-1 theorem 0.0 2 1 20 0 6 0 0 0 4 20 64 0 0 [0.00] LCL188-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 27 0 0 [0.00] LCL189-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 26 0 0 [0.00] LCL190-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 14 0 0 [0.00] LCL192-1 theorem 0.1 2 1 282 0 6 0 0 0 5 282 1119 0 0 [0.00] LCL193-1 theorem 0.1 2 1 247 0 6 0 0 0 5 247 974 0 0 [0.00] LCL194-1 theorem 16.4 7 1 4866 0 6 0 0 0 6 4866 22017 0 0 [0.00] LCL197-1 theorem 0.0 2 1 9 0 6 0 0 0 5 9 37 0 0 [0.00] LCL199-1 theorem 0.1 2 1 308 0 6 0 0 0 5 308 1220 0 0 [0.00] LCL200-1 theorem 0.0 2 1 13 0 6 0 0 0 5 13 52 0 0 [0.00] LCL201-1 theorem 7.9 5 1 1516 0 6 0 0 0 6 1516 9378 0 0 [0.00] LCL202-1 theorem 6.6 4 1 220 0 6 0 0 0 6 220 1851 0 0 [0.00] LCL203-1 theorem 11.1 5 1 210 0 6 0 0 0 6 210 1590 0 0 [0.00] LCL204-1 theorem 2.1 4 1 1478 0 6 0 0 0 6 1478 7687 0 0 [0.00] LCL205-1 theorem 11.3 5 1 691 0 6 0 0 0 6 691 5382 0 0 [0.00] LCL206-1 theorem 3.7 3 1 665 0 6 0 0 0 6 665 4071 0 0 [0.00] LCL207-1 theorem 7.2 4 1 529 0 6 0 0 0 6 529 3733 0 0 [0.00] LCL208-1 theorem 0.2 2 1 626 0 6 0 0 0 5 626 2144 0 0 [0.00] LCL210-1 theorem 0.2 2 1 638 0 6 0 0 0 5 638 2205 0 0 [0.00] LCL211-1 theorem 0.2 2 1 589 0 6 0 0 0 5 589 2056 0 0 [0.00] LCL212-1 theorem 2.0 4 1 1688 0 6 0 0 0 6 1688 8314 0 0 [0.00] LCL213-1 theorem 1.1 3 1 1401 0 6 0 0 0 6 1401 6106 0 0 [0.00] LCL214-1 theorem 4.0 3 1 1398 0 6 0 0 0 6 1398 6762 0 0 [0.00] LCL215-1 theorem 4.1 4 1 1451 0 6 0 0 0 6 1451 7696 0 0 [0.00] LCL216-1 theorem 0.2 2 1 584 0 6 0 0 0 5 584 1999 0 0 [0.00] LCL217-1 theorem 0.2 2 1 587 0 6 0 0 0 5 587 2012 0 0 [0.00] LCL218-1 timeout 500.0 51 [0.00] LCL226-1 theorem 0.0 2 1 7 0 6 0 0 0 5 7 16 0 0 [0.00] LCL230-1 timeout 500.0 49 [0.00] LCL236-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 25 0 0 [0.00] LCL238-1 theorem 0.1 2 1 298 0 6 0 0 0 5 298 1157 0 0 [0.00] LCL257-1 theorem 0.0 2 1 28 0 2 0 2 0 5 28 369 0 0 [0.00] LCL355-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 4 0 0 [0.00] LCL356-1 theorem 0.0 2 1 20 0 4 0 1 0 5 20 104 0 0 [0.00] LCL357-1 theorem 0.0 2 1 20 0 4 0 1 0 5 20 105 0 0 [0.00] LCL359-1 theorem 0.0 2 1 21 0 4 0 1 0 5 21 109 0 0 [0.00] LCL360-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 4 0 0 [0.00] LCL361-1 theorem 0.0 2 1 24 0 4 0 2 0 5 24 123 0 0 [0.00] LCL362-1 theorem 0.0 2 1 31 0 4 0 2 0 5 31 217 0 0 [0.00] LCL363-1 theorem 0.0 2 1 31 0 4 0 2 0 5 31 220 0 0 [0.00] LCL364-1 theorem 0.0 2 1 40 0 4 0 2 0 5 40 455 0 0 [0.00] LCL366-1 theorem 0.0 2 1 9 0 4 0 0 0 5 9 40 0 0 [0.00] LCL397-1 theorem 0.0 2 1 39 0 4 0 2 0 5 39 321 0 0 [0.00] LCL398-1 theorem 0.0 2 1 6 0 4 0 0 0 5 6 16 0 0 [0.00] LCL399-1 theorem 0.0 2 1 42 0 4 0 2 0 5 42 539 0 0 [0.00] LCL414-1 theorem 0.0 2 1 6 0 4 0 0 0 3 6 9 0 0 [0.00] LCL428-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 6 0 0 [0.00] MGT001-1 theorem 0.0 2 1 19 0 10 0 0 0 2 19 30 0 0 [0.00] MGT002-1 theorem 0.0 2 1 12 0 7 0 0 0 2 12 26 0 0 [0.00] MGT003-1 theorem 0.0 2 1 12 0 7 0 0 0 2 12 26 0 0 [0.00] MGT006-1 theorem 0.0 2 1 13 0 9 1 0 0 2 13 23 0 0 [0.00] MGT008-1 theorem 0.0 2 1 15 0 12 0 0 0 2 15 25 0 0 [0.00] MGT009-1 theorem 0.0 2 1 15 0 12 0 0 0 2 15 25 0 0 [0.00] MGT010-1 theorem 0.0 2 1 18 0 14 1 0 0 2 18 28 0 0 [0.00] MGT015-1 theorem 0.0 2 1 17 0 13 0 0 0 2 17 27 0 0 [0.00] MGT017-1 theorem 0.0 2 1 17 0 13 0 0 0 2 17 27 0 0 [0.00] MGT032-2 theorem 0.0 2 1 7 0 2 0 0 0 4 7 11 0 0 [0.00] MGT036-3 theorem 0.0 2 1 6 0 4 0 0 0 2 6 9 0 0 [0.00] MSC005-1 theorem 0.0 2 1 15 0 3 0 0 0 4 15 175 0 0 [0.00] NLP104-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 0 1 0 0 [0.00] NLP105-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 0 1 0 0 [0.00] NLP106-1 non_thm 0.0 4 0 24 0 2 0 0 0 2 0 25 0 0 [0.00] NLP107-1 non_thm 0.0 4 0 46 0 3 0 0 0 2 0 48 0 0 [0.00] NLP108-1 non_thm 0.0 4 0 99 0 10 0 0 0 2 0 105 0 0 [0.00] NLP109-1 non_thm 0.0 4 0 46 0 3 0 0 0 2 0 48 0 0 [0.00] NLP110-1 non_thm 0.0 4 0 77 0 9 0 0 0 2 0 82 0 0 [0.00] NLP111-1 non_thm 0.0 2 0 99 0 10 0 0 0 2 0 105 0 0 [0.00] NLP112-1 non_thm 0.0 4 0 99 0 10 0 0 0 2 0 105 0 0 [0.00] NLP113-1 non_thm 0.0 4 0 23 0 2 0 0 0 2 0 24 0 0 [0.00] NUM001-1 theorem 0.0 2 1 26 0 8 0 0 0 3 26 347 0 0 [0.00] NUM002-1 theorem 0.0 2 1 27 0 8 0 0 0 3 27 356 0 0 [0.00] NUM003-1 theorem 0.0 2 1 25 0 8 0 0 0 3 25 341 0 0 [0.00] NUM004-1 theorem 0.0 2 1 27 0 8 0 0 0 3 27 356 0 0 [0.00] NUM019-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 18 0 0 [0.00] NUM020-1 theorem 0.0 2 1 9 0 8 0 0 0 3 9 48 0 0 [0.00] NUM023-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 20 0 0 [0.00] NUM024-1 theorem 0.0 2 1 38 0 8 0 1 0 3 38 314 0 0 [0.00] NUM025-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 17 0 0 [0.00] NUM286-1 timeout 500.0 37 [0.00] PLA003-1 theorem 0.0 2 1 15 0 5 2 3 0 2 15 33 0 0 [0.00] PLA006-1 theorem 0.0 2 1 21 0 20 0 0 0 2 21 38 0 0 [0.00] PLA017-1 theorem 0.0 2 1 68 0 20 0 0 0 3 68 216 0 0 [0.00] PLA020-1 theorem 0.0 2 1 18 0 18 0 0 0 2 18 43 0 0 [0.00] PLA029-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.00] PLA030-1 timeout 500.0 59 [0.00] PUZ003-1 theorem 0.0 2 1 9 0 6 0 0 0 2 9 18 0 0 [0.00] PUZ008-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 6 0 0 [0.00] PUZ008-2 theorem 0.0 2 1 15 0 16 14 0 0 3 15 19 0 0 [0.00] PUZ008-3 theorem 0.0 2 1 37 0 4 0 0 0 6 37 69 0 0 [0.00] PUZ011-1 theorem 0.0 2 1 18 0 18 0 0 0 2 18 55 0 0 [0.00] PUZ022-1 theorem 0.0 2 1 38 0 31 0 0 0 2 38 64 0 0 [0.00] PUZ036-1.005 theorem 0.0 2 1 61 0 2 0 0 0 2 61 184 0 0 [0.00] PUZ037-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 28 0 0 [0.00] PUZ037-2 theorem 0.0 2 1 6 0 2 0 0 0 2 6 102 0 0 [0.00] PUZ038-1 theorem 0.0 3 1 2 0 2 0 0 0 2 2 2 0 0 [0.00] PUZ047-1 theorem 0.0 2 1 10 0 10 11 0 0 2 10 16 0 0 [0.00] RNG038-2 theorem 0.0 2 1 11 0 9 0 0 0 2 11 321 0 0 [0.00] SWV010-1 non_thm 0.0 4 0 8 0 5 0 0 0 6 0 8 0 0 [0.00] SWV011-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 2 0 0 [0.00] SWV013-1 timeout 500.0 303 [0.00] SWV015-1 timeout 500.0 308 [0.00] SWV016-1 timeout 500.0 277 [0.00] SWV017-1 timeout 500.0 4 [0.00] SWV018-1 timeout 500.0 14 [0.00] SYN003-1.006 theorem 0.0 2 1 18 0 18 18 0 0 2 18 26 0 0 [0.00] SYN004-1.007 theorem 0.0 2 1 14 0 14 14 0 0 2 14 17 0 0 [0.00] SYN005-1.010 theorem 0.0 2 1 10 0 10 0 0 0 2 10 20 0 0 [0.00] SYN010-1.005.005 theorem 0.0 2 1 26 0 26 26 0 0 2 26 32 0 0 [0.00] SYN033-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 5 0 0 [0.00] SYN035-1 theorem 0.0 2 1 2 0 2 6 0 0 2 2 6 0 0 [0.00] SYN040-1 theorem 0.0 2 1 2 0 4 2 0 0 2 2 4 0 0 [0.00] SYN041-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 4 0 0 [0.00] SYN046-1 theorem 0.0 2 1 2 0 2 2 0 0 2 2 4 0 0 [0.00] SYN048-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 2 0 0 [0.00] SYN049-1 theorem 0.0 2 1 2 0 2 2 0 0 2 2 4 0 0 [0.00] SYN050-1 theorem 0.0 2 1 3 0 3 1 0 0 2 3 7 0 0 [0.00] SYN057-1 theorem 0.0 2 1 7 0 4 0 0 0 2 7 12 0 0 [0.00] SYN058-1 theorem 0.0 2 1 5 0 6 1 0 0 2 5 8 0 0 [0.00] SYN062-1 theorem 0.0 2 1 5 0 3 0 0 0 2 5 8 0 0 [0.00] SYN063-2 theorem 0.0 2 1 2 0 2 2 0 0 2 2 4 0 0 [0.00] SYN064-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 2 0 0 [0.00] SYN065-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 6 0 0 [0.00] SYN068-1 theorem 0.0 2 1 5 0 1 0 0 0 2 5 9 0 0 [0.00] SYN079-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 6 0 0 [0.00] SYN085-1.010 theorem 0.0 2 1 11 0 11 11 0 0 2 11 22 0 0 [0.00] SYN086-1.003 non_thm 0.0 2 0 1 0 1 1 0 0 2 0 1 0 0 [0.00] SYN087-1.003 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.00] SYN088-1.010 theorem 0.0 2 1 21 0 21 0 0 0 2 21 1055 0 0 [0.00] SYN089-1.002 theorem 0.0 2 1 5 0 10 5 0 0 2 5 11 0 0 [0.00] SYN090-1.008 theorem 0.0 2 1 34 0 36 58 0 0 2 34 65 0 0 [0.00] SYN095-1.002 theorem 0.0 2 1 4 0 5 1 0 0 2 4 10 0 0 [0.00] SYN096-1.008 theorem 0.0 2 1 34 0 4 0 0 0 2 34 67 0 0 [0.00] SYN101-1.002.002 theorem 0.0 2 1 10 0 5 0 0 0 2 10 24 0 0 [0.00] SYN102-1.007.007 theorem 0.5 4 1 3727 0 15 1 0 0 2 3727 7185 0 0 [0.00] SYN103-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN104-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN105-1 theorem 0.0 2 1 22 0 29 31 0 0 2 22 209 0 0 [0.00] SYN106-1 theorem 0.0 2 1 17 0 24 30 0 0 2 17 167 0 0 [0.00] SYN107-1 theorem 0.0 2 1 34 0 41 36 0 0 2 34 326 0 0 [0.00] SYN108-1 theorem 0.0 2 1 34 0 41 35 0 0 2 34 326 0 0 [0.00] SYN109-1 theorem 0.0 2 1 58 0 91 87 0 0 2 58 474 0 0 [0.00] SYN110-1 theorem 0.0 2 1 55 0 92 85 0 0 2 55 456 0 0 [0.00] SYN111-1 theorem 0.0 2 1 59 0 91 88 0 0 2 59 489 0 0 [0.00] SYN112-1 theorem 0.0 2 1 34 0 40 36 0 0 2 34 327 0 0 [0.00] SYN113-1 theorem 0.0 2 1 56 0 90 85 0 0 2 56 462 0 0 [0.00] SYN114-1 theorem 0.0 2 1 35 0 47 36 0 0 2 35 356 0 0 [0.00] SYN115-1 theorem 0.1 2 1 184 0 112 149 3 0 2 184 1579 0 0 [0.00] SYN116-1 theorem 0.0 2 1 53 0 108 86 0 0 2 53 464 0 0 [0.00] SYN117-1 theorem 0.0 2 1 53 0 107 85 0 0 2 53 463 0 0 [0.00] SYN118-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN119-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN120-1 theorem 0.0 2 1 17 0 24 30 0 0 2 17 168 0 0 [0.00] SYN121-1 theorem 0.0 2 1 70 0 94 101 1 0 2 70 550 0 0 [0.00] SYN122-1 theorem 0.0 2 1 69 0 92 92 0 0 2 69 530 0 0 [0.00] SYN123-1 theorem 0.0 2 1 34 0 39 35 0 0 2 34 327 0 0 [0.00] SYN124-1 theorem 0.0 2 1 37 0 56 47 0 0 2 37 368 0 0 [0.00] SYN125-1 theorem 0.1 2 1 237 0 122 156 6 0 2 237 1966 0 0 [0.00] SYN126-1 theorem 0.0 2 1 40 0 62 60 0 0 2 40 392 0 0 [0.00] SYN127-1 theorem 0.0 2 1 40 0 62 60 0 0 2 40 393 0 0 [0.00] SYN128-1 theorem 0.0 2 1 52 0 87 83 0 0 2 52 445 0 0 [0.00] SYN129-1 theorem 0.0 2 1 52 0 87 83 0 0 2 52 445 0 0 [0.00] SYN130-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN131-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN132-1 theorem 0.0 2 1 12 0 18 29 0 0 2 12 135 0 0 [0.00] SYN133-1 theorem 0.0 2 1 5 0 4 9 0 0 2 5 52 0 0 [0.00] SYN134-1 theorem 0.0 2 1 34 0 58 36 0 0 2 34 342 0 0 [0.00] SYN135-1 theorem 0.0 2 1 35 0 48 36 0 0 2 35 349 0 0 [0.00] SYN136-1 theorem 0.0 2 1 35 0 47 36 0 0 2 35 349 0 0 [0.00] SYN137-1 theorem 0.0 2 1 83 0 100 121 1 0 2 83 653 0 0 [0.00] SYN138-1 theorem 0.0 2 1 182 0 113 147 3 0 2 182 1570 0 0 [0.00] SYN139-1 theorem 0.0 2 1 195 0 119 150 4 0 2 195 1638 0 0 [0.00] SYN140-1 theorem 0.1 2 1 195 0 119 150 4 0 2 195 1639 0 0 [0.00] SYN141-1 theorem 0.1 2 1 186 0 113 149 3 0 2 186 1591 0 0 [0.00] SYN142-1 theorem 0.1 2 1 232 0 124 154 4 0 2 232 1923 0 0 [0.00] SYN143-1 theorem 0.1 2 1 232 0 124 154 4 0 2 232 1923 0 0 [0.00] SYN144-1 theorem 0.1 2 1 139 0 104 137 1 0 2 139 979 0 0 [0.00] SYN145-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN146-1 theorem 0.0 2 1 4 0 4 10 0 0 2 4 50 0 0 [0.00] SYN147-1 theorem 0.0 2 1 6 0 8 13 0 0 2 6 68 0 0 [0.00] SYN148-1 theorem 0.0 2 1 119 0 102 134 1 0 2 119 811 0 0 [0.00] SYN149-1 theorem 0.0 2 1 12 0 20 30 0 0 2 12 140 0 0 [0.00] SYN150-1 theorem 0.0 2 1 34 0 42 38 0 0 2 34 333 0 0 [0.00] SYN151-1 theorem 0.0 2 1 34 0 39 35 0 0 2 34 330 0 0 [0.00] SYN152-1 theorem 0.0 2 1 34 0 42 37 0 0 2 34 326 0 0 [0.00] SYN153-1 theorem 0.0 2 1 35 0 48 36 0 0 2 35 349 0 0 [0.00] SYN154-1 theorem 0.0 2 1 35 0 48 36 0 0 2 35 349 0 0 [0.00] SYN155-1 theorem 0.0 2 1 99 0 105 132 1 0 2 99 754 0 0 [0.00] SYN156-1 theorem 0.1 2 1 190 0 116 148 3 0 2 190 1619 0 0 [0.00] SYN157-1 theorem 0.0 2 1 46 0 81 73 0 0 2 46 440 0 0 [0.00] SYN158-1 theorem 0.0 2 1 46 0 81 72 0 0 2 46 438 0 0 [0.00] SYN159-1 theorem 0.1 2 1 174 0 113 150 3 0 2 174 1380 0 0 [0.00] SYN160-1 theorem 0.0 2 1 46 0 81 72 0 0 2 46 438 0 0 [0.00] SYN161-1 theorem 0.0 2 1 46 0 81 72 0 0 2 46 438 0 0 [0.00] SYN162-1 theorem 0.0 2 1 46 0 81 72 0 0 2 46 438 0 0 [0.00] SYN163-1 theorem 0.0 2 1 174 0 113 151 3 0 2 174 1377 0 0 [0.00] SYN164-1 theorem 0.0 2 1 7 0 10 16 0 0 2 7 78 0 0 [0.00] SYN165-1 theorem 0.0 2 1 5 0 6 10 0 0 2 5 56 0 0 [0.00] SYN166-1 theorem 0.0 2 1 141 0 105 137 2 0 2 141 1041 0 0 [0.00] SYN167-1 theorem 0.0 2 1 12 0 18 29 0 0 2 12 140 0 0 [0.00] SYN168-1 theorem 0.0 2 1 37 0 60 52 0 0 2 37 373 0 0 [0.00] SYN169-1 theorem 0.0 2 1 35 0 44 36 0 0 2 35 349 0 0 [0.00] SYN170-1 theorem 0.0 2 1 40 0 66 61 0 0 2 40 393 0 0 [0.00] SYN171-1 theorem 0.1 2 1 178 0 112 147 3 0 2 178 1493 0 0 [0.00] SYN172-1 theorem 0.0 2 1 6 0 7 12 0 0 2 6 71 0 0 [0.00] SYN173-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 271 0 0 [0.00] SYN174-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 271 0 0 [0.00] SYN175-1 theorem 0.0 2 1 34 0 46 38 0 0 2 34 331 0 0 [0.00] SYN176-1 theorem 0.0 2 1 69 0 92 92 0 0 2 69 534 0 0 [0.00] SYN177-1 theorem 0.0 2 1 37 0 57 47 0 0 2 37 377 0 0 [0.00] SYN178-1 theorem 0.0 2 1 43 0 70 66 0 0 2 43 430 0 0 [0.00] SYN179-1 theorem 0.0 2 1 83 0 100 121 1 0 2 83 665 0 0 [0.00] SYN180-1 theorem 0.0 2 1 46 0 79 71 0 0 2 46 441 0 0 [0.00] SYN181-1 theorem 0.0 2 1 46 0 79 71 0 0 2 46 438 0 0 [0.00] SYN182-1 theorem 0.0 2 1 46 0 81 72 0 0 2 46 436 0 0 [0.00] SYN183-1 theorem 0.0 2 1 46 0 81 72 0 0 2 46 436 0 0 [0.00] SYN184-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN185-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN186-1 theorem 0.0 2 1 34 0 40 35 0 0 2 34 331 0 0 [0.00] SYN187-1 theorem 0.0 2 1 34 0 40 35 0 0 2 34 332 0 0 [0.00] SYN188-1 theorem 0.0 2 1 34 0 41 36 0 0 2 34 326 0 0 [0.00] SYN189-1 theorem 0.0 2 1 38 0 61 52 0 0 2 38 379 0 0 [0.00] SYN190-1 theorem 0.0 2 1 83 0 100 121 1 0 2 83 658 0 0 [0.00] SYN191-1 theorem 0.0 2 1 130 0 103 134 1 0 2 130 910 0 0 [0.00] SYN192-1 theorem 0.0 2 1 47 0 85 79 0 0 2 47 443 0 0 [0.00] SYN193-1 theorem 0.0 2 1 47 0 84 79 0 0 2 47 444 0 0 [0.00] SYN194-1 theorem 0.0 2 1 97 0 104 129 1 0 2 97 728 0 0 [0.00] SYN195-1 theorem 0.0 2 1 60 0 90 89 0 0 2 60 493 0 0 [0.00] SYN196-1 theorem 0.0 2 1 34 0 40 36 0 0 2 34 337 0 0 [0.00] SYN197-1 theorem 0.0 2 1 8 0 15 20 0 0 2 8 82 0 0 [0.00] SYN198-1 theorem 0.0 2 1 34 0 46 36 1 0 2 34 326 0 0 [0.00] SYN199-1 theorem 0.0 2 1 34 0 40 36 0 0 2 34 338 0 0 [0.00] SYN200-1 theorem 0.0 2 1 34 0 46 36 1 0 2 34 326 0 0 [0.00] SYN201-1 theorem 0.0 2 1 43 0 71 66 0 0 2 43 428 0 0 [0.00] SYN202-1 theorem 0.0 2 1 69 0 93 92 0 0 2 69 527 0 0 [0.00] SYN203-1 theorem 0.0 2 1 50 0 89 81 0 0 2 50 445 0 0 [0.00] SYN204-1 theorem 0.0 2 1 150 0 108 138 3 0 2 150 1175 0 0 [0.00] SYN205-1 theorem 0.0 2 1 150 0 108 138 3 0 2 150 1175 0 0 [0.00] SYN206-1 theorem 0.0 2 1 69 0 92 92 0 0 2 69 528 0 0 [0.00] SYN207-1 theorem 0.0 2 1 85 0 101 121 1 0 2 85 652 0 0 [0.00] SYN208-1 theorem 0.0 2 1 70 0 94 102 1 0 2 70 546 0 0 [0.00] SYN209-1 theorem 0.0 2 1 48 0 83 78 0 0 2 48 446 0 0 [0.00] SYN210-1 theorem 0.0 2 1 48 0 83 78 0 0 2 48 441 0 0 [0.00] SYN211-1 theorem 0.0 2 1 48 0 82 78 0 0 2 48 442 0 0 [0.00] SYN212-1 theorem 0.0 2 1 48 0 84 78 0 0 2 48 445 0 0 [0.00] SYN213-1 theorem 0.0 2 1 55 0 97 86 0 0 2 55 455 0 0 [0.00] SYN214-1 theorem 0.0 2 1 55 0 97 86 0 0 2 55 455 0 0 [0.00] SYN215-1 theorem 0.0 2 1 55 0 97 86 0 0 2 55 455 0 0 [0.00] SYN216-1 theorem 0.0 2 1 34 0 40 36 0 0 2 34 335 0 0 [0.00] SYN217-1 theorem 0.0 2 1 34 0 39 35 0 0 2 34 330 0 0 [0.00] SYN218-1 theorem 0.0 2 1 34 0 41 37 0 0 2 34 332 0 0 [0.00] SYN219-1 theorem 0.0 2 1 70 0 94 101 1 0 2 70 550 0 0 [0.00] SYN220-1 theorem 0.0 2 1 35 0 47 36 0 0 2 35 358 0 0 [0.00] SYN221-1 theorem 0.0 2 1 37 0 56 49 0 0 2 37 371 0 0 [0.00] SYN222-1 theorem 0.0 2 1 37 0 56 48 0 0 2 37 371 0 0 [0.00] SYN223-1 theorem 0.0 2 1 35 0 48 36 0 0 2 35 358 0 0 [0.00] SYN224-1 theorem 0.0 2 1 37 0 56 47 0 0 2 37 368 0 0 [0.00] SYN225-1 theorem 0.0 2 1 63 0 93 90 0 0 2 63 516 0 0 [0.00] SYN226-1 theorem 0.0 2 1 35 0 47 36 0 0 2 35 357 0 0 [0.00] SYN227-1 theorem 0.1 2 1 235 0 122 155 6 0 2 235 1938 0 0 [0.00] SYN228-1 theorem 0.0 2 1 128 0 104 134 1 0 2 128 883 0 0 [0.00] SYN229-1 theorem 0.0 2 1 37 0 56 48 0 0 2 37 369 0 0 [0.00] SYN230-1 theorem 0.0 2 1 37 0 56 48 0 0 2 37 369 0 0 [0.00] SYN231-1 theorem 0.0 2 1 37 0 56 49 0 0 2 37 369 0 0 [0.00] SYN232-1 theorem 0.0 2 1 37 0 56 48 0 0 2 37 369 0 0 [0.00] SYN233-1 theorem 0.0 2 1 35 0 47 36 0 0 2 35 357 0 0 [0.00] SYN234-1 theorem 0.0 2 1 63 0 92 90 0 0 2 63 516 0 0 [0.00] SYN235-1 theorem 0.0 2 1 130 0 103 134 1 0 2 130 933 0 0 [0.00] SYN236-1 theorem 0.0 2 1 35 0 47 36 0 0 2 35 357 0 0 [0.00] SYN237-1 theorem 0.0 2 1 6 0 8 13 0 0 2 6 80 0 0 [0.00] SYN238-1 theorem 0.0 2 1 4 0 4 6 0 0 2 4 53 0 0 [0.00] SYN239-1 theorem 0.0 2 1 4 0 5 9 0 0 2 4 53 0 0 [0.00] SYN240-1 theorem 0.0 2 1 12 0 19 30 0 0 2 12 138 0 0 [0.00] SYN241-1 theorem 0.0 2 1 12 0 19 30 0 0 2 12 138 0 0 [0.00] SYN242-1 theorem 0.0 2 1 27 0 33 35 0 0 2 27 271 0 0 [0.00] SYN243-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 272 0 0 [0.00] SYN244-1 theorem 0.0 2 1 4 0 4 9 0 0 2 4 53 0 0 [0.00] SYN245-1 theorem 0.0 2 1 12 0 18 31 0 0 2 12 138 0 0 [0.00] SYN246-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 273 0 0 [0.00] SYN247-1 theorem 0.0 2 1 6 0 10 12 0 0 2 6 78 0 0 [0.00] SYN248-1 theorem 0.0 2 1 55 0 91 84 0 0 2 55 455 0 0 [0.00] SYN249-1 theorem 0.0 2 1 55 0 92 84 0 0 2 55 455 0 0 [0.00] SYN250-1 theorem 0.1 2 1 263 0 123 161 7 0 2 263 2105 0 0 [0.00] SYN251-1 theorem 0.0 2 1 30 0 36 34 0 0 2 30 300 0 0 [0.00] SYN252-1 theorem 0.0 2 1 151 0 109 138 3 0 2 151 1181 0 0 [0.00] SYN253-1 theorem 0.1 2 1 195 0 120 150 4 0 2 195 1639 0 0 [0.00] SYN254-1 theorem 0.1 2 1 195 0 119 150 4 0 2 195 1637 0 0 [0.00] SYN255-1 theorem 0.0 2 1 34 0 41 38 0 0 2 34 328 0 0 [0.00] SYN256-1 theorem 0.0 2 1 34 0 39 37 0 0 2 34 334 0 0 [0.00] SYN257-1 theorem 0.0 2 1 12 0 18 29 0 0 2 12 135 0 0 [0.00] SYN258-1 theorem 0.0 2 1 7 0 11 16 0 0 2 7 89 0 0 [0.00] SYN259-1 theorem 0.0 2 1 7 0 11 16 0 0 2 7 89 0 0 [0.00] SYN260-1 theorem 0.0 2 1 12 0 18 29 0 0 2 12 140 0 0 [0.00] SYN261-1 theorem 0.0 2 1 12 0 19 30 0 0 2 12 140 0 0 [0.00] SYN262-1 theorem 0.0 2 1 34 0 39 35 0 0 2 34 330 0 0 [0.00] SYN263-1 theorem 0.0 2 1 37 0 57 47 0 0 2 37 372 0 0 [0.00] SYN264-1 theorem 0.0 2 1 34 0 39 35 0 0 2 34 331 0 0 [0.00] SYN265-1 theorem 0.0 2 1 37 0 60 51 0 0 2 37 369 0 0 [0.00] SYN266-1 theorem 0.0 2 1 131 0 104 134 1 0 2 131 889 0 0 [0.00] SYN267-1 theorem 0.0 2 1 40 0 67 60 0 0 2 40 395 0 0 [0.00] SYN268-1 theorem 0.0 2 1 40 0 66 60 0 0 2 40 393 0 0 [0.00] SYN269-1 theorem 0.1 2 1 178 0 112 147 3 0 2 178 1493 0 0 [0.00] SYN270-1 theorem 0.0 2 1 156 0 108 139 3 0 2 156 1255 0 0 [0.00] SYN271-1 theorem 0.0 2 1 178 0 112 147 3 0 2 178 1493 0 0 [0.00] SYN272-1 theorem 0.0 2 1 77 0 99 114 1 0 2 77 605 0 0 [0.00] SYN273-1 theorem 0.0 2 1 88 0 100 126 1 0 2 88 705 0 0 [0.00] SYN274-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN275-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 [0.00] SYN276-1 theorem 0.0 2 1 12 0 18 29 0 0 2 12 135 0 0 [0.00] SYN277-1 theorem 0.0 2 1 6 0 10 11 0 0 2 6 69 0 0 [0.00] SYN278-1 theorem 0.0 2 1 4 0 5 9 0 0 2 4 64 0 0 [0.00] SYN279-1 theorem 0.0 2 1 13 0 19 29 0 0 2 13 142 0 0 [0.00] SYN280-1 theorem 0.0 2 1 4 0 4 10 0 0 2 4 65 0 0 [0.00] SYN281-1 theorem 0.0 2 1 12 0 18 29 0 0 2 12 137 0 0 [0.00] SYN282-1 theorem 0.0 2 1 6 0 9 12 0 0 2 6 73 0 0 [0.00] SYN283-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 275 0 0 [0.00] SYN284-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 273 0 0 [0.00] SYN285-1 theorem 0.0 2 1 34 0 39 35 0 0 2 34 330 0 0 [0.00] SYN286-1 theorem 0.0 2 1 17 0 23 30 0 0 2 17 167 0 0 [0.00] SYN287-1 theorem 0.0 2 1 4 0 4 10 0 0 2 4 64 0 0 [0.00] SYN288-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 271 0 0 [0.00] SYN289-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 275 0 0 [0.00] SYN290-1 theorem 0.0 2 1 6 0 10 10 0 0 2 6 69 0 0 [0.00] SYN291-1 theorem 0.0 2 1 6 0 10 12 0 0 2 6 69 0 0 [0.00] SYN292-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 271 0 0 [0.00] SYN293-1 theorem 0.0 1 1 34 0 39 36 0 0 2 34 333 0 0 [0.00] SYN294-1 theorem 0.0 2 1 34 0 39 37 0 0 2 34 334 0 0 [0.00] SYN295-1 theorem 0.0 2 1 27 0 34 35 0 0 2 27 271 0 0 [0.00] SYN296-1 theorem 0.0 2 1 27 0 33 34 0 0 2 27 275 0 0 [0.00] SYN297-1 theorem 0.0 2 1 27 0 34 34 0 0 2 27 271 0 0 [0.00] SYN298-1 theorem 0.0 2 1 69 0 92 92 0 0 2 69 537 0 0 [0.00] SYN299-1 theorem 0.0 2 1 69 0 92 92 0 0 2 69 532 0 0 [0.00] SYN300-1 theorem 0.0 2 1 69 0 92 92 0 0 2 69 528 0 0 [0.00] SYN301-1 theorem 0.0 2 1 48 0 82 78 0 0 2 48 443 0 0 [0.00] SYN302-1.003 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.00] SYN310-1 theorem 0.1 2 1 1101 0 2 0 0 0 3 1101 3584 0 0 [0.00] SYN312-1 theorem 6.6 6 1 2818 0 3 0 0 0 3 2818 47015 0 0 [0.00] SYN318-1 theorem 0.0 2 1 2 0 2 2 0 0 2 2 6 0 0 [0.00] SYN322-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.00] SYN329-1 non_thm 0.0 2 0 3 0 4 0 0 0 2 0 4 0 0 [0.00] SYN333-1 theorem 0.0 2 1 2 0 2 6 0 0 2 2 6 0 0 [0.00] SYN336-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 5 0 0 [0.00] SYN337-1 non_thm 0.0 2 0 4 0 5 0 0 0 2 0 5 0 0 [0.00] SYN338-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 3 0 0 [0.00] SYN339-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 2 0 0 [0.00] SYN340-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 2 0 0 [0.00] SYN341-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 2 0 0 [0.00] SYN342-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 [0.00] SYN346-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 4 0 0 [0.00] SYN553-1 theorem 0.0 2 1 14 0 7 0 0 0 3 14 103 0 0 [0.00] SYN555-1 theorem 0.0 2 1 9 0 6 0 0 0 2 9 28 0 0 [0.00] SYN557-1 theorem 22.2 10 1 560 0 7 0 0 0 4 560 120412 0 0 [0.00] SYN558-1 theorem 0.0 2 1 32 0 6 0 2 0 2 32 108 0 0 [0.00] SYN559-1 theorem 0.0 2 1 10 0 6 0 0 0 3 10 114 0 0 [0.00] SYN561-1 theorem 0.1 2 1 14 0 6 0 0 0 4 14 307 0 0 [0.00] SYN562-1 theorem 0.0 1 1 7 0 7 0 0 0 2 7 31 0 0 [0.00] SYN563-1 theorem 0.0 2 1 58 0 6 0 0 0 3 58 404 0 0 [0.00] SYN564-1 theorem 0.0 2 1 30 0 7 0 0 0 4 30 299 0 0 [0.00] SYN565-1 theorem 0.0 2 1 30 0 7 0 0 0 4 30 299 0 0 [0.00] SYN566-1 theorem 0.0 2 1 19 0 8 0 0 0 3 19 69 0 0 [0.00] SYN569-1 theorem 0.0 2 1 35 0 7 0 0 0 3 35 176 0 0 [0.00] SYN570-1 theorem 0.0 2 1 14 0 10 0 0 0 3 14 45 0 0 [0.00] SYN584-1 theorem 0.0 2 1 10 0 9 0 0 0 8 10 34 0 0 [0.00] SYN588-1 theorem 0.0 2 1 12 0 12 0 0 0 2 12 30 0 0 [0.00] SYN589-1 theorem 0.0 2 1 12 0 12 0 0 0 2 12 30 0 0 [0.00] SYN590-1 theorem 0.0 2 1 144 0 8 0 0 0 4 144 786 0 0 [0.00] SYN596-1 theorem 0.0 2 1 12 0 11 0 0 0 5 12 37 0 0 [0.00] SYN618-1 theorem 0.0 2 1 28 0 16 0 0 0 3 28 114 0 0 [0.00] SYN632-1 theorem 0.0 2 1 26 0 12 0 0 0 7 26 76 0 0 [0.00] SYN637-1 theorem 0.0 2 1 24 0 14 0 0 0 7 24 108 0 0 [0.00] SYN638-1 theorem 0.0 2 1 24 0 14 0 0 0 7 24 108 0 0 [0.00] SYN649-1 timeout 500.0 96 [0.00] SYN651-1 theorem 0.0 2 1 23 0 15 0 0 0 6 23 73 0 0 [0.00] SYN652-1 theorem 0.0 2 1 26 0 20 0 0 0 3 26 86 0 0 [0.00] SYN654-1 timeout 500.0 3 [0.00] SYN655-1 timeout 500.0 3 [0.00] SYN688-1 theorem 0.0 2 1 40 0 28 0 0 0 3 40 95 0 0 [0.00] SYN689-1 theorem 0.0 2 1 40 0 28 0 0 0 3 40 95 0 0 [0.00] SYN691-1 theorem 0.0 2 1 33 0 24 0 1 0 8 33 96 0 0 [0.00] SYN702-1 theorem 0.0 4 1 31 0 28 0 0 0 9 31 90 0 0 [0.00] SYN703-1 theorem 0.0 4 1 37 0 29 0 1 0 9 37 114 0 0 [0.00] SYN705-1 theorem 0.0 4 1 37 0 29 0 1 0 9 37 114 0 0 [0.00] SYN706-1 theorem 0.0 4 1 41 0 31 0 0 0 6 41 130 0 0 [0.00] SYN709-1 theorem 0.0 4 1 41 0 35 0 0 0 4 41 114 0 0 [0.00] SYN712-1 theorem 0.1 4 1 42 0 36 0 1 0 10 42 127 0 0 [0.00] SYN715-1 theorem 0.0 4 1 40 0 36 0 0 0 10 40 117 0 0 [0.00] SYN716-1 theorem 0.0 4 1 41 0 36 0 0 0 10 41 122 0 0 [0.00] SYN719-1 theorem 0.0 4 1 49 0 46 0 0 0 3 49 133 0 0 [0.00] SYN720-1 non_thm 0.1 4 0 423 0 132 171 6 0 2 0 3107 0 0 [0.00] SYN721-1 theorem 0.0 4 1 3 0 1 0 0 0 2 3 5 0 0 [0.00] SYN727-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 4 0 0 [0.00] SYN729-1 theorem 0.0 4 1 34 0 1 0 0 0 4 34 71 0 0 [0.00] SYN731-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 0 [0.12] LCL025-1 theorem 5.2 5 1 270 0 4 0 4 0 5 270 18828 0 0 [0.12] LCL045-1 theorem 158.8 11 1 1197 0 6 0 28 0 5 1197 168394 0 0 [0.12] LCL064-2 theorem 0.7 2 1 137 0 3 0 2 0 5 137 5086 0 0 [0.12] LCL065-1 theorem 0.4 2 1 133 0 4 0 1 0 5 133 4748 0 0 [0.12] LCL066-1 theorem 0.5 2 1 146 0 4 0 1 0 5 146 5169 0 0 [0.12] LCL069-1 theorem 3.4 5 1 451 0 4 0 6 0 5 451 21025 0 0 [0.12] LCL072-1 theorem 7.8 7 1 574 0 4 0 13 0 5 574 32921 0 0 [0.12] LCL077-1 theorem 0.3 2 1 109 0 4 0 1 0 5 109 3206 0 0 [0.12] LCL083-1 theorem 1.7 3 1 189 0 2 0 68 0 6 189 7274 0 0 [0.12] LCL083-2 theorem 0.9 2 1 89 0 3 0 1 0 6 89 2953 0 0 [0.12] LCL089-1 theorem 0.3 2 1 86 0 2 0 11 0 6 86 2992 0 0 [0.12] LCL090-1 theorem 0.0 2 1 42 0 2 0 15 0 6 42 485 0 0 [0.12] LCL094-1 theorem 0.5 2 1 78 0 2 0 8 0 6 78 3632 0 0 [0.12] LCL130-1 theorem 235.9 48 1 2303 0 2 0 3 0 6 2303 1919996 0 0 [0.12] LCL195-1 theorem 14.1 7 1 5032 0 6 0 0 0 6 5032 26402 0 0 [0.12] LCL198-1 theorem 0.3 2 1 764 0 6 0 0 0 5 764 2618 0 0 [0.12] LCL231-1 timeout 500.0 46 [0.12] LCL358-1 theorem 0.0 2 1 25 0 4 0 2 0 5 25 136 0 0 [0.12] LCL365-1 theorem 0.1 2 1 70 0 4 0 2 0 5 70 1547 0 0 [0.12] PLA001-1 theorem 0.0 2 1 23 0 12 0 0 0 2 23 41 0 0 [0.12] RNG001-3 theorem 0.0 2 1 9 0 4 0 0 0 2 9 93 0 0 [0.12] RNG005-2 theorem 0.0 3 1 11 0 11 0 0 0 2 11 585 0 0 [0.12] RNG006-2 theorem 0.0 2 1 14 0 13 0 0 0 2 14 695 0 0 [0.12] RNG037-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 310 0 0 [0.12] RNG039-2 theorem 1.2 5 1 64 0 50 0 6 0 2 64 31718 0 0 [0.12] SYN597-1 theorem 0.4 5 1 214 0 11 0 0 0 4 214 5232 0 0 [0.12] SYN601-1 theorem 0.4 5 1 241 0 12 0 0 0 4 241 5656 0 0 [0.12] SYN602-1 theorem 0.1 2 1 89 0 7 0 0 0 3 89 620 0 0 [0.20] PUZ046-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.20] SYN303-1 timeout 500.0 12 [0.25] GRP048-2 theorem 2.3 4 1 45 0 5 0 0 0 3 45 9873 0 0 [0.25] LCL004-1 theorem 2.7 8 1 310 0 2 0 198 0 8 310 29297 0 0 [0.25] LCL006-1 theorem 0.5 2 1 132 0 3 0 0 0 5 132 5234 0 0 [0.25] LCL029-1 theorem 0.7 2 1 138 0 5 0 0 0 5 138 6542 0 0 [0.25] LCL034-1 theorem 19.0 8 1 349 0 2 0 15 0 7 349 50552 0 0 [0.25] LCL036-1 theorem 4.3 4 1 153 0 2 0 7 0 7 153 9617 0 0 [0.25] LCL047-1 theorem 0.1 2 1 86 0 4 0 2 0 5 86 2048 0 0 [0.25] LCL048-1 theorem 0.2 2 1 98 0 4 0 2 0 5 98 2352 0 0 [0.25] LCL049-1 theorem 0.4 2 1 139 0 4 0 6 0 5 139 4871 0 0 [0.25] LCL050-1 theorem 0.5 2 1 141 0 4 0 6 0 5 141 5038 0 0 [0.25] LCL053-1 theorem 0.7 3 1 156 0 4 0 9 0 5 156 6485 0 0 [0.25] LCL056-1 theorem 0.5 2 1 136 0 4 0 7 0 5 136 5122 0 0 [0.25] LCL057-1 theorem 0.3 2 1 120 0 4 0 7 0 5 120 4607 0 0 [0.25] LCL064-1 theorem 18.8 8 1 716 0 4 0 17 0 5 716 58528 0 0 [0.25] LCL068-1 theorem 15.0 5 1 612 0 4 0 18 0 5 612 45060 0 0 [0.25] LCL076-1 theorem 0.2 2 1 94 0 4 0 1 0 5 94 3082 0 0 [0.25] LCL080-2 theorem 1.0 3 1 144 0 5 0 1 0 5 144 6521 0 0 [0.25] LCL092-1 theorem 0.7 2 1 109 0 2 0 12 0 6 109 4568 0 0 [0.25] LCL095-1 theorem 0.4 2 1 121 0 2 0 14 0 6 121 4145 0 0 [0.25] LCL115-1 theorem 0.7 3 1 202 0 5 0 0 0 5 202 8306 0 0 [0.25] LCL123-1 theorem 45.7 10 1 362 0 2 0 3 0 7 362 69980 0 0 [0.25] LCL196-1 theorem 0.4 2 1 787 0 6 0 0 0 5 787 2704 0 0 [0.25] LCL224-1 theorem 14.1 6 1 3424 0 6 0 0 0 6 3424 14060 0 0 [0.25] LCL225-1 theorem 14.3 5 1 3424 0 6 0 0 0 6 3424 13993 0 0 [0.25] LCL234-1 theorem 4.2 4 1 2607 0 6 0 0 0 6 2607 10879 0 0 [0.25] LCL237-1 theorem 4.2 4 1 2608 0 6 0 0 0 6 2608 10884 0 0 [0.25] LCL256-1 theorem 0.2 2 1 110 0 4 0 7 0 5 110 4117 0 0 [0.25] LCL367-1 theorem 0.1 2 1 78 0 4 0 3 0 5 78 1863 0 0 [0.25] LCL379-1 theorem 0.4 2 1 124 0 4 0 7 0 5 124 4762 0 0 [0.25] LCL380-1 theorem 0.7 2 1 156 0 4 0 7 0 5 156 5716 0 0 [0.25] LCL381-1 theorem 0.9 3 1 172 0 4 0 7 0 5 172 6459 0 0 [0.25] LCL396-1 theorem 0.7 3 1 151 0 4 0 7 0 5 151 5921 0 0 [0.25] LCL405-1 theorem 0.5 2 1 160 0 4 0 10 0 5 160 7551 0 0 [0.25] LCL416-1 theorem 0.4 3 1 37 0 2 0 0 0 10 37 659 0 0 [0.25] NUM017-1 timeout 500.0 104 [0.25] NUM283-1.005 theorem 0.2 2 1 155 0 4 0 0 0 25 155 158 0 0 [0.25] PLA004-1 timeout 500.0 59 [0.25] PLA004-2 timeout 500.0 60 [0.25] PLA005-1 timeout 500.0 59 [0.25] PLA005-2 timeout 500.0 59 [0.25] PLA009-1 timeout 500.0 59 [0.25] PLA009-2 timeout 500.0 59 [0.25] PLA011-1 timeout 500.0 59 [0.25] PLA011-2 timeout 500.0 60 [0.25] PLA013-1 timeout 500.0 59 [0.25] PLA014-1 timeout 500.0 59 [0.25] PLA014-2 timeout 500.0 59 [0.25] PLA021-1 timeout 500.0 59 [0.25] PLA022-1 theorem 2.5 8 1 1066 0 20 0 0 0 4 1066 20905 0 0 [0.25] PLA022-2 theorem 2.5 8 1 1066 0 20 0 0 0 4 1066 20905 0 0 [0.25] PUZ039-1 timeout 500.0 450 [0.25] PUZ040-1 timeout 500.0 491 [0.25] PUZ042-1 timeout 500.0 456 [0.25] RNG001-5 theorem 0.5 3 1 57 0 8 0 0 0 2 57 12262 0 0 [0.25] SYN311-1 theorem 2.1 11 1 13067 0 2 0 0 0 3 13067 40552 0 0 [0.25] SYN572-1 theorem 0.5 4 1 141 0 9 0 0 0 5 141 4216 0 0 [0.25] SYN577-1 theorem 0.1 2 1 80 0 12 0 0 0 3 80 905 0 0 [0.25] SYN598-1 timeout 500.0 49 [0.25] SYN599-1 timeout 500.0 48 [0.25] SYN603-1 theorem 17.9 24 1 863 0 7 0 0 0 4 863 81397 0 0 [0.25] SYN616-1 theorem 0.5 6 1 156 0 13 0 0 0 3 156 5731 0 0 [0.25] SYN628-1 theorem 0.3 4 1 111 0 15 0 0 0 3 111 3904 0 0 [0.25] SYN653-1 timeout 500.0 3 [0.25] SYN704-1 timeout 500.0 114 [0.25] SYN707-1 timeout 500.0 26 [0.25] SYN708-1 timeout 500.0 26 [0.38] LCL003-1 theorem 461.7 30 1 2838 0 2 0 415 0 8 2838 1951196 0 0 [0.38] LCL014-1 theorem 9.6 7 1 245 0 2 0 1 0 7 245 29886 0 0 [0.38] LCL016-1 theorem 116.0 21 1 635 0 2 0 0 0 8 635 188208 0 0 [0.38] LCL024-1 timeout 500.0 82 [0.38] LCL026-1 theorem 22.3 6 1 458 0 4 0 4 0 5 458 45121 0 0 [0.38] LCL031-1 theorem 168.8 9 1 838 0 5 0 27 0 5 838 151755 0 0 [0.38] LCL039-1 theorem 58.1 9 1 1062 0 6 0 4 0 5 1062 115810 0 0 [0.38] LCL040-1 theorem 26.7 8 1 946 0 6 0 14 0 5 946 60040 0 0 [0.38] LCL042-1 theorem 180.4 13 1 1298 0 6 0 29 0 5 1298 181161 0 0 [0.38] LCL051-1 theorem 0.5 2 1 131 0 4 0 6 0 5 131 4764 0 0 [0.38] LCL052-1 theorem 0.5 2 1 134 0 4 0 7 0 5 134 5093 0 0 [0.38] LCL055-1 theorem 1.0 3 1 185 0 4 0 6 0 5 185 6852 0 0 [0.38] LCL058-1 theorem 48.7 8 1 789 0 4 0 17 0 5 789 89959 0 0 [0.38] LCL059-1 theorem 0.9 3 1 164 0 4 0 9 0 5 164 6603 0 0 [0.38] LCL067-1 timeout 500.0 20 [0.38] LCL070-1 theorem 27.3 9 1 966 0 4 0 56 0 5 966 68707 0 0 [0.38] LCL071-1 theorem 15.2 5 1 621 0 4 0 21 0 5 621 46437 0 0 [0.38] LCL080-1 theorem 1.0 2 1 144 0 4 0 1 0 5 144 6520 0 0 [0.38] LCL093-1 theorem 59.6 8 1 423 0 2 0 19 0 6 423 63419 0 0 [0.38] LCL113-1 theorem 33.2 7 1 800 0 5 0 11 0 5 800 67077 0 0 [0.38] LCL121-1 theorem 4.8 6 1 183 0 2 0 3 0 7 183 20094 0 0 [0.38] LCL128-1 theorem 0.2 2 1 48 0 2 0 1 0 7 48 1587 0 0 [0.38] LCL131-1 theorem 0.4 2 1 150 0 2 0 1 0 5 150 10311 0 0 [0.38] LCL250-1 theorem 5.0 7 1 6335 0 6 0 0 0 6 6335 24523 0 0 [0.38] LCL368-1 theorem 0.7 3 1 157 0 4 0 6 0 5 157 5688 0 0 [0.38] LCL378-1 theorem 0.8 3 1 165 0 4 0 6 0 5 165 6057 0 0 [0.38] LCL385-1 theorem 1.1 3 1 182 0 4 0 10 0 5 182 9270 0 0 [0.38] LCL386-1 theorem 1.3 3 1 194 0 4 0 13 0 5 194 8600 0 0 [0.38] LCL387-1 theorem 5.0 5 1 368 0 4 0 16 0 5 368 22439 0 0 [0.38] LCL388-1 theorem 107.3 10 1 1053 0 4 0 21 0 5 1053 143278 0 0 [0.38] LCL389-1 theorem 28.0 8 1 662 0 4 0 13 0 5 662 74347 0 0 [0.38] LCL400-1 theorem 1.3 3 1 181 0 4 0 9 0 5 181 7344 0 0 [0.38] LCL401-1 theorem 2.1 4 1 225 0 4 0 12 0 5 225 11731 0 0 [0.38] LCL402-1 theorem 1.6 3 1 206 0 4 0 12 0 5 206 10548 0 0 [0.38] NUM284-1.014 theorem 32.0 6 1 249 0 4 0 0 0 234 249 524 0 0 [0.38] PLA007-1 timeout 500.0 59 [0.38] PLA016-1 timeout 500.0 58 [0.38] PLA019-1 timeout 500.0 59 [0.38] PLA023-1 timeout 500.0 59 [0.38] RNG001-2 theorem 0.8 3 1 64 0 7 0 0 0 2 64 16590 0 0 [0.38] RNG004-3 timeout 500.0 289 [0.38] SWV014-1 timeout 500.0 305 [0.38] SYN556-1 timeout 500.0 12 [0.38] SYN600-1 timeout 500.0 201 [0.38] SYN617-1 timeout 500.0 167 [0.38] SYN629-1 theorem 0.3 4 1 111 0 15 0 0 0 3 111 3904 0 0 [0.38] SYN639-1 timeout 500.0 204 [0.38] SYN640-1 timeout 500.0 191 [0.38] SYN646-1 timeout 500.0 136 [0.38] SYN647-1 timeout 500.0 136 [0.38] SYN711-1 timeout 500.0 39 [0.40] GRP394-2 timeout 500.0 262 [0.40] LCL411-1 timeout 500.0 85 [0.40] LCL415-1 timeout 500.0 302 [0.40] NUM286-2 timeout 500.0 176 [0.40] NUM287-1 timeout 500.0 54 [0.40] SWV012-1 timeout 500.0 311 [0.50] ANA003-2 timeout 500.0 137 [0.50] LCL005-1 timeout 500.0 39 [0.50] LCL012-1 theorem 30.9 11 1 410 0 2 0 0 0 7 410 71592 0 0 [0.50] LCL015-1 theorem 134.3 14 1 402 0 2 0 0 0 8 402 78866 0 0 [0.50] LCL017-1 timeout 500.0 26 [0.50] LCL018-1 theorem 95.1 14 1 349 0 2 0 0 0 9 349 66924 0 0 [0.50] LCL019-1 timeout 500.0 81 [0.50] LCL028-1 theorem 359.5 12 1 1159 0 4 0 93 0 5 1159 244393 0 0 [0.50] LCL054-1 theorem 137.6 12 1 1170 0 4 0 27 0 5 1170 155100 0 0 [0.50] LCL060-1 theorem 265.6 15 1 1466 0 4 0 31 0 5 1466 225874 0 0 [0.50] LCL085-1 timeout 500.0 22 [0.50] LCL114-1 theorem 44.0 8 1 869 0 5 0 24 0 5 869 80481 0 0 [0.50] LCL116-1 theorem 78.6 8 1 1037 0 5 0 14 0 5 1037 123260 0 0 [0.50] LCL119-1 timeout 500.0 70 [0.50] LCL122-1 theorem 50.3 32 1 894 0 2 0 3 0 7 894 370005 0 0 [0.50] LCL127-1 theorem 2.8 5 1 127 0 2 0 5 0 7 127 10172 0 0 [0.50] LCL129-1 theorem 65.0 6 1 341 0 2 0 2 0 6 341 50295 0 0 [0.50] LCL167-1 timeout 500.0 58 [0.50] LCL191-1 theorem 18.3 8 1 4435 0 6 0 0 0 6 4435 22814 0 0 [0.50] LCL223-1 theorem 27.7 18 1 21633 0 6 0 0 0 6 21633 73813 0 0 [0.50] LCL227-1 timeout 500.0 84 [0.50] LCL369-1 theorem 0.7 2 1 155 0 4 0 11 0 5 155 6421 0 0 [0.50] LCL370-1 theorem 0.9 3 1 169 0 4 0 12 0 5 169 7234 0 0 [0.50] LCL371-1 theorem 0.9 3 1 169 0 4 0 12 0 5 169 7234 0 0 [0.50] LCL372-1 theorem 3.3 4 1 298 0 4 0 15 0 5 298 17990 0 0 [0.50] LCL373-1 theorem 5.1 6 1 352 0 4 0 19 0 5 352 22638 0 0 [0.50] LCL374-1 theorem 9.1 7 1 452 0 4 0 17 0 5 452 31319 0 0 [0.50] LCL382-1 theorem 1.1 3 1 196 0 4 0 10 0 5 196 9813 0 0 [0.50] LCL383-1 theorem 26.2 8 1 661 0 4 0 13 0 5 661 70075 0 0 [0.50] LCL384-1 theorem 0.3 2 1 125 0 4 0 6 0 5 125 4277 0 0 [0.50] LCL390-1 theorem 4.0 5 1 332 0 4 0 17 0 5 332 19832 0 0 [0.50] LCL391-1 timeout 500.0 15 [0.50] LCL392-1 theorem 287.0 15 1 1523 0 4 0 30 0 5 1523 229619 0 0 [0.50] PLA008-1 timeout 500.0 59 [0.50] PLA010-1 timeout 500.0 59 [0.50] PLA012-1 timeout 500.0 59 [0.50] PLA015-1 timeout 500.0 59 [0.50] PLA018-1 timeout 500.0 59 [0.50] PUZ037-3 theorem 0.6 13 1 173 0 2 0 0 0 2 173 3105 0 0 [0.50] SYN631-1 timeout 500.0 91 [0.60] PUZ048-1 timeout 500.0 408 [0.60] PUZ049-1 timeout 500.0 458 [0.62] LCL020-1 timeout 500.0 58 [0.62] LCL021-1 timeout 500.0 69 [0.62] LCL038-1 timeout 500.0 28 [0.62] LCL061-1 timeout 500.0 18 [0.62] LCL100-1 theorem 434.4 66 1 2865 0 3 0 0 0 6 2865 2873747 0 0 [0.62] LCL166-1 timeout 500.0 83 [0.62] LCL222-1 theorem 31.1 17 1 19631 0 6 0 0 0 6 19631 67543 0 0 [0.62] LCL375-1 timeout 500.0 17 [0.62] LCL393-1 timeout 500.0 17 [0.62] LCL403-1 theorem 84.7 9 1 955 0 4 0 18 0 5 955 126640 0 0 [0.62] LCL404-1 theorem 22.4 7 1 606 0 4 0 13 0 5 606 65695 0 0 [0.62] SYN614-1 timeout 500.0 340 [0.75] LCL002-1 timeout 500.0 38 [0.75] LCL030-1 theorem 44.2 7 1 496 0 5 0 14 0 5 496 59839 0 0 [0.75] LCL062-1 timeout 500.0 15 [0.75] LCL084-2 timeout 500.0 28 [0.75] LCL103-1 theorem 3.7 6 1 347 0 3 0 0 0 6 347 52313 0 0 [0.75] LCL105-1 timeout 500.0 84 [0.75] LCL124-1 timeout 500.0 62 [0.75] LCL221-1 theorem 28.1 16 1 18689 0 6 0 0 0 6 18689 65074 0 0 [0.75] LCL249-1 timeout 500.0 80 [0.75] LCL253-1 timeout 500.0 85 [0.75] LCL376-1 theorem 430.8 18 1 1679 0 4 0 27 0 5 1679 277887 0 0 [0.75] LCL377-1 timeout 500.0 18 [0.75] LCL394-1 timeout 500.0 14 [0.75] LCL395-1 timeout 500.0 18 [0.75] SYN615-1 timeout 500.0 387 [0.80] LCL078-1 timeout 500.0 10 [0.80] LCL168-1 timeout 500.0 139 [0.80] LCL179-1 timeout 500.0 77 [0.80] LCL180-1 timeout 500.0 79 [0.80] LCL181-1 timeout 500.0 66 [0.80] LCL183-1 timeout 500.0 51 [0.80] LCL184-1 timeout 500.0 81 [0.80] LCL209-1 timeout 500.0 69 [0.80] LCL219-1 timeout 500.0 71 [0.80] LCL220-1 timeout 500.0 78 [0.80] LCL235-1 timeout 500.0 43 [0.80] LCL239-1 timeout 500.0 84 [0.80] LCL240-1 timeout 500.0 81 [0.80] LCL241-1 timeout 500.0 81 [0.80] LCL242-1 timeout 500.0 46 [0.80] LCL244-1 timeout 500.0 50 [0.80] LCL245-1 timeout 500.0 50 [0.80] LCL246-1 timeout 500.0 82 [0.80] LCL247-1 timeout 500.0 84 [0.80] LCL248-1 timeout 500.0 51 [0.80] LCL252-1 timeout 500.0 60 [0.80] LCL255-1 timeout 500.0 58 [0.88] LCL032-1 timeout 500.0 51 [0.88] LCL037-1 timeout 500.0 45 [0.88] LCL084-3 timeout 500.0 27 [0.88] LCL099-1 theorem 454.0 68 1 2905 0 3 0 1 0 6 2905 2966051 0 0 [0.88] LCL125-1 timeout 500.0 85 [1.00] ANA004-2 timeout 500.0 126 [1.00] ANA005-2 timeout 500.0 133 [1.00] GEO001-4 timeout 500.0 60 [1.00] LCL001-1 timeout 500.0 10 [1.00] LCL063-1 timeout 500.0 17 [1.00] LCL073-1 timeout 500.0 48 [1.00] LCL074-1 timeout 500.0 71 [1.00] LCL109-1 timeout 500.0 13 [1.00] LCL228-1 timeout 500.0 84 [1.00] LCL229-1 timeout 500.0 83 [1.00] LCL243-1 timeout 500.0 81 [1.00] LCL251-1 timeout 500.0 58 [1.00] LCL254-1 timeout 500.0 84 [1.00] LCL417-1 timeout 500.0 71 [1.00] LCL418-1 timeout 500.0 17 [1.00] LCL419-1 timeout 500.0 11 [1.00] LCL420-1 timeout 500.0 10 [1.00] LCL421-1 timeout 500.0 11 [1.00] LCL422-1 timeout 500.0 11 [1.00] LCL423-1 timeout 500.0 34 [1.00] LCL424-1 timeout 500.0 10 [1.00] LCL425-1 timeout 500.0 45 [1.00] LCL426-1 timeout 500.0 28 [1.00] LCL427-1 timeout 500.0 19 [1.00] NUM026-1 timeout 500.0 33 [1.00] PUZ041-1 timeout 500.0 458 [1.00] PUZ050-1 memory 331.8 499 [1.00] PUZ051-1 timeout 500.0 466 [1.00] ROB025-1 timeout 500.0 96