%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SYN520+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n017.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:03:15 EDT 2022 % Result : CounterSatisfiable 5.52s 5.70s % Output : FiniteModel 5.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SYN520+1 : TPTP v8.1.0. Released v2.1.0. % 0.11/0.12 % Command : do_Crossbow---0.1 %s % 0.12/0.33 % Computer : n017.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 03:10:19 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 /export/starexec/sandbox/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.70 % SZS status CounterSatisfiable for theBenchmark.p % 5.52/5.70 % SZS output start FiniteModel for theBenchmark.p % 5.52/5.70 % domain size: 3 % 5.52/5.70 fof(interp, fi_domain, ![X] : (X = 0 | X = 1 | X = 2)). % 5.52/5.70 fof(interp, fi_functors, a1323 = 0). % 5.52/5.70 fof(interp, fi_functors, a1324 = 0). % 5.52/5.70 fof(interp, fi_functors, a1325 = 1). % 5.52/5.70 fof(interp, fi_functors, a1326 = 0). % 5.52/5.70 fof(interp, fi_functors, a1327 = 0). % 5.52/5.70 fof(interp, fi_functors, a1328 = 0). % 5.52/5.70 fof(interp, fi_functors, a1329 = 0). % 5.52/5.70 fof(interp, fi_functors, a1330 = 0). % 5.52/5.70 fof(interp, fi_functors, a1331 = 0). % 5.52/5.70 fof(interp, fi_functors, a1332 = 0). % 5.52/5.70 fof(interp, fi_functors, a1333 = 2). % 5.52/5.70 fof(interp, fi_functors, a1334 = 2). % 5.52/5.70 fof(interp, fi_functors, a1335 = 1). % 5.52/5.70 fof(interp, fi_functors, a1336 = 2). % 5.52/5.70 fof(interp, fi_functors, a1337 = 1). % 5.52/5.70 fof(interp, fi_functors, a1338 = 1). % 5.52/5.70 fof(interp, fi_functors, a1339 = 1). % 5.52/5.70 fof(interp, fi_functors, a1340 = 0). % 5.52/5.70 fof(interp, fi_functors, a1341 = 2). % 5.52/5.70 fof(interp, fi_functors, a1342 = 1). % 5.52/5.70 fof(interp, fi_functors, a1343 = 2). % 5.52/5.70 fof(interp, fi_functors, a1344 = 1). % 5.52/5.70 fof(interp, fi_functors, a1345 = 1). % 5.52/5.70 fof(interp, fi_functors, a1346 = 0). % 5.52/5.70 fof(interp, fi_functors, a1347 = 0). % 5.52/5.70 fof(interp, fi_functors, a1348 = 0). % 5.52/5.70 fof(interp, fi_functors, a1349 = 0). % 5.52/5.70 fof(interp, fi_functors, a1350 = 2). % 5.52/5.70 fof(interp, fi_functors, a1351 = 0). % 5.52/5.70 fof(interp, fi_functors, a1352 = 0). % 5.52/5.70 fof(interp, fi_functors, a1353 = 0). % 5.52/5.70 fof(interp, fi_functors, a1354 = 0). % 5.52/5.70 fof(interp, fi_functors, a1355 = 0). % 5.52/5.70 fof(interp, fi_functors, a1356 = 1). % 5.52/5.70 fof(interp, fi_functors, a1357 = 2). % 5.52/5.70 fof(interp, fi_functors, a1358 = 1). % 5.52/5.70 fof(interp, fi_functors, a1359 = 1). % 5.52/5.70 fof(interp, fi_functors, a1360 = 1). % 5.52/5.70 fof(interp, fi_functors, a1361 = 1). % 5.52/5.70 fof(interp, fi_functors, a1362 = 0). % 5.52/5.70 fof(interp, fi_functors, a1363 = 2). % 5.52/5.70 fof(interp, fi_functors, a1364 = 0). % 5.52/5.70 fof(interp, fi_functors, a1365 = 1). % 5.52/5.70 fof(interp, fi_functors, a1366 = 0). % 5.52/5.70 fof(interp, fi_functors, a1367 = 1). % 5.52/5.70 fof(interp, fi_functors, a1368 = 1). % 5.52/5.70 fof(interp, fi_functors, a1369 = 0). % 5.52/5.70 fof(interp, fi_functors, a1370 = 1). % 5.52/5.70 fof(interp, fi_functors, a1371 = 2). % 5.52/5.70 fof(interp, fi_functors, a1372 = 0). % 5.52/5.70 fof(interp, fi_functors, a1373 = 0). % 5.52/5.70 fof(interp, fi_functors, a1374 = 0). % 5.52/5.70 fof(interp, fi_functors, a1375 = 0). % 5.52/5.70 fof(interp, fi_functors, a1376 = 0). % 5.52/5.70 fof(interp, fi_functors, a1377 = 0). % 5.52/5.70 fof(interp, fi_functors, a1378 = 1). % 5.52/5.70 fof(interp, fi_functors, a1379 = 0). % 5.52/5.70 fof(interp, fi_functors, a1380 = 0). % 5.52/5.70 fof(interp, fi_functors, a1381 = 0). % 5.52/5.70 fof(interp, fi_functors, a1382 = 0). % 5.52/5.70 fof(interp, fi_functors, a1383 = 0). % 5.52/5.70 fof(interp, fi_functors, a1384 = 0). % 5.52/5.70 fof(interp, fi_functors, a1385 = 0). % 5.52/5.70 fof(interp, fi_functors, a1386 = 2). % 5.52/5.70 fof(interp, fi_functors, a1387 = 0). % 5.52/5.70 fof(interp, fi_functors, a1388 = 2). % 5.52/5.70 fof(interp, fi_functors, a1389 = 2). % 5.52/5.70 fof(interp, fi_functors, a1390 = 1). % 5.52/5.70 fof(interp, fi_functors, a1391 = 2). % 5.52/5.70 fof(interp, fi_functors, a1392 = 0). % 5.52/5.70 fof(interp, fi_functors, a1393 = 2). % 5.52/5.70 fof(interp, fi_functors, a1394 = 2). % 5.52/5.70 fof(interp, fi_functors, a1395 = 2). % 5.52/5.70 fof(interp, fi_functors, a1396 = 0). % 5.52/5.70 fof(interp, fi_functors, a1397 = 0). % 5.52/5.70 fof(interp, fi_functors, a1398 = 0). % 5.52/5.70 fof(interp, fi_functors, a1399 = 0). % 5.52/5.70 fof(interp, fi_functors, a1400 = 0). % 5.52/5.70 fof(interp, fi_functors, a1401 = 0). % 5.52/5.70 fof(interp, fi_functors, a1402 = 0). % 5.52/5.70 fof(interp, fi_functors, a1403 = 0). % 5.52/5.70 fof(interp, fi_functors, a1404 = 0). % 5.52/5.70 fof(interp, fi_functors, a1405 = 0). % 5.52/5.70 fof(interp, fi_functors, a1406 = 0). % 5.52/5.70 fof(interp, fi_functors, a1407 = 2). % 5.52/5.70 fof(interp, fi_functors, a1408 = 2). % 5.52/5.70 fof(interp, fi_functors, a1409 = 2). % 5.52/5.70 fof(interp, fi_functors, a1410 = 2). % 5.52/5.70 fof(interp, fi_functors, a1411 = 1). % 5.52/5.70 fof(interp, fi_functors, a1412 = 1). % 5.52/5.70 fof(interp, fi_functors, a1413 = 0). % 5.52/5.70 fof(interp, fi_functors, a1414 = 2). % 5.52/5.70 fof(interp, fi_functors, a1415 = 0). % 5.52/5.70 fof(interp, fi_functors, a1416 = 0). % 5.52/5.70 fof(interp, fi_functors, a1417 = 0). % 5.52/5.70 fof(interp, fi_functors, a1418 = 0). % 5.52/5.70 fof(interp, fi_functors, a1419 = 0). % 5.52/5.70 fof(interp, fi_functors, a1420 = 1). % 5.52/5.70 fof(interp, fi_functors, a1421 = 2). % 5.52/5.70 fof(interp, fi_functors, a1422 = 1). % 5.52/5.70 fof(interp, fi_functors, a1423 = 1). % 5.52/5.70 fof(interp, fi_functors, a1424 = 1). % 5.52/5.70 fof(interp, fi_functors, a1425 = 1). % 5.52/5.70 fof(interp, fi_functors, a1426 = 0). % 5.52/5.70 fof(interp, fi_functors, a1427 = 0). % 5.52/5.70 fof(interp, fi_functors, a1428 = 0). % 5.52/5.70 fof(interp, fi_functors, a1429 = 1). % 5.52/5.70 fof(interp, fi_functors, a1430 = 1). % 5.52/5.70 fof(interp, fi_functors, a1431 = 1). % 5.52/5.70 fof(interp, fi_functors, a1432 = 0). % 5.52/5.70 fof(interp, fi_functors, a1433 = 1). % 5.52/5.70 fof(interp, fi_functors, a1434 = 1). % 5.52/5.70 fof(interp, fi_functors, a1435 = 0). % 5.52/5.70 fof(interp, fi_functors, a1436 = 2). % 5.52/5.70 fof(interp, fi_functors, a1437 = 0). % 5.52/5.70 fof(interp, fi_functors, a1438 = 2). % 5.52/5.70 fof(interp, fi_functors, a1439 = 0). % 5.52/5.70 fof(interp, fi_functors, a1440 = 0). % 5.52/5.70 fof(interp, fi_functors, a1441 = 2). % 5.52/5.70 fof(interp, fi_functors, a1442 = 0). % 5.52/5.70 fof(interp, fi_functors, a1443 = 1). % 5.52/5.70 fof(interp, fi_functors, a1444 = 2). % 5.52/5.70 fof(interp, fi_functors, a1445 = 0). % 5.52/5.70 fof(interp, fi_functors, a1446 = 1). % 5.52/5.70 fof(interp, fi_functors, a1447 = 0). % 5.52/5.70 fof(interp, fi_functors, a1448 = 0). % 5.52/5.70 fof(interp, fi_functors, a1449 = 0). % 5.52/5.70 fof(interp, fi_functors, a1450 = 2). % 5.52/5.70 fof(interp, fi_functors, a1451 = 0). % 5.52/5.70 fof(interp, fi_functors, a1452 = 1). % 5.52/5.70 fof(interp, fi_functors, a1453 = 0). % 5.52/5.70 fof(interp, fi_functors, a1454 = 1). % 5.52/5.70 fof(interp, fi_functors, a1455 = 0). % 5.52/5.70 fof(interp, fi_functors, a1456 = 1). % 5.52/5.70 fof(interp, fi_functors, a1457 = 2). % 5.52/5.70 fof(interp, fi_functors, a1458 = 0). % 5.52/5.70 fof(interp, fi_functors, a1459 = 1). % 5.52/5.70 fof(interp, fi_functors, a1460 = 1). % 5.52/5.70 fof(interp, fi_functors, a1461 = 0). % 5.52/5.70 fof(interp, fi_functors, a1462 = 0). % 5.52/5.70 fof(interp, fi_functors, a1463 = 0). % 5.52/5.70 fof(interp, fi_functors, a1464 = 0). % 5.52/5.70 fof(interp, fi_functors, a1465 = 0). % 5.52/5.70 fof(interp, fi_functors, a1466 = 0). % 5.52/5.70 fof(interp, fi_functors, a1467 = 0). % 5.52/5.70 fof(interp, fi_functors, a1468 = 0). % 5.52/5.70 fof(interp, fi_functors, a1469 = 1). % 5.52/5.70 fof(interp, fi_functors, a1470 = 1). % 5.52/5.70 fof(interp, fi_functors, a1471 = 0). % 5.52/5.70 fof(interp, fi_functors, a1472 = 2). % 5.52/5.70 fof(interp, fi_functors, a1473 = 0). % 5.52/5.70 fof(interp, fi_functors, a1474 = 1). % 5.52/5.70 fof(interp, fi_functors, a1475 = 1). % 5.52/5.70 fof(interp, fi_functors, a1476 = 0). % 5.52/5.70 fof(interp, fi_functors, a1477 = 0). % 5.52/5.70 fof(interp, fi_functors, a1478 = 0). % 5.52/5.70 fof(interp, fi_functors, a1479 = 0). % 5.52/5.70 fof(interp, fi_functors, a1480 = 0). % 5.52/5.70 fof(interp, fi_functors, a1481 = 0). % 5.52/5.70 fof(interp, fi_functors, a1482 = 1). % 5.52/5.70 fof(interp, fi_functors, a1483 = 2). % 5.52/5.70 fof(interp, fi_functors, a1484 = 1). % 5.52/5.70 fof(interp, fi_functors, a1485 = 0). % 5.52/5.70 fof(interp, fi_functors, a1486 = 0). % 5.52/5.70 fof(interp, fi_functors, a1487 = 0). % 5.52/5.70 fof(interp, fi_functors, a1488 = 1). % 5.52/5.70 fof(interp, fi_functors, a1489 = 2). % 5.52/5.70 fof(interp, fi_functors, a1490 = 0). % 5.52/5.70 fof(interp, fi_functors, a1491 = 1). % 5.52/5.70 fof(interp, fi_functors, a1492 = 0). % 5.52/5.70 fof(interp, fi_functors, a1493 = 1). % 5.52/5.70 fof(interp, fi_functors, a1494 = 0). % 5.52/5.70 fof(interp, fi_functors, a1495 = 0). % 5.52/5.70 fof(interp, fi_functors, a1496 = 0). % 5.52/5.70 fof(interp, fi_functors, a1497 = 0). % 5.52/5.70 fof(interp, fi_functors, a1498 = 1). % 5.52/5.70 fof(interp, fi_functors, a1499 = 1). % 5.52/5.70 fof(interp, fi_functors, a1500 = 2). % 5.52/5.70 fof(interp, fi_functors, a1501 = 2). % 5.52/5.70 fof(interp, fi_functors, a1502 = 0). % 5.52/5.70 fof(interp, fi_functors, a1503 = 2). % 5.52/5.70 fof(interp, fi_functors, a1504 = 2). % 5.52/5.70 fof(interp, fi_functors, a1505 = 1). % 5.52/5.70 fof(interp, fi_functors, a1506 = 0). % 5.52/5.70 fof(interp, fi_functors, a1507 = 2). % 5.52/5.70 fof(interp, fi_functors, a1508 = 0). % 5.52/5.70 fof(interp, fi_functors, a1509 = 1). % 5.52/5.70 fof(interp, fi_functors, a1510 = 1). % 5.52/5.70 fof(interp, fi_functors, a1511 = 2). % 5.52/5.70 fof(interp, fi_functors, a1512 = 0). % 5.52/5.70 fof(interp, fi_functors, a1513 = 0). % 5.52/5.70 fof(interp, fi_functors, a1514 = 0). % 5.52/5.70 fof(interp, fi_functors, a1515 = 1). % 5.52/5.70 fof(interp, fi_functors, a1516 = 2). % 5.52/5.70 fof(interp, fi_functors, a1517 = 0). % 5.52/5.70 fof(interp, fi_functors, a1518 = 0). % 5.52/5.70 fof(interp, fi_functors, a1519 = 1). % 5.52/5.70 fof(interp, fi_functors, a1520 = 0). % 5.52/5.70 fof(interp, fi_functors, a1521 = 0). % 5.52/5.70 fof(interp, fi_functors, a1522 = 1). % 5.52/5.70 fof(interp, fi_functors, a1523 = 2). % 5.52/5.70 fof(interp, fi_functors, a1524 = 2). % 5.52/5.70 fof(interp, fi_functors, a1525 = 0). % 5.52/5.70 fof(interp, fi_functors, a1526 = 1). % 5.52/5.70 fof(interp, fi_predicates, ~c1_0). % 5.52/5.70 fof(interp, fi_predicates, c1_1(0) & ~c1_1(1) & c1_1(2)). % 5.52/5.70 fof(interp, fi_predicates, c1_2(0, 0) & c1_2(0, 1) & ~c1_2(0, 2) & ~c1_2(1, 0) & % 5.52/5.70 ~c1_2(1, 1) & % 5.52/5.70 c1_2(1, 2) & % 5.52/5.70 c1_2(2, 0) & % 5.52/5.70 c1_2(2, 1) & % 5.52/5.70 ~c1_2(2, 2)). % 5.52/5.70 fof(interp, fi_predicates, ~c2_0). % 5.52/5.70 fof(interp, fi_predicates, c2_1(0) & c2_1(1) & ~c2_1(2)). % 5.52/5.70 fof(interp, fi_predicates, c2_2(0, 0) & c2_2(0, 1) & ~c2_2(0, 2) & c2_2(1, 0) & % 5.52/5.70 c2_2(1, 1) & % 5.52/5.70 ~c2_2(1, 2) & % 5.52/5.70 ~c2_2(2, 0) & % 5.52/5.70 ~c2_2(2, 1) & % 5.52/5.70 c2_2(2, 2)). % 5.52/5.70 fof(interp, fi_predicates, c3_0). % 5.52/5.70 fof(interp, fi_predicates, c3_1(0) & ~c3_1(1) & ~c3_1(2)). % 5.52/5.70 fof(interp, fi_predicates, c3_2(0, 0) & ~c3_2(0, 1) & c3_2(0, 2) & c3_2(1, 0) & % 5.52/5.70 c3_2(1, 1) & % 5.52/5.70 c3_2(1, 2) & % 5.52/5.70 ~c3_2(2, 0) & % 5.52/5.70 ~c3_2(2, 1) & % 5.52/5.70 c3_2(2, 2)). % 5.52/5.70 fof(interp, fi_predicates, ~c4_0). % 5.52/5.70 fof(interp, fi_predicates, ~c4_1(0) & c4_1(1) & ~c4_1(2)). % 5.52/5.70 fof(interp, fi_predicates, ~c4_2(0, 0) & c4_2(0, 1) & ~c4_2(0, 2) & c4_2(1, 0) & % 5.52/5.70 c4_2(1, 1) & % 5.52/5.70 ~c4_2(1, 2) & % 5.52/5.70 ~c4_2(2, 0) & % 5.52/5.70 c4_2(2, 1) & % 5.52/5.70 c4_2(2, 2)). % 5.52/5.70 fof(interp, fi_predicates, ~c5_0). % 5.52/5.70 fof(interp, fi_predicates, c5_1(0) & ~c5_1(1) & c5_1(2)). % 5.52/5.70 fof(interp, fi_predicates, ~c5_2(0, 0) & ~c5_2(0, 1) & ~c5_2(0, 2) & c5_2(1, 0) & % 5.52/5.70 c5_2(1, 1) & % 5.52/5.70 c5_2(1, 2) & % 5.52/5.70 c5_2(2, 0) & % 5.52/5.70 ~c5_2(2, 1) & % 5.52/5.70 c5_2(2, 2)). % 5.52/5.70 fof(interp, fi_predicates, epred10_0). % 5.52/5.70 fof(interp, fi_predicates, ~epred11_0). % 5.52/5.70 fof(interp, fi_predicates, ~epred12_0). % 5.52/5.70 fof(interp, fi_predicates, ~epred1_0). % 5.52/5.70 fof(interp, fi_predicates, ~epred2_0). % 5.52/5.70 fof(interp, fi_predicates, ~epred3_0). % 5.52/5.70 fof(interp, fi_predicates, ~epred4_0). % 5.52/5.70 fof(interp, fi_predicates, epred5_0). % 5.52/5.70 fof(interp, fi_predicates, epred6_0). % 5.52/5.70 fof(interp, fi_predicates, ~epred7_0). % 5.52/5.70 fof(interp, fi_predicates, epred8_0). % 5.52/5.70 fof(interp, fi_predicates, ~epred9_0). % 5.52/5.70 fof(interp, fi_predicates, ndr1_0). % 5.52/5.70 fof(interp, fi_predicates, ndr1_1(0) & ndr1_1(1) & ndr1_1(2)). % 5.52/5.70 % SZS output end FiniteModel for theBenchmark.p % 5.52/5.70 % 20 lemma(s) from E % 5.52/5.70 % cnf(cl, axiom, epred6_0). % 5.52/5.70 % cnf(cl, axiom, ~c2_0). % 5.52/5.70 % cnf(cl, axiom, ~c1_0). % 5.52/5.70 % cnf(cl, axiom, ~c4_0). % 5.52/5.70 % cnf(cl, axiom, c2_1(a1442)). % 5.52/5.70 % cnf(cl, axiom, c3_1(a1442)). % 5.52/5.70 % cnf(cl, axiom, c4_1(a1475)). % 5.52/5.70 % cnf(cl, axiom, c5_1(a1350)). % 5.52/5.70 % cnf(cl, axiom, c4_1(a1424)). % 5.52/5.70 % cnf(cl, axiom, ndr1_1(a1333)). % 5.52/5.70 % cnf(cl, axiom, c1_1(a1333)). % 5.52/5.70 % cnf(cl, axiom, ndr1_1(a1452)). % 5.52/5.70 % cnf(cl, axiom, ndr1_1(a1363)). % 5.52/5.70 % cnf(cl, axiom, ndr1_1(a1436)). % 5.52/5.70 % cnf(cl, axiom, ndr1_1(a1350)). % 5.52/5.70 % cnf(cl, axiom, c1_1(a1458)). % 5.52/5.70 % cnf(cl, axiom, ~c5_1(a1475)). % 5.52/5.70 % cnf(cl, axiom, ~c2_1(a1350)). % 5.52/5.70 % cnf(cl, axiom, ~c1_1(a1424)). % 5.52/5.70 % cnf(cl, axiom, ~c5_1(a1446)). % 5.52/5.70 % 523 pred(s) % 5.52/5.70 % 204 func(s) % 5.52/5.70 % 2 sort(s) % 5.52/5.70 % 1767 clause(s) % 5.52/5.70 % Instantiating 1 (5218 ms) % 5.52/5.70 % Solving (5232 ms) % 5.52/5.70 % Instantiating 2 (5232 ms) % 5.52/5.70 % Solving (5240 ms) % 5.52/5.70 % Instantiating 3 (5241 ms) % 5.52/5.70 % Solving (5259 ms) % 5.52/5.70 % % 5.52/5.70 % 1 model found (5273 ms) %------------------------------------------------------------------------------