%------------------------------------------------------------------------------ % File : SETHEO---3.3 % Problem : MSC015-1.025 : TPTP v5.0.0. Released v3.5.0. % Transfm : add_equality % Format : setheo % Command : setheo-wrapper %s % Computer : art01.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz % Memory : 2018MB % OS : Linux 2.6.26.8-57.fc8 % CPULimit : 300s % DateTime : Fri Dec 24 17:32:40 EST 2010 % Result : GaveUp 5.88s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % /tmp/SystemOnTPTP2801/MSC MSC015-1.025+noeq /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq % MUST DELETE /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq.hex % MUST DELETE /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq.log % MUST DELETE /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq.tree % codegen: 227 [199999] labels, 0 colls [610 accesses] % Assembler optimization: 106 labels read, 34 labels output % /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq.hex generated in 0.00 seconds % inwasm V4.02b [wasm-less] Copyright TU Munich 1998 (03/30/98) % Command line: /home/graph/tptp/Systems/SETHEO---3.3/setheo.linux/inwasm -cons -foldup /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq % Parsing input-file. % Preprocessing: Generating weak-unification. % Preprocessing: purity % Message: Deleted clauses : None. % Message: Making sortarray. % Preprocessing: orbranch reordering % Preprocessing: inserting tautology-constraints % Preprocessing: inserting subsumption-constraints % Preprocessing: removing redundant constraints % Message: 0 constraints deleted. % Preprocessing: inserting reduction steps % Preprocessing: subgoal reordering % Codegeneration. % SAM V4.0[LINUX,PIL] Copyright TU Munich (June 1999) % 32 bit word format % main.c built on Feb 12 2004 at 21:51:21 % run Fri Dec 24 17:32:41 2010 % Options : -dr -cons -dynsgreord 2 /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq % using antilemma-constraints % using regularity-constraints % using tautology-constraints % using subsumption-constraints % Loading code... % Initializing memory... % Initializing registers1... % Initializing registers2... % Initializing bounds... % Initializing signals... % Start proving... % -d: 2 time < 0.01 sec inferences = 3 fails = 2 % -d: 3 time < 0.01 sec inferences = 27 fails = 25 % -d: 4 time < 0.01 sec inferences = 29 fails = 26 % -d: 5 time < 0.01 sec inferences = 53 fails = 49 % -d: 6 time < 0.01 sec inferences = 55 fails = 50 % -d: 7 time < 0.01 sec inferences = 79 fails = 73 % -d: 8 time < 0.01 sec inferences = 81 fails = 74 % -d: 9 time < 0.01 sec inferences = 105 fails = 97 % -d: 10 time < 0.01 sec inferences = 107 fails = 98 % -d: 11 time < 0.01 sec inferences = 131 fails = 121 % -d: 12 time < 0.01 sec inferences = 133 fails = 122 % -d: 13 time < 0.01 sec inferences = 157 fails = 145 % -d: 14 time < 0.01 sec inferences = 159 fails = 146 % -d: 15 time < 0.01 sec inferences = 183 fails = 169 % -d: 16 time < 0.01 sec inferences = 185 fails = 170 % -d: 17 time < 0.01 sec inferences = 209 fails = 193 % -d: 18 time < 0.01 sec inferences = 211 fails = 194 % -d: 19 time < 0.01 sec inferences = 235 fails = 217 % -d: 20 time < 0.01 sec inferences = 237 fails = 218 % -d: 21 time < 0.01 sec inferences = 261 fails = 241 % -d: 22 time < 0.01 sec inferences = 263 fails = 242 % -d: 23 time < 0.01 sec inferences = 287 fails = 265 % -d: 24 time < 0.01 sec inferences = 289 fails = 266 % -d: 25 time < 0.01 sec inferences = 313 fails = 289 % -d: 26 time < 0.01 sec inferences = 315 fails = 290 % -d: 27 time < 0.01 sec inferences = 339 fails = 313 % -d: 28 time < 0.01 sec inferences = 341 fails = 314 % -d: 29 time < 0.01 sec inferences = 365 fails = 337 % -d: 30 time < 0.01 sec inferences = 367 fails = 338 % -d: 31 time < 0.01 sec inferences = 391 fails = 361 % -d: 32 time < 0.01 sec inferences = 393 fails = 362 % -d: 33 time = 0.01 sec inferences = 417 fails = 385 % -d: 34 time < 0.01 sec inferences = 419 fails = 386 % -d: 35 time < 0.01 sec inferences = 443 fails = 409 % -d: 36 time < 0.01 sec inferences = 445 fails = 410 % -d: 37 time < 0.01 sec inferences = 469 fails = 433 % -d: 38 time < 0.01 sec inferences = 471 fails = 434 % -d: 39 time < 0.01 sec inferences = 495 fails = 457 % -d: 40 time < 0.01 sec inferences = 497 fails = 458 % -d: 41 time < 0.01 sec inferences = 521 fails = 481 % -d: 42 time < 0.01 sec inferences = 523 fails = 482 % -d: 43 time = 0.01 sec inferences = 547 fails = 505 % -d: 44 time < 0.01 sec inferences = 549 fails = 506 % -d: 45 time < 0.01 sec inferences = 573 fails = 529 % -d: 46 time < 0.01 sec inferences = 575 fails = 530 % -d: 47 time < 0.01 sec inferences = 599 fails = 553 % -d: 48 time < 0.01 sec inferences = 601 fails = 554 % -d: 49 time < 0.01 sec inferences = 625 fails = 577 % -d: 50 time = 0.01 sec inferences = 627 fails = 578 % -d: 51 time < 0.01 sec inferences = 651 fails = 601 % -d: 52 time < 0.01 sec inferences = 653 fails = 602 % -d: 53 time < 0.01 sec inferences = 677 fails = 625 % -d: 54 time < 0.01 sec inferences = 679 fails = 626 % -d: 55 time = 0.01 sec inferences = 703 fails = 649 % -d: 56 time < 0.01 sec inferences = 705 fails = 650 % -d: 57 time < 0.01 sec inferences = 729 fails = 673 % -d: 58 time < 0.01 sec inferences = 731 fails = 674 % -d: 59 time < 0.01 sec inferences = 755 fails = 697 % -d: 60 time < 0.01 sec inferences = 757 fails = 698 % -d: 61 time < 0.01 sec inferences = 781 fails = 721 % -d: 62 time < 0.01 sec inferences = 783 fails = 722 % -d: 63 time < 0.01 sec inferences = 807 fails = 745 % -d: 64 time < 0.01 sec inferences = 809 fails = 746 % -d: 65 time = 0.01 sec inferences = 833 fails = 769 % -d: 66 time < 0.01 sec inferences = 835 fails = 770 % -d: 67 time < 0.01 sec inferences = 859 fails = 793 % -d: 68 time < 0.01 sec inferences = 861 fails = 794 % -d: 69 time < 0.01 sec inferences = 885 fails = 817 % -d: 70 time < 0.01 sec inferences = 887 fails = 818 % -d: 71 time < 0.01 sec inferences = 911 fails = 841 % -d: 72 time < 0.01 sec inferences = 913 fails = 842 % -d: 73 time = 0.01 sec inferences = 937 fails = 865 % -d: 74 time < 0.01 sec inferences = 939 fails = 866 % -d: 75 time < 0.01 sec inferences = 963 fails = 889 % -d: 76 time < 0.01 sec inferences = 965 fails = 890 % -d: 77 time < 0.01 sec inferences = 989 fails = 913 % -d: 78 time < 0.01 sec inferences = 991 fails = 914 % -d: 79 time < 0.01 sec inferences = 1015 fails = 937 % -d: 80 time < 0.01 sec inferences = 1017 fails = 938 % -d: 81 time < 0.01 sec inferences = 1041 fails = 961 % -d: 82 time < 0.01 sec inferences = 1043 fails = 962 % -d: 83 time = 0.01 sec inferences = 1067 fails = 985 % -d: 84 time < 0.01 sec inferences = 1069 fails = 986 % -d: 85 time = 0.01 sec inferences = 1093 fails = 1009 % -d: 86 time < 0.01 sec inferences = 1095 fails = 1010 % -d: 87 time < 0.01 sec inferences = 1119 fails = 1033 % -d: 88 time = 0.01 sec inferences = 1121 fails = 1034 % -d: 89 time < 0.01 sec inferences = 1145 fails = 1057 % -d: 90 time < 0.01 sec inferences = 1147 fails = 1058 % -d: 91 time < 0.01 sec inferences = 1171 fails = 1081 % -d: 92 time < 0.01 sec inferences = 1173 fails = 1082 % -d: 93 time < 0.01 sec inferences = 1197 fails = 1105 % -d: 94 time < 0.01 sec inferences = 1199 fails = 1106 % -d: 95 time = 0.01 sec inferences = 1223 fails = 1129 % -d: 96 time < 0.01 sec inferences = 1225 fails = 1130 % -d: 97 time < 0.01 sec inferences = 1249 fails = 1153 % -d: 98 time < 0.01 sec inferences = 1251 fails = 1154 % -d: 99 time < 0.01 sec inferences = 1275 fails = 1177 % -d: 100 time < 0.01 sec inferences = 1277 fails = 1178 % -d: 101 time = 0.01 sec inferences = 1301 fails = 1201 % -d: 102 time < 0.01 sec inferences = 1303 fails = 1202 % -d: 103 time < 0.01 sec inferences = 1327 fails = 1225 % -d: 104 time < 0.01 sec inferences = 1329 fails = 1226 % -d: 105 time = 0.01 sec inferences = 1353 fails = 1249 % -d: 106 time = 0.01 sec inferences = 1355 fails = 1250 % -d: 107 time < 0.01 sec inferences = 1379 fails = 1273 % -d: 108 time < 0.01 sec inferences = 1381 fails = 1274 % -d: 109 time < 0.01 sec inferences = 1405 fails = 1297 % -d: 110 time = 0.01 sec inferences = 1407 fails = 1298 % -d: 111 time < 0.01 sec inferences = 1431 fails = 1321 % -d: 112 time < 0.01 sec inferences = 1433 fails = 1322 % -d: 113 time = 0.01 sec inferences = 1457 fails = 1345 % -d: 114 time < 0.01 sec inferences = 1459 fails = 1346 % -d: 115 time < 0.01 sec inferences = 1483 fails = 1369 % -d: 116 time < 0.01 sec inferences = 1485 fails = 1370 % -d: 117 time = 0.01 sec inferences = 1509 fails = 1393 % -d: 118 time < 0.01 sec inferences = 1511 fails = 1394 % -d: 119 time < 0.01 sec inferences = 1535 fails = 1417 % -d: 120 time < 0.01 sec inferences = 1537 fails = 1418 % -d: 121 time < 0.01 sec inferences = 1561 fails = 1441 % -d: 122 time = 0.01 sec inferences = 1563 fails = 1442 % -d: 123 time < 0.01 sec inferences = 1587 fails = 1465 % -d: 124 time < 0.01 sec inferences = 1589 fails = 1466 % -d: 125 time < 0.01 sec inferences = 1613 fails = 1489 % -d: 126 time = 0.01 sec inferences = 1615 fails = 1490 % -d: 127 time < 0.01 sec inferences = 1639 fails = 1513 % -d: 128 time < 0.01 sec inferences = 1641 fails = 1514 % -d: 129 time = 0.01 sec inferences = 1665 fails = 1537 % -d: 130 time = 0.01 sec inferences = 1667 fails = 1538 % -d: 131 time < 0.01 sec inferences = 1691 fails = 1561 % -d: 132 time = 0.01 sec inferences = 1693 fails = 1562 % -d: 133 time < 0.01 sec inferences = 1717 fails = 1585 % -d: 134 time = 0.01 sec inferences = 1719 fails = 1586 % -d: 135 time < 0.01 sec inferences = 1743 fails = 1609 % -d: 136 time = 0.01 sec inferences = 1745 fails = 1610 % -d: 137 time = 0.01 sec inferences = 1769 fails = 1633 % -d: 138 time < 0.01 sec inferences = 1771 fails = 1634 % -d: 139 time = 0.01 sec inferences = 1795 fails = 1657 % -d: 140 time = 0.01 sec inferences = 1797 fails = 1658 % -d: 141 time < 0.01 sec inferences = 1821 fails = 1681 % -d: 142 time < 0.01 sec inferences = 1823 fails = 1682 % -d: 143 time = 0.01 sec inferences = 1847 fails = 1705 % -d: 144 time = 0.01 sec inferences = 1849 fails = 1706 % -d: 145 time = 0.01 sec inferences = 1873 fails = 1729 % -d: 146 time < 0.01 sec inferences = 1875 fails = 1730 % -d: 147 time < 0.01 sec inferences = 1899 fails = 1753 % -d: 148 time < 0.01 sec inferences = 1901 fails = 1754 % -d: 149 time = 0.02 sec inferences = 1925 fails = 1777 % -d: 150 time = 0.01 sec inferences = 1927 fails = 1778 % -d: 151 time < 0.01 sec inferences = 1951 fails = 1801 % -d: 152 time < 0.01 sec inferences = 1953 fails = 1802 % -d: 153 time < 0.01 sec inferences = 1977 fails = 1825 % -d: 154 time = 0.01 sec inferences = 1979 fails = 1826 % -d: 155 time = 0.02 sec inferences = 2003 fails = 1849 % -d: 156 time < 0.01 sec inferences = 2005 fails = 1850 % -d: 157 time < 0.01 sec inferences = 2029 fails = 1873 % -d: 158 time < 0.01 sec inferences = 2031 fails = 1874 % -d: 159 time = 0.02 sec inferences = 2055 fails = 1897 % -d: 160 time = 0.01 sec inferences = 2057 fails = 1898 % -d: 161 time < 0.01 sec inferences = 2081 fails = 1921 % -d: 162 time = 0.02 sec inferences = 2083 fails = 1922 % -d: 163 time < 0.01 sec inferences = 2107 fails = 1945 % -d: 164 time = 0.01 sec inferences = 2109 fails = 1946 % -d: 165 time = 0.02 sec inferences = 2133 fails = 1969 % -d: 166 time < 0.01 sec inferences = 2135 fails = 1970 % -d: 167 time < 0.01 sec inferences = 2159 fails = 1993 % -d: 168 time = 0.02 sec inferences = 2161 fails = 1994 % -d: 169 time = 0.01 sec inferences = 2185 fails = 2017 % -d: 170 time = 0.02 sec inferences = 2187 fails = 2018 % -d: 171 time < 0.01 sec inferences = 2211 fails = 2041 % -d: 172 time = 0.02 sec inferences = 2213 fails = 2042 % -d: 173 time = 0.01 sec inferences = 2237 fails = 2065 % -d: 174 time = 0.02 sec inferences = 2239 fails = 2066 % -d: 175 time < 0.01 sec inferences = 2263 fails = 2089 % -d: 176 time = 0.02 sec inferences = 2265 fails = 2090 % -d: 177 time = 0.01 sec inferences = 2289 fails = 2113 % -d: 178 time = 0.02 sec inferences = 2291 fails = 2114 % -d: 179 time < 0.01 sec inferences = 2315 fails = 2137 % -d: 180 time = 0.02 sec inferences = 2317 fails = 2138 % -d: 181 time = 0.02 sec inferences = 2341 fails = 2161 % -d: 182 time = 0.01 sec inferences = 2343 fails = 2162 % -d: 183 time = 0.02 sec inferences = 2367 fails = 2185 % -d: 184 time = 0.02 sec inferences = 2369 fails = 2186 % -d: 185 time < 0.01 sec inferences = 2393 fails = 2209 % -d: 186 time = 0.02 sec inferences = 2395 fails = 2210 % -d: 187 time = 0.02 sec inferences = 2419 fails = 2233 % -d: 188 time = 0.02 sec inferences = 2421 fails = 2234 % -d: 189 time = 0.01 sec inferences = 2445 fails = 2257 % -d: 190 time = 0.02 sec inferences = 2447 fails = 2258 % -d: 191 time = 0.02 sec inferences = 2471 fails = 2281 % -d: 192 time = 0.02 sec inferences = 2473 fails = 2282 % -d: 193 time = 0.02 sec inferences = 2497 fails = 2305 % -d: 194 time < 0.01 sec inferences = 2499 fails = 2306 % -d: 195 time = 0.02 sec inferences = 2523 fails = 2329 % -d: 196 time = 0.02 sec inferences = 2525 fails = 2330 % -d: 197 time = 0.02 sec inferences = 2549 fails = 2353 % -d: 198 time = 0.02 sec inferences = 2551 fails = 2354 % -d: 199 time = 0.02 sec inferences = 2575 fails = 2377 % -d: 200 time = 0.02 sec inferences = 2577 fails = 2378 % -d: 201 time = 0.02 sec inferences = 2601 fails = 2401 % -d: 202 time = 0.02 sec inferences = 2603 fails = 2402 % -d: 203 time = 0.02 sec inferences = 2627 fails = 2425 % -d: 204 time = 0.02 sec inferences = 2629 fails = 2426 % -d: 205 time = 0.02 sec inferences = 2653 fails = 2449 % -d: 206 time = 0.02 sec inferences = 2655 fails = 2450 % -d: 207 time = 0.02 sec inferences = 2679 fails = 2473 % -d: 208 time = 0.02 sec inferences = 2681 fails = 2474 % -d: 209 time = 0.02 sec inferences = 2705 fails = 2497 % -d: 210 time = 0.03 sec inferences = 2707 fails = 2498 % -d: 211 time = 0.02 sec inferences = 2731 fails = 2521 % -d: 212 time = 0.02 sec inferences = 2733 fails = 2522 % -d: 213 time = 0.02 sec inferences = 2757 fails = 2545 % -d: 214 time = 0.02 sec inferences = 2759 fails = 2546 % -d: 215 time = 0.03 sec inferences = 2783 fails = 2569 % -d: 216 time = 0.02 sec inferences = 2785 fails = 2570 % -d: 217 time = 0.02 sec inferences = 2809 fails = 2593 % -d: 218 time = 0.03 sec inferences = 2811 fails = 2594 % -d: 219 time = 0.02 sec inferences = 2835 fails = 2617 % -d: 220 time = 0.02 sec inferences = 2837 fails = 2618 % -d: 221 time = 0.03 sec inferences = 2861 fails = 2641 % -d: 222 time = 0.02 sec inferences = 2863 fails = 2642 % -d: 223 time = 0.02 sec inferences = 2887 fails = 2665 % -d: 224 time = 0.03 sec inferences = 2889 fails = 2666 % -d: 225 time = 0.02 sec inferences = 2913 fails = 2689 % -d: 226 time = 0.03 sec inferences = 2915 fails = 2690 % -d: 227 time = 0.02 sec inferences = 2939 fails = 2713 % -d: 228 time = 0.03 sec inferences = 2941 fails = 2714 % -d: 229 time = 0.02 sec inferences = 2965 fails = 2737 % -d: 230 time = 0.03 sec inferences = 2967 fails = 2738 % -d: 231 time = 0.02 sec inferences = 2991 fails = 2761 % -d: 232 time = 0.03 sec inferences = 2993 fails = 2762 % -d: 233 time = 0.03 sec inferences = 3017 fails = 2785 % -d: 234 time = 0.02 sec inferences = 3019 fails = 2786 % -d: 235 time = 0.03 sec inferences = 3043 fails = 2809 % -d: 236 time = 0.03 sec inferences = 3045 fails = 2810 % -d: 237 time = 0.02 sec inferences = 3069 fails = 2833 % -d: 238 time = 0.03 sec inferences = 3071 fails = 2834 % -d: 239 time = 0.03 sec inferences = 3095 fails = 2857 % -d: 240 time = 0.03 sec inferences = 3097 fails = 2858 % -d: 241 time = 0.02 sec inferences = 3121 fails = 2881 % -d: 242 time = 0.03 sec inferences = 3123 fails = 2882 % -d: 243 time = 0.03 sec inferences = 3147 fails = 2905 % -d: 244 time = 0.03 sec inferences = 3149 fails = 2906 % -d: 245 time = 0.03 sec inferences = 3173 fails = 2929 % -d: 246 time = 0.03 sec inferences = 3175 fails = 2930 % -d: 247 time = 0.03 sec inferences = 3199 fails = 2953 % -d: 248 time = 0.03 sec inferences = 3201 fails = 2954 % -d: 249 time = 0.03 sec inferences = 3225 fails = 2977 % -d: 250 time = 0.03 sec inferences = 3227 fails = 2978 % -d: 251 time = 0.03 sec inferences = 3251 fails = 3001 % -d: 252 time = 0.03 sec inferences = 3253 fails = 3002 % -d: 253 time = 0.03 sec inferences = 3277 fails = 3025 % -d: 254 time = 0.03 sec inferences = 3279 fails = 3026 % -d: 255 time = 0.03 sec inferences = 3303 fails = 3049 % -d: 256 time = 0.03 sec inferences = 3305 fails = 3050 % -d: 257 time = 0.04 sec inferences = 3329 fails = 3073 % -d: 258 time = 0.03 sec inferences = 3331 fails = 3074 % -d: 259 time = 0.03 sec inferences = 3355 fails = 3097 % -d: 260 time = 0.03 sec inferences = 3357 fails = 3098 % -d: 261 time = 0.04 sec inferences = 3381 fails = 3121 % -d: 262 time = 0.03 sec inferences = 3383 fails = 3122 % -d: 263 time = 0.03 sec inferences = 3407 fails = 3145 % -d: 264 time = 0.04 sec inferences = 3409 fails = 3146 % -d: 265 time = 0.03 sec inferences = 3433 fails = 3169 % -d: 266 time = 0.03 sec inferences = 3435 fails = 3170 % -d: 267 time = 0.04 sec inferences = 3459 fails = 3193 % -d: 268 time = 0.03 sec inferences = 3461 fails = 3194 % -d: 269 time = 0.04 sec inferences = 3485 fails = 3217 % -d: 270 time = 0.03 sec inferences = 3487 fails = 3218 % -d: 271 time = 0.04 sec inferences = 3511 fails = 3241 % -d: 272 time = 0.03 sec inferences = 3513 fails = 3242 % -d: 273 time = 0.04 sec inferences = 3537 fails = 3265 % -d: 274 time = 0.03 sec inferences = 3539 fails = 3266 % -d: 275 time = 0.04 sec inferences = 3563 fails = 3289 % -d: 276 time = 0.04 sec inferences = 3565 fails = 3290 % -d: 277 time = 0.03 sec inferences = 3589 fails = 3313 % -d: 278 time = 0.04 sec inferences = 3591 fails = 3314 % -d: 279 time = 0.04 sec inferences = 3615 fails = 3337 % -d: 280 time = 0.03 sec inferences = 3617 fails = 3338 % -d: 281 time = 0.04 sec inferences = 3641 fails = 3361 % -d: 282 time = 0.04 sec inferences = 3643 fails = 3362 % -d: 283 time = 0.04 sec inferences = 3667 fails = 3385 % -d: 284 time = 0.04 sec inferences = 3669 fails = 3386 % -d: 285 time = 0.04 sec inferences = 3693 fails = 3409 % -d: 286 time = 0.03 sec inferences = 3695 fails = 3410 % -d: 287 time = 0.04 sec inferences = 3719 fails = 3433 % -d: 288 time = 0.04 sec inferences = 3721 fails = 3434 % -d: 289 time = 0.04 sec inferences = 3745 fails = 3457 % -d: 290 time = 0.04 sec inferences = 3747 fails = 3458 % -d: 291 time = 0.04 sec inferences = 3771 fails = 3481 % -d: 292 time = 0.04 sec inferences = 3773 fails = 3482 % -d: 293 time = 0.04 sec inferences = 3797 fails = 3505 % -d: 294 time = 0.04 sec inferences = 3799 fails = 3506 % -d: 295 time = 0.04 sec inferences = 3823 fails = 3529 % -d: 296 time = 0.05 sec inferences = 3825 fails = 3530 % -d: 297 time = 0.04 sec inferences = 3849 fails = 3553 % -d: 298 time = 0.04 sec inferences = 3851 fails = 3554 % -d: 299 time = 0.04 sec inferences = 3875 fails = 3577 % -d: 300 time = 0.04 sec inferences = 3877 fails = 3578 % -d: 301 time = 0.05 sec inferences = 3901 fails = 3601 % -d: 302 time = 0.04 sec inferences = 3903 fails = 3602 % -d: 303 time = 0.04 sec inferences = 3927 fails = 3625 % -d: 304 time = 0.05 sec inferences = 3929 fails = 3626 % -d: 305 time = 0.04 sec inferences = 3953 fails = 3649 % -d: 306 time = 0.05 sec inferences = 3955 fails = 3650 % -d: 307 time = 0.04 sec inferences = 3979 fails = 3673 % -d: 308 time = 0.04 sec inferences = 3981 fails = 3674 % -d: 309 time = 0.05 sec inferences = 4005 fails = 3697 % -d: 310 time = 0.05 sec inferences = 4007 fails = 3698 % -d: 311 time = 0.04 sec inferences = 4031 fails = 3721 % -d: 312 time = 0.05 sec inferences = 4033 fails = 3722 % -d: 313 time = 0.04 sec inferences = 4057 fails = 3745 % -d: 314 time = 0.05 sec inferences = 4059 fails = 3746 % -d: 315 time = 0.05 sec inferences = 4083 fails = 3769 % -d: 316 time = 0.04 sec inferences = 4085 fails = 3770 % -d: 317 time = 0.05 sec inferences = 4109 fails = 3793 % -d: 318 time = 0.05 sec inferences = 4111 fails = 3794 % -d: 319 time = 0.05 sec inferences = 4135 fails = 3817 % -d: 320 time = 0.04 sec inferences = 4137 fails = 3818 % -d: 321 time = 0.05 sec inferences = 4161 fails = 3841 % -d: 322 time = 0.05 sec inferences = 4163 fails = 3842 % -d: 323 time = 0.05 sec inferences = 4187 fails = 3865 % -d: 324 time = 0.05 sec inferences = 4189 fails = 3866 % -d: 325 time = 0.05 sec inferences = 4213 fails = 3889 % -d: 326 time = 0.05 sec inferences = 4215 fails = 3890 % -d: 327 time = 0.05 sec inferences = 4239 fails = 3913 % -d: 328 time = 0.05 sec inferences = 4241 fails = 3914 % -d: 329 time = 0.05 sec inferences = 4265 fails = 3937 % -d: 330 time = 0.05 sec inferences = 4267 fails = 3938 % -d: 331 time = 0.05 sec inferences = 4291 fails = 3961 % -d: 332 time = 0.05 sec inferences = 4293 fails = 3962 % -d: 333 time = 0.05 sec inferences = 4317 fails = 3985 % -d: 334 time = 0.06 sec inferences = 4319 fails = 3986 % -d: 335 time = 0.05 sec inferences = 4343 fails = 4009 % -d: 336 time = 0.05 sec inferences = 4345 fails = 4010 % -d: 337 time = 0.05 sec inferences = 4369 fails = 4033 % -d: 338 time = 0.06 sec inferences = 4371 fails = 4034 % -d: 339 time = 0.05 sec inferences = 4395 fails = 4057 % -d: 340 time = 0.05 sec inferences = 4397 fails = 4058 % -d: 341 time = 0.06 sec inferences = 4421 fails = 4081 % -d: 342 time = 0.05 sec inferences = 4423 fails = 4082 % -d: 343 time = 0.06 sec inferences = 4447 fails = 4105 % -d: 344 time = 0.05 sec inferences = 4449 fails = 4106 % -d: 345 SETHEO ERROR: stack overflow % time = 0.04 sec inferences = 685 fails = 340 % ******** INTERRUPT FAILURE ************ % Intermediate free variables : 0 % Intermediate inferences : 345 % Intermediate open subgoals : 1 % Generated antilemmata : 0 % Number of unifications : 766084 % - E/R/F/L : 766084/ 0/ 0/ 0 % Number of fails : 706743 % - unification : 706400 % - depth bound : 343 % Instructions executed : 11317177 % Abstract machine time (seconds) : 6.61 % Overall time (seconds) : 6.61 % Cleaning up before exit % Delete /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq.hex /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq.log /tmp/SystemOnTPTP2801/MSC/MSC015-1.025+noeq.tree % That's all folks % WARNING: TreeLimitedRun lost 5.86s, total lost is 5.86s % Killed 1 orphans % %------------------------------------------------------------------------------