%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SYN425+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n014.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 : 600s % DateTime : Thu Jul 21 03:02:12 EDT 2022 % Result : CounterSatisfiable 5.52s 5.71s % Output : FiniteModel 5.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYN425+1 : TPTP v8.1.0. Released v2.1.0. % 0.04/0.13 % Command : do_Crossbow---0.1 %s % 0.12/0.33 % Computer : n014.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jul 12 04:38:34 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 /export/starexec/sandbox2/solver/bin % 0.12/0.34 crossbow.opt % 0.12/0.34 do_Crossbow---0.1 % 0.12/0.34 eprover % 0.12/0.34 runsolver % 0.12/0.34 starexec_run_Crossbow---0.1 % 5.52/5.71 % SZS status CounterSatisfiable for theBenchmark.p % 5.52/5.71 % SZS output start FiniteModel for theBenchmark.p % 5.52/5.71 % domain size: 2 % 5.52/5.71 fof(interp, fi_domain, ![X] : (X = 0 | X = 1)). % 5.52/5.71 fof(interp, fi_functors, a1190 = 0). % 5.52/5.71 fof(interp, fi_functors, a1191 = 0). % 5.52/5.71 fof(interp, fi_functors, a1192 = 0). % 5.52/5.71 fof(interp, fi_functors, a1193 = 1). % 5.52/5.71 fof(interp, fi_functors, a1194 = 1). % 5.52/5.71 fof(interp, fi_functors, a1195 = 1). % 5.52/5.71 fof(interp, fi_functors, a1196 = 0). % 5.52/5.71 fof(interp, fi_functors, a1197 = 0). % 5.52/5.71 fof(interp, fi_functors, a1198 = 0). % 5.52/5.71 fof(interp, fi_functors, a1199 = 0). % 5.52/5.71 fof(interp, fi_functors, a1200 = 0). % 5.52/5.71 fof(interp, fi_functors, a1201 = 0). % 5.52/5.71 fof(interp, fi_functors, a1202 = 0). % 5.52/5.71 fof(interp, fi_functors, a1203 = 0). % 5.52/5.71 fof(interp, fi_functors, a1204 = 0). % 5.52/5.71 fof(interp, fi_functors, a1205 = 0). % 5.52/5.71 fof(interp, fi_functors, a1206 = 0). % 5.52/5.71 fof(interp, fi_functors, a1207 = 1). % 5.52/5.71 fof(interp, fi_functors, a1208 = 1). % 5.52/5.71 fof(interp, fi_functors, a1209 = 0). % 5.52/5.71 fof(interp, fi_functors, a1210 = 0). % 5.52/5.71 fof(interp, fi_functors, a1211 = 0). % 5.52/5.71 fof(interp, fi_functors, a1212 = 0). % 5.52/5.71 fof(interp, fi_functors, a1213 = 0). % 5.52/5.71 fof(interp, fi_functors, a1214 = 0). % 5.52/5.71 fof(interp, fi_functors, a1215 = 0). % 5.52/5.71 fof(interp, fi_functors, a1216 = 0). % 5.52/5.71 fof(interp, fi_functors, a1217 = 0). % 5.52/5.71 fof(interp, fi_functors, a1218 = 1). % 5.52/5.71 fof(interp, fi_functors, a1219 = 0). % 5.52/5.71 fof(interp, fi_functors, a1220 = 0). % 5.52/5.71 fof(interp, fi_functors, a1221 = 1). % 5.52/5.71 fof(interp, fi_functors, a1222 = 0). % 5.52/5.71 fof(interp, fi_functors, a1223 = 1). % 5.52/5.71 fof(interp, fi_functors, a1224 = 0). % 5.52/5.71 fof(interp, fi_functors, a1225 = 0). % 5.52/5.71 fof(interp, fi_functors, a1226 = 0). % 5.52/5.71 fof(interp, fi_functors, a1227 = 0). % 5.52/5.71 fof(interp, fi_functors, a1228 = 0). % 5.52/5.71 fof(interp, fi_functors, a1229 = 0). % 5.52/5.71 fof(interp, fi_functors, a1230 = 0). % 5.52/5.71 fof(interp, fi_functors, a1231 = 1). % 5.52/5.71 fof(interp, fi_functors, a1232 = 0). % 5.52/5.71 fof(interp, fi_functors, a1233 = 0). % 5.52/5.71 fof(interp, fi_functors, a1234 = 0). % 5.52/5.71 fof(interp, fi_functors, a1235 = 0). % 5.52/5.71 fof(interp, fi_functors, a1236 = 0). % 5.52/5.71 fof(interp, fi_functors, a1237 = 0). % 5.52/5.71 fof(interp, fi_functors, a1238 = 0). % 5.52/5.71 fof(interp, fi_functors, a1239 = 0). % 5.52/5.71 fof(interp, fi_functors, a1240 = 1). % 5.52/5.71 fof(interp, fi_functors, a1241 = 0). % 5.52/5.71 fof(interp, fi_functors, a1242 = 1). % 5.52/5.71 fof(interp, fi_functors, a1243 = 1). % 5.52/5.71 fof(interp, fi_functors, a1244 = 0). % 5.52/5.71 fof(interp, fi_functors, a1245 = 1). % 5.52/5.71 fof(interp, fi_functors, a1246 = 0). % 5.52/5.71 fof(interp, fi_functors, a1247 = 0). % 5.52/5.71 fof(interp, fi_functors, a1248 = 0). % 5.52/5.71 fof(interp, fi_functors, a1249 = 0). % 5.52/5.71 fof(interp, fi_functors, a1250 = 0). % 5.52/5.71 fof(interp, fi_functors, a1251 = 0). % 5.52/5.71 fof(interp, fi_functors, a1252 = 0). % 5.52/5.71 fof(interp, fi_functors, a1253 = 0). % 5.52/5.71 fof(interp, fi_functors, a1254 = 0). % 5.52/5.71 fof(interp, fi_functors, a1255 = 0). % 5.52/5.71 fof(interp, fi_functors, a1256 = 0). % 5.52/5.71 fof(interp, fi_functors, a1257 = 0). % 5.52/5.71 fof(interp, fi_functors, a1258 = 0). % 5.52/5.71 fof(interp, fi_functors, a1259 = 0). % 5.52/5.71 fof(interp, fi_functors, a1260 = 1). % 5.52/5.71 fof(interp, fi_functors, a1261 = 0). % 5.52/5.71 fof(interp, fi_functors, a1262 = 0). % 5.52/5.71 fof(interp, fi_functors, a1263 = 0). % 5.52/5.71 fof(interp, fi_functors, a1264 = 0). % 5.52/5.71 fof(interp, fi_functors, a1265 = 0). % 5.52/5.71 fof(interp, fi_functors, a1266 = 0). % 5.52/5.71 fof(interp, fi_functors, a1267 = 0). % 5.52/5.71 fof(interp, fi_functors, a1268 = 0). % 5.52/5.71 fof(interp, fi_functors, a1269 = 0). % 5.52/5.71 fof(interp, fi_functors, a1270 = 1). % 5.52/5.71 fof(interp, fi_functors, a1271 = 1). % 5.52/5.71 fof(interp, fi_functors, a1272 = 0). % 5.52/5.71 fof(interp, fi_functors, a1273 = 0). % 5.52/5.71 fof(interp, fi_functors, a1274 = 0). % 5.52/5.71 fof(interp, fi_functors, a1275 = 0). % 5.52/5.71 fof(interp, fi_functors, a1276 = 0). % 5.52/5.71 fof(interp, fi_functors, a1277 = 0). % 5.52/5.71 fof(interp, fi_functors, a1278 = 0). % 5.52/5.71 fof(interp, fi_functors, a1279 = 0). % 5.52/5.71 fof(interp, fi_functors, a1280 = 0). % 5.52/5.71 fof(interp, fi_functors, a1281 = 0). % 5.52/5.71 fof(interp, fi_functors, a1282 = 0). % 5.52/5.71 fof(interp, fi_functors, a1283 = 0). % 5.52/5.71 fof(interp, fi_functors, a1284 = 0). % 5.52/5.71 fof(interp, fi_functors, a1285 = 0). % 5.52/5.71 fof(interp, fi_functors, a1286 = 0). % 5.52/5.71 fof(interp, fi_functors, a1287 = 0). % 5.52/5.71 fof(interp, fi_functors, a1288 = 0). % 5.52/5.71 fof(interp, fi_functors, a1289 = 0). % 5.52/5.71 fof(interp, fi_functors, a1290 = 0). % 5.52/5.71 fof(interp, fi_functors, a1291 = 0). % 5.52/5.71 fof(interp, fi_functors, a1292 = 0). % 5.52/5.71 fof(interp, fi_functors, a1293 = 1). % 5.52/5.71 fof(interp, fi_functors, a1294 = 0). % 5.52/5.71 fof(interp, fi_functors, a1295 = 0). % 5.52/5.71 fof(interp, fi_functors, a1296 = 0). % 5.52/5.71 fof(interp, fi_functors, a1297 = 0). % 5.52/5.71 fof(interp, fi_functors, a1298 = 0). % 5.52/5.71 fof(interp, fi_functors, a1299 = 0). % 5.52/5.71 fof(interp, fi_functors, a1300 = 0). % 5.52/5.71 fof(interp, fi_functors, a1301 = 0). % 5.52/5.71 fof(interp, fi_functors, a1302 = 0). % 5.52/5.71 fof(interp, fi_functors, a1303 = 0). % 5.52/5.71 fof(interp, fi_functors, a1304 = 0). % 5.52/5.71 fof(interp, fi_functors, a1305 = 0). % 5.52/5.71 fof(interp, fi_functors, a1306 = 0). % 5.52/5.71 fof(interp, fi_functors, a1307 = 1). % 5.52/5.71 fof(interp, fi_functors, a1308 = 0). % 5.52/5.71 fof(interp, fi_functors, a1309 = 0). % 5.52/5.71 fof(interp, fi_functors, a1310 = 0). % 5.52/5.71 fof(interp, fi_functors, a1311 = 0). % 5.52/5.71 fof(interp, fi_functors, a1312 = 0). % 5.52/5.71 fof(interp, fi_functors, a1313 = 0). % 5.52/5.71 fof(interp, fi_functors, a1314 = 0). % 5.52/5.71 fof(interp, fi_functors, a1315 = 0). % 5.52/5.71 fof(interp, fi_functors, a1316 = 0). % 5.52/5.71 fof(interp, fi_functors, a1317 = 0). % 5.52/5.71 fof(interp, fi_functors, a1318 = 0). % 5.52/5.71 fof(interp, fi_functors, a1319 = 0). % 5.52/5.71 fof(interp, fi_functors, a1320 = 0). % 5.52/5.71 fof(interp, fi_functors, a1321 = 0). % 5.52/5.71 fof(interp, fi_functors, a1322 = 0). % 5.52/5.71 fof(interp, fi_functors, a1323 = 0). % 5.52/5.71 fof(interp, fi_functors, a1324 = 0). % 5.52/5.71 fof(interp, fi_functors, a1325 = 1). % 5.52/5.71 fof(interp, fi_functors, a1326 = 1). % 5.52/5.71 fof(interp, fi_functors, a1327 = 0). % 5.52/5.71 fof(interp, fi_functors, a1328 = 0). % 5.52/5.71 fof(interp, fi_functors, a1329 = 0). % 5.52/5.71 fof(interp, fi_functors, a1330 = 0). % 5.52/5.71 fof(interp, fi_functors, a1331 = 0). % 5.52/5.71 fof(interp, fi_functors, a1332 = 0). % 5.52/5.71 fof(interp, fi_functors, a1333 = 0). % 5.52/5.71 fof(interp, fi_functors, a1334 = 0). % 5.52/5.71 fof(interp, fi_functors, a1335 = 1). % 5.52/5.71 fof(interp, fi_functors, a1336 = 0). % 5.52/5.71 fof(interp, fi_functors, a1337 = 0). % 5.52/5.71 fof(interp, fi_functors, a1338 = 0). % 5.52/5.71 fof(interp, fi_functors, a1339 = 0). % 5.52/5.71 fof(interp, fi_functors, a1340 = 0). % 5.52/5.71 fof(interp, fi_functors, a1341 = 0). % 5.52/5.71 fof(interp, fi_functors, a1342 = 0). % 5.52/5.71 fof(interp, fi_functors, a1343 = 0). % 5.52/5.71 fof(interp, fi_functors, a1344 = 0). % 5.52/5.71 fof(interp, fi_functors, a1345 = 0). % 5.52/5.71 fof(interp, fi_functors, a1346 = 0). % 5.52/5.71 fof(interp, fi_functors, a1347 = 1). % 5.52/5.71 fof(interp, fi_functors, a1348 = 0). % 5.52/5.71 fof(interp, fi_functors, a1349 = 0). % 5.52/5.71 fof(interp, fi_functors, a1350 = 0). % 5.52/5.71 fof(interp, fi_functors, a1351 = 1). % 5.52/5.71 fof(interp, fi_functors, a1352 = 1). % 5.52/5.71 fof(interp, fi_functors, a1353 = 0). % 5.52/5.71 fof(interp, fi_functors, a1354 = 0). % 5.52/5.71 fof(interp, fi_functors, a1355 = 0). % 5.52/5.71 fof(interp, fi_functors, a1356 = 0). % 5.52/5.71 fof(interp, fi_functors, a1357 = 0). % 5.52/5.71 fof(interp, fi_functors, a1358 = 0). % 5.52/5.71 fof(interp, fi_functors, a1359 = 0). % 5.52/5.71 fof(interp, fi_functors, a1360 = 0). % 5.52/5.71 fof(interp, fi_functors, a1361 = 0). % 5.52/5.71 fof(interp, fi_functors, a1362 = 0). % 5.52/5.71 fof(interp, fi_functors, a1363 = 1). % 5.52/5.71 fof(interp, fi_functors, a1364 = 1). % 5.52/5.71 fof(interp, fi_predicates, ~c10_0). % 5.52/5.71 fof(interp, fi_predicates, ~c10_1(0) & ~c10_1(1)). % 5.52/5.71 fof(interp, fi_predicates, c10_2(0, 0) & c10_2(0, 1) & ~c10_2(1, 0) & % 5.52/5.71 ~c10_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, c1_0). % 5.52/5.71 fof(interp, fi_predicates, c1_1(0) & c1_1(1)). % 5.52/5.71 fof(interp, fi_predicates, c1_2(0, 0) & ~c1_2(0, 1) & ~c1_2(1, 0) & ~c1_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, c2_0). % 5.52/5.71 fof(interp, fi_predicates, ~c2_1(0) & c2_1(1)). % 5.52/5.71 fof(interp, fi_predicates, c2_2(0, 0) & ~c2_2(0, 1) & ~c2_2(1, 0) & c2_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, c3_0). % 5.52/5.71 fof(interp, fi_predicates, ~c3_1(0) & ~c3_1(1)). % 5.52/5.71 fof(interp, fi_predicates, c3_2(0, 0) & c3_2(0, 1) & c3_2(1, 0) & c3_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, c4_0). % 5.52/5.71 fof(interp, fi_predicates, ~c4_1(0) & ~c4_1(1)). % 5.52/5.71 fof(interp, fi_predicates, c4_2(0, 0) & ~c4_2(0, 1) & ~c4_2(1, 0) & c4_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, ~c5_0). % 5.52/5.71 fof(interp, fi_predicates, ~c5_1(0) & c5_1(1)). % 5.52/5.71 fof(interp, fi_predicates, ~c5_2(0, 0) & c5_2(0, 1) & c5_2(1, 0) & c5_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, ~c6_0). % 5.52/5.71 fof(interp, fi_predicates, c6_1(0) & ~c6_1(1)). % 5.52/5.71 fof(interp, fi_predicates, ~c6_2(0, 0) & c6_2(0, 1) & ~c6_2(1, 0) & ~c6_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, ~c7_0). % 5.52/5.71 fof(interp, fi_predicates, c7_1(0) & ~c7_1(1)). % 5.52/5.71 fof(interp, fi_predicates, c7_2(0, 0) & c7_2(0, 1) & c7_2(1, 0) & ~c7_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, c8_0). % 5.52/5.71 fof(interp, fi_predicates, ~c8_1(0) & ~c8_1(1)). % 5.52/5.71 fof(interp, fi_predicates, ~c8_2(0, 0) & c8_2(0, 1) & c8_2(1, 0) & c8_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, c9_0). % 5.52/5.71 fof(interp, fi_predicates, ~c9_1(0) & c9_1(1)). % 5.52/5.71 fof(interp, fi_predicates, c9_2(0, 0) & c9_2(0, 1) & ~c9_2(1, 0) & c9_2(1, 1)). % 5.52/5.71 fof(interp, fi_predicates, ~epred1_0). % 5.52/5.71 fof(interp, fi_predicates, epred2_0). % 5.52/5.71 fof(interp, fi_predicates, epred3_0). % 5.52/5.71 fof(interp, fi_predicates, ~epred4_0). % 5.52/5.71 fof(interp, fi_predicates, ~epred5_0). % 5.52/5.71 fof(interp, fi_predicates, epred6_0). % 5.52/5.71 fof(interp, fi_predicates, epred7_0). % 5.52/5.71 fof(interp, fi_predicates, ~epred8_0). % 5.52/5.71 fof(interp, fi_predicates, ndr1_0). % 5.52/5.71 fof(interp, fi_predicates, ndr1_1(0) & ndr1_1(1)). % 5.52/5.71 % SZS output end FiniteModel for theBenchmark.p % 5.52/5.71 % 6 lemma(s) from E % 5.52/5.71 % cnf(cl, axiom, ndr1_1(a1226)). % 5.52/5.71 % cnf(cl, axiom, c7_1(a1226)). % 5.52/5.71 % cnf(cl, axiom, ~c9_1(a1226)). % 5.52/5.71 % cnf(cl, axiom, ~c8_2(a1226, a1227)). % 5.52/5.71 % cnf(cl, axiom, ~c6_2(a1226, a1227)). % 5.52/5.71 % cnf(cl, axiom, ~c5_2(a1226, a1227)). % 5.52/5.71 % 1191 pred(s) % 5.52/5.71 % 175 func(s) % 5.52/5.71 % 2 sort(s) % 5.52/5.71 % 2564 clause(s) % 5.52/5.71 % Instantiating 1 (5251 ms) % 5.52/5.71 % Solving (5254 ms) % 5.52/5.71 % Instantiating 2 (5254 ms) % 5.52/5.71 % Solving (5261 ms) % 5.52/5.71 % % 5.52/5.71 % 1 model found (5263 ms) %------------------------------------------------------------------------------