%------------------------------------------------------------------------------ % File : SETHEO---3.3 % Problem : MSC015-1.015 : TPTP v5.0.0. Released v3.5.0. % Transfm : add_equality % Format : setheo % Command : setheo-wrapper %s % Computer : art06.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:26 EST 2010 % Result : GaveUp 3.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/SystemOnTPTP7177/MSC MSC015-1.015+noeq /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+noeq % MUST DELETE /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+noeq.hex % MUST DELETE /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+noeq.log % MUST DELETE /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+noeq.tree % codegen: 147 [199999] labels, 0 colls [390 accesses] % Assembler optimization: 66 labels read, 24 labels output % /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+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/SystemOnTPTP7177/MSC/MSC015-1.015+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:26 2010 % Options : -dr -cons -dynsgreord 2 /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+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 = 17 fails = 15 % -d: 4 time < 0.01 sec inferences = 19 fails = 16 % -d: 5 time < 0.01 sec inferences = 33 fails = 29 % -d: 6 time < 0.01 sec inferences = 35 fails = 30 % -d: 7 time < 0.01 sec inferences = 49 fails = 43 % -d: 8 time < 0.01 sec inferences = 51 fails = 44 % -d: 9 time < 0.01 sec inferences = 65 fails = 57 % -d: 10 time < 0.01 sec inferences = 67 fails = 58 % -d: 11 time < 0.01 sec inferences = 81 fails = 71 % -d: 12 time < 0.01 sec inferences = 83 fails = 72 % -d: 13 time < 0.01 sec inferences = 97 fails = 85 % -d: 14 time < 0.01 sec inferences = 99 fails = 86 % -d: 15 time < 0.01 sec inferences = 113 fails = 99 % -d: 16 time < 0.01 sec inferences = 115 fails = 100 % -d: 17 time < 0.01 sec inferences = 129 fails = 113 % -d: 18 time < 0.01 sec inferences = 131 fails = 114 % -d: 19 time < 0.01 sec inferences = 145 fails = 127 % -d: 20 time < 0.01 sec inferences = 147 fails = 128 % -d: 21 time < 0.01 sec inferences = 161 fails = 141 % -d: 22 time < 0.01 sec inferences = 163 fails = 142 % -d: 23 time < 0.01 sec inferences = 177 fails = 155 % -d: 24 time < 0.01 sec inferences = 179 fails = 156 % -d: 25 time < 0.01 sec inferences = 193 fails = 169 % -d: 26 time < 0.01 sec inferences = 195 fails = 170 % -d: 27 time < 0.01 sec inferences = 209 fails = 183 % -d: 28 time < 0.01 sec inferences = 211 fails = 184 % -d: 29 time < 0.01 sec inferences = 225 fails = 197 % -d: 30 time < 0.01 sec inferences = 227 fails = 198 % -d: 31 time < 0.01 sec inferences = 241 fails = 211 % -d: 32 time < 0.01 sec inferences = 243 fails = 212 % -d: 33 time < 0.01 sec inferences = 257 fails = 225 % -d: 34 time < 0.01 sec inferences = 259 fails = 226 % -d: 35 time < 0.01 sec inferences = 273 fails = 239 % -d: 36 time < 0.01 sec inferences = 275 fails = 240 % -d: 37 time < 0.01 sec inferences = 289 fails = 253 % -d: 38 time < 0.01 sec inferences = 291 fails = 254 % -d: 39 time < 0.01 sec inferences = 305 fails = 267 % -d: 40 time < 0.01 sec inferences = 307 fails = 268 % -d: 41 time < 0.01 sec inferences = 321 fails = 281 % -d: 42 time < 0.01 sec inferences = 323 fails = 282 % -d: 43 time < 0.01 sec inferences = 337 fails = 295 % -d: 44 time < 0.01 sec inferences = 339 fails = 296 % -d: 45 time < 0.01 sec inferences = 353 fails = 309 % -d: 46 time < 0.01 sec inferences = 355 fails = 310 % -d: 47 time < 0.01 sec inferences = 369 fails = 323 % -d: 48 time < 0.01 sec inferences = 371 fails = 324 % -d: 49 time < 0.01 sec inferences = 385 fails = 337 % -d: 50 time < 0.01 sec inferences = 387 fails = 338 % -d: 51 time < 0.01 sec inferences = 401 fails = 351 % -d: 52 time < 0.01 sec inferences = 403 fails = 352 % -d: 53 time < 0.01 sec inferences = 417 fails = 365 % -d: 54 time < 0.01 sec inferences = 419 fails = 366 % -d: 55 time = 0.01 sec inferences = 433 fails = 379 % -d: 56 time < 0.01 sec inferences = 435 fails = 380 % -d: 57 time < 0.01 sec inferences = 449 fails = 393 % -d: 58 time < 0.01 sec inferences = 451 fails = 394 % -d: 59 time < 0.01 sec inferences = 465 fails = 407 % -d: 60 time < 0.01 sec inferences = 467 fails = 408 % -d: 61 time < 0.01 sec inferences = 481 fails = 421 % -d: 62 time < 0.01 sec inferences = 483 fails = 422 % -d: 63 time = 0.01 sec inferences = 497 fails = 435 % -d: 64 time < 0.01 sec inferences = 499 fails = 436 % -d: 65 time < 0.01 sec inferences = 513 fails = 449 % -d: 66 time < 0.01 sec inferences = 515 fails = 450 % -d: 67 time < 0.01 sec inferences = 529 fails = 463 % -d: 68 time < 0.01 sec inferences = 531 fails = 464 % -d: 69 time < 0.01 sec inferences = 545 fails = 477 % -d: 70 time = 0.01 sec inferences = 547 fails = 478 % -d: 71 time < 0.01 sec inferences = 561 fails = 491 % -d: 72 time < 0.01 sec inferences = 563 fails = 492 % -d: 73 time < 0.01 sec inferences = 577 fails = 505 % -d: 74 time < 0.01 sec inferences = 579 fails = 506 % -d: 75 time < 0.01 sec inferences = 593 fails = 519 % -d: 76 time < 0.01 sec inferences = 595 fails = 520 % -d: 77 time = 0.01 sec inferences = 609 fails = 533 % -d: 78 time < 0.01 sec inferences = 611 fails = 534 % -d: 79 time < 0.01 sec inferences = 625 fails = 547 % -d: 80 time < 0.01 sec inferences = 627 fails = 548 % -d: 81 time < 0.01 sec inferences = 641 fails = 561 % -d: 82 time < 0.01 sec inferences = 643 fails = 562 % -d: 83 time < 0.01 sec inferences = 657 fails = 575 % -d: 84 time < 0.01 sec inferences = 659 fails = 576 % -d: 85 time < 0.01 sec inferences = 673 fails = 589 % -d: 86 time < 0.01 sec inferences = 675 fails = 590 % -d: 87 time = 0.01 sec inferences = 689 fails = 603 % -d: 88 time < 0.01 sec inferences = 691 fails = 604 % -d: 89 time < 0.01 sec inferences = 705 fails = 617 % -d: 90 time < 0.01 sec inferences = 707 fails = 618 % -d: 91 time < 0.01 sec inferences = 721 fails = 631 % -d: 92 time < 0.01 sec inferences = 723 fails = 632 % -d: 93 time < 0.01 sec inferences = 737 fails = 645 % -d: 94 time < 0.01 sec inferences = 739 fails = 646 % -d: 95 time < 0.01 sec inferences = 753 fails = 659 % -d: 96 time = 0.01 sec inferences = 755 fails = 660 % -d: 97 time < 0.01 sec inferences = 769 fails = 673 % -d: 98 time < 0.01 sec inferences = 771 fails = 674 % -d: 99 time < 0.01 sec inferences = 785 fails = 687 % -d: 100 time < 0.01 sec inferences = 787 fails = 688 % -d: 101 time < 0.01 sec inferences = 801 fails = 701 % -d: 102 time < 0.01 sec inferences = 803 fails = 702 % -d: 103 time < 0.01 sec inferences = 817 fails = 715 % -d: 104 time < 0.01 sec inferences = 819 fails = 716 % -d: 105 time < 0.01 sec inferences = 833 fails = 729 % -d: 106 time = 0.01 sec inferences = 835 fails = 730 % -d: 107 time < 0.01 sec inferences = 849 fails = 743 % -d: 108 time < 0.01 sec inferences = 851 fails = 744 % -d: 109 time < 0.01 sec inferences = 865 fails = 757 % -d: 110 time = 0.01 sec inferences = 867 fails = 758 % -d: 111 time < 0.01 sec inferences = 881 fails = 771 % -d: 112 time = 0.01 sec inferences = 883 fails = 772 % -d: 113 time < 0.01 sec inferences = 897 fails = 785 % -d: 114 time < 0.01 sec inferences = 899 fails = 786 % -d: 115 time < 0.01 sec inferences = 913 fails = 799 % -d: 116 time < 0.01 sec inferences = 915 fails = 800 % -d: 117 time < 0.01 sec inferences = 929 fails = 813 % -d: 118 time < 0.01 sec inferences = 931 fails = 814 % -d: 119 time < 0.01 sec inferences = 945 fails = 827 % -d: 120 time < 0.01 sec inferences = 947 fails = 828 % -d: 121 time = 0.01 sec inferences = 961 fails = 841 % -d: 122 time < 0.01 sec inferences = 963 fails = 842 % -d: 123 time < 0.01 sec inferences = 977 fails = 855 % -d: 124 time < 0.01 sec inferences = 979 fails = 856 % -d: 125 time < 0.01 sec inferences = 993 fails = 869 % -d: 126 time < 0.01 sec inferences = 995 fails = 870 % -d: 127 time = 0.01 sec inferences = 1009 fails = 883 % -d: 128 time < 0.01 sec inferences = 1011 fails = 884 % -d: 129 time < 0.01 sec inferences = 1025 fails = 897 % -d: 130 time < 0.01 sec inferences = 1027 fails = 898 % -d: 131 time < 0.01 sec inferences = 1041 fails = 911 % -d: 132 time = 0.01 sec inferences = 1043 fails = 912 % -d: 133 time < 0.01 sec inferences = 1057 fails = 925 % -d: 134 time = 0.01 sec inferences = 1059 fails = 926 % -d: 135 time < 0.01 sec inferences = 1073 fails = 939 % -d: 136 time < 0.01 sec inferences = 1075 fails = 940 % -d: 137 time = 0.01 sec inferences = 1089 fails = 953 % -d: 138 time < 0.01 sec inferences = 1091 fails = 954 % -d: 139 time < 0.01 sec inferences = 1105 fails = 967 % -d: 140 time < 0.01 sec inferences = 1107 fails = 968 % -d: 141 time = 0.01 sec inferences = 1121 fails = 981 % -d: 142 time < 0.01 sec inferences = 1123 fails = 982 % -d: 143 time < 0.01 sec inferences = 1137 fails = 995 % -d: 144 time < 0.01 sec inferences = 1139 fails = 996 % -d: 145 time < 0.01 sec inferences = 1153 fails = 1009 % -d: 146 time = 0.01 sec inferences = 1155 fails = 1010 % -d: 147 time < 0.01 sec inferences = 1169 fails = 1023 % -d: 148 time < 0.01 sec inferences = 1171 fails = 1024 % -d: 149 time < 0.01 sec inferences = 1185 fails = 1037 % -d: 150 time < 0.01 sec inferences = 1187 fails = 1038 % -d: 151 time = 0.01 sec inferences = 1201 fails = 1051 % -d: 152 time < 0.01 sec inferences = 1203 fails = 1052 % -d: 153 time < 0.01 sec inferences = 1217 fails = 1065 % -d: 154 time < 0.01 sec inferences = 1219 fails = 1066 % -d: 155 time < 0.01 sec inferences = 1233 fails = 1079 % -d: 156 time = 0.01 sec inferences = 1235 fails = 1080 % -d: 157 time < 0.01 sec inferences = 1249 fails = 1093 % -d: 158 time < 0.01 sec inferences = 1251 fails = 1094 % -d: 159 time < 0.01 sec inferences = 1265 fails = 1107 % -d: 160 time = 0.01 sec inferences = 1267 fails = 1108 % -d: 161 time < 0.01 sec inferences = 1281 fails = 1121 % -d: 162 time = 0.01 sec inferences = 1283 fails = 1122 % -d: 163 time < 0.01 sec inferences = 1297 fails = 1135 % -d: 164 time = 0.01 sec inferences = 1299 fails = 1136 % -d: 165 time < 0.01 sec inferences = 1313 fails = 1149 % -d: 166 time = 0.01 sec inferences = 1315 fails = 1150 % -d: 167 time < 0.01 sec inferences = 1329 fails = 1163 % -d: 168 time = 0.01 sec inferences = 1331 fails = 1164 % -d: 169 time < 0.01 sec inferences = 1345 fails = 1177 % -d: 170 time = 0.01 sec inferences = 1347 fails = 1178 % -d: 171 time < 0.01 sec inferences = 1361 fails = 1191 % -d: 172 time = 0.01 sec inferences = 1363 fails = 1192 % -d: 173 time = 0.01 sec inferences = 1377 fails = 1205 % -d: 174 time < 0.01 sec inferences = 1379 fails = 1206 % -d: 175 time < 0.01 sec inferences = 1393 fails = 1219 % -d: 176 time < 0.01 sec inferences = 1395 fails = 1220 % -d: 177 time = 0.01 sec inferences = 1409 fails = 1233 % -d: 178 time = 0.01 sec inferences = 1411 fails = 1234 % -d: 179 time = 0.01 sec inferences = 1425 fails = 1247 % -d: 180 time < 0.01 sec inferences = 1427 fails = 1248 % -d: 181 time < 0.01 sec inferences = 1441 fails = 1261 % -d: 182 time < 0.01 sec inferences = 1443 fails = 1262 % -d: 183 time < 0.01 sec inferences = 1457 fails = 1275 % -d: 184 time = 0.01 sec inferences = 1459 fails = 1276 % -d: 185 time = 0.01 sec inferences = 1473 fails = 1289 % -d: 186 time = 0.01 sec inferences = 1475 fails = 1290 % -d: 187 time < 0.01 sec inferences = 1489 fails = 1303 % -d: 188 time < 0.01 sec inferences = 1491 fails = 1304 % -d: 189 time < 0.01 sec inferences = 1505 fails = 1317 % -d: 190 time = 0.01 sec inferences = 1507 fails = 1318 % -d: 191 time = 0.01 sec inferences = 1521 fails = 1331 % -d: 192 time = 0.01 sec inferences = 1523 fails = 1332 % -d: 193 time < 0.01 sec inferences = 1537 fails = 1345 % -d: 194 time < 0.01 sec inferences = 1539 fails = 1346 % -d: 195 time < 0.01 sec inferences = 1553 fails = 1359 % -d: 196 time = 0.01 sec inferences = 1555 fails = 1360 % -d: 197 time = 0.01 sec inferences = 1569 fails = 1373 % -d: 198 time = 0.01 sec inferences = 1571 fails = 1374 % -d: 199 time < 0.01 sec inferences = 1585 fails = 1387 % -d: 200 time < 0.01 sec inferences = 1587 fails = 1388 % -d: 201 time = 0.02 sec inferences = 1601 fails = 1401 % -d: 202 time = 0.01 sec inferences = 1603 fails = 1402 % -d: 203 time = 0.01 sec inferences = 1617 fails = 1415 % -d: 204 time = 0.01 sec inferences = 1619 fails = 1416 % -d: 205 time < 0.01 sec inferences = 1633 fails = 1429 % -d: 206 time < 0.01 sec inferences = 1635 fails = 1430 % -d: 207 time < 0.01 sec inferences = 1649 fails = 1443 % -d: 208 time = 0.01 sec inferences = 1651 fails = 1444 % -d: 209 time = 0.02 sec inferences = 1665 fails = 1457 % -d: 210 time < 0.01 sec inferences = 1667 fails = 1458 % -d: 211 time < 0.01 sec inferences = 1681 fails = 1471 % -d: 212 time < 0.01 sec inferences = 1683 fails = 1472 % -d: 213 time = 0.01 sec inferences = 1697 fails = 1485 % -d: 214 time = 0.02 sec inferences = 1699 fails = 1486 % -d: 215 time < 0.01 sec inferences = 1713 fails = 1499 % -d: 216 time < 0.01 sec inferences = 1715 fails = 1500 % -d: 217 time < 0.01 sec inferences = 1729 fails = 1513 % -d: 218 time = 0.02 sec inferences = 1731 fails = 1514 % -d: 219 time = 0.01 sec inferences = 1745 fails = 1527 % -d: 220 time < 0.01 sec inferences = 1747 fails = 1528 % -d: 221 time = 0.02 sec inferences = 1761 fails = 1541 % -d: 222 time < 0.01 sec inferences = 1763 fails = 1542 % -d: 223 time = 0.01 sec inferences = 1777 fails = 1555 % -d: 224 time = 0.02 sec inferences = 1779 fails = 1556 % -d: 225 time = 0.01 sec inferences = 1793 fails = 1569 % -d: 226 time = 0.01 sec inferences = 1795 fails = 1570 % -d: 227 time = 0.02 sec inferences = 1809 fails = 1583 % -d: 228 time < 0.01 sec inferences = 1811 fails = 1584 % -d: 229 time = 0.02 sec inferences = 1825 fails = 1597 % -d: 230 time < 0.01 sec inferences = 1827 fails = 1598 % -d: 231 time < 0.01 sec inferences = 1841 fails = 1611 % -d: 232 time = 0.02 sec inferences = 1843 fails = 1612 % -d: 233 time = 0.01 sec inferences = 1857 fails = 1625 % -d: 234 time = 0.02 sec inferences = 1859 fails = 1626 % -d: 235 time = 0.01 sec inferences = 1873 fails = 1639 % -d: 236 time = 0.02 sec inferences = 1875 fails = 1640 % -d: 237 time < 0.01 sec inferences = 1889 fails = 1653 % -d: 238 time = 0.02 sec inferences = 1891 fails = 1654 % -d: 239 time < 0.01 sec inferences = 1905 fails = 1667 % -d: 240 time = 0.02 sec inferences = 1907 fails = 1668 % -d: 241 time = 0.01 sec inferences = 1921 fails = 1681 % -d: 242 time = 0.02 sec inferences = 1923 fails = 1682 % -d: 243 time = 0.02 sec inferences = 1937 fails = 1695 % -d: 244 time < 0.01 sec inferences = 1939 fails = 1696 % -d: 245 time = 0.02 sec inferences = 1953 fails = 1709 % -d: 246 time < 0.01 sec inferences = 1955 fails = 1710 % -d: 247 time = 0.02 sec inferences = 1969 fails = 1723 % -d: 248 time = 0.02 sec inferences = 1971 fails = 1724 % -d: 249 time = 0.01 sec inferences = 1985 fails = 1737 % -d: 250 time = 0.02 sec inferences = 1987 fails = 1738 % -d: 251 time = 0.02 sec inferences = 2001 fails = 1751 % -d: 252 time < 0.01 sec inferences = 2003 fails = 1752 % -d: 253 time = 0.02 sec inferences = 2017 fails = 1765 % -d: 254 time = 0.02 sec inferences = 2019 fails = 1766 % -d: 255 time = 0.02 sec inferences = 2033 fails = 1779 % -d: 256 time = 0.01 sec inferences = 2035 fails = 1780 % -d: 257 time = 0.02 sec inferences = 2049 fails = 1793 % -d: 258 time = 0.02 sec inferences = 2051 fails = 1794 % -d: 259 time = 0.02 sec inferences = 2065 fails = 1807 % -d: 260 time < 0.01 sec inferences = 2067 fails = 1808 % -d: 261 time = 0.02 sec inferences = 2081 fails = 1821 % -d: 262 time = 0.02 sec inferences = 2083 fails = 1822 % -d: 263 time = 0.02 sec inferences = 2097 fails = 1835 % -d: 264 time = 0.02 sec inferences = 2099 fails = 1836 % -d: 265 time = 0.01 sec inferences = 2113 fails = 1849 % -d: 266 time = 0.02 sec inferences = 2115 fails = 1850 % -d: 267 time = 0.02 sec inferences = 2129 fails = 1863 % -d: 268 time = 0.02 sec inferences = 2131 fails = 1864 % -d: 269 time = 0.02 sec inferences = 2145 fails = 1877 % -d: 270 time = 0.02 sec inferences = 2147 fails = 1878 % -d: 271 time = 0.02 sec inferences = 2161 fails = 1891 % -d: 272 time = 0.02 sec inferences = 2163 fails = 1892 % -d: 273 time = 0.02 sec inferences = 2177 fails = 1905 % -d: 274 time = 0.02 sec inferences = 2179 fails = 1906 % -d: 275 time = 0.02 sec inferences = 2193 fails = 1919 % -d: 276 time = 0.02 sec inferences = 2195 fails = 1920 % -d: 277 time = 0.02 sec inferences = 2209 fails = 1933 % -d: 278 time = 0.02 sec inferences = 2211 fails = 1934 % -d: 279 time = 0.02 sec inferences = 2225 fails = 1947 % -d: 280 time = 0.02 sec inferences = 2227 fails = 1948 % -d: 281 time = 0.02 sec inferences = 2241 fails = 1961 % -d: 282 time = 0.02 sec inferences = 2243 fails = 1962 % -d: 283 time = 0.02 sec inferences = 2257 fails = 1975 % -d: 284 time = 0.02 sec inferences = 2259 fails = 1976 % -d: 285 time = 0.02 sec inferences = 2273 fails = 1989 % -d: 286 time = 0.02 sec inferences = 2275 fails = 1990 % -d: 287 time = 0.03 sec inferences = 2289 fails = 2003 % -d: 288 time = 0.02 sec inferences = 2291 fails = 2004 % -d: 289 time = 0.02 sec inferences = 2305 fails = 2017 % -d: 290 time = 0.02 sec inferences = 2307 fails = 2018 % -d: 291 time = 0.02 sec inferences = 2321 fails = 2031 % -d: 292 time = 0.02 sec inferences = 2323 fails = 2032 % -d: 293 time = 0.03 sec inferences = 2337 fails = 2045 % -d: 294 time = 0.02 sec inferences = 2339 fails = 2046 % -d: 295 time = 0.02 sec inferences = 2353 fails = 2059 % -d: 296 time = 0.02 sec inferences = 2355 fails = 2060 % -d: 297 time = 0.03 sec inferences = 2369 fails = 2073 % -d: 298 time = 0.02 sec inferences = 2371 fails = 2074 % -d: 299 time = 0.02 sec inferences = 2385 fails = 2087 % -d: 300 time = 0.03 sec inferences = 2387 fails = 2088 % -d: 301 time = 0.02 sec inferences = 2401 fails = 2101 % -d: 302 time = 0.02 sec inferences = 2403 fails = 2102 % -d: 303 time = 0.03 sec inferences = 2417 fails = 2115 % -d: 304 time = 0.02 sec inferences = 2419 fails = 2116 % -d: 305 time = 0.03 sec inferences = 2433 fails = 2129 % -d: 306 time = 0.02 sec inferences = 2435 fails = 2130 % -d: 307 time = 0.03 sec inferences = 2449 fails = 2143 % -d: 308 time = 0.02 sec inferences = 2451 fails = 2144 % -d: 309 time = 0.02 sec inferences = 2465 fails = 2157 % -d: 310 time = 0.03 sec inferences = 2467 fails = 2158 % -d: 311 time = 0.02 sec inferences = 2481 fails = 2171 % -d: 312 time = 0.03 sec inferences = 2483 fails = 2172 % -d: 313 time = 0.02 sec inferences = 2497 fails = 2185 % -d: 314 time = 0.03 sec inferences = 2499 fails = 2186 % -d: 315 time = 0.02 sec inferences = 2513 fails = 2199 % -d: 316 time = 0.03 sec inferences = 2515 fails = 2200 % -d: 317 time = 0.03 sec inferences = 2529 fails = 2213 % -d: 318 time = 0.02 sec inferences = 2531 fails = 2214 % -d: 319 time = 0.03 sec inferences = 2545 fails = 2227 % -d: 320 time = 0.02 sec inferences = 2547 fails = 2228 % -d: 321 time = 0.03 sec inferences = 2561 fails = 2241 % -d: 322 time = 0.03 sec inferences = 2563 fails = 2242 % -d: 323 time = 0.02 sec inferences = 2577 fails = 2255 % -d: 324 time = 0.03 sec inferences = 2579 fails = 2256 % -d: 325 time = 0.03 sec inferences = 2593 fails = 2269 % -d: 326 time = 0.02 sec inferences = 2595 fails = 2270 % -d: 327 time = 0.03 sec inferences = 2609 fails = 2283 % -d: 328 time = 0.03 sec inferences = 2611 fails = 2284 % -d: 329 time = 0.03 sec inferences = 2625 fails = 2297 % -d: 330 time = 0.02 sec inferences = 2627 fails = 2298 % -d: 331 time = 0.03 sec inferences = 2641 fails = 2311 % -d: 332 time = 0.03 sec inferences = 2643 fails = 2312 % -d: 333 time = 0.03 sec inferences = 2657 fails = 2325 % -d: 334 time = 0.03 sec inferences = 2659 fails = 2326 % -d: 335 time = 0.03 sec inferences = 2673 fails = 2339 % -d: 336 time = 0.02 sec inferences = 2675 fails = 2340 % -d: 337 time = 0.03 sec inferences = 2689 fails = 2353 % -d: 338 time = 0.03 sec inferences = 2691 fails = 2354 % -d: 339 time = 0.03 sec inferences = 2705 fails = 2367 % -d: 340 time = 0.03 sec inferences = 2707 fails = 2368 % -d: 341 time = 0.03 sec inferences = 2721 fails = 2381 % -d: 342 time = 0.03 sec inferences = 2723 fails = 2382 % -d: 343 time = 0.03 sec inferences = 2737 fails = 2395 % -d: 344 time = 0.03 sec inferences = 2739 fails = 2396 % -d: 345 time = 0.03 sec inferences = 2753 fails = 2409 % -d: 346 time = 0.03 sec inferences = 2755 fails = 2410 % -d: 347 time = 0.03 sec inferences = 2769 fails = 2423 % -d: 348 time = 0.03 sec inferences = 2771 fails = 2424 % -d: 349 time = 0.03 sec inferences = 2785 fails = 2437 % -d: 350 time = 0.04 sec inferences = 2787 fails = 2438 % -d: 351 time = 0.03 sec inferences = 2801 fails = 2451 % -d: 352 time = 0.03 sec inferences = 2803 fails = 2452 % -d: 353 time = 0.03 sec inferences = 2817 fails = 2465 % -d: 354 time = 0.03 sec inferences = 2819 fails = 2466 % -d: 355 time = 0.03 sec inferences = 2833 fails = 2479 % -d: 356 time = 0.04 sec inferences = 2835 fails = 2480 % -d: 357 time = 0.03 sec inferences = 2849 fails = 2493 % -d: 358 time = 0.03 sec inferences = 2851 fails = 2494 % -d: 359 time = 0.03 sec inferences = 2865 fails = 2507 % -d: 360 time = 0.04 sec inferences = 2867 fails = 2508 % -d: 361 time = 0.03 sec inferences = 2881 fails = 2521 % -d: 362 time = 0.03 sec inferences = 2883 fails = 2522 % -d: 363 time = 0.04 sec inferences = 2897 fails = 2535 % -d: 364 time = 0.03 sec inferences = 2899 fails = 2536 % -d: 365 time = 0.03 sec inferences = 2913 fails = 2549 % -d: 366 time = 0.04 sec inferences = 2915 fails = 2550 % -d: 367 time = 0.03 sec inferences = 2929 fails = 2563 % -d: 368 time = 0.04 sec inferences = 2931 fails = 2564 % -d: 369 time = 0.03 sec inferences = 2945 fails = 2577 % -d: 370 time = 0.03 sec inferences = 2947 fails = 2578 % -d: 371 time = 0.04 sec inferences = 2961 fails = 2591 % -d: 372 time = 0.03 sec inferences = 2963 fails = 2592 % -d: 373 time = 0.04 sec inferences = 2977 fails = 2605 % -d: 374 time = 0.03 sec inferences = 2979 fails = 2606 % -d: 375 time = 0.04 sec inferences = 2993 fails = 2619 % -d: 376 time = 0.04 sec inferences = 2995 fails = 2620 % -d: 377 time = 0.03 sec inferences = 3009 fails = 2633 % -d: 378 time = 0.04 sec inferences = 3011 fails = 2634 % -d: 379 time = 0.03 sec inferences = 3025 fails = 2647 % -d: 380 time = 0.04 sec inferences = 3027 fails = 2648 % -d: 381 time = 0.04 sec inferences = 3041 fails = 2661 % -d: 382 time = 0.03 sec inferences = 3043 fails = 2662 % -d: 383 time = 0.04 sec inferences = 3057 fails = 2675 % -d: 384 time = 0.04 sec inferences = 3059 fails = 2676 % -d: 385 time = 0.03 sec inferences = 3073 fails = 2689 % -d: 386 time = 0.04 sec inferences = 3075 fails = 2690 % -d: 387 time = 0.04 sec inferences = 3089 fails = 2703 % -d: 388 time = 0.03 sec inferences = 3091 fails = 2704 % -d: 389 time = 0.04 sec inferences = 3105 fails = 2717 % -d: 390 time = 0.04 sec inferences = 3107 fails = 2718 % -d: 391 time = 0.04 sec inferences = 3121 fails = 2731 % -d: 392 time = 0.04 sec inferences = 3123 fails = 2732 % -d: 393 time = 0.04 sec inferences = 3137 fails = 2745 % -d: 394 time = 0.04 sec inferences = 3139 fails = 2746 % -d: 395 time = 0.04 sec inferences = 3153 fails = 2759 % -d: 396 time = 0.03 sec inferences = 3155 fails = 2760 % -d: 397 time = 0.04 sec inferences = 3169 fails = 2773 % -d: 398 time = 0.04 sec inferences = 3171 fails = 2774 % -d: 399 time = 0.04 sec inferences = 3185 fails = 2787 % -d: 400 time = 0.04 sec inferences = 3187 fails = 2788 % -d: 401 time = 0.05 sec inferences = 3201 fails = 2801 % -d: 402 SETHEO ERROR: stack overflow % time = 0.02 sec inferences = 799 fails = 397 % ******** INTERRUPT FAILURE ************ % Intermediate free variables : 0 % Intermediate inferences : 402 % Intermediate open subgoals : 1 % Generated antilemmata : 0 % Number of unifications : 641599 % - E/R/F/L : 641599/ 0/ 0/ 0 % Number of fails : 560997 % - unification : 560597 % - depth bound : 400 % Instructions executed : 6378784 % Abstract machine time (seconds) : 5.63 % Overall time (seconds) : 5.63 % Cleaning up before exit % Delete /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+noeq.hex /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+noeq.log /tmp/SystemOnTPTP7177/MSC/MSC015-1.015+noeq.tree % That's all folks % WARNING: TreeLimitedRun lost 3.87s, total lost is 3.87s % Killed 1 orphans % %------------------------------------------------------------------------------