%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : LCL681+1.015 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n005.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:28:15 PM UTC 2026 % Result : CounterSatisfiable 3.27s 1.52s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : LCL681+1.015 : TPTP v9.2.1. Released v4.0.0. % 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.33 % Computer : n005.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Thu May 7 12:36:31 EDT 2026 % 0.16/0.33 % CPUTime : % 0.16/0.33 SPASS-SCL-FOL version: % 0.19/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 3.27/1.51 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.27/1.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.27/1.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.27/1.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.27/1.51 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.27/1.51 Execution resolution_1 ended with status: satisfiable % 3.27/1.51 Used heuristic: resolution_1 % 3.27/1.51 % 3.27/1.51 Input Clauses: % 3.27/1.51 % 3.27/1.51 Predicates: r1 p2 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75 ren76 ren77 ren78 ren79 ren80 ren81 ren82 ren83 ren84 ren85 ren86 ren87 ren88 ren89 ren90 ren91 ren92 ren93 ren94 ren95 ren96 ren97 ren98 ren99 ren100 ren101 ren102 ren103 ren104 ren105 ren106 ren107 ren108 ren109 ren110 ren111 ren112 ren113 ren114 ren115 ren116 ren117 ren118 ren119 ren120 ren121 ren122 ren123 ren124 ren125 ren126 ren127 ren128 ren129 ren130 ren131 ren132 ren133 ren134 ren135 ren136 ren137 ren138 ren139 ren140 ren141 ren142 ren143 ren144 ren145 ren146 ren147 ren148 ren149 ren150 ren151 ren152 ren153 ren154 ren155 ren156 ren157 ren158 ren159 ren160 ren161 ren162 ren163 ren164 ren165 ren166 ren167 ren168 ren169 ren170 ren171 ren172 ren173 ren174 ren175 ren176 ren177 ren178 ren179 ren180 ren181 ren182 ren183 ren184 ren185 ren186 ren187 ren188 ren189 ren190 ren191 ren192 ren193 ren194 ren195 ren196 ren197 ren198 ren199 ren200 ren201 ren202 ren203 ren204 ren205 ren206 ren207 ren208 ren209 ren210 ren211 ren212 ren213 ren214 ren215 ren216 ren217 ren218 ren219 ren220 ren221 ren222 ren223 ren224 ren225 ren226 ren227 ren228 ren229 ren230 ren231 ren232 ren233 ren234 ren235 ren236 ren237 ren238 ren239 ren240 ren241 ren242 ren243 ren244 ren245 ren246 ren247 ren248 ren249 ren250 ren251 ren252 ren253 ren254 ren255 ren256 ren257 ren258 ren259 ren260 ren261 ren262 ren263 ren264 ren265 ren266 ren267 ren268 ren269 ren270 ren271 ren272 ren273 ren274 ren275 ren276 ren277 ren278 ren279 ren280 ren281 ren282 ren283 ren284 ren285 ren286 ren287 ren288 ren289 ren290 ren291 ren292 ren293 ren294 ren295 ren296 ren297 ren298 ren299 ren300 ren301 ren302 ren303 ren304 ren305 ren306 ren307 ren308 ren309 ren310 ren311 ren312 ren313 ren314 ren315 ren316 ren317 ren318 ren319 ren320 ren321 ren322 ren323 ren324 ren325 ren326 ren327 ren328 ren329 ren330 ren331 ren332 ren333 ren334 ren335 ren336 ren337 ren338 ren339 ren340 ren341 ren342 ren343 ren344 ren345 ren346 ren347 ren348 ren349 ren350 ren351 ren352 ren353 ren354 ren355 ren356 ren357 ren358 ren359 ren360 ren361 ren362 ren363 ren364 ren365 ren366 ren367 ren368 ren369 ren370 ren371 ren372 ren373 ren374 ren375 ren376 ren377 ren378 ren379 ren380 ren381 ren382 ren383 ren384 ren385 ren386 ren387 ren388 ren389 ren390 ren391 ren392 ren393 ren394 ren395 ren396 ren397 ren398 ren399 ren400 ren401 ren402 ren403 ren404 ren405 ren406 ren407 ren408 ren409 ren410 ren411 ren412 ren413 ren414 ren415 ren416 ren417 ren418 ren419 ren420 ren421 ren422 ren423 ren424 ren425 ren426 ren427 ren428 ren429 ren430 ren431 ren432 ren433 ren434 ren435 ren436 ren437 ren438 ren439 ren440 ren441 ren442 ren443 ren444 ren445 ren446 ren447 ren448 ren449 ren450 ren451 ren452 ren453 ren454 ren455 ren456 ren457 ren458 ren459 ren460 ren461 ren462 ren463 ren464 ren465 ren466 ren467 ren468 ren469 ren470 ren471 ren472 ren473 ren474 ren475 ren476 ren477 ren478 ren479 ren480 ren481 ren482 ren483 ren484 ren485 ren486 ren487 ren488 ren489 ren490 ren491 ren492 ren493 ren494 ren495 ren496 ren497 ren498 ren499 ren500 ren501 ren502 ren503 ren504 ren505 ren506 ren507 ren508 ren509 ren510 ren511 ren512 ren513 ren514 ren515 ren516 ren517 ren518 ren519 ren520 ren521 ren522 ren523 ren524 ren525 ren526 ren527 ren528 ren529 ren530 ren531 ren532 ren533 ren534 ren535 ren536 ren537 ren538 ren539 ren540 ren541 ren542 ren543 ren544 ren545 ren546 ren547 ren548 ren549 ren550 ren551 ren552 ren553 ren554 ren555 ren556 ren557 ren558 ren559 ren560 ren561 ren562 ren563 ren564 ren565 ren566 ren567 ren568 ren569 ren570 ren571 ren572 ren573 ren574 ren575 ren576 ren577 ren578 ren579 ren580 ren581 ren582 ren583 ren584 ren585 ren586 ren587 ren588 ren589 ren590 ren591 ren592 ren593 ren594 ren595 ren596 ren597 ren598 ren599 ren600 ren601 ren602 ren603 ren604 ren605 ren606 ren607 ren608 ren609 ren610 ren611 ren612 ren613 ren614 ren615 ren616 ren617 ren618 ren619 ren620 ren621 ren622 ren623 ren624 ren625 ren626 ren627 ren628 ren629 ren630 ren631 ren632 ren633 ren634 ren635 ren636 ren637 ren638 ren639 ren640 ren641 ren642 ren643 ren644 ren645 ren646 ren647 ren648 ren649 ren650 ren651 ren652 ren653 ren654 ren655 ren656 ren657 ren658 ren659 ren660 ren661 ren662 ren663 ren664 ren665 ren666 ren667 ren668 ren669 ren670 ren671 ren672 ren673 ren674 ren675 ren676 ren677 ren678 ren679 ren680 ren681 ren682 ren683 ren684 ren685 ren686 ren687 ren688 ren689 ren690 ren691 ren692 ren693 ren694 ren695 ren696 ren697 ren698 ren699 ren700 ren701 ren702 ren703 ren704 ren705 ren706 ren707 ren708 ren709 ren710 ren711 ren712 ren713 ren714 ren715 ren716 ren717 ren718 ren719 ren720 ren721 ren722 ren723 ren724 ren725 ren726 ren727 ren728 ren729 ren730 ren731 ren732 ren733 ren734 ren735 ren736 ren737 ren738 ren739 ren740 ren741 ren742 ren743 ren744 ren745 ren746 ren747 ren748 ren749 ren750 ren751 ren752 ren753 ren754 ren755 ren756 ren757 ren758 ren759 ren760 ren761 ren762 ren763 ren764 ren765 ren766 ren767 ren768 ren769 ren770 ren771 ren772 ren773 ren774 ren775 ren776 ren777 ren778 ren779 ren780 ren781 ren782 ren783 ren784 ren785 ren786 ren787 ren788 ren789 ren790 ren791 ren792 ren793 ren794 ren795 ren796 ren797 ren798 ren799 ren800 ren801 ren802 ren803 ren804 ren805 ren806 ren807 ren808 ren809 ren810 ren811 ren812 ren813 ren814 ren815 ren816 ren817 ren818 ren819 ren820 ren821 ren822 ren823 ren824 ren825 ren826 ren827 ren828 ren829 ren830 ren831 ren832 ren833 ren834 ren835 ren836 ren837 ren838 ren839 ren840 ren841 ren842 ren843 ren844 ren845 ren846 ren847 ren848 ren849 ren850 ren851 ren852 ren853 ren854 ren855 ren856 ren857 ren858 ren859 ren860 ren861 ren862 ren863 ren864 ren865 ren866 ren867 ren868 ren869 ren870 ren871 ren872 ren873 ren874 ren875 ren876 ren877 ren878 ren879 ren880 ren881 ren882 ren883 ren884 ren885 ren886 ren887 ren888 ren889 ren890 ren891 ren892 ren893 ren894 ren895 ren896 ren897 ren898 ren899 ren900 ren901 ren902 ren903 ren904 ren905 ren906 ren907 ren908 ren909 ren910 ren911 ren912 ren913 ren914 ren915 ren916 ren917 ren918 ren919 ren920 ren921 ren922 ren923 ren924 ren925 ren926 ren927 ren928 ren929 ren930 ren931 ren932 ren933 ren934 ren935 ren936 ren937 ren938 ren939 ren940 ren941 ren942 ren943 ren944 ren945 ren946 ren947 ren948 ren949 ren950 ren951 ren952 ren953 ren954 ren955 ren956 ren957 ren958 ren959 ren960 ren961 ren962 ren963 ren964 ren965 ren966 ren967 ren968 ren969 ren970 ren971 ren972 ren973 ren974 ren975 ren976 ren977 ren978 ren979 ren980 ren981 ren982 ren983 ren984 ren985 ren986 ren987 ren988 ren989 ren990 ren991 ren992 ren993 ren994 ren995 ren996 ren997 ren998 ren999 ren1000 ren1001 ren1002 ren1003 ren1004 ren1005 ren1006 ren1007 ren1008 ren1009 ren1010 ren1011 ren1012 ren1013 ren1014 ren1015 ren1016 ren1017 ren1018 ren1019 ren1020 ren1021 ren1022 ren1023 ren1024 ren1025 ren1026 ren1027 ren1028 ren1029 ren1030 ren1031 ren1032 ren1033 ren1034 ren1035 ren1036 ren1037 ren1038 ren1039 ren1040 ren1041 ren1042 ren1043 ren1044 ren1045 ren1046 ren1047 ren1048 ren1049 ren1050 ren1051 ren1052 ren1053 ren1054 ren1055 ren1056 ren1057 ren1058 ren1059 ren1060 ren1061 ren1062 ren1063 ren1064 ren1065 ren1066 ren1067 ren1068 ren1069 ren1070 ren1071 ren1072 ren1073 ren1074 ren1075 ren1076 ren1077 ren1078 ren1079 ren1080 ren1081 ren1082 ren1083 ren1084 ren1085 ren1086 ren1087 ren1088 ren1089 ren1090 ren1091 ren1092 ren1093 ren1094 ren1095 ren1096 ren1097 ren1098 ren1099 ren1100 ren1101 ren1102 ren1103 ren1104 ren1105 ren1106 ren1107 ren1108 ren1109 ren1110 ren1111 ren1112 ren1113 ren1114 ren1115 ren1116 ren1117 ren1118 ren1119 ren1120 ren1121 ren1122 ren1123 ren1124 ren1125 ren1126 ren1127 ren1128 ren1129 ren1130 ren1131 ren1132 ren1133 ren1134 ren1135 ren1136 ren1137 ren1138 ren1139 ren1140 ren1141 ren1142 ren1143 ren1144 ren1145 ren1146 ren1147 ren1148 ren1149 ren1150 ren1151 ren1152 ren1153 ren1154 ren1155 ren1156 ren1157 ren1158 ren1159 ren1160 ren1161 ren1162 ren1163 ren1164 ren1165 ren1166 ren1167 ren1168 ren1169 ren1170 ren1171 ren1172 ren1173 ren1174 ren1175 ren1176 ren1177 ren1178 ren1179 ren1180 ren1181 ren1182 ren1183 ren1184 ren1185 ren1186 ren1187 ren1188 ren1189 ren1190 ren1191 ren1192 ren1193 ren1194 ren1195 ren1196 ren1197 ren1198 ren1199 ren1200 ren1201 ren1202 ren1203 ren1204 ren1205 ren1206 ren1207 ren1208 ren1209 ren1210 ren1211 ren1212 ren1213 ren1214 ren1215 ren1216 ren1217 ren1218 ren1219 ren1220 ren1221 ren1222 ren1223 ren1224 ren1225 ren1226 ren1227 ren1228 ren1229 ren1230 ren1231 ren1232 ren1233 ren1234 ren1235 ren1236 ren1237 ren1238 ren1239 ren1240 ren1241 ren1242 ren1243 ren1244 ren1245 ren1246 ren1247 ren1248 ren1249 ren1250 ren1251 ren1252 ren1253 ren1254 ren1255 ren1256 ren1257 ren1258 ren1259 ren1260 ren1261 ren1262 ren1263 ren1264 ren1265 ren1266 ren1267 ren1268 ren1269 ren1270 ren1271 ren1272 ren1273 ren1274 ren1275 ren1276 ren1277 ren1278 ren1279 ren1280 ren1281 ren1282 ren1283 ren1284 ren1285 ren1286 ren1287 ren1288 ren1289 ren1290 ren1291 ren1292 ren1293 ren1294 ren1295 ren1296 ren1297 ren1298 ren1299 ren1300 ren1301 ren1302 ren1303 ren1304 ren1305 ren1306 ren1307 ren1308 ren1309 ren1310 ren1311 ren1312 ren1313 ren1314 ren1315 ren1316 ren1317 ren1318 ren1319 ren1320 ren1321 ren1322 ren1323 ren1324 ren1325 ren1326 ren1327 ren1328 ren1329 ren1330 ren1331 ren1332 ren1333 ren1334 ren1335 ren1336 ren1337 ren1338 ren1339 ren1340 ren1341 ren1342 ren1343 ren1344 ren1345 ren1346 ren1347 ren1348 ren1349 ren1350 ren1351 ren1352 ren1353 ren1354 ren1355 ren1356 ren1357 ren1358 ren1359 ren1360 ren1361 ren1362 ren1363 ren1364 ren1365 ren1366 ren1367 ren1368 ren1369 ren1370 ren1371 ren1372 ren1373 ren1374 ren1375 ren1376 ren1377 ren1378 ren1379 ren1380 ren1381 ren1382 ren1383 ren1384 ren1385 ren1386 ren1387 ren1388 ren1389 ren1390 ren1391 ren1392 ren1393 ren1394 ren1395 ren1396 ren1397 ren1398 ren1399 ren1400 ren1401 ren1402 ren1403 ren1404 ren1405 ren1406 ren1407 ren1408 ren1409 ren1410 ren1411 ren1412 ren1413 ren1414 ren1415 ren1416 ren1417 ren1418 ren1419 ren1420 ren1421 ren1422 ren1423 ren1424 ren1425 ren1426 ren1427 ren1428 ren1429 ren1430 ren1431 ren1432 ren1433 ren1434 ren1435 ren1436 ren1437 ren1438 ren1439 ren1440 ren1441 ren1442 ren1443 ren1444 ren1445 ren1446 ren1447 ren1448 ren1449 ren1450 ren1451 ren1452 ren1453 ren1454 ren1455 ren1456 ren1457 % 3.27/1.51 Fol Constants: skc104 % 3.27/1.51 Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf21 skf22 skf23 skf24 skf25 skf26 skf27 skf28 skf29 skf30 skf31 skf32 skf33 skf34 skf35 skf36 skf37 skf38 skf39 skf40 skf41 skf42 skf43 skf44 skf45 skf46 skf47 skf48 skf49 skf50 skf51 skf52 skf53 skf54 skf55 skf56 skf57 skf58 skf59 skf60 skf61 skf62 skf63 skf64 skf65 skf66 skf67 skf68 skf69 skf70 skf71 skf72 skf73 skf74 skf75 skf76 skf77 skf78 skf79 skf80 skf81 skf82 skf83 skf84 skf85 skf86 skf87 skf88 skf89 skf90 skf91 skf92 skf93 skf94 skf95 skf96 skf97 skf98 skf99 skf100 skf101 skf102 skf103 skf105 skf106 % 3.27/1.51 Problem Properties: % 3.27/1.51 This is a full first-order problem without equality. % 3.27/1.51 % 3.27/1.51 After reduction: Problem Properties: % 3.27/1.51 This is a full first-order problem without equality. % 3.27/1.51 % 3.27/1.51 % 3.27/1.51 Reduced Input Clauses: % 3.27/1.52 3050:2:1:[3049.0,3048.2]:Top: r1(skc104,x0),ren1457(x0,skf106(x0)) -> % 3.27/1.52 % 3.27/1.52 Most General Atoms: r1(x0,x2) p2(x0) p1(x1) ren1(x1) ren2(x1) ren3(x1) ren4(x1) ren5(x1) ren6(x1) ren7(x1) ren8(x1) ren9(x1) ren10(x1) ren11(x1) ren12(x1) ren13(x1) ren14(x2,x0) ren15(x1) ren16(x1) ren17(x1) ren18(x1) ren19(x1) ren20(x1) ren21(x1) ren22(x1) ren23(x1) ren24(x1) ren25(x1) ren26(x1) ren27(x2,x0) ren28(x1) ren29(x1) ren30(x1) ren31(x1) ren32(x1) ren33(x1) ren34(x1) ren35(x1) ren36(x1) ren37(x1) ren38(x1) ren39(x1) ren40(x2,x0) ren41(x1) ren42(x1) ren43(x1) ren44(x1) ren45(x1) ren46(x1) ren47(x1) ren48(x1) ren49(x1) ren50(x1) ren51(x1) ren52(x1) ren53(x2,x0) ren54(x1) ren55(x1) ren56(x1) ren57(x1) ren58(x1) ren59(x1) ren60(x1) ren61(x1) ren62(x1) ren63(x1) ren64(x1) ren65(x1) ren66(x2,x0) ren67(x1) ren68(x1) ren69(x1) ren70(x1) ren71(x1) ren72(x1) ren73(x1) ren74(x1) ren75(x1) ren76(x1) ren77(x1) ren78(x1) ren79(x2,x0) ren80(x1) ren81(x1) ren82(x1) ren83(x1) ren84(x1) ren85(x1) ren86(x1) ren87(x1) ren88(x1) ren89(x1) ren90(x1) ren91(x1) ren92(x2,x0) ren93(x1) ren94(x1) ren95(x1) ren96(x1) ren97(x1) ren98(x1) ren99(x1) ren100(x1) ren101(x1) ren102(x1) ren103(x1) ren104(x1) ren105(x2,x0) ren106(x1) ren107(x1) ren108(x1) ren109(x1) ren110(x1) ren111(x1) ren112(x1) ren113(x1) ren114(x1) ren115(x1) ren116(x1) ren117(x1) ren118(x2,x0) ren119(x1) ren120(x1) ren121(x1) ren122(x1) ren123(x1) ren124(x1) ren125(x1) ren126(x1) ren127(x1) ren128(x1) ren129(x1) ren130(x1) ren131(x2,x0) ren132(x1) ren133(x1) ren134(x1) ren135(x1) ren136(x1) ren137(x1) ren138(x1) ren139(x1) ren140(x1) ren141(x1) ren142(x1) ren143(x1) ren144(x2,x0) ren145(x1) ren146(x1) ren147(x1) ren148(x1) ren149(x1) ren150(x1) ren151(x1) ren152(x1) ren153(x1) ren154(x1) ren155(x1) ren156(x1) ren157(x2,x0) ren158(x1) ren159(x1) ren160(x1) ren161(x1) ren162(x1) ren163(x1) ren164(x1) ren165(x1) ren166(x1) ren167(x1) ren168(x1) ren169(x1) ren170(x2,x0) ren171(x1) ren172(x1) ren173(x1) ren174(x1) ren175(x1) ren176(x1) ren177(x1) ren178(x1) ren179(x1) ren180(x1) ren181(x1) ren182(x1) ren183(x2,x0) ren184(x1) ren185(x1) ren186(x1) ren187(x1) ren188(x1) ren189(x1) ren190(x1) ren191(x1) ren192(x1) ren193(x1) ren195(x0) ren194(x1) ren196(x1) ren197(x1) ren198(x1) ren199(x1) ren200(x1) ren201(x1) ren202(x1) ren203(x1) ren204(x1) ren205(x1) ren206(x1) ren207(x1) ren208(x1) ren209(x2,x0) ren210(x1) ren211(x1) ren212(x1) ren213(x1) ren214(x1) ren215(x1) ren216(x1) ren217(x1) ren218(x1) ren219(x1) ren220(x1) ren221(x1) ren222(x2,x0) ren223(x1) ren224(x1) ren225(x1) ren226(x1) ren227(x1) ren228(x1) ren229(x1) ren230(x1) ren231(x1) ren232(x1) ren233(x1) ren234(x1) ren235(x2,x0) ren236(x1) ren237(x1) ren238(x1) ren239(x1) ren240(x1) ren241(x1) ren242(x1) ren243(x1) ren244(x1) ren245(x1) ren246(x1) ren247(x1) ren248(x2,x0) ren249(x1) ren250(x1) ren251(x1) ren252(x1) ren253(x1) ren254(x1) ren255(x1) ren256(x1) ren257(x1) ren258(x1) ren259(x1) ren260(x1) ren261(x2,x0) ren262(x1) ren263(x1) ren264(x1) ren265(x1) ren266(x1) ren267(x1) ren268(x1) ren269(x1) ren270(x1) ren271(x1) ren272(x1) ren273(x1) ren274(x2,x0) ren275(x1) ren276(x1) ren277(x1) ren278(x1) ren279(x1) ren280(x1) ren281(x1) ren282(x1) ren283(x1) ren284(x1) ren285(x1) ren286(x1) ren287(x2,x0) ren288(x1) ren289(x1) ren290(x1) ren291(x1) ren292(x1) ren293(x1) ren294(x1) ren295(x1) ren296(x1) ren297(x1) ren298(x1) ren299(x1) ren300(x2,x0) ren301(x1) ren302(x1) ren303(x1) ren304(x1) ren305(x1) ren306(x1) ren307(x1) ren308(x1) ren309(x1) ren310(x1) ren311(x1) ren312(x1) ren313(x2,x0) ren314(x1) ren315(x1) ren316(x1) ren317(x1) ren318(x1) ren319(x1) ren320(x1) ren321(x1) ren322(x1) ren323(x1) ren324(x1) ren325(x1) ren326(x2,x0) ren327(x1) ren328(x1) ren329(x1) ren330(x1) ren331(x1) ren332(x1) ren333(x1) ren334(x1) ren335(x1) ren336(x1) ren337(x1) ren338(x1) ren339(x2,x0) ren340(x1) ren341(x1) ren342(x1) ren343(x1) ren344(x1) ren345(x1) ren346(x1) ren347(x1) ren348(x1) ren349(x1) ren350(x1) ren351(x1) ren352(x2,x0) ren353(x1) ren354(x1) ren355(x1) ren356(x1) ren357(x1) ren358(x1) ren359(x1) ren360(x1) ren361(x1) ren362(x1) ren363(x1) ren364(x1) ren365(x2,x0) ren366(x1) ren367(x1) ren368(x1) ren369(x1) ren370(x1) ren371(x1) ren372(x1) ren373(x1) ren374(x1) ren376(x0) ren375(x1) ren377(x1) ren378(x1) ren379(x1) ren380(x1) ren381(x1) ren382(x1) ren383(x1) ren384(x1) ren385(x1) ren386(x1) ren387(x1) ren388(x1) ren389(x1) ren390(x2,x0) ren391(x1) ren392(x1) ren393(x1) ren394(x1) ren395(x1) ren396(x1) ren397(x1) ren398(x1) ren399(x1) ren400(x1) ren401(x1) ren402(x1) ren403(x2,x0) ren404(x1) ren405(x1) ren406(x1) ren407(x1) ren408(x1) ren409(x1) ren410(x1) ren411(x1) ren412(x1) ren413(x1) ren414(x1) ren415(x1) ren416(x2,x0) ren417(x1) ren418(x1) ren419(x1) ren420(x1) ren421(x1) ren422(x1) ren423(x1) ren424(x1) ren425(x1) ren426(x1) ren427(x1) ren428(x1) ren429(x2,x0) ren430(x1) ren431(x1) ren432(x1) ren433(x1) ren434(x1) ren435(x1) ren436(x1) ren437(x1) ren438(x1) ren439(x1) ren440(x1) ren441(x1) ren442(x2,x0) ren443(x1) ren444(x1) ren445(x1) ren446(x1) ren447(x1) ren448(x1) ren449(x1) ren450(x1) ren451(x1) ren452(x1) ren453(x1) ren454(x1) ren455(x2,x0) ren456(x1) ren457(x1) ren458(x1) ren459(x1) ren460(x1) ren461(x1) ren462(x1) ren463(x1) ren464(x1) ren465(x1) ren466(x1) ren467(x1) ren468(x2,x0) ren469(x1) ren470(x1) ren471(x1) ren472(x1) ren473(x1) ren474(x1) ren475(x1) ren476(x1) ren477(x1) ren478(x1) ren479(x1) ren480(x1) ren481(x2,x0) ren482(x1) ren483(x1) ren484(x1) ren485(x1) ren486(x1) ren487(x1) ren488(x1) ren489(x1) ren490(x1) ren491(x1) ren492(x1) ren493(x1) ren494(x2,x0) ren495(x1) ren496(x1) ren497(x1) ren498(x1) ren499(x1) ren500(x1) ren501(x1) ren502(x1) ren503(x1) ren504(x1) ren505(x1) ren506(x1) ren507(x2,x0) ren508(x1) ren509(x1) ren510(x1) ren511(x1) ren512(x1) ren513(x1) ren514(x1) ren515(x1) ren516(x1) ren517(x1) ren518(x1) ren519(x1) ren520(x2,x0) ren521(x1) ren522(x1) ren523(x1) ren524(x1) ren525(x1) ren526(x1) ren527(x1) ren528(x1) ren529(x1) ren530(x1) ren531(x1) ren532(x1) ren533(x2,x0) ren534(x1) ren535(x1) ren536(x1) ren537(x1) ren538(x1) ren539(x1) ren540(x1) ren541(x1) ren543(x0) ren542(x1) ren544(x1) ren545(x1) ren546(x1) ren547(x1) ren548(x1) ren549(x1) ren550(x1) ren551(x1) ren552(x1) ren553(x1) ren554(x1) ren555(x1) ren556(x1) ren557(x2,x0) ren558(x1) ren559(x1) ren560(x1) ren561(x1) ren562(x1) ren563(x1) ren564(x1) ren565(x1) ren566(x1) ren567(x1) ren568(x1) ren569(x1) ren570(x2,x0) ren571(x1) ren572(x1) ren573(x1) ren574(x1) ren575(x1) ren576(x1) ren577(x1) ren578(x1) ren579(x1) ren580(x1) ren581(x1) ren582(x1) ren583(x2,x0) ren584(x1) ren585(x1) ren586(x1) ren587(x1) ren588(x1) ren589(x1) ren590(x1) ren591(x1) ren592(x1) ren593(x1) ren594(x1) ren595(x1) ren596(x2,x0) ren597(x1) ren598(x1) ren599(x1) ren600(x1) ren601(x1) ren602(x1) ren603(x1) ren604(x1) ren605(x1) ren606(x1) ren607(x1) ren608(x1) ren609(x2,x0) ren610(x1) ren611(x1) ren612(x1) ren613(x1) ren614(x1) ren615(x1) ren616(x1) ren617(x1) ren618(x1) ren619(x1) ren620(x1) ren621(x1) ren622(x2,x0) ren623(x1) ren624(x1) ren625(x1) ren626(x1) ren627(x1) ren628(x1) ren629(x1) ren630(x1) ren631(x1) ren632(x1) ren633(x1) ren634(x1) ren635(x2,x0) ren636(x1) ren637(x1) ren638(x1) ren639(x1) ren640(x1) ren641(x1) ren642(x1) ren643(x1) ren644(x1) ren645(x1) ren646(x1) ren647(x1) ren648(x2,x0) ren649(x1) ren650(x1) ren651(x1) ren652(x1) ren653(x1) ren654(x1) ren655(x1) ren656(x1) ren657(x1) ren658(x1) ren659(x1) ren660(x1) ren661(x2,x0) ren662(x1) ren663(x1) ren664(x1) ren665(x1) ren666(x1) ren667(x1) ren668(x1) ren669(x1) ren670(x1) ren671(x1) ren672(x1) ren673(x1) ren674(x2,x0) ren675(x1) ren676(x1) ren677(x1) ren678(x1) ren679(x1) ren680(x1) ren681(x1) ren682(x1) ren683(x1) ren684(x1) ren685(x1) ren686(x1) ren687(x2,x0) ren688(x1) ren689(x1) ren690(x1) ren691(x1) ren692(x1) ren693(x1) ren694(x1) ren696(x0) ren695(x1) ren697(x1) ren698(x1) ren699(x1) ren700(x1) ren701(x1) ren702(x1) ren703(x1) ren704(x1) ren705(x1) ren706(x1) ren707(x1) ren708(x1) ren709(x1) ren710(x2,x0) ren711(x1) ren712(x1) ren713(x1) ren714(x1) ren715(x1) ren716(x1) ren717(x1) ren718(x1) ren719(x1) ren720(x1) ren721(x1) ren722(x1) ren723(x2,x0) ren724(x1) ren725(x1) ren726(x1) ren727(x1) ren728(x1) ren729(x1) ren730(x1) ren731(x1) ren732(x1) ren733(x1) ren734(x1) ren735(x1) ren736(x2,x0) ren737(x1) ren738(x1) ren739(x1) ren740(x1) ren741(x1) ren742(x1) ren743(x1) ren744(x1) ren745(x1) ren746(x1) ren747(x1) ren748(x1) ren749(x2,x0) ren750(x1) ren751(x1) ren752(x1) ren753(x1) ren754(x1) ren755(x1) ren756(x1) ren757(x1) ren758(x1) ren759(x1) ren760(x1) ren761(x1) ren762(x2,x0) ren763(x1) ren764(x1) ren765(x1) ren766(x1) ren767(x1) ren768(x1) ren769(x1) ren770(x1) ren771(x1) ren772(x1) ren773(x1) ren774(x1) ren775(x2,x0) ren776(x1) ren777(x1) ren778(x1) ren779(x1) ren780(x1) ren781(x1) ren782(x1) ren783(x1) ren784(x1) ren785(x1) ren786(x1) ren787(x1) ren788(x2,x0) ren789(x1) ren790(x1) ren791(x1) ren792(x1) ren793(x1) ren794(x1) ren795(x1) ren796(x1) ren797(x1) ren798(x1) ren799(x1) ren800(x1) ren801(x2,x0) ren802(x1) ren803(x1) ren804(x1) ren805(x1) ren806(x1) ren807(x1) ren808(x1) ren809(x1) ren810(x1) ren811(x1) ren812(x1) ren813(x1) ren814(x2,x0) ren815(x1) ren816(x1) ren817(x1) ren818(x1) ren819(x1) ren820(x1) ren821(x1) ren822(x1) ren823(x1) ren824(x1) ren825(x1) ren826(x1) ren827(x2,x0) ren828(x1) ren829(x1) ren830(x1) ren831(x1) ren832(x1) ren833(x1) ren835(x0) ren834(x1) ren836(x1) ren837(x1) ren838(x1) ren839(x1) ren840(x1) ren841(x1) ren842(x1) ren843(x1) ren844(x1) ren845(x1) ren846(x1) ren847(x1) ren848(x1) ren849(x2,x0) ren850(x1) ren851(x1) ren852(x1) ren853(x1) ren854(x1) ren855(x1) ren856(x1) ren857(x1) ren858(x1) ren859(x1) ren860(x1) ren861(x1) ren862(x2,x0) ren863(x1) ren864(x1) ren865(x1) ren866(x1) ren867(x1) ren868(x1) ren869(x1) ren870(x1) ren871(x1) ren872(x1) ren873(x1) ren874(x1) ren875(x2,x0) ren876(x1) ren877(x1) ren878(x1) ren879(x1) ren880(x1) ren881(x1) ren882(x1) ren883(x1) ren884(x1) ren885(x1) ren886(x1) ren887(x1) ren888(x2,x0) ren889(x1) ren890(x1) ren891(x1) ren892(x1) ren893(x1) ren894(x1) ren895(x1) ren896(x1) ren897(x1) ren898(x1) ren899(x1) ren900(x1) ren901(x2,x0) ren902(x1) ren903(x1) ren904(x1) ren905(x1) ren906(x1) ren907(x1) ren908(x1) ren909(x1) ren910(x1) ren911(x1) ren912(x1) ren913(x1) ren914(x2,x0) ren915(x1) ren916(x1) ren917(x1) ren918(x1) ren919(x1) ren920(x1) ren921(x1) ren922(x1) ren923(x1) ren924(x1) ren925(x1) ren926(x1) ren927(x2,x0) ren928(x1) ren929(x1) ren930(x1) ren931(x1) ren932(x1) ren933(x1) ren934(x1) ren935(x1) ren936(x1) ren937(x1) ren938(x1) ren939(x1) ren940(x2,x0) ren941(x1) ren942(x1) ren943(x1) ren944(x1) ren945(x1) ren946(x1) ren947(x1) ren948(x1) ren949(x1) ren950(x1) ren951(x1) ren952(x1) ren953(x2,x0) ren954(x1) ren955(x1) ren956(x1) ren957(x1) ren958(x1) ren960(x0) ren959(x1) ren961(x1) ren962(x1) ren963(x1) ren964(x1) ren965(x1) ren966(x1) ren967(x1) ren968(x1) ren969(x1) ren970(x1) ren971(x1) ren972(x1) ren973(x1) ren974(x2,x0) ren975(x1) ren976(x1) ren977(x1) ren978(x1) ren979(x1) ren980(x1) ren981(x1) ren982(x1) ren983(x1) ren984(x1) ren985(x1) ren986(x1) ren987(x2,x0) ren988(x1) ren989(x1) ren990(x1) ren991(x1) ren992(x1) ren993(x1) ren994(x1) ren995(x1) ren996(x1) ren997(x1) ren998(x1) ren999(x1) ren1000(x2,x0) ren1001(x1) ren1002(x1) ren1003(x1) ren1004(x1) ren1005(x1) ren1006(x1) ren1007(x1) ren1008(x1) ren1009(x1) ren1010(x1) ren1011(x1) ren1012(x1) ren1013(x2,x0) ren1014(x1) ren1015(x1) ren1016(x1) ren1017(x1) ren1018(x1) ren1019(x1) ren1020(x1) ren1021(x1) ren1022(x1) ren1023(x1) ren1024(x1) ren1025(x1) ren1026(x2,x0) ren1027(x1) ren1028(x1) ren1029(x1) ren1030(x1) ren1031(x1) ren1032(x1) ren1033(x1) ren1034(x1) ren1035(x1) ren1036(x1) ren1037(x1) ren1038(x1) ren1039(x2,x0) ren1040(x1) ren1041(x1) ren1042(x1) ren1043(x1) ren1044(x1) ren1045(x1) ren1046(x1) ren1047(x1) ren1048(x1) ren1049(x1) ren1050(x1) ren1051(x1) ren1052(x2,x0) ren1053(x1) ren1054(x1) ren1055(x1) ren1056(x1) ren1057(x1) ren1058(x1) ren1059(x1) ren1060(x1) ren1061(x1) ren1062(x1) ren1063(x1) ren1064(x1) ren1065(x2,x0) ren1066(x1) ren1067(x1) ren1068(x1) ren1069(x1) ren1071(x0) ren1070(x1) ren1072(x1) ren1073(x1) ren1074(x1) ren1075(x1) ren1076(x1) ren1077(x1) ren1078(x1) ren1079(x1) ren1080(x1) ren1081(x1) ren1082(x1) ren1083(x1) ren1084(x1) ren1085(x2,x0) ren1086(x1) ren1087(x1) ren1088(x1) ren1089(x1) ren1090(x1) ren1091(x1) ren1092(x1) ren1093(x1) ren1094(x1) ren1095(x1) ren1096(x1) ren1097(x1) ren1098(x2,x0) ren1099(x1) ren1100(x1) ren1101(x1) ren1102(x1) ren1103(x1) ren1104(x1) ren1105(x1) ren1106(x1) ren1107(x1) ren1108(x1) ren1109(x1) ren1110(x1) ren1111(x2,x0) ren1112(x1) ren1113(x1) ren1114(x1) ren1115(x1) ren1116(x1) ren1117(x1) ren1118(x1) ren1119(x1) ren1120(x1) ren1121(x1) ren1122(x1) ren1123(x1) ren1124(x2,x0) ren1125(x1) ren1126(x1) ren1127(x1) ren1128(x1) ren1129(x1) ren1130(x1) ren1131(x1) ren1132(x1) ren1133(x1) ren1134(x1) ren1135(x1) ren1136(x1) ren1137(x2,x0) ren1138(x1) ren1139(x1) ren1140(x1) ren1141(x1) ren1142(x1) ren1143(x1) ren1144(x1) ren1145(x1) ren1146(x1) ren1147(x1) ren1148(x1) ren1149(x1) ren1150(x2,x0) ren1151(x1) ren1152(x1) ren1153(x1) ren1154(x1) ren1155(x1) ren1156(x1) ren1157(x1) ren1158(x1) ren1159(x1) ren1160(x1) ren1161(x1) ren1162(x1) ren1163(x2,x0) ren1164(x1) ren1165(x1) ren1166(x1) ren1168(x0) ren1167(x1) ren1169(x1) ren1170(x1) ren1171(x1) ren1172(x1) ren1173(x1) ren1174(x1) ren1175(x1) ren1176(x1) ren1177(x1) ren1178(x1) ren1179(x1) ren1180(x1) ren1181(x1) ren1182(x2,x0) ren1183(x1) ren1184(x1) ren1185(x1) ren1186(x1) ren1187(x1) ren1188(x1) ren1189(x1) ren1190(x1) ren1191(x1) ren1192(x1) ren1193(x1) ren1194(x1) ren1195(x2,x0) ren1196(x1) ren1197(x1) ren1198(x1) ren1199(x1) ren1200(x1) ren1201(x1) ren1202(x1) ren1203(x1) ren1204(x1) ren1205(x1) ren1206(x1) ren1207(x1) ren1208(x2,x0) ren1209(x1) ren1210(x1) ren1211(x1) ren1212(x1) ren1213(x1) ren1214(x1) ren1215(x1) ren1216(x1) ren1217(x1) ren1218(x1) ren1219(x1) ren1220(x1) ren1221(x2,x0) ren1222(x1) ren1223(x1) ren1224(x1) ren1225(x1) ren1226(x1) ren1227(x1) ren1228(x1) ren1229(x1) ren1230(x1) ren1231(x1) ren1232(x1) ren1233(x1) ren1234(x2,x0) ren1235(x1) ren1236(x1) ren1237(x1) ren1238(x1) ren1239(x1) ren1240(x1) ren1241(x1) ren1242(x1) ren1243(x1) ren1244(x1) ren1245(x1) ren1246(x1) ren1247(x2,x0) ren1248(x1) ren1249(x1) ren1251(x0) ren1250(x1) ren1252(x1) ren1253(x1) ren1254(x1) ren1255(x1) ren1256(x1) ren1257(x1) ren1258(x1) ren1259(x1) ren1260(x1) ren1261(x1) ren1262(x1) ren1263(x1) ren1264(x1) ren1265(x2,x0) ren1266(x1) ren1267(x1) ren1268(x1) ren1269(x1) ren1270(x1) ren1271(x1) ren1272(x1) ren1273(x1) ren1274(x1) ren1275(x1) ren1276(x1) ren1277(x1) ren1278(x2,x0) ren1279(x1) ren1280(x1) ren1281(x1) ren1282(x1) ren1283(x1) ren1284(x1) ren1285(x1) ren1286(x1) ren1287(x1) ren1288(x1) ren1289(x1) ren1290(x1) ren1291(x2,x0) ren1292(x1) ren1293(x1) ren1294(x1) ren1295(x1) ren1296(x1) ren1297(x1) ren1298(x1) ren1299(x1) ren1300(x1) ren1301(x1) ren1302(x1) ren1303(x1) ren1304(x2,x0) ren1305(x1) ren1306(x1) ren1307(x1) ren1308(x1) ren1309(x1) ren1310(x1) ren1311(x1) ren1312(x1) ren1313(x1) ren1314(x1) ren1315(x1) ren1316(x1) ren1317(x2,x0) ren1318(x1) ren1320(x0) ren1319(x1) ren1321(x1) ren1322(x1) ren1323(x1) ren1324(x1) ren1325(x1) ren1326(x1) ren1327(x1) ren1328(x1) ren1329(x1) ren1330(x1) ren1331(x1) ren1332(x1) ren1333(x1) ren1334(x2,x0) ren1335(x1) ren1336(x1) ren1337(x1) ren1338(x1) ren1339(x1) ren1340(x1) ren1341(x1) ren1342(x1) ren1343(x1) ren1344(x1) ren1345(x1) ren1346(x1) ren1347(x2,x0) ren1348(x1) ren1349(x1) ren1350(x1) ren1351(x1) ren1352(x1) ren1353(x1) ren1354(x1) ren1355(x1) ren1356(x1) ren1357(x1) ren1358(x1) ren1359(x1) ren1360(x2,x0) ren1361(x1) ren1362(x1) ren1363(x1) ren1364(x1) ren1365(x1) ren1366(x1) ren1367(x1) ren1368(x1) ren1369(x1) ren1370(x1) ren1371(x1) ren1372(x1) ren1373(x2,x0) ren1375(x0) ren1374(x1) ren1376(x1) ren1377(x1) ren1378(x1) ren1379(x1) ren1380(x1) ren1381(x1) ren1382(x1) ren1383(x1) ren1384(x1) ren1385(x1) ren1386(x1) ren1387(x1) ren1388(x1) ren1389(x2,x0) ren1390(x1) ren1391(x1) ren1392(x1) ren1393(x1) ren1394(x1) ren1395(x1) ren1396(x1) ren1397(x1) ren1398(x1) ren1399(x1) ren1400(x1) ren1401(x1) ren1402(x2,x0) ren1403(x1) ren1404(x1) ren1405(x1) ren1406(x1) ren1407(x1) ren1408(x1) ren1409(x1) ren1410(x1) ren1411(x1) ren1412(x1) ren1413(x1) ren1414(x1) ren1415(x2,x0) ren1416(x0) ren1417(x1) ren1418(x1) ren1419(x1) ren1420(x1) ren1421(x1) ren1422(x1) ren1423(x1) ren1424(x1) ren1425(x1) ren1426(x1) ren1427(x1) ren1428(x1) ren1429(x1) ren1430(x2,x0) ren1431(x1) ren1432(x1) ren1433(x1) ren1434(x1) ren1435(x1) ren1436(x1) ren1437(x1) ren1438(x1) ren1439(x1) ren1440(x1) ren1441(x1) ren1442(x1) ren1443(x2,x0) ren1444(x1) ren1445(x1) ren1446(x1) ren1447(x1) ren1448(x1) ren1449(x1) ren1450(x1) ren1451(x1) ren1452(x1) ren1453(x1) ren1454(x1) ren1455(x1) ren1456(x1) ren1457(x2,x0) % 3.27/1.52 % 3.27/1.52 === Starting SPASS-SCL-FOL A Little Less Naive, considering 52 atoms initially, heuristics mode: resolution_1 === % 3.27/1.52 % 3.27/1.52 === Backtracking. Learning clause 3051:5:3:[30.2,33.3]:TopTopTop: p2(skf1(x0)),r1(x1,x2),r1(x2,x0) -> p1(x2),ren15(x1) % 3.27/1.52 === Backtracking. Learning clause 3052:5:3:[29.2,33.3]:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x2,skf1(x2)),p1(x1),ren15(x0) % 3.27/1.52 === Backtracking. Learning clause 3053:3:2:[57.2,60.2]:TopTop: p2(skf2(x0)),r1(x1,x0) -> ren28(x1) % 3.27/1.52 === Backtracking. Learning clause 3054:3:2:[56.2,60.2]:TopTop: r1(x0,x1) -> r1(x1,skf2(x1)),ren28(x0) % 3.27/1.52 === Backtracking. Learning clause 3055:3:2:[84.2,87.2]:TopTop: p2(skf3(x0)),r1(x1,x0) -> ren41(x1) % 3.27/1.52 === Backtracking. Learning clause 3056:3:2:[83.2,87.2]:TopTop: r1(x0,x1) -> r1(x1,skf3(x1)),ren41(x0) % 3.27/1.52 % 3.27/1.52 Linear Model Building succeeded. % 3.27/1.52 SZS status Satisfiable % 3.27/1.52 % 3.27/1.52 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 3.27/1.52 % 3.27/1.52 SPASS-SCL-FOL Statistics: % 3.27/1.52 Number of learned clauses: 6 % 3.27/1.52 Number of propagations: 38 % 3.27/1.52 Number of decisions: 80 % 3.27/1.52 Number of resolutions: 6 % 3.27/1.52 Number of condensations: 0 % 3.27/1.52 Number of sub resolutions: 1 % 3.27/1.52 Number of input literals (deduplicated): 1569 % 3.27/1.52 Number of grows: 0 % 3.27/1.52 Number of considered ground atoms: 52 % 3.27/1.52 % 3.27/1.52 Needed: 0:00:00.99 % 3.27/1.52 %------------------------------------------------------------------------------