-------------------------------------------------------------------------------- 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 -------------------------------------------------------------------------------- Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug ALG001-1 timeout 500.0 8 ALG001-2 memory 440.0 499 ALG001-3 timeout 500.0 65 ALG009-1 memory 442.6 499 ANA003-3 timeout 500.0 90 ANA004-3 timeout 500.0 91 ANA005-3 timeout 500.0 93 ANA006-2 timeout 500.0 284 CAT001-3 theorem 452.4 14 1 441 0 8 0 0 0 3 441 6157 5627 0 CAT002-3 theorem 88.2 7 1 119 0 8 0 0 0 3 119 983 755 0 CAT003-3 theorem 332.1 10 1 195 0 8 0 0 0 3 195 1906 1725 0 CAT004-3 theorem 83.8 7 1 117 0 8 0 0 0 3 117 955 751 0 CAT005-3 theorem 0.7 3 1 46 0 6 0 0 0 3 46 351 278 0 CAT006-3 theorem 0.7 3 1 43 0 6 0 0 0 3 43 328 255 0 CAT009-3 timeout 500.0 73 CAT011-3 timeout 500.0 53 CAT012-3 theorem 0.0 2 1 20 0 6 0 0 0 3 20 127 118 0 CAT013-3 theorem 0.0 2 1 9 0 6 0 0 0 3 9 48 38 0 CAT014-3 timeout 500.0 53 CAT015-3 non_thm 0.0 2 0 7 0 24 20 4 47 5 0 52 49 0 CAT015-4 non_thm 0.0 2 0 7 0 19 15 4 36 5 0 42 38 0 CAT016-3 theorem 0.0 2 1 15 0 6 0 0 0 2 15 61 18 0 CAT017-3 theorem 0.0 2 1 15 0 6 0 0 0 2 15 61 18 0 CAT018-3 timeout 500.0 63 CAT019-3 theorem 0.0 2 1 35 0 5 0 0 0 2 35 156 22 0 CAT020-3 timeout 500.0 151 COL074-1 timeout 500.0 58 COL074-2 timeout 500.0 54 COL074-3 timeout 500.0 21 COL075-1 timeout 500.0 58 COL076-1 timeout 500.0 56 COL077-1 timeout 500.0 41 COL078-1 timeout 500.0 41 COL079-1 timeout 500.0 49 COL080-1 timeout 500.0 40 COL081-1 timeout 500.0 40 COL082-1 timeout 500.0 14 GEO001-1 timeout 500.0 124 GEO001-2 timeout 500.0 121 GEO001-3 timeout 500.0 114 GEO002-1 theorem 9.1 9 1 54 0 8 0 6 0 2 54 1531 68593 0 GEO002-2 theorem 8.4 8 1 48 0 8 0 3 0 2 48 1227 52544 0 GEO002-3 theorem 0.0 2 1 15 0 15 0 0 0 2 15 292 715 0 GEO003-1 theorem 0.0 2 1 12 0 8 0 0 0 2 12 150 273 0 GEO003-2 theorem 0.0 2 1 11 0 8 0 0 0 2 11 115 209 0 GEO003-3 theorem 0.0 2 1 14 0 14 0 0 0 2 14 232 443 0 GEO004-1 timeout 500.0 126 GEO004-2 timeout 500.0 120 GEO005-1 timeout 500.0 125 GEO005-2 timeout 500.0 120 GEO006-1 timeout 500.0 121 GEO006-2 timeout 500.0 122 GEO006-3 timeout 500.0 104 GEO007-1 timeout 500.0 126 GEO007-2 timeout 500.0 121 GEO007-3 timeout 500.0 69 GEO008-1 timeout 500.0 123 GEO008-2 timeout 500.0 120 GEO008-3 timeout 500.0 71 GEO009-1 timeout 500.0 124 GEO009-2 timeout 500.0 122 GEO009-3 timeout 500.0 70 GEO010-1 timeout 500.0 127 GEO010-2 timeout 500.0 124 GEO010-3 timeout 500.0 68 GEO011-1 timeout 500.0 126 GEO011-2 theorem 0.0 2 1 8 0 8 0 0 0 2 8 72 61 0 GEO011-3 theorem 0.3 3 1 24 0 25 0 0 0 2 24 2483 4272 0 GEO011-4 theorem 0.0 2 1 7 0 7 0 0 0 2 7 68 50 0 GEO011-5 theorem 0.0 2 1 7 0 7 0 0 0 2 7 52 30 0 GEO012-1 timeout 500.0 123 GEO012-2 timeout 500.0 122 GEO012-3 timeout 500.0 67 GEO013-1 timeout 500.0 122 GEO013-2 timeout 500.0 125 GEO013-3 timeout 500.0 67 GEO014-2 theorem 0.0 2 1 8 0 8 0 0 0 2 8 72 51 0 GEO015-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 92 58 0 GEO015-3 theorem 0.0 2 1 10 0 10 0 0 0 2 10 109 176 0 GEO016-2 theorem 0.0 2 1 9 0 9 0 0 0 2 9 80 55 0 GEO016-3 theorem 0.0 2 1 10 0 10 0 0 0 2 10 111 178 0 GEO017-2 theorem 0.0 2 1 11 0 9 0 0 0 2 11 117 185 0 GEO017-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 120 187 0 GEO018-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 89 58 0 GEO018-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 129 187 0 GEO019-2 theorem 0.0 2 1 9 0 9 0 0 0 2 9 82 56 0 GEO019-3 theorem 0.0 2 1 10 0 10 0 0 0 2 10 119 184 0 GEO020-2 theorem 0.0 2 1 11 0 9 0 0 0 2 11 114 183 0 GEO020-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 120 187 0 GEO021-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 89 58 0 GEO021-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 129 187 0 GEO022-2 theorem 0.0 2 1 12 0 10 0 0 0 2 12 130 195 0 GEO022-3 theorem 0.0 2 1 12 0 11 0 0 0 2 12 168 223 0 GEO024-2 theorem 0.0 2 1 11 0 8 0 0 0 2 11 120 188 0 GEO024-3 theorem 0.0 2 1 15 0 14 0 0 0 2 15 250 328 0 GEO025-2 timeout 500.0 123 GEO025-3 timeout 500.0 119 GEO026-2 theorem 0.0 2 1 14 0 12 0 0 0 2 14 157 275 0 GEO026-3 theorem 0.0 2 1 20 0 19 0 0 0 2 20 409 739 0 GEO027-2 theorem 0.1 2 1 20 0 10 0 0 0 2 20 442 1239 0 GEO027-3 theorem 0.0 2 1 18 0 17 0 0 0 2 18 344 632 0 GEO028-2 timeout 500.0 116 GEO028-3 timeout 500.0 113 GEO029-2 timeout 500.0 117 GEO029-3 theorem 7.4 6 1 52 0 16 0 0 0 2 52 4258 41496 0 GEO030-2 timeout 500.0 120 GEO030-3 timeout 500.0 102 GEO031-2 timeout 500.0 118 GEO031-3 timeout 500.0 102 GEO032-2 timeout 500.0 124 GEO032-3 theorem 0.2 2 1 27 0 28 0 0 0 2 27 1652 3159 0 GEO033-2 timeout 500.0 119 GEO033-3 theorem 0.3 3 1 31 0 31 0 0 0 2 31 2362 4694 0 GEO034-2 timeout 500.0 119 GEO034-3 timeout 500.0 93 GEO035-2 theorem 0.0 2 1 8 0 8 0 0 0 2 8 66 51 0 GEO035-3 theorem 0.0 2 1 9 0 9 0 0 0 2 9 118 199 0 GEO036-2 timeout 500.0 121 GEO036-3 timeout 500.0 105 GEO037-2 timeout 500.0 119 GEO037-3 timeout 500.0 103 GEO038-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 86 64 0 GEO038-3 theorem 0.0 2 1 12 0 11 0 0 0 2 12 159 244 0 GEO039-2 timeout 500.0 122 GEO039-3 timeout 500.0 115 GEO040-2 timeout 500.0 121 GEO040-3 timeout 500.0 104 GEO041-2 timeout 500.0 120 GEO041-3 timeout 500.0 104 GEO042-2 timeout 500.0 121 GEO042-3 timeout 500.0 104 GEO043-2 timeout 500.0 120 GEO043-3 timeout 500.0 105 GEO044-2 timeout 500.0 124 GEO044-3 timeout 500.0 103 GEO045-2 timeout 500.0 122 GEO045-3 timeout 500.0 103 GEO046-2 timeout 500.0 120 GEO046-3 timeout 500.0 103 GEO047-2 timeout 500.0 120 GEO047-3 timeout 500.0 104 GEO048-2 timeout 500.0 122 GEO048-3 timeout 500.0 102 GEO049-2 timeout 500.0 123 GEO049-3 timeout 500.0 65 GEO050-2 timeout 500.0 125 GEO050-3 timeout 500.0 69 GEO051-2 timeout 500.0 125 GEO051-3 timeout 500.0 69 GEO052-2 timeout 500.0 122 GEO052-3 timeout 500.0 70 GEO053-2 timeout 500.0 119 GEO053-3 theorem 0.6 3 1 29 0 29 0 0 0 2 29 3658 6484 0 GEO054-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 85 65 0 GEO054-3 theorem 0.0 2 1 11 0 11 0 0 0 2 11 154 239 0 GEO055-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 89 62 0 GEO055-3 theorem 0.0 2 1 12 0 11 0 0 0 2 12 185 235 0 GEO056-2 timeout 500.0 108 GEO056-3 theorem 0.0 2 1 15 0 14 0 0 0 2 15 265 377 0 GEO057-2 theorem 0.0 2 1 14 0 9 0 0 0 2 14 152 233 0 GEO057-3 theorem 0.0 2 1 13 0 13 0 0 0 2 13 191 300 0 GEO058-2 timeout 500.0 113 GEO058-3 theorem 0.1 2 1 23 0 15 0 0 0 2 23 570 1207 0 GEO059-2 timeout 500.0 109 GEO059-3 theorem 0.1 2 1 22 0 15 0 0 0 2 22 505 1128 0 GEO060-2 timeout 500.0 110 GEO061-2 timeout 500.0 108 GEO061-3 timeout 500.0 95 GEO062-2 timeout 500.0 108 GEO062-3 timeout 500.0 68 GEO063-2 timeout 500.0 105 GEO063-3 timeout 500.0 65 GEO064-2 timeout 500.0 124 GEO064-3 theorem 0.5 3 1 28 0 28 0 0 0 2 28 3383 6051 0 GEO065-2 timeout 500.0 124 GEO065-3 theorem 0.5 3 1 28 0 28 0 0 0 2 28 3383 6051 0 GEO066-2 timeout 500.0 124 GEO066-3 theorem 0.5 3 1 28 0 28 0 0 0 2 28 3383 6051 0 GEO067-2 timeout 500.0 124 GEO067-3 timeout 500.0 66 GEO068-2 timeout 500.0 125 GEO068-3 timeout 500.0 65 GEO069-2 timeout 500.0 124 GEO069-3 timeout 500.0 68 GEO070-2 timeout 500.0 120 GEO070-3 timeout 500.0 66 GEO071-2 timeout 500.0 119 GEO071-3 timeout 500.0 67 GEO072-2 timeout 500.0 119 GEO072-3 timeout 500.0 68 GEO073-1 timeout 500.0 119 GEO073-2 timeout 500.0 121 GEO073-3 timeout 500.0 69 GEO074-2 timeout 500.0 120 GEO075-2 timeout 500.0 96 GEO076-4 theorem 0.3 2 1 108 0 3 0 0 0 3 108 898 2793 0 GEO077-4 theorem 0.3 3 1 89 0 13 0 0 0 2 89 491 7913 0 GEO078-4 timeout 500.0 21 GEO078-5 timeout 500.0 40 GEO080-1 theorem 0.0 2 1 4 0 3 0 0 0 2 4 18 21 0 GEO081-1 theorem 0.0 2 1 52 0 5 0 0 0 2 52 254 350 0 GEO082-1 theorem 0.1 2 2 117 9 5 0 0 916 2 125 1307 1715 0 GEO083-1 timeout 500.0 34 GEO084-1 timeout 500.0 52 GEO085-1 timeout 500.0 188 GEO086-1 theorem 0.0 2 1 12 0 5 0 0 0 2 12 75 51 0 GEO087-1 theorem 0.0 2 1 7 0 4 0 0 0 2 7 46 33 0 GEO088-1 timeout 500.0 101 GEO089-1 timeout 500.0 101 GEO090-1 timeout 500.0 17 GEO091-1 timeout 500.0 12 GEO092-1 timeout 500.0 122 GEO093-1 timeout 500.0 39 GEO094-1 theorem 0.0 2 1 52 0 6 0 0 0 2 52 254 477 0 GEO095-1 memory 474.4 499 GEO096-1 timeout 500.0 15 GEO097-1 timeout 500.0 123 GEO098-1 timeout 500.0 108 GEO099-1 timeout 500.0 13 GEO100-1 timeout 500.0 181 GEO101-1 timeout 500.0 182 GEO102-1 timeout 500.0 12 GEO103-1 timeout 500.0 14 GEO104-1 timeout 500.0 38 GEO105-1 timeout 500.0 12 GEO106-1 timeout 500.0 13 GEO107-1 timeout 500.0 38 GEO108-1 timeout 500.0 31 GEO109-1 timeout 500.0 146 GEO110-1 timeout 500.0 16 GEO111-1 theorem 0.0 2 1 42 0 4 5 0 0 2 42 212 394 0 GEO112-1 theorem 0.0 2 1 22 0 4 0 0 0 2 22 96 111 0 GEO113-1 timeout 500.0 116 GEO114-1 timeout 500.0 191 GEO115-1 timeout 500.0 29 GEO116-1 timeout 500.0 11 GEO117-1 theorem 0.0 2 1 7 0 5 0 0 0 2 7 37 25 0 GEO118-1 theorem 0.0 2 1 8 0 6 0 0 0 2 8 46 32 0 GEO119-1 timeout 500.0 30 GEO120-1 timeout 500.0 28 GEO121-1 timeout 500.0 37 GEO122-1 timeout 500.0 189 GEO123-1 timeout 500.0 24 GEO124-1 theorem 0.0 2 1 26 0 7 0 0 0 2 26 107 134 0 GEO125-1 theorem 0.0 2 1 26 0 7 0 0 0 2 26 106 134 0 GEO126-1 timeout 500.0 199 GEO127-1 timeout 500.0 27 GEO128-1 timeout 500.0 24 GEO129-1 timeout 500.0 58 GEO130-1 timeout 500.0 20 GEO131-1 timeout 500.0 25 GEO132-1 timeout 500.0 10 GEO133-1 timeout 500.0 13 GEO134-1 timeout 500.0 16 GEO135-1 timeout 500.0 44 GEO136-1 timeout 500.0 16 GEO137-1 timeout 500.0 8 GEO138-1 timeout 500.0 8 GEO139-1 memory 201.5 499 GEO140-1 timeout 500.0 21 GEO141-1 timeout 500.0 24 GEO142-1 timeout 500.0 23 GEO143-1 timeout 500.0 19 GEO144-1 timeout 500.0 12 GEO145-1 timeout 500.0 295 GEO146-1 timeout 500.0 74 GEO147-1 timeout 500.0 83 GEO148-1 timeout 500.0 54 GEO149-1 timeout 500.0 28 GEO150-1 timeout 500.0 143 GEO151-1 timeout 500.0 21 GEO152-1 timeout 500.0 21 GEO153-1 timeout 500.0 128 GEO153-2 timeout 500.0 121 GEO154-1 timeout 500.0 127 GEO154-2 timeout 500.0 123 GEO155-1 timeout 500.0 110 GEO156-1 timeout 500.0 109 GEO157-1 timeout 500.0 63 GEO158-1 timeout 500.0 57 GEO159-1 timeout 500.0 70 GEO160-1 timeout 500.0 214 GEO161-1 timeout 500.0 130 GRP001-3 timeout 500.0 460 GRP008-1 theorem 3.8 6 2 81 1 7 0 0 42222 2 81 42594 42367 0 GRP015-1 memory 462.2 499 GRP016-1 memory 481.5 499 GRP024-4 timeout 500.0 391 GRP025-1 timeout 500.0 79 GRP025-2 timeout 500.0 129 GRP025-4 timeout 500.0 131 GRP026-1 timeout 500.0 101 GRP026-2 timeout 500.0 164 GRP026-4 timeout 500.0 170 GRP027-1 timeout 500.0 27 GRP039-1 timeout 500.0 87 GRP039-2 timeout 500.0 29 GRP039-3 timeout 500.0 89 GRP039-4 timeout 500.0 88 GRP039-5 timeout 500.0 29 GRP039-7 timeout 500.0 30 GRP040-3 timeout 500.0 159 GRP040-4 timeout 500.0 155 GRP113-1 timeout 500.0 20 GRP208-1 timeout 500.0 66 GRP209-1 timeout 500.0 66 GRP210-1 timeout 500.0 63 GRP211-1 timeout 500.0 79 GRP212-1 timeout 500.0 119 GRP213-1 timeout 500.0 119 GRP214-1 timeout 500.0 45 GRP215-1 timeout 500.0 65 GRP216-1 timeout 500.0 122 GRP217-1 timeout 500.0 63 GRP218-1 timeout 500.0 66 GRP219-1 timeout 500.0 68 GRP220-1 timeout 500.0 120 GRP221-1 timeout 500.0 120 GRP222-1 timeout 500.0 65 GRP223-1 timeout 500.0 76 GRP224-1 timeout 500.0 63 GRP225-1 timeout 500.0 68 GRP226-1 timeout 500.0 77 GRP227-1 timeout 500.0 119 GRP228-1 timeout 500.0 120 GRP229-1 timeout 500.0 122 GRP230-1 timeout 500.0 63 GRP231-1 timeout 500.0 119 GRP232-1 timeout 500.0 119 GRP233-1 timeout 500.0 119 GRP234-1 timeout 500.0 121 GRP235-1 timeout 500.0 119 GRP236-1 timeout 500.0 116 GRP237-1 timeout 500.0 119 GRP238-1 timeout 500.0 121 GRP239-1 timeout 500.0 119 GRP240-1 timeout 500.0 123 GRP241-1 timeout 500.0 122 GRP242-1 timeout 500.0 121 GRP243-1 timeout 500.0 75 GRP244-1 timeout 500.0 65 GRP245-1 timeout 500.0 72 GRP246-1 timeout 500.0 63 GRP247-1 timeout 500.0 77 GRP248-1 timeout 500.0 70 GRP249-1 timeout 500.0 74 GRP250-1 timeout 500.0 76 GRP251-1 timeout 500.0 75 GRP252-1 timeout 500.0 68 GRP253-1 timeout 500.0 71 GRP254-1 timeout 500.0 66 GRP255-1 timeout 500.0 69 GRP256-1 timeout 500.0 74 GRP257-1 timeout 500.0 70 GRP258-1 timeout 500.0 67 GRP259-1 timeout 500.0 69 GRP260-1 timeout 500.0 67 GRP261-1 timeout 500.0 74 GRP262-1 timeout 500.0 69 GRP263-1 timeout 500.0 67 GRP264-1 timeout 500.0 75 GRP265-1 timeout 500.0 67 GRP266-1 timeout 500.0 69 GRP267-1 timeout 500.0 94 GRP268-1 timeout 500.0 90 GRP269-1 timeout 500.0 67 GRP270-1 timeout 500.0 69 GRP271-1 timeout 500.0 67 GRP272-1 timeout 500.0 67 GRP273-1 timeout 500.0 67 GRP274-1 timeout 500.0 61 GRP275-1 timeout 500.0 75 GRP276-1 timeout 500.0 121 GRP277-1 timeout 500.0 73 GRP278-1 timeout 500.0 67 GRP279-1 timeout 500.0 63 GRP280-1 timeout 500.0 77 GRP281-1 timeout 500.0 74 GRP282-1 timeout 500.0 119 GRP283-1 timeout 500.0 122 GRP284-1 timeout 500.0 74 GRP285-1 timeout 500.0 75 GRP286-1 timeout 500.0 70 GRP287-1 timeout 500.0 79 GRP288-1 timeout 500.0 67 GRP289-1 timeout 500.0 69 GRP290-1 timeout 500.0 63 GRP291-1 timeout 500.0 61 GRP292-1 timeout 500.0 38 GRP293-1 timeout 500.0 73 GRP294-1 timeout 500.0 77 GRP295-1 timeout 500.0 74 GRP296-1 timeout 500.0 75 GRP297-1 timeout 500.0 84 GRP298-1 timeout 500.0 80 GRP299-1 timeout 500.0 86 GRP300-1 timeout 500.0 122 GRP301-1 timeout 500.0 121 GRP302-1 timeout 500.0 180 GRP303-1 timeout 500.0 73 GRP304-1 timeout 500.0 175 GRP305-1 timeout 500.0 126 GRP306-1 timeout 500.0 96 GRP307-1 timeout 500.0 68 GRP308-1 timeout 500.0 139 GRP309-1 timeout 500.0 128 GRP310-1 timeout 500.0 90 GRP311-1 timeout 500.0 126 GRP312-1 timeout 500.0 67 GRP313-1 timeout 500.0 75 GRP314-1 timeout 500.0 77 GRP315-1 timeout 500.0 76 GRP316-1 timeout 500.0 62 GRP317-1 timeout 500.0 119 GRP318-1 timeout 500.0 68 GRP319-1 timeout 500.0 77 GRP320-1 timeout 500.0 69 GRP321-1 timeout 500.0 69 GRP322-1 timeout 500.0 80 GRP323-1 timeout 500.0 79 GRP324-1 timeout 500.0 119 GRP325-1 timeout 500.0 96 GRP326-1 timeout 500.0 64 GRP327-1 timeout 500.0 63 GRP328-1 timeout 500.0 119 GRP329-1 timeout 500.0 119 GRP330-1 timeout 500.0 67 GRP331-1 timeout 500.0 75 GRP332-1 timeout 500.0 73 GRP333-1 timeout 500.0 70 GRP334-1 timeout 500.0 121 GRP335-1 timeout 500.0 74 GRP336-1 timeout 500.0 79 GRP337-1 timeout 500.0 119 GRP338-1 timeout 500.0 67 GRP339-1 timeout 500.0 62 GRP340-1 timeout 500.0 67 GRP341-1 timeout 500.0 69 GRP342-1 timeout 500.0 63 GRP343-1 timeout 500.0 53 GRP344-1 timeout 500.0 66 GRP345-1 timeout 500.0 131 GRP346-1 timeout 500.0 127 GRP347-1 timeout 500.0 121 GRP348-1 timeout 500.0 67 GRP349-1 timeout 500.0 127 GRP350-1 timeout 500.0 67 GRP351-1 timeout 500.0 75 GRP352-1 timeout 500.0 68 GRP353-1 timeout 500.0 51 GRP354-1 timeout 500.0 80 GRP355-1 timeout 500.0 74 GRP356-1 timeout 500.0 79 GRP357-1 timeout 500.0 178 GRP358-1 timeout 500.0 140 GRP359-1 timeout 500.0 176 GRP360-1 timeout 500.0 124 GRP361-1 timeout 500.0 182 GRP362-1 timeout 500.0 119 GRP363-1 timeout 500.0 127 GRP364-1 timeout 500.0 66 GRP365-1 timeout 500.0 66 GRP366-1 timeout 500.0 128 GRP367-1 timeout 500.0 63 GRP368-1 timeout 500.0 70 GRP369-1 timeout 500.0 121 GRP370-1 timeout 500.0 62 GRP371-1 timeout 500.0 122 GRP372-1 timeout 500.0 122 GRP373-1 timeout 500.0 119 GRP374-1 timeout 500.0 119 GRP375-1 timeout 500.0 122 GRP376-1 timeout 500.0 122 GRP377-1 timeout 500.0 122 GRP378-1 timeout 500.0 122 GRP379-1 timeout 500.0 120 GRP380-1 timeout 500.0 121 GRP381-1 timeout 500.0 122 GRP382-1 timeout 500.0 121 GRP383-1 timeout 500.0 120 GRP384-1 timeout 500.0 120 GRP385-1 timeout 500.0 118 GRP386-1 timeout 500.0 121 GRP387-1 timeout 500.0 121 GRP388-1 timeout 500.0 118 GRP389-1 timeout 500.0 92 GRP390-1 timeout 500.0 98 GRP391-1 timeout 500.0 136 HWV009-1 theorem 89.7 6 1 565 0 8 3 33 0 3 565 19188 4813 0 HWV009-2 timeout 500.0 39 HWV009-3 theorem 0.0 2 1 13 0 13 0 0 0 2 13 179 140 0 HWV009-4 theorem 0.0 2 1 13 0 13 0 0 0 2 13 179 140 0 HWV010-1 theorem 0.1 2 2 103 1 11 4 7 348 2 102 1139 434 0 HWV010-2 theorem 0.0 2 1 29 0 28 0 0 0 2 29 203 147 0 HWV010-3 theorem 0.0 2 1 37 0 28 0 1 0 2 37 264 200 0 HWV011-1 theorem 0.1 2 2 103 1 11 4 7 348 2 102 1123 430 0 HWV011-2 theorem 0.0 2 1 29 0 28 0 0 0 2 29 199 147 0 HWV011-3 theorem 0.1 2 1 37 0 28 0 1 0 2 37 262 200 0 HWV012-1 theorem 0.0 2 1 14 0 10 0 0 0 2 14 98 91 0 HWV012-2 theorem 0.1 2 1 61 0 29 0 1 0 2 61 540 371 0 HWV013-1 timeout 500.0 24 HWV013-2 timeout 500.0 56 HWV014-1 timeout 500.0 22 HWV014-2 timeout 500.0 43 HWV015-1 timeout 500.0 22 HWV015-2 timeout 500.0 43 HWV016-1 timeout 500.0 22 HWV016-2 timeout 500.0 53 HWV017-1 timeout 500.0 21 HWV017-2 timeout 500.0 53 HWV018-1 timeout 500.0 23 HWV018-2 timeout 500.0 41 HWV018-3 theorem 0.1 2 1 107 0 31 0 1 0 2 107 863 505 0 HWV019-1 theorem 0.0 2 1 53 0 10 2 7 0 2 53 470 238 0 HWV019-2 theorem 0.1 2 1 42 0 30 0 1 0 2 42 292 229 0 HWV019-3 theorem 0.0 2 1 15 0 15 0 0 0 2 15 189 170 0 HWV020-1 timeout 500.0 22 HWV020-2 timeout 500.0 43 HWV020-3 theorem 0.1 2 1 107 0 31 0 1 0 2 107 881 512 0 HWV021-1 theorem 0.0 2 1 57 0 11 0 7 0 2 57 521 257 0 HWV021-2 theorem 0.1 2 1 145 0 30 9 7 0 2 145 1568 985 0 HWV022-1 timeout 500.0 22 HWV022-2 timeout 500.0 53 HWV023-1 timeout 500.0 25 HWV023-2 timeout 500.0 43 HWV024-1 theorem 0.1 2 4 109 3 17 8 7 354 2 107 1164 524 0 HWV024-2 timeout 500.0 35 HWV025-1 theorem 0.1 2 4 109 3 17 8 7 354 2 107 1144 516 0 HWV025-2 theorem 0.0 2 1 31 0 30 0 0 0 2 31 204 180 0 HWV025-3 theorem 0.0 2 1 31 0 30 0 0 0 2 31 204 179 0 HWV026-1 theorem 0.0 2 2 106 2 13 4 7 353 2 107 1120 469 0 HWV026-2 theorem 0.0 2 1 15 0 15 0 0 0 2 15 189 166 0 HWV026-3 theorem 0.0 2 1 15 0 15 0 0 0 2 15 187 162 0 HWV027-1 timeout 500.0 79 HWV027-2 timeout 500.0 40 HWV028-1 timeout 500.0 11 HWV028-2 timeout 500.0 50 HWV029-1 timeout 500.0 24 HWV029-2 timeout 500.0 51 HWV030-1 timeout 500.0 11 HWV030-2 timeout 500.0 50 HWV031-1 timeout 500.0 11 HWV031-2 timeout 500.0 50 HWV032-1 timeout 500.0 11 HWV032-2 timeout 500.0 49 HWV033-1 timeout 500.0 25 HWV033-2 timeout 500.0 52 HWV037-1 timeout 500.0 40 HWV038-1 timeout 500.0 39 LAT003-1 timeout 500.0 286 LAT004-1 timeout 500.0 292 LAT058-1 timeout 500.0 263 LCL144-1 timeout 500.0 221 LCL406-1 timeout 500.0 3 LDA005-1 timeout 500.0 34 LDA005-2 timeout 500.0 35 LDA006-1 timeout 500.0 30 LDA006-2 timeout 500.0 37 LDA007-1 theorem 65.8 13 1 1128 0 16 0 0 0 3 1128 31543 9675 0 LDA007-2 theorem 3.6 8 1 1289 0 16 0 35 0 3 1289 34953 9120 0 LDA008-1 timeout 500.0 29 LDA008-2 timeout 500.0 27 LDA009-1 timeout 500.0 30 LDA009-2 timeout 500.0 36 LDA010-1 timeout 500.0 31 LDA010-2 timeout 500.0 36 LDA011-1 timeout 500.0 31 LDA011-2 timeout 500.0 36 LDA012-1 timeout 500.0 30 LDA012-2 timeout 500.0 36 LDA013-1 timeout 500.0 20 LDA014-1 timeout 500.0 19 MGT005-1 theorem 0.1 2 1 166 0 20 0 0 0 2 166 849 181 0 MGT005-2 theorem 0.0 2 1 59 0 23 1 0 0 2 59 340 122 0 MGT013-1 theorem 0.0 2 1 24 0 10 0 0 0 2 24 99 50 0 MGT014-1 theorem 0.0 2 1 24 0 10 0 0 0 2 24 99 50 0 MGT019-2 non_thm 0.0 2 0 12 2 6 0 0 33 4 0 47 35 0 MGT020-1 theorem 0.0 2 1 17 0 4 0 0 0 4 17 64 48 0 MGT021-1 theorem 0.0 2 1 10 0 4 0 0 0 3 10 38 30 0 MGT023-1 theorem 0.0 2 1 11 0 4 0 0 0 4 11 40 25 0 MGT023-2 theorem 0.0 2 10 52 12 4 0 0 42 4 25 322 177 0 MGT024-1 theorem 0.0 2 4 29 3 14 6 0 41 2 23 152 107 0 MGT025-1 theorem 0.1 2 4 88 3 11 7 0 317 3 71 497 431 0 MGT026-1 theorem 0.0 2 3 43 2 5 0 0 39 2 26 213 121 0 MGT027-1 theorem 0.0 2 4 57 3 3 0 0 66 4 35 319 177 0 MGT029-1 timeout 500.0 137 MGT031-1 non_thm 0.0 2 0 21 0 4 0 0 44 3 0 77 44 0 MGT033-1 timeout 500.0 130 MGT033-2 timeout 500.0 59 MGT034-1 non_thm 0.0 2 0 31 4 6 0 0 85 4 0 134 91 0 MGT034-2 theorem 0.1 3 3 195 3 6 0 0 74 4 110 2270 2179 0 MGT035-1 timeout 500.0 139 MGT035-2 timeout 500.0 102 MGT037-1 timeout 500.0 85 MGT037-2 timeout 500.0 160 MGT038-2 timeout 500.0 319 MGT039-1 theorem 0.0 2 1 33 0 6 4 0 0 3 33 120 58 0 MGT039-2 theorem 0.9 3 20 1109 19 6 4 0 6953 4 446 11396 8886 0 MGT040-1 non_thm 0.0 2 0 10 5 7 4 0 25 3 0 40 31 0 MGT040-2 non_thm 0.0 2 0 10 5 7 4 0 25 3 0 40 31 0 MGT042-1 theorem 0.0 2 5 83 5 16 8 0 85 2 47 432 307 0 MGT043-1 theorem 0.0 2 1 34 0 8 0 0 0 2 34 184 178 0 MGT044-1 theorem 0.0 2 1 9 0 4 0 0 0 2 9 51 44 0 MGT045-1 theorem 0.0 2 1 5 0 4 0 0 0 2 5 29 19 0 MGT046-1 theorem 0.0 2 1 30 0 5 0 0 0 2 30 135 113 0 MGT047-1 theorem 0.0 2 1 216 0 8 2 0 0 2 216 1039 585 0 MGT048-1 theorem 0.0 2 1 9 0 4 0 0 0 2 9 51 44 0 MGT049-1 theorem 0.0 2 1 5 0 4 0 0 0 2 5 30 19 0 MGT050-1 theorem 0.0 2 1 31 0 5 0 0 0 2 31 156 140 0 MGT051-1 theorem 0.0 2 1 178 0 8 2 0 0 2 178 875 504 0 MGT052-1 theorem 0.0 2 2 5 1 2 0 0 15 2 6 21 22 0 MGT053-1 theorem 0.0 2 4 11 3 5 6 0 21 2 8 63 45 0 MGT054-1 theorem 0.0 2 1 78 0 8 0 0 0 2 78 477 272 0 MGT055-1 theorem 0.0 2 1 238 0 11 2 0 0 2 238 1454 766 0 MGT056-1 theorem 0.0 2 1 63 0 9 1 0 0 2 63 303 178 0 MGT057-1 theorem 0.0 2 1 56 0 8 1 0 0 2 56 289 182 0 MGT058-1 theorem 0.0 2 2 82 1 7 0 0 67 2 65 594 400 0 MGT059-1 theorem 0.0 2 1 12 0 5 0 0 0 2 12 54 43 0 MGT060-1 theorem 0.0 2 2 173 2 10 0 0 441 2 174 995 489 0 MGT061-1 theorem 0.1 2 1 278 0 14 1 0 0 2 278 1865 1023 0 MGT062-1 theorem 0.1 2 1 216 0 12 1 0 0 2 216 1576 1268 0 MGT063-1 theorem 0.2 2 2 660 6 20 4 0 1293 2 574 5094 2451 0 MGT064-1 theorem 0.1 2 1 485 0 19 2 0 0 2 485 3605 1723 0 MGT065-1 theorem 0.1 2 1 292 0 19 1 0 0 2 292 1831 996 0 MGT066-1 non_thm 0.0 2 1 3 6 1 0 0 34 2 6 9 46 0 MSC007-2.005 theorem 0.1 2 24 800 23 26 0 0 344 2 150 6166 1335 0 NLP004-1 theorem 0.0 2 2 59 1 59 5 0 18 2 39 137 136 0 NLP005-1 non_thm 0.0 2 0 42 1 38 2 0 81 2 0 105 82 0 NLP006-1 non_thm 0.0 2 1 61 1 57 4 0 64 2 36 152 129 0 NLP007-1 theorem 0.0 2 2 59 1 59 5 0 18 2 39 137 136 0 NLP008-1 non_thm 0.0 2 0 42 1 38 2 0 81 2 0 105 82 0 NLP009-1 theorem 0.0 2 2 53 1 53 5 0 16 2 35 125 124 0 NLP011-1 theorem 0.0 2 2 59 1 59 5 0 18 2 39 137 136 0 NLP012-1 non_thm 0.0 2 0 42 1 38 2 0 81 2 0 105 82 0 NLP013-1 non_thm 0.0 2 0 42 1 38 2 0 81 2 0 105 82 0 NLP036-1 non_thm 0.0 4 0 26 0 4 0 0 11 2 0 79 11 0 NLP037-1 non_thm 0.0 4 0 56 0 5 0 0 49 2 0 182 49 0 NLP038-1 non_thm 0.0 4 0 223 0 7 0 0 338 2 0 854 343 0 NLP039-1 non_thm 0.0 4 0 223 0 7 0 0 339 2 0 854 344 0 NLP040-1 non_thm 0.0 4 0 26 0 4 0 0 11 2 0 79 11 0 NLP041-1 non_thm 0.0 4 0 184 0 6 0 0 300 2 0 665 305 0 NLP049-1 non_thm 264.3 171 0 514 0 22 0 0 1059303 3 0 2140 1059352 0 NLP050-1 non_thm 255.8 169 0 499 0 22 0 0 1059303 3 0 2088 1059352 0 NLP051-1 non_thm 251.3 165 0 499 0 22 0 0 1059303 3 0 2090 1059352 0 NLP052-1 non_thm 263.6 175 0 508 0 22 0 0 1059301 3 0 2119 1059350 0 NLP053-1 non_thm 254.1 165 0 499 0 22 0 0 1059303 3 0 2088 1059352 0 NLP054-1 non_thm 0.1 4 0 168 1 14 0 0 152 2 0 604 153 0 NLP055-1 non_thm 0.0 4 0 168 1 14 0 0 152 2 0 604 153 0 NLP056-1 non_thm 0.0 4 0 168 1 14 0 0 152 2 0 604 153 0 NLP057-1 non_thm 0.0 4 0 168 1 14 0 0 152 2 0 604 153 0 NLP058-1 non_thm 0.0 4 0 168 1 14 0 0 151 2 0 604 152 0 NLP069-1 memory 240.9 499 NLP070-1 memory 234.2 499 NLP071-1 memory 309.6 499 NLP072-1 memory 241.2 499 NLP073-1 memory 236.8 499 NLP074-1 memory 242.8 499 NLP075-1 memory 424.0 499 NLP076-1 memory 174.8 499 NLP077-1 memory 174.1 499 NLP078-1 memory 176.5 499 NLP082-1 timeout 500.0 471 NLP083-1 timeout 500.0 477 NLP084-1 memory 417.6 499 NLP085-1 memory 416.3 499 NLP086-1 memory 424.9 499 NLP087-1 memory 417.4 499 NLP088-1 memory 343.0 499 NLP089-1 memory 344.4 499 NLP090-1 memory 345.5 499 NLP091-1 memory 343.0 499 NLP092-1 memory 345.1 499 NLP093-1 memory 344.2 499 NLP140-1 non_thm 0.0 4 0 381 0 21 0 0 281 2 0 1538 282 0 NLP141-1 theorem 0.0 4 1 421 0 24 0 0 0 2 421 1714 297 0 NLP142-1 non_thm 0.0 4 0 381 0 21 0 0 281 2 0 1538 282 0 NLP143-1 theorem 0.0 4 1 421 0 24 0 0 0 2 421 1714 297 0 NLP144-1 non_thm 0.0 4 0 433 0 21 0 0 307 2 0 1764 308 0 NLP145-1 theorem 0.1 4 1 473 0 24 0 0 0 2 473 1935 323 0 NLP146-1 non_thm 0.1 4 0 381 0 21 0 0 281 2 0 1538 282 0 NLP147-1 theorem 0.0 4 1 421 0 24 0 0 0 2 421 1714 297 0 NLP148-1 non_thm 0.0 4 0 381 0 21 0 0 281 2 0 1538 282 0 NLP149-1 theorem 0.1 4 1 421 0 24 0 0 0 2 421 1714 297 0 NLP150-1 non_thm 0.0 4 0 185 1 19 0 0 166 2 0 657 167 0 NLP151-1 non_thm 0.0 4 0 185 1 19 0 0 165 2 0 657 166 0 NLP152-1 non_thm 0.0 4 0 185 1 19 0 0 166 2 0 657 167 0 NLP153-1 non_thm 0.0 4 0 185 1 19 0 0 165 2 0 657 166 0 NLP154-1 non_thm 0.0 4 0 224 1 19 0 0 192 2 0 800 193 0 NLP155-1 non_thm 0.0 4 0 224 1 19 0 0 191 2 0 800 192 0 NLP156-1 non_thm 0.0 4 0 185 1 19 0 0 166 2 0 657 167 0 NLP157-1 non_thm 0.0 4 0 185 1 19 0 0 165 2 0 657 166 0 NLP158-1 non_thm 0.0 4 0 185 1 19 0 0 166 2 0 657 167 0 NLP159-1 non_thm 0.0 4 0 185 1 19 0 0 165 2 0 657 166 0 NLP170-1 timeout 500.0 16 NLP171-1 timeout 500.0 15 NLP172-1 timeout 500.0 15 NLP173-1 timeout 500.0 15 NLP174-1 timeout 500.0 15 NLP175-1 timeout 500.0 16 NLP176-1 timeout 500.0 15 NLP177-1 timeout 500.0 16 NLP178-1 timeout 500.0 15 NLP179-1 timeout 500.0 15 NLP180-1 timeout 500.0 14 NLP181-1 timeout 500.0 14 NLP182-1 timeout 500.0 14 NLP183-1 timeout 500.0 14 NLP184-1 timeout 500.0 15 NLP185-1 timeout 500.0 14 NLP186-1 timeout 500.0 14 NLP187-1 timeout 500.0 14 NLP188-1 timeout 500.0 14 NLP189-1 timeout 500.0 14 NLP200-1 timeout 500.0 14 NLP201-1 timeout 500.0 15 NLP202-1 timeout 500.0 15 NLP203-1 timeout 500.0 15 NLP204-1 theorem 0.0 4 1 89 0 31 0 0 0 2 89 373 260 0 NLP205-1 timeout 500.0 15 NLP206-1 timeout 500.0 15 NLP207-1 timeout 500.0 15 NLP208-1 theorem 0.0 4 1 89 0 31 0 0 0 2 89 373 260 0 NLP209-1 timeout 500.0 15 NLP210-1 timeout 500.0 15 NLP211-1 timeout 500.0 14 NLP212-1 timeout 500.0 14 NLP213-1 timeout 500.0 14 NLP214-1 timeout 500.0 15 NLP215-1 timeout 500.0 15 NLP216-1 timeout 500.0 15 NLP217-1 timeout 500.0 15 NLP218-1 timeout 500.0 15 NLP219-1 timeout 500.0 15 NUM005-1 timeout 500.0 369 NUM006-1 timeout 500.0 283 NUM007-1 timeout 500.0 190 NUM008-1 timeout 500.0 432 NUM009-1 theorem 0.1 2 1 16 0 13 0 0 0 2 16 258 240 0 NUM010-1 timeout 500.0 457 NUM011-1 timeout 500.0 437 NUM012-1 timeout 500.0 433 NUM013-1 timeout 500.0 410 NUM018-1 timeout 500.0 493 NUM028-1 timeout 500.0 70 NUM029-1 timeout 500.0 84 NUM030-1 timeout 500.0 33 NUM031-1 timeout 500.0 83 NUM032-1 timeout 500.0 71 NUM033-1 timeout 500.0 81 NUM034-1 timeout 500.0 86 NUM035-1 timeout 500.0 70 NUM036-1 timeout 500.0 75 NUM037-1 timeout 500.0 70 NUM038-1 timeout 500.0 74 NUM039-1 timeout 500.0 53 NUM040-1 timeout 500.0 40 NUM041-1 timeout 500.0 69 NUM042-1 timeout 500.0 69 NUM043-1 timeout 500.0 72 NUM044-1 timeout 500.0 73 NUM045-1 timeout 500.0 76 NUM046-1 timeout 500.0 56 NUM047-1 timeout 500.0 60 NUM048-1 timeout 500.0 72 NUM049-1 timeout 500.0 71 NUM050-1 timeout 500.0 51 NUM051-1 timeout 500.0 74 NUM052-1 timeout 500.0 58 NUM053-1 timeout 500.0 45 NUM054-1 timeout 500.0 94 NUM055-1 timeout 500.0 43 NUM056-1 timeout 500.0 74 NUM057-1 timeout 500.0 31 NUM058-1 timeout 500.0 31 NUM059-1 timeout 500.0 51 NUM060-1 timeout 500.0 83 NUM061-1 timeout 500.0 88 NUM062-1 timeout 500.0 50 NUM063-1 timeout 500.0 49 NUM064-1 timeout 500.0 60 NUM065-1 timeout 500.0 58 NUM066-1 timeout 500.0 54 NUM067-1 timeout 500.0 89 NUM068-1 timeout 500.0 73 NUM069-1 timeout 500.0 85 NUM070-1 timeout 500.0 51 NUM071-1 timeout 500.0 53 NUM072-1 timeout 500.0 58 NUM073-1 timeout 500.0 45 NUM074-1 timeout 500.0 50 NUM075-1 timeout 500.0 57 NUM076-1 timeout 500.0 53 NUM077-1 timeout 500.0 53 NUM078-1 timeout 500.0 52 NUM079-1 timeout 500.0 31 NUM080-1 timeout 500.0 69 NUM081-1 timeout 500.0 73 NUM082-1 timeout 500.0 58 NUM083-1 timeout 500.0 26 NUM084-1 timeout 500.0 67 NUM085-1 timeout 500.0 33 NUM086-1 timeout 500.0 71 NUM087-1 timeout 500.0 72 NUM088-1 timeout 500.0 52 NUM089-1 timeout 500.0 62 NUM090-1 timeout 500.0 34 NUM091-1 timeout 500.0 55 NUM092-1 timeout 500.0 53 NUM093-1 timeout 500.0 53 NUM094-1 timeout 500.0 61 NUM095-1 timeout 500.0 60 NUM096-1 timeout 500.0 62 NUM097-1 timeout 500.0 60 NUM098-1 timeout 500.0 38 NUM099-1 timeout 500.0 33 NUM100-1 timeout 500.0 34 NUM101-1 timeout 500.0 30 NUM102-1 timeout 500.0 36 NUM103-1 timeout 500.0 53 NUM104-1 timeout 500.0 29 NUM105-1 timeout 500.0 32 NUM106-1 timeout 500.0 63 NUM107-1 timeout 500.0 54 NUM108-1 timeout 500.0 56 NUM109-1 timeout 500.0 28 NUM110-1 timeout 500.0 35 NUM111-1 timeout 500.0 30 NUM112-1 timeout 500.0 32 NUM113-1 timeout 500.0 74 NUM114-1 timeout 500.0 32 NUM115-1 timeout 500.0 54 NUM116-1 timeout 500.0 31 NUM117-1 timeout 500.0 33 NUM118-1 timeout 500.0 46 NUM119-1 timeout 500.0 54 NUM120-1 timeout 500.0 31 NUM121-1 timeout 500.0 31 NUM122-1 timeout 500.0 31 NUM123-1 timeout 500.0 30 NUM124-1 timeout 500.0 31 NUM125-1 timeout 500.0 53 NUM126-1 timeout 500.0 73 NUM127-1 timeout 500.0 72 NUM128-1 timeout 500.0 73 NUM129-1 timeout 500.0 46 NUM130-1 timeout 500.0 43 NUM131-1 timeout 500.0 48 NUM132-1 timeout 500.0 54 NUM133-1 timeout 500.0 58 NUM134-1 timeout 500.0 55 NUM135-1 timeout 500.0 73 NUM136-1 timeout 500.0 49 NUM137-1 timeout 500.0 55 NUM138-1 timeout 500.0 30 NUM139-1 timeout 500.0 31 NUM140-1 timeout 500.0 51 NUM141-1 timeout 500.0 52 NUM142-1 timeout 500.0 31 NUM143-1 timeout 500.0 69 NUM144-1 timeout 500.0 30 NUM145-1 timeout 500.0 39 NUM146-1 timeout 500.0 30 NUM147-1 timeout 500.0 54 NUM148-1 timeout 500.0 32 NUM149-1 timeout 500.0 28 NUM150-1 timeout 500.0 53 NUM151-1 timeout 500.0 50 NUM152-1 timeout 500.0 32 NUM153-1 timeout 500.0 48 NUM154-1 timeout 500.0 74 NUM155-1 timeout 500.0 81 NUM156-1 timeout 500.0 54 NUM157-1 timeout 500.0 53 NUM158-1 timeout 500.0 32 NUM159-1 timeout 500.0 30 NUM160-1 timeout 500.0 35 NUM161-1 timeout 500.0 72 NUM162-1 timeout 500.0 72 NUM163-1 timeout 500.0 71 NUM164-1 timeout 500.0 72 NUM165-1 timeout 500.0 51 NUM166-1 timeout 500.0 44 NUM167-1 timeout 500.0 70 NUM168-1 timeout 500.0 73 NUM169-1 timeout 500.0 54 NUM170-1 timeout 500.0 56 NUM171-1 timeout 500.0 74 NUM172-1 timeout 500.0 51 NUM173-1 timeout 500.0 59 NUM174-1 timeout 500.0 31 NUM175-1 timeout 500.0 35 NUM176-1 timeout 500.0 49 NUM177-1 timeout 500.0 54 NUM178-1 timeout 500.0 41 NUM179-1 timeout 500.0 45 NUM180-1 theorem 0.1 2 1 235 0 48 0 0 0 2 235 1632 560 0 NUM181-1 timeout 500.0 52 NUM182-1 timeout 500.0 54 NUM183-1 timeout 500.0 31 NUM184-1 timeout 500.0 70 NUM185-1 timeout 500.0 59 NUM186-1 timeout 500.0 72 NUM187-1 timeout 500.0 56 NUM188-1 timeout 500.0 50 NUM189-1 timeout 500.0 56 NUM190-1 timeout 500.0 71 NUM191-1 timeout 500.0 51 NUM192-1 timeout 500.0 55 NUM193-1 timeout 500.0 84 NUM194-1 timeout 500.0 45 NUM195-1 timeout 500.0 62 NUM196-1 timeout 500.0 57 NUM197-1 timeout 500.0 33 NUM198-1 timeout 500.0 55 NUM199-1 timeout 500.0 52 NUM200-1 timeout 500.0 54 NUM201-1 timeout 500.0 55 NUM202-1 timeout 500.0 55 NUM203-1 timeout 500.0 61 NUM204-1 timeout 500.0 50 NUM205-1 timeout 500.0 51 NUM206-1 timeout 500.0 54 NUM207-1 timeout 500.0 54 NUM208-1 timeout 500.0 53 NUM209-1 timeout 500.0 55 NUM210-1 timeout 500.0 53 NUM211-1 timeout 500.0 71 NUM212-1 timeout 500.0 74 NUM213-1 timeout 500.0 65 NUM214-1 timeout 500.0 35 NUM215-1 timeout 500.0 36 NUM216-1 timeout 500.0 50 NUM217-1 timeout 500.0 43 NUM218-1 timeout 500.0 31 NUM219-1 timeout 500.0 31 NUM220-1 timeout 500.0 75 NUM221-1 timeout 500.0 32 NUM222-1 timeout 500.0 44 NUM223-1 timeout 500.0 30 NUM224-1 timeout 500.0 72 NUM225-1 timeout 500.0 33 NUM226-1 timeout 500.0 49 NUM227-1 timeout 500.0 75 NUM228-1 theorem 0.1 2 1 66 0 49 0 0 0 2 66 372 252 0 NUM229-1 timeout 500.0 91 NUM230-1 timeout 500.0 61 NUM231-1 timeout 500.0 60 NUM232-1 timeout 500.0 59 NUM233-1 timeout 500.0 60 NUM234-1 timeout 500.0 59 NUM235-1 timeout 500.0 59 NUM236-1 timeout 500.0 90 NUM237-1 timeout 500.0 97 NUM238-1 timeout 500.0 78 NUM239-1 timeout 500.0 55 NUM240-1 timeout 500.0 49 NUM241-1 timeout 500.0 69 NUM242-1 timeout 500.0 77 NUM243-1 timeout 500.0 34 NUM244-1 timeout 500.0 34 NUM245-1 timeout 500.0 89 NUM245-2 timeout 500.0 92 NUM246-1 timeout 500.0 54 NUM246-2 timeout 500.0 54 NUM247-1 timeout 500.0 25 NUM247-2 timeout 500.0 25 NUM248-1 timeout 500.0 72 NUM248-2 timeout 500.0 74 NUM249-1 timeout 500.0 75 NUM249-2 timeout 500.0 71 NUM250-1 timeout 500.0 32 NUM250-2 timeout 500.0 32 NUM251-1 timeout 500.0 31 NUM251-2 timeout 500.0 32 NUM252-1 timeout 500.0 75 NUM252-2 timeout 500.0 72 NUM253-1 timeout 500.0 50 NUM253-2 timeout 500.0 51 NUM254-1 timeout 500.0 50 NUM254-2 timeout 500.0 50 NUM255-1 timeout 500.0 50 NUM255-2 timeout 500.0 51 NUM256-1 timeout 500.0 51 NUM256-2 timeout 500.0 50 NUM257-1 timeout 500.0 49 NUM257-2 timeout 500.0 50 NUM258-1 timeout 500.0 70 NUM258-2 timeout 500.0 73 NUM259-1 timeout 500.0 72 NUM259-2 timeout 500.0 73 NUM260-1 timeout 500.0 74 NUM260-2 timeout 500.0 74 NUM261-1 timeout 500.0 72 NUM261-2 timeout 500.0 72 NUM262-1 timeout 500.0 70 NUM262-2 timeout 500.0 73 NUM263-1 timeout 500.0 53 NUM263-2 timeout 500.0 54 NUM264-1 timeout 500.0 58 NUM264-2 timeout 500.0 55 NUM265-1 timeout 500.0 71 NUM266-1 timeout 500.0 53 NUM267-1 timeout 500.0 55 NUM268-1 timeout 500.0 55 NUM269-1 timeout 500.0 77 NUM270-1 timeout 500.0 72 NUM271-1 timeout 500.0 44 NUM272-1 timeout 500.0 31 NUM273-1 timeout 500.0 35 NUM274-1 timeout 500.0 64 NUM275-1 timeout 500.0 67 NUM276-1 timeout 500.0 44 NUM277-1 timeout 500.0 31 NUM277-2 timeout 500.0 55 NUM278-1 timeout 500.0 54 NUM279-1 timeout 500.0 73 NUM280-1 timeout 500.0 71 NUM281-1 timeout 500.0 54 NUM282-1 timeout 500.0 57 NUM286-3 memory 482.8 499 NUM289-1 timeout 500.0 75 PUZ001-2 theorem 0.0 2 1 42 0 9 0 0 0 2 42 194 92 0 PUZ006-1 theorem 0.0 2 1 21 0 14 8 0 0 2 21 82 40 0 PUZ007-1 theorem 0.0 2 2 33 1 18 15 0 35 2 22 128 82 0 PUZ020-1 theorem 0.0 2 1 16 0 9 2 0 0 2 16 59 17 0 PUZ043-1 non_thm 0.0 3 1 1 5 1 0 0 10 2 5 4 16 0 RNG040-1 theorem 0.0 3 1 14 0 14 0 0 0 2 14 634 565 0 RNG040-2 theorem 2.1 6 1 77 0 14 0 0 0 2 77 23821 22814 0 RNG041-1 theorem 0.4 0 1 45 0 14 0 0 0 2 45 9186 3512 0 SET002-6 timeout 500.0 61 SET012-3 memory 371.7 499 SET012-4 theorem 0.0 2 2 137 1 5 0 0 69 2 88 663 309 0 SET013-3 memory 370.7 499 SET013-4 theorem 0.1 2 2 246 1 5 0 0 146 2 150 1880 504 0 SET014-3 memory 356.3 499 SET014-4 timeout 500.0 19 SET014-6 timeout 500.0 60 SET015-3 memory 366.3 499 SET015-4 timeout 500.0 33 SET016-1 theorem 0.0 2 1 38 0 7 0 0 0 3 38 289 105 0 SET016-3 memory 449.3 499 SET016-6 timeout 500.0 33 SET016-7 theorem 0.0 2 1 41 0 41 0 0 0 2 41 401 351 0 SET017-3 memory 457.2 499 SET017-4 memory 441.2 499 SET017-6 theorem 0.2 2 1 260 0 33 0 1 0 2 260 2119 1260 0 SET017-7 theorem 0.8 3 1 713 0 41 0 1 0 2 713 13708 3291 0 SET018-1 theorem 0.5 3 1 611 0 7 0 43 0 3 611 7030 1171 0 SET018-3 timeout 500.0 106 SET018-4 timeout 500.0 97 SET018-6 timeout 500.0 34 SET018-7 theorem 0.0 2 1 41 0 41 0 0 0 2 41 401 353 0 SET019-3 timeout 500.0 468 SET019-4 memory 357.5 499 SET020-3 timeout 500.0 24 SET020-4 memory 440.0 499 SET020-6 timeout 500.0 137 SET020-7 timeout 500.0 35 SET021-3 timeout 500.0 24 SET021-4 memory 452.6 499 SET021-6 timeout 500.0 136 SET021-7 timeout 500.0 35 SET022-3 timeout 500.0 453 SET022-4 memory 389.9 499 SET023-3 timeout 500.0 435 SET023-4 memory 398.7 499 SET024-3 theorem 0.0 2 1 26 0 14 0 0 0 2 26 277 241 0 SET024-4 theorem 0.0 2 1 26 0 14 0 0 0 2 26 252 216 0 SET024-6 theorem 0.0 2 1 33 0 32 0 0 0 2 33 165 135 0 SET024-7 theorem 0.0 2 1 43 0 42 0 0 0 2 43 341 276 0 SET025-3 theorem 19.9 11 1 957 0 13 0 0 0 2 957 68179 60307 0 SET025-4 theorem 7.5 11 1 957 0 13 0 0 0 2 957 65905 58218 0 SET025-6 theorem 0.0 2 1 24 0 24 0 0 0 2 24 144 112 0 SET025-7 theorem 0.0 2 1 36 0 36 0 0 0 2 36 329 275 0 SET025-8 theorem 0.1 2 1 74 0 15 0 0 0 2 74 1881 861 0 SET025-9 theorem 0.1 2 1 156 0 14 0 0 0 2 156 2501 1050 0 SET027-3 theorem 404.9 17 1 1454 0 16 0 0 0 2 1454 114704 63554 0 SET027-4 theorem 10.4 13 1 1413 0 15 0 0 0 2 1413 73327 58824 0 SET027-6 theorem 0.0 2 1 92 0 33 0 0 0 2 92 585 295 0 SET027-7 theorem 0.0 2 1 92 0 34 0 0 0 2 92 585 295 0 SET028-3 timeout 500.0 236 SET028-4 memory 370.9 499 SET029-3 timeout 500.0 241 SET029-4 memory 357.3 499 SET030-3 timeout 500.0 164 SET030-4 memory 398.8 499 SET030-6 timeout 500.0 62 SET031-3 timeout 500.0 184 SET031-4 memory 447.0 499 SET032-3 timeout 500.0 218 SET032-4 memory 355.6 499 SET032-6 timeout 500.0 61 SET033-3 timeout 500.0 220 SET033-4 memory 356.1 498 SET033-6 timeout 500.0 61 SET034-3 timeout 500.0 23 SET034-4 memory 456.0 499 SET034-6 timeout 500.0 63 SET035-3 timeout 500.0 23 SET035-4 memory 389.6 499 SET035-6 timeout 500.0 62 SET036-3 timeout 500.0 23 SET036-4 memory 437.6 499 SET036-6 timeout 500.0 134 SET037-3 timeout 500.0 23 SET037-4 timeout 500.0 444 SET037-6 timeout 500.0 33 SET038-3 timeout 500.0 18 SET038-4 timeout 500.0 107 SET038-6 timeout 500.0 101 SET039-3 timeout 500.0 23 SET039-4 timeout 500.0 442 SET040-3 timeout 500.0 46 SET040-4 memory 373.0 499 SET040-6 timeout 500.0 62 SET041-3 timeout 500.0 24 SET041-4 timeout 500.0 446 SET041-6 timeout 500.0 50 SET042-3 timeout 500.0 24 SET042-4 memory 479.7 499 SET050-6 theorem 0.0 2 1 38 0 32 0 2 0 2 38 209 153 0 SET051-6 theorem 0.0 2 1 38 0 32 0 2 0 2 38 208 153 0 SET052-6 theorem 0.0 2 1 33 0 32 0 1 0 2 33 173 123 0 SET053-6 theorem 0.0 2 1 33 0 32 0 1 0 2 33 172 123 0 SET054-6 theorem 0.0 2 1 5 0 5 0 0 0 2 5 99 67 0 SET054-7 theorem 0.0 2 1 5 0 5 0 0 0 2 5 99 67 0 SET056-6 theorem 0.0 2 1 38 0 33 0 0 0 2 38 189 141 0 SET056-7 theorem 0.0 2 1 38 0 34 0 0 0 2 38 208 159 0 SET057-6 theorem 0.0 2 1 38 0 33 0 0 0 2 38 199 148 0 SET057-7 theorem 0.0 2 1 38 0 34 0 0 0 2 38 221 166 0 SET058-6 theorem 0.0 2 1 38 0 33 0 0 0 2 38 199 148 0 SET058-7 theorem 0.0 2 1 38 0 34 0 0 0 2 38 221 166 0 SET059-6 theorem 0.0 2 1 38 0 33 0 0 0 2 38 199 153 0 SET059-7 theorem 0.0 2 1 38 0 34 0 0 0 2 38 221 171 0 SET060-6 theorem 0.0 2 1 38 0 31 0 0 0 2 38 206 179 0 SET060-7 theorem 0.0 2 1 38 0 32 0 0 0 2 38 230 203 0 SET061-6 timeout 500.0 42 SET061-7 timeout 500.0 46 SET062-6 theorem 0.1 2 1 176 0 31 0 0 0 2 176 1132 408 0 SET062-7 theorem 0.0 2 1 7 0 7 0 0 0 2 7 119 81 0 SET063-6 theorem 0.1 2 1 202 0 32 0 0 0 2 202 1314 446 0 SET063-7 theorem 0.0 2 1 9 0 9 0 0 0 2 9 145 98 0 SET064-6 theorem 0.1 2 1 258 0 32 0 0 0 2 258 1734 495 0 SET064-7 theorem 0.0 2 1 17 0 17 0 0 0 2 17 191 139 0 SET065-6 theorem 0.0 2 1 32 0 31 0 0 0 2 32 161 122 0 SET065-7 theorem 0.0 2 1 36 0 35 0 0 0 2 36 253 189 0 SET066-6 timeout 500.0 62 SET066-7 timeout 500.0 37 SET067-6 timeout 500.0 62 SET067-7 timeout 500.0 35 SET068-6 timeout 500.0 62 SET068-7 timeout 500.0 35 SET069-6 timeout 500.0 49 SET069-7 timeout 500.0 27 SET070-6 timeout 500.0 49 SET070-7 timeout 500.0 27 SET071-6 timeout 500.0 29 SET071-7 timeout 500.0 21 SET072-6 theorem 0.2 2 1 261 0 33 0 1 0 2 261 2169 1285 0 SET072-7 theorem 0.2 2 1 234 0 41 0 0 0 2 234 3934 1339 0 SET073-6 timeout 500.0 44 SET073-7 theorem 0.0 2 1 41 0 40 0 0 0 2 41 322 269 0 SET074-6 timeout 500.0 44 SET074-7 theorem 0.0 2 1 41 0 40 0 0 0 2 41 322 269 0 SET075-6 timeout 500.0 98 SET075-7 theorem 0.0 2 1 41 0 40 0 0 0 2 41 314 263 0 SET076-6 timeout 500.0 134 SET076-7 timeout 500.0 40 SET077-6 theorem 0.0 2 1 8 0 8 0 0 0 2 8 121 93 0 SET077-7 theorem 0.0 2 1 16 0 16 0 0 0 2 16 235 184 0 SET078-6 theorem 0.0 2 1 32 0 31 0 0 0 2 32 145 122 0 SET078-7 theorem 0.0 2 1 33 0 33 0 0 0 2 33 288 236 0 SET079-6 timeout 500.0 43 SET079-7 theorem 0.0 2 1 43 0 42 0 0 0 2 43 353 291 0 SET080-6 theorem 0.0 2 1 41 0 31 0 0 0 2 41 229 195 0 SET080-7 theorem 0.0 2 1 17 0 17 0 0 0 2 17 248 193 0 SET081-6 theorem 0.0 2 1 35 0 32 0 0 0 2 35 174 143 0 SET081-7 theorem 0.0 2 1 44 0 43 0 0 0 2 44 338 267 0 SET082-6 timeout 500.0 52 SET082-7 theorem 0.0 2 1 48 0 43 0 1 0 2 48 411 291 0 SET083-6 theorem 0.0 2 1 73 0 33 0 0 0 2 73 463 349 0 SET083-7 theorem 0.1 2 1 108 0 44 0 0 0 2 108 1564 834 0 SET084-6 theorem 0.0 2 1 82 0 33 0 0 0 2 82 529 375 0 SET084-7 theorem 0.1 2 1 171 0 44 0 3 0 2 171 2693 999 0 SET085-6 theorem 0.0 2 1 89 0 34 0 0 0 2 89 586 350 0 SET085-7 theorem 0.1 2 1 241 0 45 0 0 0 2 241 3955 1290 0 SET086-6 timeout 500.0 43 SET086-7 timeout 500.0 32 SET087-6 timeout 500.0 43 SET087-7 timeout 500.0 32 SET088-6 timeout 500.0 63 SET088-7 timeout 500.0 31 SET089-6 timeout 500.0 62 SET089-7 timeout 500.0 31 SET090-6 timeout 500.0 43 SET090-7 timeout 500.0 32 SET091-6 timeout 500.0 63 SET091-7 timeout 500.0 41 SET092-6 timeout 500.0 63 SET092-7 timeout 500.0 42 SET093-6 theorem 0.0 2 1 39 0 32 0 1 0 2 39 223 157 0 SET093-7 theorem 0.0 2 1 24 0 24 0 0 0 2 24 300 237 0 SET094-6 timeout 500.0 138 SET094-7 timeout 500.0 19 SET095-6 timeout 500.0 39 SET095-7 theorem 0.0 2 1 44 0 43 0 0 0 2 44 367 293 0 SET096-6 timeout 500.0 35 SET096-7 theorem 0.1 2 1 200 0 44 0 0 0 2 200 3145 1098 0 SET097-6 timeout 500.0 53 SET097-7 timeout 500.0 34 SET098-6 timeout 500.0 54 SET098-7 timeout 500.0 33 SET099-6 timeout 500.0 53 SET099-7 timeout 500.0 34 SET100-6 timeout 500.0 62 SET100-7 timeout 500.0 32 SET101-6 timeout 500.0 62 SET101-7 timeout 500.0 33 SET102-6 timeout 500.0 62 SET102-7 timeout 500.0 32 SET103-6 timeout 500.0 50 SET103-7 timeout 500.0 30 SET104-6 timeout 500.0 50 SET104-7 timeout 500.0 30 SET105-6 timeout 500.0 29 SET105-7 timeout 500.0 21 SET108-6 timeout 500.0 131 SET108-7 timeout 500.0 37 SET109-6 timeout 500.0 64 SET109-7 timeout 500.0 37 SET110-6 timeout 500.0 64 SET110-7 timeout 500.0 38 SET111-6 timeout 500.0 62 SET111-7 timeout 500.0 37 SET112-6 timeout 500.0 64 SET112-7 timeout 500.0 38 SET113-6 timeout 500.0 63 SET113-7 timeout 500.0 44 SET114-6 timeout 500.0 65 SET114-7 timeout 500.0 44 SET115-6 timeout 500.0 63 SET115-7 timeout 500.0 43 SET116-6 timeout 500.0 63 SET116-7 timeout 500.0 43 SET117-6 theorem 0.0 2 1 40 0 32 0 1 0 2 40 229 165 0 SET117-7 theorem 0.0 2 1 40 0 40 0 0 0 2 40 378 327 0 SET118-6 theorem 0.0 2 1 13 0 13 0 0 0 2 13 137 99 0 SET118-7 theorem 0.0 2 1 27 0 27 0 0 0 2 27 346 292 0 SET119-6 timeout 500.0 49 SET119-7 timeout 500.0 34 SET120-6 timeout 500.0 49 SET120-7 timeout 500.0 34 SET121-6 timeout 500.0 49 SET121-7 timeout 500.0 24 SET122-6 timeout 500.0 49 SET122-7 timeout 500.0 24 SET123-6 timeout 500.0 20 SET124-6 timeout 500.0 44 SET125-6 timeout 500.0 99 SET126-6 timeout 500.0 62 SET127-6 timeout 500.0 62 SET128-6 timeout 500.0 62 SET129-6 timeout 500.0 35 SET130-6 timeout 500.0 42 SET131-6 timeout 500.0 44 SET132-6 timeout 500.0 44 SET133-6 timeout 500.0 123 SET134-6 timeout 500.0 42 SET135-6 timeout 500.0 43 SET136-6 timeout 500.0 42 SET137-6 timeout 500.0 131 SET138-6 timeout 500.0 141 SET139-6 timeout 500.0 62 SET140-6 timeout 500.0 62 SET141-6 timeout 500.0 62 SET142-6 timeout 500.0 62 SET143-6 timeout 500.0 61 SET144-6 timeout 500.0 61 SET145-6 timeout 500.0 62 SET146-6 timeout 500.0 63 SET147-6 timeout 500.0 61 SET148-6 timeout 500.0 61 SET149-6 timeout 500.0 61 SET150-6 timeout 500.0 60 SET151-6 timeout 500.0 61 SET152-6 timeout 500.0 61 SET153-6 timeout 500.0 60 SET154-6 timeout 500.0 61 SET155-6 timeout 500.0 61 SET156-6 timeout 500.0 62 SET157-6 timeout 500.0 87 SET158-6 theorem 0.0 2 1 42 0 41 0 0 0 2 42 240 203 0 SET159-6 timeout 500.0 62 SET160-6 timeout 500.0 61 SET161-6 timeout 500.0 61 SET162-6 timeout 500.0 61 SET163-6 timeout 500.0 61 SET165-6 timeout 500.0 61 SET166-6 timeout 500.0 22 SET167-6 timeout 500.0 98 SET168-6 timeout 500.0 100 SET169-6 timeout 500.0 61 SET170-6 timeout 500.0 61 SET171-6 timeout 500.0 61 SET172-6 timeout 500.0 61 SET173-6 timeout 500.0 61 SET174-6 timeout 500.0 61 SET175-6 timeout 500.0 62 SET176-6 timeout 500.0 61 SET177-6 timeout 500.0 62 SET178-6 timeout 500.0 61 SET179-6 timeout 500.0 61 SET180-6 timeout 500.0 61 SET181-6 timeout 500.0 61 SET182-6 timeout 500.0 61 SET183-6 timeout 500.0 71 SET184-6 theorem 0.1 2 1 88 0 40 0 0 0 2 88 514 319 0 SET185-6 timeout 500.0 71 SET186-6 timeout 500.0 49 SET187-6 timeout 500.0 73 SET188-6 timeout 500.0 47 SET189-6 timeout 500.0 49 SET190-6 timeout 500.0 71 SET191-6 timeout 500.0 49 SET192-6 timeout 500.0 50 SET193-6 theorem 0.1 2 1 167 0 40 0 0 0 2 167 989 417 0 SET194-6 timeout 500.0 61 SET195-6 timeout 500.0 62 SET196-6 timeout 500.0 67 SET197-6 timeout 500.0 67 SET199-6 timeout 500.0 59 SET200-6 timeout 500.0 70 SET201-6 timeout 500.0 74 SET202-6 timeout 500.0 66 SET203-6 theorem 0.0 2 1 45 0 41 0 0 0 2 45 248 191 0 SET204-6 theorem 0.0 2 1 46 0 40 0 0 0 2 46 219 175 0 SET205-6 timeout 500.0 62 SET206-6 timeout 500.0 62 SET207-6 timeout 500.0 61 SET208-6 timeout 500.0 49 SET209-6 timeout 500.0 48 SET210-6 timeout 500.0 61 SET211-6 timeout 500.0 61 SET212-6 timeout 500.0 61 SET213-6 timeout 500.0 61 SET214-6 timeout 500.0 62 SET215-6 timeout 500.0 61 SET216-6 timeout 500.0 61 SET217-6 timeout 500.0 61 SET218-6 timeout 500.0 62 SET219-6 timeout 500.0 61 SET220-6 timeout 500.0 61 SET221-6 timeout 500.0 61 SET222-6 timeout 500.0 61 SET223-6 timeout 500.0 61 SET224-6 timeout 500.0 60 SET225-6 timeout 500.0 60 SET226-6 timeout 500.0 48 SET227-6 timeout 500.0 49 SET228-6 timeout 500.0 48 SET229-6 timeout 500.0 46 SET230-6 timeout 500.0 62 SET231-6 timeout 500.0 69 SET232-6 timeout 500.0 66 SET233-6 timeout 500.0 67 SET234-6 timeout 500.0 67 SET235-6 timeout 500.0 45 SET236-6 timeout 500.0 49 SET237-6 timeout 500.0 68 SET238-6 timeout 500.0 50 SET239-6 theorem 0.2 2 1 456 0 40 0 0 0 2 456 2791 558 0 SET240-6 timeout 500.0 66 SET241-6 timeout 500.0 65 SET242-6 timeout 500.0 99 SET243-6 timeout 500.0 61 SET244-6 timeout 500.0 61 SET245-6 timeout 500.0 64 SET246-6 timeout 500.0 62 SET247-6 timeout 500.0 63 SET248-6 timeout 500.0 61 SET249-6 timeout 500.0 61 SET250-6 timeout 500.0 62 SET251-6 timeout 500.0 48 SET252-6 timeout 500.0 68 SET253-6 timeout 500.0 61 SET254-6 timeout 500.0 46 SET255-6 timeout 500.0 49 SET256-6 timeout 500.0 47 SET257-6 timeout 500.0 62 SET258-6 timeout 500.0 34 SET259-6 timeout 500.0 34 SET260-6 timeout 500.0 128 SET261-6 timeout 500.0 45 SET262-6 timeout 500.0 69 SET263-6 timeout 500.0 63 SET264-6 timeout 500.0 44 SET265-6 timeout 500.0 67 SET266-6 timeout 500.0 69 SET267-6 timeout 500.0 61 SET268-6 timeout 500.0 61 SET269-6 timeout 500.0 61 SET270-6 timeout 500.0 61 SET271-6 timeout 500.0 61 SET272-6 timeout 500.0 61 SET273-6 timeout 500.0 67 SET274-6 timeout 500.0 61 SET275-6 timeout 500.0 61 SET276-6 timeout 500.0 61 SET277-6 timeout 500.0 61 SET278-6 timeout 500.0 61 SET279-6 timeout 500.0 122 SET280-6 timeout 500.0 64 SET281-6 timeout 500.0 63 SET282-6 timeout 500.0 66 SET283-6 timeout 500.0 52 SET284-6 timeout 500.0 62 SET285-6 timeout 500.0 135 SET286-6 timeout 500.0 134 SET287-6 timeout 500.0 72 SET288-6 timeout 500.0 50 SET289-6 timeout 500.0 63 SET290-6 timeout 500.0 66 SET291-6 timeout 500.0 134 SET292-6 timeout 500.0 67 SET293-6 timeout 500.0 61 SET294-6 timeout 500.0 61 SET295-6 timeout 500.0 61 SET296-6 theorem 0.0 2 1 9 0 8 0 0 0 2 9 131 99 0 SET297-6 timeout 500.0 61 SET298-6 timeout 500.0 61 SET299-6 timeout 500.0 62 SET300-6 timeout 500.0 61 SET301-6 timeout 500.0 61 SET302-6 timeout 500.0 33 SET303-6 timeout 500.0 33 SET304-6 timeout 500.0 127 SET305-6 timeout 500.0 73 SET306-6 timeout 500.0 61 SET307-6 timeout 500.0 61 SET308-6 timeout 500.0 47 SET309-6 timeout 500.0 62 SET310-6 timeout 500.0 62 SET311-6 timeout 500.0 62 SET312-6 timeout 500.0 61 SET313-6 timeout 500.0 56 SET314-6 timeout 500.0 61 SET315-6 timeout 500.0 62 SET316-6 timeout 500.0 61 SET317-6 timeout 500.0 62 SET318-6 timeout 500.0 61 SET319-6 timeout 500.0 62 SET320-6 timeout 500.0 61 SET321-6 timeout 500.0 48 SET322-6 timeout 500.0 50 SET323-6 timeout 500.0 57 SET324-6 timeout 500.0 34 SET325-6 timeout 500.0 33 SET326-6 timeout 500.0 50 SET327-6 timeout 500.0 50 SET328-6 timeout 500.0 123 SET329-6 timeout 500.0 120 SET330-6 timeout 500.0 131 SET331-6 timeout 500.0 60 SET332-6 timeout 500.0 61 SET333-6 timeout 500.0 49 SET334-6 timeout 500.0 49 SET335-6 timeout 500.0 62 SET336-6 timeout 500.0 63 SET337-6 timeout 500.0 63 SET338-6 timeout 500.0 60 SET339-6 timeout 500.0 20 SET340-6 timeout 500.0 117 SET341-6 timeout 500.0 54 SET342-6 timeout 500.0 62 SET343-6 timeout 500.0 62 SET344-6 timeout 500.0 48 SET345-6 timeout 500.0 49 SET346-6 timeout 500.0 129 SET347-6 timeout 500.0 67 SET348-6 timeout 500.0 61 SET349-6 timeout 500.0 60 SET350-6 timeout 500.0 53 SET351-6 timeout 500.0 49 SET352-6 timeout 500.0 134 SET353-6 timeout 500.0 117 SET354-6 timeout 500.0 134 SET355-6 timeout 500.0 33 SET356-6 timeout 500.0 61 SET357-6 timeout 500.0 60 SET358-6 timeout 500.0 61 SET359-6 timeout 500.0 62 SET360-6 timeout 500.0 61 SET361-6 timeout 500.0 62 SET362-6 timeout 500.0 45 SET363-6 timeout 500.0 20 SET364-6 timeout 500.0 34 SET365-6 timeout 500.0 48 SET366-6 timeout 500.0 52 SET367-6 timeout 500.0 62 SET368-6 timeout 500.0 61 SET369-6 timeout 500.0 52 SET370-6 timeout 500.0 61 SET371-6 timeout 500.0 62 SET372-6 timeout 500.0 61 SET373-6 timeout 500.0 60 SET374-6 timeout 500.0 131 SET375-6 timeout 500.0 128 SET376-6 timeout 500.0 124 SET377-6 timeout 500.0 34 SET378-6 timeout 500.0 62 SET379-6 timeout 500.0 61 SET380-6 timeout 500.0 70 SET381-6 timeout 500.0 62 SET382-6 timeout 500.0 62 SET383-6 timeout 500.0 61 SET384-6 timeout 500.0 61 SET385-6 timeout 500.0 60 SET386-6 timeout 500.0 56 SET387-6 timeout 500.0 135 SET388-6 timeout 500.0 125 SET389-6 timeout 500.0 134 SET390-6 timeout 500.0 132 SET391-6 timeout 500.0 133 SET392-6 timeout 500.0 61 SET393-6 timeout 500.0 61 SET394-6 timeout 500.0 61 SET395-6 timeout 500.0 62 SET396-6 timeout 500.0 68 SET397-6 timeout 500.0 62 SET398-6 timeout 500.0 61 SET399-6 timeout 500.0 62 SET400-6 timeout 500.0 64 SET401-6 timeout 500.0 60 SET402-6 timeout 500.0 61 SET403-6 timeout 500.0 61 SET404-6 timeout 500.0 49 SET405-6 timeout 500.0 49 SET406-6 timeout 500.0 72 SET407-6 timeout 500.0 72 SET408-6 timeout 500.0 61 SET409-6 timeout 500.0 123 SET410-6 timeout 500.0 135 SET411-6 theorem 0.1 2 1 279 0 40 0 1 0 2 279 2009 400 0 SET412-6 timeout 500.0 61 SET413-6 timeout 500.0 103 SET414-6 timeout 500.0 61 SET415-6 timeout 500.0 49 SET416-6 timeout 500.0 61 SET417-6 timeout 500.0 64 SET418-6 timeout 500.0 61 SET419-6 timeout 500.0 134 SET420-6 timeout 500.0 47 SET421-6 timeout 500.0 61 SET422-6 timeout 500.0 50 SET423-6 timeout 500.0 62 SET424-6 timeout 500.0 114 SET425-6 timeout 500.0 123 SET426-6 timeout 500.0 66 SET427-6 timeout 500.0 66 SET428-6 timeout 500.0 62 SET429-6 timeout 500.0 62 SET430-6 timeout 500.0 50 SET431-6 timeout 500.0 61 SET432-6 timeout 500.0 121 SET433-6 timeout 500.0 68 SET434-6 timeout 500.0 68 SET435-6 timeout 500.0 62 SET436-6 timeout 500.0 61 SET437-6 timeout 500.0 61 SET438-6 timeout 500.0 46 SET439-6 timeout 500.0 26 SET440-6 timeout 500.0 61 SET441-6 timeout 500.0 62 SET442-6 timeout 500.0 62 SET443-6 timeout 500.0 63 SET444-6 timeout 500.0 63 SET445-6 timeout 500.0 61 SET446-6 timeout 500.0 48 SET447-6 timeout 500.0 71 SET448-6 timeout 500.0 36 SET449-6 timeout 500.0 36 SET450-6 timeout 500.0 36 SET451-6 timeout 500.0 44 SET452-6 timeout 500.0 43 SET453-6 timeout 500.0 125 SET454-6 timeout 500.0 51 SET455-6 timeout 500.0 62 SET456-6 timeout 500.0 137 SET457-6 timeout 500.0 62 SET458-6 timeout 500.0 61 SET459-6 timeout 500.0 71 SET460-6 timeout 500.0 61 SET461-6 timeout 500.0 61 SET462-6 timeout 500.0 61 SET463-6 timeout 500.0 62 SET464-6 timeout 500.0 61 SET465-6 timeout 500.0 62 SET466-6 timeout 500.0 61 SET467-6 timeout 500.0 43 SET468-6 timeout 500.0 34 SET469-6 timeout 500.0 33 SET470-6 timeout 500.0 48 SET471-6 timeout 500.0 58 SET472-6 timeout 500.0 58 SET473-6 timeout 500.0 54 SET474-6 timeout 500.0 70 SET475-6 timeout 500.0 61 SET476-6 timeout 500.0 62 SET477-6 timeout 500.0 21 SET478-6 timeout 500.0 52 SET479-6 timeout 500.0 34 SET480-6 timeout 500.0 48 SET481-6 timeout 500.0 118 SET482-6 timeout 500.0 32 SET483-6 timeout 500.0 48 SET484-6 timeout 500.0 35 SET485-6 timeout 500.0 49 SET486-6 timeout 500.0 45 SET487-6 timeout 500.0 44 SET488-6 timeout 500.0 43 SET489-6 timeout 500.0 34 SET490-6 timeout 500.0 32 SET491-6 timeout 500.0 47 SET492-6 timeout 500.0 33 SET493-6 timeout 500.0 48 SET494-6 timeout 500.0 62 SET495-6 timeout 500.0 49 SET496-6 timeout 500.0 34 SET497-6 timeout 500.0 49 SET498-6 timeout 500.0 24 SET499-6 timeout 500.0 64 SET500-6 timeout 500.0 61 SET501-6 timeout 500.0 61 SET502-6 timeout 500.0 61 SET503-6 timeout 500.0 124 SET504-6 timeout 500.0 131 SET505-6 timeout 500.0 136 SET506-6 timeout 500.0 45 SET507-6 timeout 500.0 47 SET508-6 timeout 500.0 66 SET509-6 timeout 500.0 67 SET510-6 timeout 500.0 68 SET511-6 timeout 500.0 61 SET512-6 timeout 500.0 61 SET513-6 timeout 500.0 63 SET514-6 timeout 500.0 47 SET515-6 timeout 500.0 50 SET516-6 timeout 500.0 51 SET517-6 timeout 500.0 46 SET518-6 timeout 500.0 133 SET519-6 timeout 500.0 47 SET520-6 timeout 500.0 48 SET521-6 timeout 500.0 134 SET522-6 timeout 500.0 134 SET523-6 timeout 500.0 37 SET524-6 timeout 500.0 62 SET525-6 timeout 500.0 62 SET526-6 timeout 500.0 47 SET527-6 timeout 500.0 46 SET528-6 timeout 500.0 28 SET529-6 timeout 500.0 42 SET530-6 timeout 500.0 42 SET531-6 timeout 500.0 50 SET532-6 timeout 500.0 49 SET533-6 timeout 500.0 50 SET534-6 timeout 500.0 49 SET535-6 timeout 500.0 48 SET536-6 timeout 500.0 61 SET537-6 timeout 500.0 129 SET538-6 timeout 500.0 61 SET539-6 timeout 500.0 47 SET540-6 timeout 500.0 46 SET541-6 timeout 500.0 61 SET542-6 timeout 500.0 50 SET543-6 timeout 500.0 114 SET544-6 timeout 500.0 50 SET545-6 timeout 500.0 51 SET546-6 timeout 500.0 41 SET547-6 timeout 500.0 62 SET548-6 timeout 500.0 45 SET549-6 timeout 500.0 71 SET550-6 timeout 500.0 61 SET551-6 timeout 500.0 40 SET552-6 timeout 500.0 61 SET553-6 timeout 500.0 66 SET554-6 timeout 500.0 48 SET555-6 timeout 500.0 48 SET556-6 timeout 500.0 49 SET557-6 timeout 500.0 62 SET558-6 timeout 500.0 63 SET559-6 timeout 500.0 60 SET560-6 timeout 500.0 62 SET561-6 timeout 500.0 136 SET562-6 timeout 500.0 130 SET563-6 timeout 500.0 59 SET564-6 timeout 500.0 62 SET565-6 timeout 500.0 63 SET566-6 timeout 500.0 63 SET567-6 timeout 500.0 62 SET781-2 memory 389.4 499 SET781-3 timeout 500.0 62 SET782-1 timeout 500.0 61 SWC001-1 timeout 500.0 5 SWC002-1 timeout 500.0 5 SWC003-1 timeout 500.0 5 SWC004-1 timeout 500.0 5 SWC005-1 timeout 500.0 5 SWC006-1 timeout 500.0 5 SWC007-1 timeout 500.0 5 SWC008-1 timeout 500.0 5 SWC009-1 timeout 500.0 5 SWC010-1 timeout 500.0 5 SWC011-1 timeout 500.0 5 SWC012-1 timeout 500.0 5 SWC013-1 timeout 500.0 5 SWC014-1 timeout 500.0 5 SWC015-1 timeout 500.0 5 SWC016-1 timeout 500.0 5 SWC017-1 timeout 500.0 5 SWC018-1 timeout 500.0 5 SWC019-1 theorem 118.9 4 1 519 0 63 1 0 0 2 519 8002 10884 0 SWC020-1 timeout 500.0 5 SWC021-1 timeout 500.0 5 SWC022-1 timeout 500.0 5 SWC023-1 theorem 59.1 4 1 452 0 66 1 0 0 2 452 6928 10415 0 SWC024-1 theorem 57.8 4 1 450 0 66 1 0 0 2 450 6887 10448 0 SWC025-1 timeout 500.0 5 SWC026-1 timeout 500.0 5 SWC027-1 timeout 500.0 5 SWC028-1 timeout 500.0 5 SWC029-1 timeout 500.0 5 SWC030-1 timeout 500.0 5 SWC031-1 timeout 500.0 5 SWC032-1 timeout 500.0 5 SWC033-1 timeout 500.0 5 SWC034-1 timeout 500.0 5 SWC035-1 theorem 27.7 3 1 104 0 64 0 0 0 2 104 4104 7632 0 SWC036-1 theorem 17.7 3 1 86 0 64 1 0 0 2 86 4052 7593 0 SWC037-1 theorem 123.0 5 1 701 0 68 1 0 0 2 701 9738 12584 0 SWC038-1 theorem 87.5 4 1 565 0 64 2 0 0 2 565 7673 10826 0 SWC039-1 timeout 500.0 5 SWC040-1 theorem 17.6 3 1 86 0 64 1 0 0 2 86 4052 7593 0 SWC041-1 theorem 99.1 4 1 420 0 67 0 0 0 2 420 6574 10170 0 SWC042-1 theorem 99.5 4 1 420 0 67 0 0 0 2 420 6574 10170 0 SWC043-1 theorem 112.3 4 1 420 0 67 0 0 0 2 420 6574 10170 0 SWC044-1 theorem 86.8 4 1 408 0 64 0 0 0 2 408 6204 9649 0 SWC045-1 timeout 500.0 5 SWC046-1 timeout 500.0 5 SWC047-1 timeout 500.0 5 SWC048-1 timeout 500.0 5 SWC049-1 timeout 500.0 5 SWC050-1 timeout 500.0 5 SWC051-1 theorem 34.3 4 1 418 0 65 1 0 0 2 418 5695 8851 0 SWC052-1 timeout 500.0 5 SWC053-1 timeout 500.0 5 SWC054-1 timeout 500.0 5 SWC055-1 timeout 500.0 5 SWC056-1 timeout 500.0 5 SWC057-1 timeout 500.0 5 SWC058-1 timeout 500.0 5 SWC059-1 timeout 500.0 5 SWC060-1 timeout 500.0 5 SWC061-1 timeout 500.0 5 SWC062-1 timeout 500.0 5 SWC063-1 timeout 500.0 5 SWC064-1 timeout 500.0 5 SWC065-1 timeout 500.0 5 SWC066-1 timeout 500.0 5 SWC067-1 timeout 500.0 5 SWC068-1 timeout 500.0 5 SWC069-1 timeout 500.0 5 SWC070-1 timeout 500.0 5 SWC071-1 timeout 500.0 5 SWC072-1 timeout 500.0 5 SWC073-1 timeout 500.0 5 SWC074-1 timeout 500.0 5 SWC075-1 timeout 500.0 5 SWC076-1 theorem 97.9 4 1 674 0 66 3 0 0 2 674 8964 12253 0 SWC077-1 timeout 500.0 5 SWC078-1 timeout 500.0 5 SWC079-1 timeout 500.0 5 SWC080-1 timeout 500.0 5 SWC081-1 timeout 500.0 5 SWC082-1 theorem 60.6 4 1 438 0 67 1 0 0 2 438 6630 10359 0 SWC083-1 timeout 500.0 5 SWC084-1 timeout 500.0 5 SWC085-1 timeout 500.0 5 SWC086-1 theorem 51.7 4 1 433 0 64 1 0 0 2 433 6349 9850 0 SWC087-1 timeout 500.0 5 SWC088-1 timeout 500.0 5 SWC089-1 timeout 500.0 5 SWC090-1 timeout 500.0 5 SWC091-1 timeout 500.0 5 SWC092-1 timeout 500.0 5 SWC093-1 timeout 500.0 5 SWC094-1 timeout 500.0 5 SWC095-1 timeout 500.0 5 SWC096-1 timeout 500.0 5 SWC097-1 timeout 500.0 5 SWC098-1 timeout 500.0 5 SWC099-1 timeout 500.0 5 SWC100-1 timeout 500.0 5 SWC101-1 theorem 88.5 4 1 662 0 66 4 0 0 2 662 8448 11544 0 SWC102-1 theorem 62.0 4 1 475 0 64 1 0 0 2 475 7571 11103 0 SWC103-1 theorem 50.7 4 1 430 0 66 2 0 0 2 430 6294 9885 0 SWC104-1 theorem 69.1 4 1 451 0 67 2 0 0 2 451 7113 10989 0 SWC105-1 timeout 500.0 5 SWC106-1 timeout 500.0 5 SWC107-1 timeout 500.0 5 SWC108-1 timeout 500.0 5 SWC109-1 timeout 500.0 5 SWC110-1 timeout 500.0 5 SWC111-1 timeout 500.0 5 SWC112-1 timeout 500.0 5 SWC113-1 timeout 500.0 5 SWC114-1 timeout 500.0 5 SWC115-1 timeout 500.0 5 SWC116-1 timeout 500.0 5 SWC117-1 timeout 500.0 5 SWC118-1 theorem 96.3 4 1 674 0 67 4 0 0 2 674 8862 12116 0 SWC119-1 timeout 500.0 5 SWC120-1 timeout 500.0 5 SWC121-1 timeout 500.0 5 SWC122-1 timeout 500.0 5 SWC123-1 timeout 500.0 5 SWC124-1 timeout 500.0 5 SWC125-1 timeout 500.0 5 SWC126-1 timeout 500.0 5 SWC127-1 theorem 51.2 4 1 433 0 64 3 0 0 2 433 6332 9879 0 SWC128-1 memory 271.0 499 SWC129-1 theorem 34.7 4 1 326 0 63 0 0 0 2 326 5258 8747 0 SWC130-1 theorem 34.6 4 1 326 0 63 0 0 0 2 326 5258 8747 0 SWC131-1 theorem 34.7 4 1 326 0 63 0 0 0 2 326 5258 8747 0 SWC132-1 theorem 34.7 4 1 326 0 63 0 0 0 2 326 5258 8747 0 SWC133-1 theorem 34.8 4 1 326 0 63 0 0 0 2 326 5258 8747 0 SWC134-1 theorem 34.9 4 1 326 0 63 0 0 0 2 326 5258 8747 0 SWC135-1 theorem 34.7 4 1 326 0 63 0 0 0 2 326 5258 8747 0 SWC136-1 theorem 7.7 3 1 62 0 62 0 0 0 2 62 3711 7423 0 SWC137-1 timeout 500.0 5 SWC138-1 theorem 7.8 3 1 62 0 62 0 0 0 2 62 3711 7423 0 SWC139-1 theorem 7.7 3 1 62 0 62 0 0 0 2 62 3711 7423 0 SWC140-1 theorem 7.7 3 1 62 0 62 0 0 0 2 62 3711 7423 0 SWC141-1 theorem 7.7 3 1 62 0 62 0 0 0 2 62 3711 7423 0 SWC142-1 theorem 7.7 3 1 62 0 62 0 0 0 2 62 3711 7423 0 SWC143-1 theorem 7.7 3 1 62 0 62 0 0 0 2 62 3711 7423 0 SWC144-1 theorem 7.9 3 1 63 0 63 0 0 0 2 63 3715 7423 0 SWC145-1 theorem 7.9 3 1 63 0 63 0 0 0 2 63 3715 7423 0 SWC146-1 theorem 7.9 3 1 63 0 63 0 0 0 2 63 3715 7423 0 SWC147-1 theorem 7.9 3 1 63 0 63 0 0 0 2 63 3715 7423 0 SWC148-1 timeout 500.0 5 SWC149-1 timeout 500.0 5 SWC150-1 theorem 8.0 3 1 63 0 63 0 0 0 2 63 3715 7423 0 SWC151-1 theorem 7.7 3 1 62 0 62 0 0 0 2 62 3717 7427 0 SWC152-1 timeout 500.0 5 SWC153-1 timeout 500.0 5 SWC154-1 timeout 500.0 5 SWC155-1 timeout 500.0 5 SWC156-1 timeout 500.0 5 SWC157-1 timeout 500.0 5 SWC158-1 timeout 500.0 5 SWC159-1 timeout 500.0 5 SWC160-1 timeout 500.0 5 SWC161-1 timeout 500.0 5 SWC162-1 timeout 500.0 5 SWC163-1 timeout 500.0 5 SWC164-1 timeout 500.0 5 SWC165-1 timeout 500.0 5 SWC166-1 timeout 500.0 5 SWC167-1 timeout 500.0 5 SWC168-1 timeout 500.0 5 SWC169-1 timeout 500.0 5 SWC170-1 timeout 500.0 5 SWC171-1 timeout 500.0 5 SWC172-1 timeout 500.0 5 SWC173-1 timeout 500.0 5 SWC174-1 timeout 500.0 5 SWC175-1 timeout 500.0 5 SWC176-1 timeout 500.0 5 SWC177-1 timeout 500.0 5 SWC178-1 timeout 500.0 5 SWC179-1 theorem 19.8 4 1 273 0 74 20 17 0 2 273 5959 9377 0 SWC180-1 timeout 500.0 5 SWC181-1 timeout 500.0 6 SWC182-1 timeout 500.0 5 SWC183-1 timeout 500.0 5 SWC184-1 timeout 500.0 5 SWC185-1 timeout 500.0 5 SWC186-1 timeout 500.0 5 SWC187-1 timeout 500.0 5 SWC188-1 timeout 500.0 5 SWC189-1 timeout 500.0 5 SWC190-1 timeout 500.0 5 SWC191-1 timeout 500.0 5 SWC192-1 timeout 500.0 5 SWC193-1 timeout 500.0 5 SWC194-1 timeout 500.0 5 SWC195-1 timeout 500.0 5 SWC196-1 timeout 500.0 5 SWC197-1 timeout 500.0 5 SWC198-1 timeout 500.0 5 SWC199-1 timeout 500.0 5 SWC200-1 timeout 500.0 5 SWC201-1 timeout 500.0 5 SWC202-1 timeout 500.0 5 SWC203-1 theorem 8.0 3 1 70 0 64 0 0 0 2 70 3902 7500 0 SWC204-1 timeout 500.0 5 SWC205-1 theorem 76.2 4 1 451 0 65 2 0 0 2 451 6160 9027 0 SWC206-1 theorem 119.3 4 1 489 0 69 1 0 0 2 489 7570 10903 0 SWC207-1 theorem 76.6 4 1 452 0 64 2 0 0 2 452 6289 9166 0 SWC208-1 theorem 77.8 4 1 450 0 64 1 0 0 2 450 6174 9104 0 SWC209-1 theorem 75.0 4 1 450 0 64 1 0 0 2 450 6174 9104 0 SWC210-1 timeout 500.0 5 SWC211-1 timeout 500.0 5 SWC212-1 timeout 500.0 5 SWC213-1 theorem 97.0 4 1 469 0 68 1 0 0 2 469 6885 10016 0 SWC214-1 timeout 500.0 5 SWC215-1 timeout 500.0 5 SWC216-1 timeout 500.0 5 SWC217-1 theorem 34.8 4 1 382 0 64 2 0 0 2 382 5456 8809 0 SWC218-1 timeout 500.0 5 SWC219-1 timeout 500.0 5 SWC220-1 timeout 500.0 5 SWC221-1 timeout 500.0 5 SWC222-1 timeout 500.0 5 SWC223-1 timeout 500.0 5 SWC224-1 timeout 500.0 5 SWC225-1 timeout 500.0 5 SWC226-1 timeout 500.0 5 SWC227-1 timeout 500.0 5 SWC228-1 timeout 500.0 5 SWC229-1 timeout 500.0 5 SWC230-1 timeout 500.0 5 SWC231-1 timeout 500.0 5 SWC232-1 timeout 500.0 5 SWC233-1 timeout 500.0 5 SWC234-1 timeout 500.0 5 SWC235-1 timeout 500.0 5 SWC236-1 timeout 500.0 5 SWC237-1 timeout 500.0 5 SWC238-1 timeout 500.0 5 SWC239-1 timeout 500.0 5 SWC240-1 timeout 500.0 5 SWC241-1 timeout 500.0 5 SWC242-1 timeout 500.0 5 SWC243-1 timeout 500.0 5 SWC244-1 timeout 500.0 5 SWC245-1 timeout 500.0 5 SWC246-1 timeout 500.0 5 SWC247-1 timeout 500.0 5 SWC248-1 timeout 500.0 5 SWC249-1 timeout 500.0 5 SWC250-1 timeout 500.0 5 SWC251-1 timeout 500.0 5 SWC252-1 timeout 500.0 5 SWC253-1 timeout 500.0 5 SWC254-1 timeout 500.0 5 SWC255-1 timeout 500.0 5 SWC256-1 theorem 33.8 4 1 410 0 64 2 0 0 2 410 5705 8884 0 SWC257-1 timeout 500.0 5 SWC258-1 timeout 500.0 5 SWC259-1 timeout 500.0 5 SWC260-1 timeout 500.0 5 SWC261-1 timeout 500.0 5 SWC262-1 theorem 7.6 3 1 64 0 63 0 0 0 2 64 3788 7431 0 SWC263-1 timeout 500.0 5 SWC264-1 timeout 500.0 5 SWC265-1 timeout 500.0 5 SWC266-1 timeout 500.0 5 SWC267-1 timeout 500.0 5 SWC268-1 timeout 500.0 5 SWC269-1 theorem 7.9 3 1 65 0 64 0 0 0 2 65 3798 7440 0 SWC270-1 timeout 500.0 5 SWC271-1 timeout 500.0 5 SWC272-1 timeout 500.0 5 SWC273-1 timeout 500.0 5 SWC274-1 timeout 500.0 5 SWC275-1 timeout 500.0 5 SWC276-1 timeout 500.0 5 SWC277-1 timeout 500.0 5 SWC278-1 timeout 500.0 5 SWC279-1 timeout 500.0 5 SWC280-1 timeout 500.0 5 SWC281-1 timeout 500.0 5 SWC282-1 timeout 500.0 5 SWC283-1 timeout 500.0 5 SWC284-1 timeout 500.0 5 SWC285-1 timeout 500.0 5 SWC286-1 timeout 500.0 5 SWC287-1 timeout 500.0 5 SWC288-1 timeout 500.0 5 SWC289-1 theorem 7.7 3 1 64 0 63 0 0 0 2 64 3788 7431 0 SWC290-1 timeout 500.0 5 SWC291-1 theorem 7.9 3 1 65 0 64 0 0 0 2 65 3791 7433 0 SWC292-1 timeout 500.0 5 SWC293-1 timeout 500.0 5 SWC294-1 timeout 500.0 5 SWC295-1 timeout 500.0 5 SWC296-1 timeout 500.0 5 SWC297-1 timeout 500.0 5 SWC298-1 timeout 500.0 5 SWC299-1 timeout 500.0 5 SWC300-1 timeout 500.0 5 SWC301-1 timeout 500.0 5 SWC302-1 timeout 500.0 5 SWC303-1 timeout 500.0 5 SWC304-1 timeout 500.0 5 SWC305-1 timeout 500.0 5 SWC306-1 timeout 500.0 5 SWC307-1 timeout 500.0 5 SWC308-1 timeout 500.0 5 SWC309-1 timeout 500.0 5 SWC310-1 timeout 500.0 5 SWC311-1 timeout 500.0 5 SWC312-1 timeout 500.0 5 SWC313-1 timeout 500.0 5 SWC314-1 timeout 500.0 5 SWC315-1 timeout 500.0 5 SWC316-1 timeout 500.0 5 SWC317-1 timeout 500.0 5 SWC318-1 timeout 500.0 5 SWC319-1 timeout 500.0 5 SWC320-1 timeout 500.0 5 SWC321-1 timeout 500.0 5 SWC322-1 timeout 500.0 5 SWC323-1 timeout 500.0 5 SWC324-1 timeout 500.0 5 SWC325-1 timeout 500.0 5 SWC326-1 timeout 500.0 5 SWC327-1 timeout 500.0 5 SWC328-1 theorem 73.9 4 1 398 0 62 2 0 0 2 398 5796 9134 0 SWC329-1 timeout 500.0 5 SWC330-1 timeout 500.0 5 SWC331-1 timeout 500.0 5 SWC332-1 timeout 500.0 5 SWC333-1 theorem 42.8 4 1 427 0 68 2 0 0 2 427 5897 9369 0 SWC334-1 timeout 500.0 5 SWC335-1 timeout 500.0 5 SWC336-1 timeout 500.0 5 SWC337-1 timeout 500.0 5 SWC338-1 timeout 500.0 5 SWC339-1 theorem 44.0 4 1 427 0 65 2 0 0 2 427 6150 9809 0 SWC340-1 timeout 500.0 5 SWC341-1 timeout 500.0 5 SWC342-1 timeout 500.0 5 SWC343-1 timeout 500.0 5 SWC344-1 timeout 500.0 5 SWC345-1 timeout 500.0 5 SWC346-1 timeout 500.0 5 SWC347-1 timeout 500.0 5 SWC348-1 timeout 500.0 5 SWC349-1 theorem 19.0 3 1 231 0 64 0 0 0 2 231 4758 8308 0 SWC350-1 theorem 7.7 3 1 69 0 65 0 0 0 2 69 3832 7475 0 SWC351-1 theorem 49.7 4 1 390 0 66 0 0 0 2 390 5652 9162 0 SWC352-1 theorem 51.0 4 1 446 0 65 2 0 0 2 446 6638 9906 0 SWC353-1 theorem 39.0 4 1 388 0 65 0 0 0 2 388 5620 9158 0 SWC354-1 timeout 500.0 5 SWC355-1 timeout 500.0 5 SWC356-1 timeout 500.0 5 SWC357-1 timeout 500.0 5 SWC358-1 theorem 34.7 4 1 419 0 63 2 0 0 2 419 5709 8840 0 SWC359-1 theorem 7.8 3 1 69 0 65 0 0 0 2 69 3814 7466 0 SWC360-1 theorem 7.9 3 1 69 0 65 0 0 0 2 69 3814 7466 0 SWC361-1 theorem 7.9 3 1 69 0 65 0 0 0 2 69 3814 7466 0 SWC362-1 timeout 500.0 5 SWC363-1 timeout 500.0 5 SWC364-1 timeout 500.0 5 SWC365-1 theorem 34.1 4 1 415 0 64 2 0 0 2 415 5685 8799 0 SWC366-1 timeout 500.0 5 SWC367-1 theorem 33.7 4 1 417 0 63 1 0 0 2 417 5723 8835 0 SWC368-1 timeout 500.0 5 SWC369-1 theorem 49.8 4 1 446 0 65 2 0 0 2 446 6602 9906 0 SWC370-1 timeout 500.0 5 SWC371-1 timeout 500.0 5 SWC372-1 timeout 500.0 5 SWC373-1 timeout 500.0 5 SWC374-1 timeout 500.0 5 SWC375-1 timeout 500.0 5 SWC376-1 timeout 500.0 5 SWC377-1 timeout 500.0 5 SWC378-1 timeout 500.0 5 SWC379-1 timeout 500.0 5 SWC380-1 timeout 500.0 5 SWC381-1 timeout 500.0 5 SWC382-1 timeout 500.0 5 SWC383-1 timeout 500.0 5 SWC384-1 timeout 500.0 5 SWC385-1 theorem 33.9 4 1 418 0 64 3 0 0 2 418 5662 8843 0 SWC386-1 timeout 500.0 5 SWC387-1 timeout 500.0 5 SWC388-1 timeout 500.0 5 SWC389-1 timeout 500.0 5 SWC390-1 timeout 500.0 5 SWC391-1 theorem 37.0 4 1 387 0 65 0 0 0 2 387 5509 8893 0 SWC392-1 timeout 500.0 5 SWC393-1 timeout 500.0 5 SWC394-1 timeout 500.0 5 SWC395-1 timeout 500.0 5 SWC396-1 timeout 500.0 5 SWC397-1 timeout 500.0 5 SWC398-1 theorem 39.9 4 1 429 0 67 0 0 0 2 429 6104 9466 0 SWC399-1 timeout 500.0 5 SWC400-1 timeout 500.0 5 SWC401-1 timeout 500.0 5 SWC402-1 timeout 500.0 5 SWC403-1 timeout 500.0 5 SWC404-1 timeout 500.0 5 SWC405-1 theorem 36.9 4 1 383 0 64 0 0 0 2 383 5423 8827 0 SWC406-1 theorem 36.2 4 1 383 0 64 0 0 0 2 383 5423 8830 0 SWC407-1 timeout 500.0 5 SWC408-1 theorem 37.3 4 1 419 0 65 0 0 0 2 419 5760 8974 0 SWC409-1 timeout 500.0 5 SWC410-1 timeout 500.0 5 SWC411-1 theorem 36.5 4 1 383 0 64 0 0 0 2 383 5422 8826 0 SWC412-1 timeout 500.0 5 SWC413-1 timeout 500.0 5 SWC414-1 timeout 500.0 5 SWC415-1 timeout 500.0 5 SWC416-1 timeout 500.0 5 SWC417-1 timeout 500.0 5 SWC418-1 timeout 500.0 5 SWC419-1 timeout 500.0 5 SWC420-1 timeout 500.0 5 SWC421-1 timeout 500.0 5 SWC422-1 timeout 500.0 5 SWC423-1 memory 279.5 496 SWV002-1 theorem 0.0 4 1 115 0 14 0 0 0 2 115 844 288 0 SWV003-1 theorem 0.0 4 1 8 0 8 0 0 0 2 8 81 30 0 SWV004-1 timeout 500.0 12 SWV005-1 theorem 0.0 4 1 12 0 12 1 0 0 2 12 85 33 0 SWV006-1 theorem 0.0 4 1 12 0 11 0 0 0 2 12 89 32 0 SWV007-1 theorem 0.0 4 1 58 0 14 0 0 0 2 58 394 130 0 SWV008-1 theorem 1.2 4 1 329 0 9 1 0 0 3 329 4520 1259 0 SWV019-1 theorem 0.0 4 1 29 0 7 8 0 0 2 29 110 27 0 SWV020-1 timeout 500.0 33 SYN013-1 theorem 0.0 2 3 39 2 4 0 0 27 2 33 200 178 0 SYN014-1 theorem 0.0 2 4 61 3 4 2 0 55 2 34 361 334 0 SYN015-1 theorem 0.0 2 11 161 10 2 0 0 122 2 39 946 769 0 SYN071-1 theorem 0.0 2 2 13 1 7 3 0 2 2 11 65 24 0 SYN072-1 theorem 0.0 2 4 54 4 5 0 0 17 2 27 271 165 0 SYN073-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 7 5 0 SYN074-1 theorem 3.8 2 53 670 456 1 0 15 55507 2 125 10709 83493 0 SYN075-1 theorem 0.5 2 13 132 72 1 0 3 7758 2 92 1751 12195 0 SYN076-1 timeout 500.0 259 SYN077-1 theorem 0.2 2 5 547 8 1 0 0 310 4 272 3171 865 0 SYN078-1 non_thm 0.0 2 0 1 1 2 0 0 5 2 0 5 6 0