%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PLA042+1 : TPTP v9.2.1. Bugfixed v5.5.1. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu May 7 07:31:16 PM UTC 2026 % Result : Unknown 3.44s 1.30s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PLA042+1 : TPTP v9.2.1. Bugfixed v5.5.1. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n004.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Thu May 7 12:56:48 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 2.80/1.26 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.80/1.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.80/1.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.80/1.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.80/1.26 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.80/1.26 Execution resolution_2 ended with status: gaveup % 2.80/1.26 Execution resolution_3 ended with status: gaveup % 2.80/1.26 Execution lmodel_grow ended with status: gaveup % 2.80/1.26 Execution normal ended with status: gaveup % 2.80/1.26 Execution resolution_1 ended with status: gaveup % 2.80/1.26 No successful execution. % 2.80/1.26 % 2.80/1.26 Input Clauses: % 2.80/1.29 % 2.80/1.29 Predicates: p = % 2.80/1.29 Fol Constants: true false skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 skc21 skc22 skc23 skc24 skc25 skc26 skc27 skc28 skc29 skc30 skc31 skc32 skc33 skc34 skc35 skc36 skc37 skc38 skc39 skc40 skc41 skc42 skc43 skc44 skc45 skc46 skc47 skc48 skc49 skc50 skc51 skc52 skc53 skc54 skc55 skc56 skc57 skc58 skc59 skc60 skc61 skc62 skc63 skc64 skc65 skc66 skc67 skc68 skc69 skc70 skc71 skc72 skc73 skc74 skc75 skc76 skc77 skc78 skc79 skc80 skc81 skc82 skc83 skc84 skc85 skc86 skc87 skc88 skc89 skc90 skc91 skc92 skc93 skc94 skc95 skc96 skc97 skc98 skc99 skc100 skc101 skc102 skc103 skc104 skc105 skc106 skc107 skc108 skc109 skc110 skc111 skc112 skc113 skc114 skc115 skc116 skc117 skc118 skc119 skc120 skc121 skc122 skc123 skc124 skc125 skc126 skc127 skc128 skc129 skc130 skc131 skc132 skc133 skc134 skc135 skc136 skc137 skc138 skc139 skc140 skc141 skc142 skc143 skc144 skc145 skc146 skc147 skc148 skc149 skc150 skc151 skc152 skc153 skc154 skc155 skc156 skc157 skc158 skc159 skc160 skc161 skc162 skc163 skc164 skc165 skc166 skc167 skc168 skc169 skc170 skc171 skc172 skc173 skc174 skc175 skc176 skc177 skc178 skc179 skc180 skc181 skc182 skc183 skc184 skc185 skc186 skc187 skc188 skc189 skc190 skc191 skc192 skc193 skc194 skc195 skc196 skc197 skc198 skc199 skc200 skc201 skc202 skc203 skc204 skc205 skc206 skc207 skc208 skc209 skc210 skc211 skc212 skc213 skc214 skc215 skc216 skc217 skc218 skc219 skc220 skc221 skc222 skc223 skc224 skc225 skc226 skc227 skc228 skc229 skc230 skc231 skc232 skc233 skc234 skc235 skc236 skc237 skc238 skc239 skc240 skc241 skc242 skc243 skc244 skc245 skc246 skc247 skc248 skc249 skc250 skc251 skc252 skc253 skc254 skc255 skc256 skc257 skc258 skc259 skc260 skc261 skc262 skc263 skc264 skc265 skc266 skc267 skc268 skc269 skc270 skc271 skc272 skc273 skc274 skc275 skc276 skc277 skc278 skc279 skc280 skc281 skc282 skc283 skc284 skc285 skc286 skc287 skc288 skc289 skc290 skc291 skc292 skc293 skc294 skc295 skc296 skc297 skc298 skc299 skc300 skc301 skc302 skc303 skc304 skc305 skc306 skc307 skc308 skc309 skc310 skc311 skc312 skc313 skc314 skc315 skc316 skc317 skc318 skc319 skc320 skc321 skc322 skc323 skc324 skc325 skc326 skc327 skc328 skc329 skc330 skc331 skc332 skc333 skc334 skc335 skc336 skc337 skc338 skc339 skc340 skc341 skc342 skc343 skc344 skc345 skc346 skc347 skc348 skc349 skc350 skc351 skc352 skc353 skc354 skc355 skc356 skc357 skc358 skc359 skc360 skc361 skc362 skc363 skc364 skc365 skc366 skc367 skc368 skc369 skc370 skc371 skc372 skc373 skc374 skc375 skc376 skc377 skc378 skc379 skc380 skc381 skc382 skc383 skc384 skc385 skc386 skc387 skc388 skc389 skc390 skc391 skc392 skc393 skc394 skc395 skc396 skc397 skc398 skc399 skc400 skc401 skc402 skc403 skc404 skc405 skc406 skc407 skc408 skc409 skc410 skc411 skc412 skc413 skc414 skc415 skc416 skc417 skc418 skc419 skc420 skc421 skc422 skc423 skc424 skc425 skc426 skc427 skc428 skc429 skc430 skc431 skc432 skc433 skc434 skc435 skc436 skc437 skc438 skc439 skc440 skc441 skc442 skc443 skc444 skc445 skc446 skc447 skc448 skc449 skc450 skc451 skc452 skc453 skc454 skc455 skc456 skc457 skc458 skc459 skc460 skc461 skc462 skc463 skc464 skc465 skc466 skc467 skc468 skc469 skc470 % 2.80/1.29 Fol Functions: skf471 skf472 skf473 skf474 skf475 skf476 skf477 skf478 skf479 skf480 skf481 skf482 skf483 skf484 skf485 skf486 skf487 skf488 skf489 skf490 skf491 skf492 skf493 skf494 skf495 skf496 skf497 skf498 skf499 skf500 skf501 skf502 skf503 skf504 skf505 skf506 skf507 skf508 skf509 skf510 skf511 skf512 skf513 skf514 skf515 skf516 skf517 skf518 skf519 skf520 skf521 skf522 skf523 skf524 skf525 skf526 skf527 skf528 skf529 skf530 skf531 skf532 skf533 skf534 skf535 skf536 skf537 skf538 skf539 skf540 skf541 skf542 skf543 skf544 skf545 skf546 skf547 skf548 skf549 skf550 skf551 skf552 skf553 skf554 skf555 skf556 skf557 skf558 skf559 skf560 skf561 skf562 skf563 skf564 skf565 skf566 skf567 skf568 skf569 skf570 skf571 skf572 skf573 skf574 skf575 skf576 skf577 skf578 skf579 skf580 skf581 skf582 skf583 skf584 skf585 skf586 skf587 skf588 skf589 skf590 skf591 skf592 skf593 skf594 skf595 skf596 skf597 skf598 skf599 skf600 skf601 skf602 skf603 skf604 skf605 skf606 skf607 skf608 skf609 skf610 skf611 skf612 skf613 skf614 skf615 skf616 skf617 skf618 skf619 skf620 skf621 skf622 skf623 skf624 skf625 skf626 skf627 skf628 skf629 skf630 skf631 skf632 skf633 skf634 skf635 skf636 skf637 skf638 skf639 skf640 skf641 skf642 skf643 skf644 skf645 skf646 skf647 skf648 skf649 skf650 skf651 skf652 skf653 skf654 skf655 skf656 skf657 skf658 skf659 skf660 skf661 skf662 skf663 skf664 skf665 skf666 skf667 skf668 skf669 skf670 skf671 skf672 skf673 skf674 skf675 skf676 skf677 skf678 skf679 skf680 skf681 skf682 skf683 skf684 skf685 skf686 skf687 skf688 skf689 skf690 skf691 skf692 skf693 skf694 skf695 skf696 skf697 skf698 skf699 skf700 skf701 skf702 skf703 skf704 skf705 skf706 skf707 skf708 skf709 skf710 skf711 skf712 skf713 skf714 skf715 skf716 skf717 skf718 skf719 skf720 skf721 skf722 skf723 skf724 skf725 skf726 skf727 skf728 skf729 skf730 skf731 skf732 skf733 skf734 skf735 skf736 skf737 skf738 skf739 skf740 skf741 skf742 skf743 skf744 skf745 skf746 skf747 skf748 skf749 skf750 skf751 skf752 skf753 skf754 skf755 skf756 skf757 skf758 skf759 skf760 skf761 skf762 skf763 skf764 skf765 skf766 skf767 skf768 skf769 skf770 skf771 skf772 skf773 skf774 skf775 skf776 skf777 skf778 skf779 skf780 skf781 skf782 skf783 skf784 skf785 skf786 skf787 skf788 skf789 skf790 skf791 skf792 skf793 skf794 skf795 skf796 skf797 skf798 skf799 skf800 skf801 skf802 skf803 skf804 skf805 skf806 skf807 skf808 skf809 skf810 skf811 skf812 skf813 skf814 skf815 skf816 skf817 skf818 skf819 skf820 skf821 skf822 skf823 skf824 skf825 skf826 skf827 skf828 skf829 skf830 skf831 skf832 skf833 skf834 skf835 skf836 skf837 skf838 skf839 skf840 skf841 skf842 skf843 skf844 skf845 skf846 skf847 skf848 skf849 skf850 skf851 skf852 skf853 skf854 skf855 skf856 skf857 skf858 skf859 skf860 skf861 skf862 skf863 skf864 skf865 skf866 skf867 skf868 skf869 skf870 skf871 skf872 skf873 skf874 skf875 skf876 skf877 skf878 skf879 skf880 skf881 skf882 skf883 skf884 skf885 skf886 skf887 skf888 skf889 skf890 skf891 skf892 skf893 skf894 skf895 skf896 skf897 skf898 skf899 skf900 skf901 skf902 skf903 skf904 skf905 skf906 skf907 skf908 skf909 skf910 skf911 skf912 skf913 skf914 skf915 skf916 skf917 skf918 skf919 skf920 skf921 skf922 skf923 skf924 skf925 skf926 skf927 skf928 skf929 skf930 skf931 skf932 skf933 skf934 skf935 skf936 skf937 skf938 skf939 skf940 skf941 skf942 skf943 skf944 skf945 skf946 skf947 skf948 skf949 skf950 skf951 skf952 skf953 skf954 skf955 skf956 skf957 skf958 skf959 skf960 skf961 skf962 skf963 skf964 skf965 skf966 skf967 skf968 skf969 skf970 skf971 skf972 skf973 skf974 skf975 skf976 skf977 skf978 skf979 skf980 skf981 skf982 skf983 skf984 skf985 skf986 skf987 skf988 skf989 skf990 skf991 skf992 skf993 skf994 skf995 skf996 skf997 skf998 skf999 skf1000 skf1001 skf1002 skf1003 skf1004 skf1005 skf1006 skf1007 skf1008 skf1009 skf1010 skf1011 skf1012 skf1013 skf1014 skf1015 skf1016 skf1017 skf1018 skf1019 skf1020 skf1021 skf1022 skf1023 skf1024 skf1025 skf1026 skf1027 skf1028 skf1029 skf1030 skf1031 skf1032 skf1033 skf1034 skf1035 skf1036 skf1037 skf1038 skf1039 skf1040 skf1041 skf1042 skf1043 skf1044 skf1045 skf1046 skf1047 skf1048 skf1049 skf1050 skf1051 skf1052 skf1053 skf1054 skf1055 skf1056 skf1057 skf1058 skf1059 skf1060 skf1061 skf1062 skf1063 skf1064 skf1065 skf1066 skf1067 skf1068 skf1069 skf1070 skf1071 skf1072 skf1073 skf1074 skf1075 skf1076 skf1077 skf1078 skf1079 skf1080 skf1081 skf1082 skf1083 skf1084 skf1085 skf1086 skf1087 skf1088 skf1089 skf1090 skf1091 skf1092 skf1093 skf1094 skf1095 skf1096 skf1097 skf1098 skf1099 skf1100 skf1101 skf1102 skf1103 skf1104 skf1105 skf1106 skf1107 skf1108 skf1109 skf1110 skf1111 skf1112 skf1113 skf1114 skf1115 skf1116 skf1117 skf1118 skf1119 skf1120 skf1121 skf1122 skf1123 skf1124 skf1125 skf1126 skf1127 skf1128 skf1129 skf1130 skf1131 skf1132 skf1133 skf1134 skf1135 skf1136 skf1137 skf1138 skf1139 skf1140 skf1141 skf1142 skf1143 skf1144 skf1145 skf1146 skf1147 skf1148 skf1149 skf1150 skf1151 skf1152 skf1153 skf1154 skf1155 skf1156 skf1157 skf1158 skf1159 skf1160 skf1161 skf1162 skf1163 skf1164 skf1165 skf1166 skf1167 skf1168 skf1169 skf1170 skf1171 skf1172 skf1173 skf1174 skf1175 skf1176 skf1177 skf1178 skf1179 skf1180 skf1181 skf1182 skf1183 skf1184 skf1185 skf1186 skf1187 skf1188 skf1189 skf1190 skf1191 skf1192 skf1193 skf1194 skf1195 skf1196 skf1197 skf1198 skf1199 skf1200 skf1201 skf1202 skf1203 skf1204 skf1205 skf1206 skf1207 skf1208 skf1209 skf1210 skf1211 skf1212 skf1213 skf1214 skf1215 skf1216 skf1217 skf1218 skf1219 skf1220 skf1221 skf1222 skf1223 skf1224 skf1225 skf1226 skf1227 skf1228 skf1229 skf1230 skf1231 skf1232 skf1233 skf1234 skf1235 skf1236 skf1237 skf1238 skf1239 skf1240 skf1241 skf1242 skf1243 skf1244 skf1245 skf1246 skf1247 skf1248 skf1249 skf1250 skf1251 skf1252 skf1253 skf1254 skf1255 skf1256 skf1257 skf1258 skf1259 skf1260 skf1261 skf1262 skf1263 skf1264 skf1265 skf1266 skf1267 skf1268 skf1269 skf1270 skf1271 skf1272 skf1273 skf1274 skf1275 skf1276 skf1277 skf1278 skf1279 skf1280 skf1281 skf1282 skf1283 skf1284 skf1285 skf1286 skf1287 skf1288 skf1289 skf1290 skf1291 skf1292 skf1293 skf1294 skf1295 skf1296 skf1297 skf1298 skf1299 skf1300 skf1301 skf1302 skf1303 skf1304 skf1305 skf1306 skf1307 skf1308 skf1309 skf1310 skf1311 skf1312 skf1313 skf1314 skf1315 skf1316 skf1317 skf1318 skf1319 skf1320 skf1321 skf1322 skf1323 skf1324 skf1325 skf1326 skf1327 skf1328 skf1329 skf1330 skf1331 skf1332 skf1333 skf1334 skf1335 skf1336 skf1337 skf1338 skf1339 skf1340 skf1341 skf1342 skf1343 skf1344 skf1345 skf1346 skf1347 skf1348 skf1349 skf1350 skf1351 skf1352 skf1353 skf1354 skf1355 skf1356 skf1357 skf1358 skf1359 skf1360 skf1361 skf1362 skf1363 skf1364 skf1365 skf1366 skf1367 skf1368 skf1369 skf1370 skf1371 skf1372 skf1373 skf1374 skf1375 skf1376 skf1377 skf1378 skf1379 skf1380 skf1381 skf1382 skf1383 skf1384 skf1385 skf1386 skf1387 skf1388 skf1389 skf1390 skf1391 skf1392 skf1393 skf1394 skf1395 skf1396 skf1397 skf1398 skf1399 skf1400 skf1401 skf1402 skf1403 skf1404 skf1405 skf1406 skf1407 skf1408 skf1409 skf1410 skf1411 skf1412 skf1413 skf1414 skf1415 skf1416 skf1417 skf1418 skf1419 skf1420 skf1421 skf1422 skf1423 skf1424 skf1425 skf1426 skf1427 skf1428 skf1429 skf1430 skf1431 skf1432 skf1433 skf1434 skf1435 skf1436 skf1437 skf1438 skf1439 skf1440 skf1441 skf1442 skf1443 skf1444 skf1445 skf1446 skf1447 skf1448 skf1449 skf1450 skf1451 skf1452 skf1453 skf1454 skf1455 skf1456 skf1457 skf1458 skf1459 skf1460 skf1461 skf1462 skf1463 skf1464 skf1465 skf1466 skf1467 skf1468 skf1469 skf1470 skf1471 skf1472 skf1473 skf1474 skf1475 skf1476 skf1477 skf1478 skf1479 skf1480 skf1481 skf1482 skf1483 skf1484 skf1485 skf1486 skf1487 skf1488 skf1489 skf1490 skf1491 skf1492 skf1493 skf1494 skf1495 skf1496 skf1497 skf1498 skf1499 skf1500 skf1501 skf1502 skf1503 skf1504 skf1505 skf1506 skf1507 skf1508 skf1509 skf1510 skf1511 skf1512 skf1513 skf1514 skf1515 skf1516 skf1517 skf1518 skf1519 skf1520 skf1521 skf1522 skf1523 skf1524 skf1525 skf1526 skf1527 skf1528 skf1529 skf1530 skf1531 skf1532 skf1533 skf1534 skf1535 skf1536 skf1537 skf1538 skf1539 skf1540 skf1541 skf1542 skf1543 skf1544 skf1545 skf1546 skf1547 skf1548 skf1549 skf1550 skf1551 skf1552 skf1553 skf1554 skf1555 skf1556 skf1557 skf1558 skf1559 skf1560 skf1561 skf1562 skf1563 skf1564 skf1565 skf1566 skf1567 skf1568 skf1569 skf1570 skf1571 skf1572 skf1573 skf1574 skf1575 skf1576 skf1577 skf1578 skf1579 skf1580 skf1581 skf1582 skf1583 skf1584 skf1585 skf1586 skf1587 skf1588 skf1589 skf1590 skf1591 skf1592 skf1593 skf1594 skf1595 skf1596 skf1597 skf1598 skf1599 skf1600 skf1601 skf1602 skf1603 skf1604 skf1605 skf1606 skf1607 skf1608 skf1609 skf1610 skf1611 skf1612 skf1613 skf1614 skf1615 skf1616 skf1617 skf1618 skf1619 skf1620 skf1621 skf1622 skf1623 skf1624 skf1625 skf1626 skf1627 skf1628 skf1629 skf1630 skf1631 skf1632 skf1633 skf1634 skf1635 skf1636 skf1637 skf1638 skf1639 skf1640 skf1641 skf1642 skf1643 skf1644 skf1645 skf1646 skf1647 skf1648 skf1649 skf1650 skf1651 skf1652 skf1653 skf1654 skf1655 skf1656 skf1657 skf1658 skf1659 skf1660 skf1661 skf1662 skf1663 skf1664 skf1665 skf1666 skf1667 skf1668 skf1669 skf1670 skf1671 skf1672 skf1673 skf1674 skf1675 skf1676 skf1677 skf1678 skf1679 skf1680 skf1681 skf1682 skf1683 skf1684 skf1685 skf1686 skf1687 skf1688 skf1689 skf1690 skf1691 skf1692 skf1693 skf1694 skf1695 skf1696 skf1697 skf1698 skf1699 skf1700 skf1701 skf1702 skf1703 skf1704 skf1705 skf1706 skf1707 skf1708 skf1709 skf1710 skf1711 skf1712 skf1713 skf1714 skf1715 skf1716 skf1717 skf1718 skf1719 skf1720 skf1721 skf1722 skf1723 skf1724 skf1725 skf1726 skf1727 skf1728 skf1729 skf1730 skf1731 skf1732 skf1733 skf1734 skf1735 skf1736 skf1737 skf1738 skf1739 skf1740 skf1741 skf1742 skf1743 skf1744 skf1745 skf1746 skf1747 skf1748 skf1749 skf1750 skf1751 skf1752 skf1753 skf1754 skf1755 skf1756 skf1757 skf1758 skf1759 skf1760 skf1761 skf1762 skf1763 skf1764 skf1765 skf1766 skf1767 skf1768 skf1769 skf1770 skf1771 skf1772 skf1773 skf1774 skf1775 skf1776 skf1777 skf1778 skf1779 skf1780 skf1781 skf1782 skf1783 skf1784 skf1785 skf1786 skf1787 skf1788 skf1789 skf1790 skf1791 skf1792 skf1793 skf1794 skf1795 skf1796 skf1797 skf1798 skf1799 skf1800 skf1801 skf1802 skf1803 skf1804 skf1805 skf1806 skf1807 skf1808 skf1809 skf1810 skf1811 skf1812 skf1813 skf1814 skf1815 skf1816 skf1817 skf1818 skf1819 skf1820 skf1821 skf1822 skf1823 skf1824 skf1825 skf1826 skf1827 skf1828 skf1829 skf1830 skf1831 skf1832 skf1833 skf1834 skf1835 skf1836 skf1837 skf1838 skf1839 skf1840 skf1841 skf1842 skf1843 skf1844 skf1845 skf1846 skf1847 skf1848 skf1849 skf1850 skf1851 skf1852 skf1853 skf1854 skf1855 skf1856 skf1857 skf1858 skf1859 skf1860 skf1861 skf1862 skf1863 skf1864 skf1865 skf1866 skf1867 skf1868 skf1869 skf1870 skf1871 skf1872 skf1873 skf1874 skf1875 skf1876 skf1877 skf1878 skf1879 skf1880 skf1881 skf1882 skf1883 skf1884 skf1885 skf1886 skf1887 skf1888 skf1889 skf1890 skf1891 skf1892 skf1893 skf1894 skf1895 skf1896 skf1897 skf1898 skf1899 skf1900 skf1901 skf1902 skf1903 skf1904 skf1905 skf1906 skf1907 skf1908 skf1909 skf1910 skf1911 skf1912 skf1913 skf1914 skf1915 skf1916 skf1917 skf1918 skf1919 skf1920 skf1921 skf1922 skf1923 skf1924 skf1925 skf1926 skf1927 skf1928 skf1929 skf1930 skf1931 skf1932 skf1933 skf1934 skf1935 skf1936 skf1937 skf1938 skf1939 skf1940 skf1941 skf1942 skf1943 skf1944 skf1945 skf1946 skf1947 skf1948 skf1949 skf1950 skf1951 skf1952 skf1953 skf1954 skf1955 skf1956 skf1957 skf1958 skf1959 skf1960 skf1961 skf1962 skf1963 skf1964 skf1965 skf1966 skf1967 skf1968 skf1969 skf1970 skf1971 skf1972 skf1973 skf1974 skf1975 skf1976 skf1977 skf1978 skf1979 skf1980 skf1981 skf1982 skf1983 skf1984 skf1985 skf1986 skf1987 skf1988 skf1989 skf1990 skf1991 skf1992 skf1993 skf1994 skf1995 skf1996 skf1997 skf1998 skf1999 skf2000 skf2001 skf2002 skf2003 skf2004 skf2005 skf2006 skf2007 skf2008 skf2009 skf2010 skf2011 skf2012 skf2013 skf2014 skf2015 skf2016 skf2017 skf2018 skf2019 skf2020 skf2021 skf2022 skf2023 skf2024 skf2025 skf2026 skf2027 skf2028 skf2029 skf2030 skf2031 skf2032 skf2033 skf2034 skf2035 skf2036 skf2037 skf2038 skf2039 skf2040 skf2041 skf2042 skf2043 skf2044 skf2045 skf2046 skf2047 skf2048 skf2049 skf2050 skf2051 skf2052 skf2053 skf2054 skf2055 skf2056 skf2057 skf2058 skf2059 skf2060 skf2061 skf2062 skf2063 skf2064 skf2065 skf2066 skf2067 skf2068 skf2069 skf2070 skf2071 skf2072 skf2073 skf2074 skf2075 skf2076 skf2077 skf2078 skf2079 skf2080 skf2081 skf2082 skf2083 skf2084 skf2085 skf2086 skf2087 skf2088 skf2089 skf2090 skf2091 skf2092 skf2093 skf2094 skf2095 skf2096 skf2097 skf2098 skf2099 skf2100 skf2101 skf2102 skf2103 skf2104 skf2105 skf2106 skf2107 skf2108 skf2109 skf2110 skf2111 skf2112 skf2113 skf2114 skf2115 skf2116 skf2117 skf2118 skf2119 skf2120 skf2121 skf2122 skf2123 skf2124 skf2125 skf2126 skf2127 skf2128 skf2129 skf2130 skf2131 skf2132 skf2133 skf2134 skf2135 skf2136 skf2137 skf2138 skf2139 skf2140 skf2141 skf2142 skf2143 skf2144 skf2145 skf2146 % 2.80/1.29 Problem Properties: % 2.80/1.29 This is a full first-order problem with equality. % 2.80/1.29 SZS status GaveUp % 2.80/1.29 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 2.80/1.29 %------------------------------------------------------------------------------