search

meelgroup / bosphorus

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter
Other
67 stars 18 forks source link

CryptoMiniSat embedded in SageMath can solve these ANFs but Bosphous reports UNSAT #34

Closed HuinaLi closed 2 years ago

HuinaLi commented 2 years ago

operating system: Linux ubuntu18.04

We use Sage to generate ANF(round4rxoodooMess.anf), and invoke the function solve_sat() to solve this SAT problem, and the solver return solution. 

nohup: ignoring input
x(718)
x(423)*x(467) + x(423)*x(476) + x(423)*x(594) + x(423)*x(603) + x(423)*x(651) + x(423)*x(660) + x(423)*x(697) + x(423)*x(851) + x(423)*x(860) + x(423)*x(978) + x(423)*x(987) + x(423)*x(1035) + x(423)*x(1044) + x(423)*x(1081) + x(446)*x(467) + x(446)*x(476) + x(446)*x(594) + x(446)*x(603) + x(446)*x(651) + x(446)*x(660) + x(446)*x(697) + x(446)*x(851) + x(446)*x(860) + x(446)*x(978) + x(446)*x(987) + x(446)*x(1035) + x(446)*x(1044) + x(446)*x(1081) + x(455) + x(467)*x(550) + x(467)*x(573) + x(467)*x(587) + x(467)*x(758) + x(467)*x(767) + x(467)*x(807) + x(467)*x(830) + x(467)*x(934) + x(467)*x(957) + x(467)*x(971) + x(467)*x(1142) + x(467)*x(1151) + x(467) + x(476)*x(550) + x(476)*x(573) + x(476)*x(587) + x(476)*x(758) + x(476)*x(767) + x(476)*x(807) + x(476)*x(830) + x(476)*x(934) + x(476)*x(957) + x(476)*x(971) + x(476)*x(1142) + x(476)*x(1151) + x(476) + x(478) + x(492) + x(550)*x(594) + x(550)*x(603) + x(550)*x(651) + x(550)*x(660) + x(550)*x(697) + x(550)*x(851) + x(550)*x(860) + x(550)*x(978) + x(550)*x(987) + x(550)*x(1035) + x(550)*x(1044) + x(550)*x(1081) + x(573)*x(594) + x(573)*x(603) + x(573)*x(651) + x(573)*x(660) + x(573)*x(697) + x(573)*x(851) + x(573)*x(860) + x(573)*x(978) + x(573)*x(987) + x(573)*x(1035) + x(573)*x(1044) + x(573)*x(1081) + x(582) + x(587)*x(594) + x(587)*x(603) + x(587)*x(651) + x(587)*x(660) + x(587)*x(697) + x(587)*x(851) + x(587)*x(860) + x(587)*x(978) + x(587)*x(987) + x(587)*x(1035) + x(587)*x(1044) + x(587)*x(1081) + x(594)*x(758) + x(594)*x(767) + x(594)*x(807) + x(594)*x(830) + x(594)*x(934) + x(594)*x(957) + x(594)*x(971) + x(594)*x(1142) + x(594)*x(1151) + x(594) + x(603)*x(758) + x(603)*x(767) + x(603)*x(807) + x(603)*x(830) + x(603)*x(934) + x(603)*x(957) + x(603)*x(971) + x(603)*x(1142) + x(603)*x(1151) + x(603) + x(605) + x(651)*x(758) + x(651)*x(767) + x(651)*x(807) + x(651)*x(830) + x(651)*x(934) + x(651)*x(957) + x(651)*x(971) + x(651)*x(1142) + x(651)*x(1151) + x(651) + x(660)*x(758) + x(660)*x(767) + x(660)*x(807) + x(660)*x(830) + x(660)*x(934) + x(660)*x(957) + x(660)*x(971) + x(660)*x(1142) + x(660)*x(1151) + x(660) + x(662) + x(671) + x(697)*x(758) + x(697)*x(767) + x(697)*x(807) + x(697)*x(830) + x(697)*x(934) + x(697)*x(957) + x(697)*x(971) + x(697)*x(1142) + x(697)*x(1151) + x(697) + x(758)*x(851) + x(758)*x(860) + x(758)*x(978) + x(758)*x(987) + x(758)*x(1035) + x(758)*x(1044) + x(758)*x(1081) + x(767)*x(851) + x(767)*x(860) + x(767)*x(978) + x(767)*x(987) + x(767)*x(1035) + x(767)*x(1044) + x(767)*x(1081) + x(1260)
x(38) + x(61) + x(75) + x(165) + x(188) + x(373) + x(382)
...
...
x(810) + x(819) + x(840)*x(842) + x(840)*x(851) + x(840)*x(888) + x(840)*x(969) + x(840)*x(978) + x(840)*x(1026) + x(840)*x(1035) + x(842)*x(863) + x(842)*x(967) + x(842)*x(990) + x(842)*x(1024) + x(842)*x(1047) + x(842)*x(1061) + x(842) + x(851)*x(863) + x(851)*x(967) + x(851)*x(990) + x(851)*x(1024) + x(851)*x(1047) + x(851)*x(1061) + x(851) + x(863)*x(888) + x(863)*x(969) + x(863)*x(978) + x(863)*x(1026) + x(863)*x(1035) + x(888)*x(967) + x(888)*x(990) + x(888)*x(1024) + x(888)*x(1047) + x(888)*x(1061) + x(888) + x(937) + x(946) + x(967)*x(969) + x(967)*x(978) + x(967)*x(1026) + x(967)*x(1035) + x(969)*x(990) + x(969)*x(1024) + x(969)*x(1047) + x(969)*x(1061) + x(969) + x(978)*x(990) + x(978)*x(1024) + x(978)*x(1047) + x(978)*x(1061) + x(978) + x(983) + x(990)*x(1026) + x(990)*x(1035) + x(1024)*x(1026) + x(1024)*x(1035) + x(1026)*x(1047) + x(1026)*x(1061) + x(1026) + x(1035)*x(1047) + x(1035)*x(1061) + x(1035) + x(1122) + x(1131) + x(1784)
x(23) + x(73)*x(103) + x(73)*x(126) + x(73)*x(230) + x(73)*x(253) + x(73)*x(310) + x(73)*x(319) + x(73)*x(324) + x(82)*x(103) + x(82)*x(126) + x(82)*x(230) + x(82)*x(253) + x(82)*x(310) + x(82)*x(319) + x(82)*x(324) + x(103)*x(200) + x(103)*x(209) + x(103)*x(246) + x(103)*x(257) + x(103)*x(266) + x(103) + x(105) + x(114) + x(126)*x(200) + x(126)*x(209) + x(126)*x(246) + x(126)*x(257) + x(126)*x(266) + x(126) + x(200)*x(230) + x(200)*x(253) + x(200)*x(310) + x(200)*x(319) + x(200)*x(324) + x(209)*x(230) + x(209)*x(253) + x(209)*x(310) + x(209)*x(319) + x(209)*x(324) + x(230)*x(246) + x(230)*x(257) + x(230)*x(266) + x(230) + x(232) + x(241) + x(246)*x(253) + x(246)*x(310) + x(246)*x(319) + x(246)*x(324) + x(253)*x(257) + x(253)*x(266) + x(253) + x(257)*x(310) + x(257)*x(319) + x(257)*x(324) + x(266)*x(310) + x(266)*x(319) + x(266)*x(324) + x(289) + x(298) + x(310) + x(319) + x(324) + x(791)
2022-06-20 16:18:47,120 - simple_example - INFO - start solve
2022-06-20 16:20:34,019 - simple_example - INFO - [{x(1919): 0, x(1918): 0, x(1917): 0, x(1916): 0, x(1915): 1, x(1914): 1, x(1913): 1, x(1912): 0, x(1911): 0, x(1910): 1, x(1909): 0, x(1908): 0, x(1907): 0, x(1906): 0, x(1905): 0, x(1904): 0, x(1903): 1, x(1902): 0, x(1901): 0, x(1900): 1, x(1899): 0, x(1898): 0, x(1897): 0, x(1896): 1, x(1895): 1, x(1894): 1, x(1893): 1, x(1892): 1, x(1891): 1, x(1890): 0, x(1889): 0, x(1888): 1, x(1887): 0, x(1886): 0, x(1885): 0, x(1884): 1, x(1883): 1, x(1882): 0, x(1881): 1, x(1880): 0, x(1879): 1, x(1878): 0, x(1877): 0, x(1876): 1, x(1875): 0, x(1874): 1, x(1873): 1, x(1872): 1, x(1871): 0, x(1870): 1, x(1869): 1, x(1868): 0, x(1867): 1, x(1866): 1, x(1865): 1, x(1864): 1, x(1863): 1, x(1862): 1, x(1861): 0, x(1860): 0, x(1859): 0, x(1858): 1, x(1857): 1, x(1856): 0, x(1855): 0, x(1854): 1, x(1853): 0, x(1852): 0, x(1851): 0, x(1850): 0, x(1849): 0, x(1848): 0, x(1847): 0, x(1846): 0, x(1845): 0, x(1844): 0, x(1843): 1, x(1842): 1, x(1841): 1, x(1840): 0, x(1839): 0, x(1838): 1, x(1837): 1, x(1836): 1, x(1835): 0, x(1834): 0, x(1833): 0, x(1832): 1, x(1831): 1, x(1830): 1, x(1829): 1, x(1828): 1, x(1827): 1, x(1826): 1, x(1825): 1, x(1824): 1, x(1823): 1, x(1822): 1, x(1821): 0, x(1820): 0, x(1819): 1, x(1818): 0, x(1817): 1, x(1816): 1, x(1815): 0, x(1814): 1, x(1813): 1, x(1812): 1, x(1811): 0, x(1810): 1, x(1809): 0, x(1808): 0, x(1807): 1, x(1806): 0, x(1805): 1, x(1804): 0, x(1803): 0, x(1802): 0, x(1801): 0, x(1800): 1, x(1799): 1, x(1798): 1, x(1797): 0, x(1796): 0, x(1795): 1, x(1794): 0, x(1793): 0, x(1792): 1, x(1791): 0, x(1790): 1, x(1789): 0, x(1788): 1, x(1787): 0, x(1786): 0, x(1785): 0, x(1784): 1, x(1783): 0, x(1782): 1, x(1781): 0, x(1780): 1, x(1779): 0, x(1778): 1, x(1777): 0, x(1776): 1, x(1775): 0, x(1774): 1, x(1773): 1, x(1772): 0, x(1771): 1, x(1770): 1, x(1769): 1, x(1768): 0, x(1767): 0, x(1766): 1, x(1765): 0, x(1764): 1, x(1763): 0, x(1762): 1, x(1761): 0, x(1760): 1, x(1759): 0, x(1758): 1, x(1757): 0, x(1756): 1, x(1755): 1, x(1754): 0, x(1753): 1, x(1752): 1, x(1751): 0, x(1750): 0, x(1749): 1, x(1748): 0, x(1747): 0, x(1746): 1, x(1745): 0, x(1744): 1, x(1743): 1, x(1742): 1, x(1741): 1, x(1740): 0, x(1739): 1, x(1738): 0, x(1737): 1, x(1736): 1, x(1735): 1, x(1734): 0, x(1733): 0, x(1732): 1, x(1731): 1, x(1730): 0, x(1729): 0, x(1728): 1, x(1727): 0, x(1726): 1, x(1725): 0, x(1724): 0, x(1723): 0, x(1722): 1, x(1721): 1, x(1720): 1, x(1719): 1, x(1718): 1, x(1717): 0, x(1716): 1, x(1715): 0, x(1714): 0, x(1713): 0, x(1712): 1, x(1711): 1, x(1710): 1, x(1709): 0, x(1708): 1, x(1707): 0, x(1706): 0, x(1705): 0, x(1704): 0, x(1703): 1, x(1702): 0, x(1701): 1, x(1700): 0, x(1699): 1, x(1698): 0, x(1697): 1, x(1696): 1, x(1695): 1, x(1694): 0, x(1693): 0, x(1692): 0, x(1691): 0, x(1690): 0, x(1689): 1, x(1688): 1, x(1687): 1, x(1686): 1, x(1685): 1, x(1684): 0, x(1683): 0, x(1682): 0, x(1681): 1, x(1680): 0, x(1679): 0, x(1678): 0, x(1677): 1, x(1676): 1, x(1675): 0, x(1674): 0, x(1673): 0, x(1672): 1, x(1671): 0, x(1670): 0, x(1669): 1, x(1668): 1, x(1667): 0, x(1666): 1, x(1665): 1, x(1664): 0, x(1663): 1, x(1662): 1, x(1661): 0, x(1660): 1, x(1659): 1, x(1658): 1, x(1657): 0, x(1656): 1, x(1655): 1, x(1654): 0, x(1653): 1, x(1652): 1, x(1651): 0, x(1650): 1, x(1649): 0, x(1648): 0, x(1647): 0, x(1646): 1, x(1645): 0, x(1644): 0, x(1643): 0, x(1642): 1, x(1641): 1, x(1640): 0, x(1639): 1, x(1638): 0, x(1637): 0, x(1636): 0, x(1635): 0, x(1634): 0, x(1633): 1, x(1632): 1, x(1631): 1, x(1630): 0, x(1629): 1, x(1628): 0, x(1627): 0, x(1626): 0, x(1625): 0, x(1624): 0, x(1623): 1, x(1622): 0, x(1621): 0, x(1620): 1, x(1619): 1, x(1618): 1, x(1617): 0, x(1616): 1, x(1615): 0, x(1614): 0, x(1613): 0, x(1612): 1, x(1611): 1, x(1610): 1, x(1609): 1, x(1608): 1, x(1607): 0, x(1606): 1, x(1605): 0, x(1604): 1, x(1603): 1, x(1602): 1, x(1601): 0, x(1600): 0, x(1599): 1, x(1598): 0, x(1597): 1, x(1596): 0, x(1595): 0, x(1594): 1, x(1593): 1, x(1592): 0, x(1591): 0, x(1590): 0, x(1589): 1, x(1588): 0, x(1587): 1, x(1586): 1, x(1585): 0, x(1584): 0, x(1583): 0, x(1582): 0, x(1581): 0, x(1580): 1, x(1579): 1, x(1578): 0, x(1577): 0, x(1576): 1, x(1575): 0, x(1574): 0, x(1573): 1, x(1572): 0, x(1571): 0, x(1570): 1, x(1569): 0, x(1568): 0, x(1567): 0, x(1566): 1, x(1565): 1, x(1564): 1, x(1563): 1, x(1562): 0, x(1561): 0, x(1560): 1, x(1559): 0, x(1558): 1, x(1557): 0, x(1556): 1, x(1555): 0, x(1554): 0, x(1553): 1, x(1552): 0, x(1551): 1, x(1550): 0, x(1549): 0, x(1548): 1, x(1547): 0, x(1546): 0, x(1545): 0, x(1544): 1, x(1543): 0, x(1542): 1, x(1541): 0, x(1540): 0, x(1539): 0, x(1538): 0, x(1537): 1, x(1536): 0, x(1535): 0, x(1534): 0, x(1533): 0, x(1532): 0, x(1531): 0, x(1530): 0, x(1529): 0, x(1528): 0, x(1527): 0, x(1526): 0, x(1525): 0, x(1524): 0, x(1523): 0, x(1522): 0, x(1521): 0, x(1520): 0, x(1519): 0, x(1518): 0, x(1517): 0, x(1516): 0, x(1515): 0, x(1514): 0, x(1513): 0, x(1512): 0, x(1511): 0, x(1510): 0, x(1509): 0, x(1508): 0, x(1507): 0, x(1506): 0, x(1505): 0, x(1504): 0, x(1503): 0, x(1502): 0, x(1501): 0, x(1500): 0, x(1499): 0, x(1498): 0, x(1497): 0, x(1496): 0, x(1495): 0, x(1494): 1, x(1493): 0, x(1492): 0, x(1491): 0, x(1490): 0, x(1489): 0, x(1488): 1, x(1487): 0, x(1486): 0, x(1485): 0, x(1484): 0, x(1483): 0, x(1482): 0, x(1481): 0, x(1480): 0, x(1479): 0, x(1478): 1, x(1477): 0, x(1476): 0, x(1475): 0, x(1474): 0, x(1473): 0, x(1472): 1, x(1471): 0, x(1470): 0, x(1469): 0, x(1468): 0, x(1467): 0, x(1466): 0, x(1465): 0, x(1464): 0, x(1463): 0, x(1462): 0, x(1461): 0, x(1460): 0, x(1459): 0, x(1458): 0, x(1457): 0, x(1456): 0, x(1455): 0, x(1454): 0, x(1453): 0, x(1452): 0, x(1451): 0, x(1450): 0, x(1449): 0, x(1448): 0, x(1447): 0, x(1446): 0, x(1445): 0, x(1444): 0, x(1443): 0, x(1442): 0, x(1441): 0, x(1440): 0, x(1439): 0, x(1438): 1, x(1437): 0, x(1436): 0, x(1435): 0, x(1434): 0, x(1433): 0, x(1432): 1, x(1431): 0, x(1430): 0, x(1429): 0, x(1428): 0, x(1427): 1, x(1426): 0, x(1425): 0, x(1424): 0, x(1423): 0, x(1422): 1, x(1421): 0, x(1420): 0, x(1419): 0, x(1418): 0, x(1417): 0, x(1416): 1, x(1415): 0, x(1414): 0, x(1413): 0, x(1412): 0, x(1411): 1, x(1410): 0, x(1409): 0, x(1408): 0, x(1407): 0, x(1406): 0, x(1405): 0, x(1404): 0, x(1403): 0, x(1402): 0, x(1401): 0, x(1400): 0, x(1399): 0, x(1398): 0, x(1397): 0, x(1396): 0, x(1395): 0, x(1394): 0, x(1393): 0, x(1392): 0, x(1391): 0, x(1390): 0, x(1389): 0, x(1388): 0, x(1387): 0, x(1386): 0, x(1385): 0, x(1384): 0, x(1383): 0, x(1382): 0, x(1381): 0, x(1380): 0, x(1379): 0, x(1378): 0, x(1377): 0, x(1376): 0, x(1375): 0, x(1374): 0, x(1373): 0, x(1372): 0, x(1371): 0, x(1370): 0, x(1369): 0, x(1368): 0, x(1367): 0, x(1366): 0, x(1365): 0, x(1364): 0, x(1363): 0, x(1362): 0, x(1361): 0, x(1360): 0, x(1359): 0, x(1358): 0, x(1357): 0, x(1356): 0, x(1355): 0, x(1354): 0, x(1353): 0, x(1352): 0, x(1351): 0, x(1350): 0, x(1349): 0, x(1348): 0, x(1347): 0, x(1346): 0, x(1345): 0, x(1344): 0, x(1343): 0, x(1342): 0, x(1341): 0, x(1340): 0, x(1339): 0, x(1338): 0, x(1337): 0, x(1336): 0, x(1335): 0, x(1334): 0, x(1333): 0, x(1332): 0, x(1331): 0, x(1330): 0, x(1329): 0, x(1328): 0, x(1327): 0, x(1326): 0, x(1325): 0, x(1324): 0, x(1323): 0, x(1322): 0, x(1321): 0, x(1320): 0, x(1319): 0, x(1318): 0, x(1317): 0, x(1316): 0, x(1315): 0, x(1314): 0, x(1313): 0, x(1312): 0, x(1311): 0, x(1310): 0, x(1309): 0, x(1308): 0, x(1307): 0, x(1306): 0, x(1305): 0, x(1304): 0, x(1303): 0, x(1302): 0, x(1301): 0, x(1300): 0, x(1299): 0, x(1298): 0, x(1297): 0, x(1296): 0, x(1295): 0, x(1294): 0, x(1293): 0, x(1292): 0, x(1291): 0, x(1290): 0, x(1289): 0, x(1288): 0, x(1287): 0, x(1286): 0, x(1285): 0, x(1284): 0, x(1283): 0, x(1282): 0, x(1281): 0, x(1280): 0, x(1279): 0, x(1278): 0, x(1277): 0, x(1276): 0, x(1275): 0, x(1274): 0, x(1273): 0, x(1272): 0, x(1271): 0, x(1270): 0, x(1269): 0, x(1268): 0, x(1267): 0, x(1266): 0, x(1265): 0, x(1264): 0, x(1263): 0, x(1262): 0, x(1261): 0, x(1260): 0, x(1259): 0, x(1258): 0, x(1257): 0, x(1256): 0, x(1255): 0, x(1254): 0, x(1253): 0, x(1252): 0, x(1251): 0, x(1250): 0, x(1249): 0, x(1248): 0, x(1247): 0, x(1246): 0, x(1245): 0, x(1244): 0, x(1243): 1, x(1242): 0, x(1241): 0, x(1240): 0, x(1239): 0, x(1238): 1, x(1237): 0, x(1236): 0, x(1235): 0, x(1234): 0, x(1233): 0, x(1232): 1, x(1231): 0, x(1230): 0, x(1229): 0, x(1228): 0, x(1227): 1, x(1226): 0, x(1225): 0, x(1224): 0, x(1223): 0, x(1222): 1, x(1221): 0, x(1220): 0, x(1219): 0, x(1218): 0, x(1217): 0, x(1216): 1, x(1215): 0, x(1214): 0, x(1213): 0, x(1212): 0, x(1211): 0, x(1210): 0, x(1209): 0, x(1208): 0, x(1207): 0, x(1206): 0, x(1205): 0, x(1204): 0, x(1203): 0, x(1202): 0, x(1201): 0, x(1200): 0, x(1199): 0, x(1198): 0, x(1197): 0, x(1196): 0, x(1195): 0, x(1194): 0, x(1193): 0, x(1192): 0, x(1191): 0, x(1190): 0, x(1189): 0, x(1188): 0, x(1187): 0, x(1186): 0, x(1185): 0, x(1184): 0, x(1183): 0, x(1182): 1, x(1181): 0, x(1180): 0, x(1179): 0, x(1178): 0, x(1177): 0, x(1176): 1, x(1175): 0, x(1174): 0, x(1173): 0, x(1172): 0, x(1171): 0, x(1170): 0, x(1169): 0, x(1168): 0, x(1167): 0, x(1166): 1, x(1165): 0, x(1164): 0, x(1163): 0, x(1162): 0, x(1161): 0, x(1160): 1, x(1159): 0, x(1158): 0, x(1157): 0, x(1156): 0, x(1155): 0, x(1154): 0, x(1153): 0, x(1152): 0, x(1151): 1, x(1150): 0, x(1149): 1, x(1148): 0, x(1147): 1, x(1146): 1, x(1145): 1, x(1144): 1, x(1143): 0, x(1142): 1, x(1141): 0, x(1140): 1, x(1139): 1, x(1138): 1, x(1137): 0, x(1136): 1, x(1135): 0, x(1134): 0, x(1133): 1, x(1132): 0, x(1131): 1, x(1130): 0, x(1129): 0, x(1128): 1, x(1127): 0, x(1126): 1, x(1125): 0, x(1124): 0, x(1123): 0, x(1122): 0, x(1121): 1, x(1120): 0, x(1119): 1, x(1118): 0, x(1117): 1, x(1116): 1, x(1115): 0, x(1114): 0, x(1113): 1, x(1112): 0, x(1111): 1, x(1110): 0, x(1109): 0, x(1108): 1, x(1107): 1, x(1106): 1, x(1105): 0, x(1104): 0, x(1103): 1, x(1102): 1, x(1101): 1, x(1100): 1, x(1099): 0, x(1098): 1, x(1097): 0, x(1096): 0, x(1095): 0, x(1094): 0, x(1093): 1, x(1092): 0, x(1091): 0, x(1090): 1, x(1089): 0, x(1088): 1, x(1087): 1, x(1086): 0, x(1085): 1, x(1084): 1, x(1083): 1, x(1082): 0, x(1081): 1, x(1080): 0, x(1079): 1, x(1078): 1, x(1077): 0, x(1076): 0, x(1075): 1, x(1074): 1, x(1073): 1, x(1072): 0, x(1071): 0, x(1070): 0, x(1069): 0, x(1068): 0, x(1067): 1, x(1066): 0, x(1065): 0, x(1064): 1, x(1063): 0, x(1062): 1, x(1061): 0, x(1060): 1, x(1059): 0, x(1058): 1, x(1057): 0, x(1056): 1, x(1055): 0, x(1054): 0, x(1053): 1, x(1052): 1, x(1051): 1, x(1050): 0, x(1049): 0, x(1048): 0, x(1047): 0, x(1046): 1, x(1045): 0, x(1044): 0, x(1043): 1, x(1042): 1, x(1041): 0, x(1040): 0, x(1039): 0, x(1038): 1, x(1037): 1, x(1036): 0, x(1035): 1, x(1034): 1, x(1033): 1, x(1032): 1, x(1031): 1, x(1030): 0, x(1029): 0, x(1028): 1, x(1027): 1, x(1026): 1, x(1025): 0, x(1024): 1, x(1023): 1, x(1022): 0, x(1021): 1, x(1020): 0, x(1019): 0, x(1018): 1, x(1017): 0, x(1016): 0, x(1015): 0, x(1014): 0, x(1013): 1, x(1012): 0, x(1011): 0, x(1010): 1, x(1009): 0, x(1008): 0, x(1007): 0, x(1006): 1, x(1005): 0, x(1004): 1, x(1003): 1, x(1002): 0, x(1001): 1, x(1000): 0, x(999): 0, x(998): 1, x(997): 0, x(996): 1, x(995): 1, x(994): 1, x(993): 0, x(992): 0, x(991): 0, x(990): 0, x(989): 0, x(988): 1, x(987): 0, x(986): 0, x(985): 1, x(984): 0, x(983): 0, x(982): 0, x(981): 1, x(980): 1, x(979): 0, x(978): 0, x(977): 1, x(976): 1, x(975): 0, x(974): 1, x(973): 0, x(972): 0, x(971): 0, x(970): 0, x(969): 0, x(968): 1, x(967): 1, x(966): 1, x(965): 0, x(964): 0, x(963): 1, x(962): 1, x(961): 1, x(960): 1, x(959): 0, x(958): 1, x(957): 0, x(956): 0, x(955): 0, x(954): 1, x(953): 0, x(952): 0, x(951): 0, x(950): 1, x(949): 0, x(948): 0, x(947): 0, x(946): 0, x(945): 1, x(944): 0, x(943): 0, x(942): 1, x(941): 0, x(940): 0, x(939): 0, x(938): 0, x(937): 0, x(936): 1, x(935): 0, x(934): 1, x(933): 1, x(932): 0, x(931): 1, x(930): 1, x(929): 0, x(928): 0, x(927): 1, x(926): 0, x(925): 1, x(924): 0, x(923): 0, x(922): 0, x(921): 0, x(920): 1, x(919): 0, x(918): 1, x(917): 0, x(916): 1, x(915): 0, x(914): 1, x(913): 1, x(912): 0, x(911): 0, x(910): 1, x(909): 1, x(908): 0, x(907): 0, x(906): 0, x(905): 1, x(904): 1, x(903): 1, x(902): 1, x(901): 0, x(900): 0, x(899): 0, x(898): 1, x(897): 0, x(896): 0, x(895): 0, x(894): 0, x(893): 1, x(892): 0, x(891): 1, x(890): 0, x(889): 0, x(888): 0, x(887): 0, x(886): 0, x(885): 0, x(884): 1, x(883): 1, x(882): 1, x(881): 0, x(880): 0, x(879): 0, x(878): 1, x(877): 0, x(876): 0, x(875): 0, x(874): 0, x(873): 1, x(872): 0, x(871): 1, x(870): 0, x(869): 1, x(868): 0, x(867): 0, x(866): 1, x(865): 1, x(864): 0, x(863): 0, x(862): 0, x(861): 0, x(860): 0, x(859): 0, x(858): 1, x(857): 0, x(856): 0, x(855): 1, x(854): 0, x(853): 0, x(852): 0, x(851): 1, x(850): 0, x(849): 0, x(848): 0, x(847): 1, x(846): 0, x(845): 1, x(844): 1, x(843): 0, x(842): 0, x(841): 0, x(840): 0, x(839): 1, x(838): 1, x(837): 0, x(836): 1, x(835): 0, x(834): 0, x(833): 1, x(832): 1, x(831): 1, x(830): 1, x(829): 0, x(828): 1, x(827): 0, x(826): 1, x(825): 0, x(824): 1, x(823): 1, x(822): 0, x(821): 0, x(820): 0, x(819): 1, x(818): 0, x(817): 1, x(816): 1, x(815): 0, x(814): 1, x(813): 0, x(812): 0, x(811): 0, x(810): 0, x(809): 0, x(808): 1, x(807): 0, x(806): 0, x(805): 1, x(804): 0, x(803): 1, x(802): 0, x(801): 0, x(800): 1, x(799): 1, x(798): 0, x(797): 0, x(796): 1, x(795): 0, x(794): 0, x(793): 1, x(792): 0, x(791): 0, x(790): 0, x(789): 0, x(788): 1, x(787): 1, x(786): 0, x(785): 1, x(784): 1, x(783): 0, x(782): 0, x(781): 0, x(780): 0, x(779): 1, x(778): 1, x(777): 0, x(776): 1, x(775): 0, x(774): 1, x(773): 1, x(772): 0, x(771): 1, x(770): 0, x(769): 0, x(768): 1, x(767): 0, x(766): 0, x(765): 0, x(764): 0, x(763): 0, x(762): 0, x(761): 0, x(760): 0, x(759): 0, x(758): 0, x(757): 0, x(756): 0, x(755): 0, x(754): 0, x(753): 0, x(752): 0, x(751): 0, x(750): 0, x(749): 0, x(748): 0, x(747): 0, x(746): 0, x(745): 0, x(744): 0, x(743): 0, x(742): 0, x(741): 0, x(740): 0, x(739): 0, x(738): 0, x(737): 0, x(736): 0, x(735): 0, x(734): 0, x(733): 0, x(732): 0, x(731): 1, x(730): 0, x(729): 0, x(728): 0, x(727): 0, x(726): 0, x(725): 0, x(724): 0, x(723): 0, x(722): 0, x(721): 0, x(720): 1, x(719): 0, x(718): 0, x(717): 0, x(716): 0, x(715): 1, x(714): 0, x(713): 0, x(712): 0, x(711): 0, x(710): 0, x(709): 0, x(708): 0, x(707): 0, x(706): 0, x(705): 0, x(704): 1, x(703): 0, x(702): 0, x(701): 0, x(700): 0, x(699): 0, x(698): 0, x(697): 0, x(696): 0, x(695): 0, x(694): 0, x(693): 0, x(692): 0, x(691): 0, x(690): 0, x(689): 0, x(688): 0, x(687): 0, x(686): 0, x(685): 0, x(684): 0, x(683): 0, x(682): 0, x(681): 0, x(680): 0, x(679): 0, x(678): 0, x(677): 0, x(676): 0, x(675): 0, x(674): 0, x(673): 0, x(672): 0, x(671): 0, x(670): 0, x(669): 0, x(668): 0, x(667): 0, x(666): 0, x(665): 0, x(664): 1, x(663): 0, x(662): 0, x(661): 0, x(660): 0, x(659): 1, x(658): 0, x(657): 0, x(656): 0, x(655): 0, x(654): 0, x(653): 0, x(652): 0, x(651): 0, x(650): 0, x(649): 0, x(648): 1, x(647): 0, x(646): 0, x(645): 0, x(644): 0, x(643): 1, x(642): 0, x(641): 0, x(640): 0, x(639): 0, x(638): 0, x(637): 0, x(636): 0, x(635): 0, x(634): 0, x(633): 0, x(632): 0, x(631): 0, x(630): 0, x(629): 0, x(628): 0, x(627): 0, x(626): 0, x(625): 0, x(624): 0, x(623): 0, x(622): 0, x(621): 0, x(620): 0, x(619): 0, x(618): 0, x(617): 0, x(616): 0, x(615): 0, x(614): 0, x(613): 0, x(612): 0, x(611): 0, x(610): 0, x(609): 0, x(608): 0, x(607): 0, x(606): 0, x(605): 0, x(604): 0, x(603): 0, x(602): 0, x(601): 0, x(600): 0, x(599): 0, x(598): 0, x(597): 0, x(596): 0, x(595): 0, x(594): 0, x(593): 0, x(592): 0, x(591): 0, x(590): 0, x(589): 0, x(588): 0, x(587): 0, x(586): 0, x(585): 0, x(584): 0, x(583): 0, x(582): 0, x(581): 0, x(580): 0, x(579): 0, x(578): 0, x(577): 0, x(576): 0, x(575): 0, x(574): 0, x(573): 0, x(572): 0, x(571): 0, x(570): 0, x(569): 0, x(568): 0, x(567): 0, x(566): 0, x(565): 0, x(564): 0, x(563): 0, x(562): 0, x(561): 0, x(560): 0, x(559): 0, x(558): 0, x(557): 0, x(556): 0, x(555): 0, x(554): 0, x(553): 0, x(552): 0, x(551): 0, x(550): 0, x(549): 0, x(548): 0, x(547): 0, x(546): 0, x(545): 0, x(544): 0, x(543): 0, x(542): 0, x(541): 0, x(540): 0, x(539): 0, x(538): 0, x(537): 0, x(536): 0, x(535): 0, x(534): 0, x(533): 0, x(532): 0, x(531): 0, x(530): 0, x(529): 0, x(528): 0, x(527): 0, x(526): 0, x(525): 0, x(524): 0, x(523): 0, x(522): 0, x(521): 0, x(520): 0, x(519): 0, x(518): 0, x(517): 0, x(516): 0, x(515): 0, x(514): 0, x(513): 0, x(512): 0, x(511): 0, x(510): 0, x(509): 0, x(508): 0, x(507): 0, x(506): 0, x(505): 0, x(504): 0, x(503): 0, x(502): 0, x(501): 0, x(500): 0, x(499): 0, x(498): 0, x(497): 0, x(496): 0, x(495): 0, x(494): 0, x(493): 0, x(492): 0, x(491): 0, x(490): 0, x(489): 0, x(488): 0, x(487): 0, x(486): 0, x(485): 0, x(484): 0, x(483): 0, x(482): 0, x(481): 0, x(480): 0, x(479): 0, x(478): 0, x(477): 0, x(476): 0, x(475): 1, x(474): 0, x(473): 0, x(472): 0, x(471): 0, x(470): 0, x(469): 0, x(468): 0, x(467): 0, x(466): 0, x(465): 0, x(464): 1, x(463): 0, x(462): 0, x(461): 0, x(460): 0, x(459): 1, x(458): 0, x(457): 0, x(456): 0, x(455): 0, x(454): 0, x(453): 0, x(452): 0, x(451): 0, x(450): 0, x(449): 0, x(448): 1, x(447): 0, x(446): 0, x(445): 0, x(444): 0, x(443): 0, x(442): 0, x(441): 0, x(440): 0, x(439): 0, x(438): 0, x(437): 0, x(436): 0, x(435): 0, x(434): 0, x(433): 0, x(432): 0, x(431): 0, x(430): 0, x(429): 0, x(428): 0, x(427): 0, x(426): 0, x(425): 0, x(424): 0, x(423): 0, x(422): 0, x(421): 0, x(420): 0, x(419): 0, x(418): 0, x(417): 0, x(416): 0, x(415): 0, x(414): 0, x(413): 0, x(412): 0, x(411): 0, x(410): 0, x(409): 0, x(408): 1, x(407): 0, x(406): 0, x(405): 0, x(404): 0, x(403): 1, x(402): 0, x(401): 0, x(400): 0, x(399): 0, x(398): 0, x(397): 0, x(396): 0, x(395): 0, x(394): 0, x(393): 0, x(392): 1, x(391): 0, x(390): 0, x(389): 0, x(388): 0, x(387): 1, x(386): 0, x(385): 0, x(384): 0, x(383): 1, x(382): 0, x(381): 1, x(380): 1, x(379): 1, x(378): 0, x(377): 0, x(376): 0, x(375): 0, x(374): 1, x(373): 0, x(372): 0, x(371): 0, x(370): 1, x(369): 0, x(368): 0, x(367): 0, x(366): 0, x(365): 1, x(364): 0, x(363): 0, x(362): 0, x(361): 0, x(360): 0, x(359): 0, x(358): 0, x(357): 0, x(356): 1, x(355): 0, x(354): 0, x(353): 1, x(352): 0, x(351): 0, x(350): 1, x(349): 0, x(348): 0, x(347): 0, x(346): 0, x(345): 0, x(344): 1, x(343): 1, x(342): 0, x(341): 1, x(340): 0, x(339): 0, x(338): 0, x(337): 0, x(336): 0, x(335): 0, x(334): 0, x(333): 1, x(332): 0, x(331): 0, x(330): 0, x(329): 0, x(328): 0, x(327): 0, x(326): 0, x(325): 1, x(324): 0, x(323): 0, x(322): 0, x(321): 0, x(320): 0, x(319): 0, x(318): 0, x(317): 0, x(316): 0, x(315): 1, x(314): 0, x(313): 1, x(312): 0, x(311): 0, x(310): 0, x(309): 0, x(308): 0, x(307): 0, x(306): 0, x(305): 0, x(304): 0, x(303): 0, x(302): 0, x(301): 0, x(300): 0, x(299): 0, x(298): 0, x(297): 0, x(296): 0, x(295): 0, x(294): 0, x(293): 0, x(292): 0, x(291): 1, x(290): 1, x(289): 0, x(288): 0, x(287): 0, x(286): 0, x(285): 0, x(284): 1, x(283): 0, x(282): 1, x(281): 0, x(280): 0, x(279): 0, x(278): 0, x(277): 0, x(276): 0, x(275): 0, x(274): 0, x(273): 0, x(272): 1, x(271): 0, x(270): 0, x(269): 0, x(268): 1, x(267): 0, x(266): 0, x(265): 0, x(264): 0, x(263): 0, x(262): 0, x(261): 0, x(260): 0, x(259): 1, x(258): 0, x(257): 0, x(256): 1, x(255): 0, x(254): 0, x(253): 0, x(252): 0, x(251): 0, x(250): 0, x(249): 0, x(248): 0, x(247): 0, x(246): 0, x(245): 0, x(244): 0, x(243): 0, x(242): 0, x(241): 0, x(240): 0, x(239): 0, x(238): 0, x(237): 0, x(236): 0, x(235): 0, x(234): 0, x(233): 0, x(232): 0, x(231): 0, x(230): 0, x(229): 0, x(228): 0, x(227): 0, x(226): 1, x(225): 0, x(224): 0, x(223): 0, x(222): 0, x(221): 0, x(220): 0, x(219): 0, x(218): 0, x(217): 0, x(216): 0, x(215): 0, x(214): 0, x(213): 0, x(212): 0, x(211): 0, x(210): 0, x(209): 0, x(208): 0, x(207): 0, x(206): 0, x(205): 0, x(204): 0, x(203): 0, x(202): 0, x(201): 1, x(200): 0, x(199): 0, x(198): 0, x(197): 0, x(196): 0, x(195): 1, x(194): 1, x(193): 0, x(192): 1, x(191): 0, x(190): 0, x(189): 1, x(188): 1, x(187): 1, x(186): 0, x(185): 0, x(184): 0, x(183): 0, x(182): 0, x(181): 0, x(180): 1, x(179): 0, x(178): 0, x(177): 1, x(176): 0, x(175): 0, x(174): 0, x(173): 0, x(172): 0, x(171): 0, x(170): 0, x(169): 0, x(168): 1, x(167): 0, x(166): 0, x(165): 1, x(164): 1, x(163): 0, x(162): 0, x(161): 1, x(160): 0, x(159): 0, x(158): 0, x(157): 0, x(156): 0, x(155): 0, x(154): 0, x(153): 0, x(152): 1, x(151): 0, x(150): 0, x(149): 1, x(148): 0, x(147): 0, x(146): 0, x(145): 0, x(144): 0, x(143): 0, x(142): 0, x(141): 0, x(140): 0, x(139): 0, x(138): 0, x(137): 0, x(136): 0, x(135): 0, x(134): 0, x(133): 0, x(132): 0, x(131): 0, x(130): 0, x(129): 1, x(128): 0, x(127): 0, x(126): 0, x(125): 0, x(124): 0, x(123): 0, x(122): 0, x(121): 0, x(120): 0, x(119): 0, x(118): 0, x(117): 0, x(116): 0, x(115): 0, x(114): 0, x(113): 0, x(112): 0, x(111): 0, x(110): 0, x(109): 0, x(108): 0, x(107): 0, x(106): 0, x(105): 0, x(104): 0, x(103): 0, x(102): 0, x(101): 0, x(100): 0, x(99): 1, x(98): 0, x(97): 0, x(96): 0, x(95): 0, x(94): 0, x(93): 0, x(92): 0, x(91): 0, x(90): 0, x(89): 0, x(88): 0, x(87): 0, x(86): 0, x(85): 1, x(84): 0, x(83): 0, x(82): 0, x(81): 0, x(80): 0, x(79): 0, x(78): 0, x(77): 0, x(76): 1, x(75): 1, x(74): 0, x(73): 0, x(72): 0, x(71): 0, x(70): 0, x(69): 0, x(68): 1, x(67): 0, x(66): 0, x(65): 0, x(64): 1, x(63): 0, x(62): 0, x(61): 0, x(60): 0, x(59): 1, x(58): 0, x(57): 0, x(56): 1, x(55): 0, x(54): 0, x(53): 0, x(52): 1, x(51): 0, x(50): 0, x(49): 0, x(48): 0, x(47): 0, x(46): 0, x(45): 0, x(44): 0, x(43): 1, x(42): 0, x(41): 1, x(40): 0, x(39): 0, x(38): 1, x(37): 0, x(36): 0, x(35): 0, x(34): 0, x(33): 0, x(32): 1, x(31): 1, x(30): 0, x(29): 0, x(28): 0, x(27): 1, x(26): 0, x(25): 0, x(24): 1, x(23): 0, x(22): 0, x(21): 0, x(20): 1, x(19): 0, x(18): 0, x(17): 0, x(16): 0, x(15): 0, x(14): 0, x(13): 0, x(12): 0, x(11): 0, x(10): 0, x(9): 0, x(8): 0, x(7): 0, x(6): 0, x(5): 0, x(4): 0, x(3): 1, x(2): 0, x(1): 0, x(0): 0}]
2022-06-20 16:20:34,023 - simple_example - INFO - end adding

However, Bosphous fails on this anf file (round4rxoodooMess.anf):

2022-06-20T07:58:17.619800542Z c Executed with command line: /usr/local/bin/bosphorus --anfread /dat/round4rxoodooMess.anf --anfwrite /dat/round4rxoodooMess_out.anf --cnfwrite /dat/round4rxoodooMess.cnf --solvewrite /dat/round4rxoodooMess_solution
2022-06-20T07:58:17.619824571Z c Compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES =  | STATICCOMPILE = ON | ONLY_SIMPLE =  | Boost_FOUND = TRUE | STATS =  | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING =  | M4RI_FOUND = TRUE | SLOW_DEBUG =  | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM =  | LIMITMEM =  | compilation date time = Apr 29 2021 22:02:25
2022-06-20T07:58:17.619835994Z c --- Configuration --
2022-06-20T07:58:17.619841676Z c maxTime = 1.00e+20
2022-06-20T07:58:17.619847392Z c XL simp (deg = 1; s = 30.00+4.00): 1
2022-06-20T07:58:17.619853535Z c EL simp (s = 30.00): 1
2022-06-20T07:58:17.619859228Z c SAT simp (10000:100000): 1
2022-06-20T07:58:17.619865200Z  using 1 threads
2022-06-20T07:58:17.619871036Z c Cut num: 5
2022-06-20T07:58:17.619876853Z c Brickenstein cutoff: 10
2022-06-20T07:58:17.619882647Z c --------------------
2022-06-20T07:58:21.689087178Z c [ANF Input] read in T: 3.94
2022-06-20T07:58:21.689162300Z c ---- ANF stats -----
2022-06-20T07:58:21.689169508Z c Num total vars: 1920
2022-06-20T07:58:21.689175978Z c Num free vars: 1920
2022-06-20T07:58:21.689181735Z c Num equations: 2704
2022-06-20T07:58:21.807457861Z c Num monoms in eqs: 179264
2022-06-20T07:58:21.851831198Z c Max deg in eqs: 2
2022-06-20T07:58:21.854066651Z c Simple XORs: 1168
2022-06-20T07:58:21.854096420Z c Num vars set: 0
2022-06-20T07:58:21.854173072Z c Num vars replaced: 0
2022-06-20T07:58:21.854187830Z c --------------------
2022-06-20T07:58:21.854293599Z c [ANF hash] Calculating ANF hash...
2022-06-20T07:58:21.865799096Z c [ANF hash] Done. T: 0.00
2022-06-20T07:58:21.865897327Z c Simplifying....
2022-06-20T07:58:21.865904919Z c [boshp] Running iterative simplification...
2022-06-20T07:58:21.865911085Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:22.769962325Z c [ANF prop] Left eqs: 808 T: 0.90
2022-06-20T07:58:22.770040407Z c [iter-simp] ------ Iteration 0
2022-06-20T07:58:22.770048489Z c [XL] Running XL... ring size: 1920
2022-06-20T07:58:26.127939826Z c [XL] Done. Learnt: 40 T: 3.30
2022-06-20T07:58:26.137337924Z c [XL] learnt 9 new facts in 3.31 seconds.
2022-06-20T07:58:26.137424810Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:26.158797584Z c [ANF prop] Left eqs: 817 T: 0.02
2022-06-20T07:58:26.158865648Z c [iter-simp] ------ Iteration 0
2022-06-20T07:58:26.158872314Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:58:41.226907049Z c [ElimLin] Done. Learnt: 99 T: 14.84
2022-06-20T07:58:41.231490344Z c [ElimLin] learnt 59 new facts in 14.85 seconds.
2022-06-20T07:58:41.231578187Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:41.368560109Z c [ANF prop] Left eqs: 852 T: 0.14
2022-06-20T07:58:41.368657046Z c [iter-simp] ------ Iteration 0
2022-06-20T07:58:41.372565145Z c [CNF-gen] Number of value assignments = 792
2022-06-20T07:58:41.372637247Z c Number of equiv assigments = 15
2022-06-20T07:58:45.254639690Z c [SAT] learnt 5 new facts in 3.81 seconds.
2022-06-20T07:58:45.254734638Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:45.295582989Z c [ANF prop] Left eqs: 847 T: 0.04
2022-06-20T07:58:45.296101886Z c [iter-simp] ------ Iteration 1
2022-06-20T07:58:45.296130123Z c [XL] Running XL... ring size: 1920
2022-06-20T07:58:46.295489505Z c [XL] Done. Learnt: 70 T: 0.99
2022-06-20T07:58:46.312866172Z c [XL] learnt 14 new facts in 1.01 seconds.
2022-06-20T07:58:46.312959147Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:46.375559114Z c [ANF prop] Left eqs: 851 T: 0.06
2022-06-20T07:58:46.375654804Z c [iter-simp] ------ Iteration 1
2022-06-20T07:58:46.375666038Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:58:50.467696215Z c [ElimLin] Done. Learnt: 79 T: 4.07
2022-06-20T07:58:50.470095980Z c [ElimLin] learnt 14 new facts in 4.07 seconds.
2022-06-20T07:58:50.470149182Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:50.535355868Z c [ANF prop] Left eqs: 865 T: 0.06
2022-06-20T07:58:50.535453328Z c [iter-simp] ------ Iteration 1
2022-06-20T07:58:50.621469804Z c [CNF-gen] Number of value assignments = 802
2022-06-20T07:58:50.621554870Z c Number of equiv assigments = 15
2022-06-20T07:58:54.933100440Z c [SAT] learnt 4 new facts in 4.38 seconds.
2022-06-20T07:58:54.933212770Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:54.969196099Z c [ANF prop] Left eqs: 861 T: 0.04
2022-06-20T07:58:54.969789128Z c [iter-simp] ------ Iteration 2
2022-06-20T07:58:54.969838139Z c [XL] Running XL... ring size: 1920
2022-06-20T07:58:55.889765109Z c [XL] Done. Learnt: 75 T: 0.92
2022-06-20T07:58:55.903924765Z c [XL] learnt 33 new facts in 0.93 seconds.
2022-06-20T07:58:55.904039661Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:55.978438165Z c [ANF prop] Left eqs: 874 T: 0.08
2022-06-20T07:58:55.978535023Z c [iter-simp] ------ Iteration 2
2022-06-20T07:58:55.978545206Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:58:58.761932698Z c [ElimLin] Done. Learnt: 78 T: 2.78
2022-06-20T07:58:58.763874554Z c [ElimLin] learnt 11 new facts in 2.78 seconds.
2022-06-20T07:58:58.763911840Z c [ANF prop] Running ANF propagation...
2022-06-20T07:58:58.834256688Z c [ANF prop] Left eqs: 885 T: 0.07
2022-06-20T07:58:58.834349010Z c [iter-simp] ------ Iteration 2
2022-06-20T07:58:58.938050793Z c [CNF-gen] Number of value assignments = 814
2022-06-20T07:58:58.938142592Z c Number of equiv assigments = 15
2022-06-20T07:59:02.759033216Z c [SAT] learnt 7 new facts in 3.92 seconds.
2022-06-20T07:59:02.759120954Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:02.813073219Z c [ANF prop] Left eqs: 878 T: 0.06
2022-06-20T07:59:02.813595612Z c [iter-simp] ------ Iteration 3
2022-06-20T07:59:02.813628110Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:03.595304894Z c [XL] Done. Learnt: 71 T: 0.78
2022-06-20T07:59:03.607622804Z c [XL] learnt 6 new facts in 0.79 seconds.
2022-06-20T07:59:03.607706063Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:03.636517663Z c [ANF prop] Left eqs: 878 T: 0.03
2022-06-20T07:59:03.636615313Z c [iter-simp] ------ Iteration 3
2022-06-20T07:59:03.636629949Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:06.503275015Z c [ElimLin] Done. Learnt: 80 T: 2.86
2022-06-20T07:59:06.505205142Z c [ElimLin] learnt 12 new facts in 2.86 seconds.
2022-06-20T07:59:06.505251433Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:06.552887902Z c [ANF prop] Left eqs: 890 T: 0.05
2022-06-20T07:59:06.552975282Z c [iter-simp] ------ Iteration 3
2022-06-20T07:59:06.628935508Z c [CNF-gen] Number of value assignments = 824
2022-06-20T07:59:06.629029964Z c Number of equiv assigments = 15
2022-06-20T07:59:10.082231185Z c [SAT] learnt 9 new facts in 3.53 seconds.
2022-06-20T07:59:10.082335692Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:10.245426899Z c [ANF prop] Left eqs: 881 T: 0.16
2022-06-20T07:59:10.246041063Z c [iter-simp] ------ Iteration 4
2022-06-20T07:59:10.246071033Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:11.072053258Z c [XL] Done. Learnt: 71 T: 0.82
2022-06-20T07:59:11.085552069Z c [XL] learnt 12 new facts in 0.84 seconds.
2022-06-20T07:59:11.085639460Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:11.110836285Z c [ANF prop] Left eqs: 886 T: 0.02
2022-06-20T07:59:11.110924175Z c [iter-simp] ------ Iteration 4
2022-06-20T07:59:11.110971998Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:14.878682038Z c [ElimLin] Done. Learnt: 85 T: 3.77
2022-06-20T07:59:14.880571202Z c [ElimLin] learnt 17 new facts in 3.77 seconds.
2022-06-20T07:59:14.880605017Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:14.927853802Z c [ANF prop] Left eqs: 902 T: 0.04
2022-06-20T07:59:14.927934476Z c [iter-simp] ------ Iteration 4
2022-06-20T07:59:15.001706938Z c [CNF-gen] Number of value assignments = 837
2022-06-20T07:59:15.001784388Z c Number of equiv assigments = 15
2022-06-20T07:59:18.613005552Z c [SAT] learnt 12 new facts in 3.69 seconds.
2022-06-20T07:59:18.613105080Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:18.663592353Z c [ANF prop] Left eqs: 888 T: 0.05
2022-06-20T07:59:18.664302469Z c [iter-simp] ------ Iteration 5
2022-06-20T07:59:18.664340439Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:19.426965627Z c [XL] Done. Learnt: 71 T: 0.76
2022-06-20T07:59:19.437345746Z c [XL] learnt 13 new facts in 0.77 seconds.
2022-06-20T07:59:19.437449821Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:19.454591070Z c [ANF prop] Left eqs: 891 T: 0.02
2022-06-20T07:59:19.454680105Z c [iter-simp] ------ Iteration 5
2022-06-20T07:59:19.454689408Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:23.942814972Z c [ElimLin] Done. Learnt: 103 T: 4.49
2022-06-20T07:59:23.949122717Z c [ElimLin] learnt 34 new facts in 4.49 seconds.
2022-06-20T07:59:23.949195092Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:24.034200227Z c [ANF prop] Left eqs: 913 T: 0.09
2022-06-20T07:59:24.034299719Z c [iter-simp] ------ Iteration 5
2022-06-20T07:59:24.115732697Z c [CNF-gen] Number of value assignments = 853
2022-06-20T07:59:24.115826187Z c Number of equiv assigments = 18
2022-06-20T07:59:27.089524936Z c [SAT] learnt 13 new facts in 3.05 seconds.
2022-06-20T07:59:27.089614748Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:27.169555359Z c [ANF prop] Left eqs: 896 T: 0.08
2022-06-20T07:59:27.170697483Z c [iter-simp] ------ Iteration 6
2022-06-20T07:59:27.170733702Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:27.921510766Z c [XL] Done. Learnt: 87 T: 0.75
2022-06-20T07:59:27.931854032Z c [XL] learnt 24 new facts in 0.76 seconds.
2022-06-20T07:59:27.931944701Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:27.962633094Z c [ANF prop] Left eqs: 908 T: 0.03
2022-06-20T07:59:27.962731885Z c [iter-simp] ------ Iteration 6
2022-06-20T07:59:27.962747578Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:31.781160183Z c [ElimLin] Done. Learnt: 111 T: 3.82
2022-06-20T07:59:31.782785054Z c [ElimLin] learnt 29 new facts in 3.82 seconds.
2022-06-20T07:59:31.782826232Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:31.896200672Z c [ANF prop] Left eqs: 908 T: 0.11
2022-06-20T07:59:31.896289048Z c [iter-simp] ------ Iteration 6
2022-06-20T07:59:31.962825438Z c [CNF-gen] Number of value assignments = 882
2022-06-20T07:59:31.962924770Z c Number of equiv assigments = 28
2022-06-20T07:59:34.661815546Z c [SAT] learnt 12 new facts in 2.76 seconds.
2022-06-20T07:59:34.661936221Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:34.727860991Z c [ANF prop] Left eqs: 898 T: 0.06
2022-06-20T07:59:34.728569188Z c [iter-simp] ------ Iteration 7
2022-06-20T07:59:34.728595537Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:35.336091982Z c [XL] Done. Learnt: 88 T: 0.60
2022-06-20T07:59:35.345916057Z c [XL] learnt 28 new facts in 0.62 seconds.
2022-06-20T07:59:35.346001907Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:35.368619827Z c [ANF prop] Left eqs: 915 T: 0.02
2022-06-20T07:59:35.368708689Z c [iter-simp] ------ Iteration 7
2022-06-20T07:59:35.368720660Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:40.231021324Z c [ElimLin] Done. Learnt: 132 T: 4.86
2022-06-20T07:59:40.233582906Z c [ElimLin] learnt 49 new facts in 4.86 seconds.
2022-06-20T07:59:40.233632430Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:40.330154049Z c [ANF prop] Left eqs: 898 T: 0.10
2022-06-20T07:59:40.330242902Z c [iter-simp] ------ Iteration 7
2022-06-20T07:59:40.390813583Z c [CNF-gen] Number of value assignments = 910
2022-06-20T07:59:40.390902131Z c Number of equiv assigments = 36
2022-06-20T07:59:42.610645098Z c [SAT] learnt 7 new facts in 2.28 seconds.
2022-06-20T07:59:42.610737296Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:42.646195297Z c [ANF prop] Left eqs: 888 T: 0.04
2022-06-20T07:59:42.647039607Z c [iter-simp] ------ Iteration 8
2022-06-20T07:59:42.647065952Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:43.190866671Z c [XL] Done. Learnt: 110 T: 0.54
2022-06-20T07:59:43.199209295Z c [XL] learnt 50 new facts in 0.55 seconds.
2022-06-20T07:59:43.199290514Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:43.257203695Z c [ANF prop] Left eqs: 894 T: 0.06
2022-06-20T07:59:43.257285621Z c [iter-simp] ------ Iteration 8
2022-06-20T07:59:43.257297947Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:47.270156265Z c [ElimLin] Done. Learnt: 127 T: 4.01
2022-06-20T07:59:47.272524026Z c [ElimLin] learnt 33 new facts in 4.02 seconds.
2022-06-20T07:59:47.272595541Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:47.332473907Z c [ANF prop] Left eqs: 919 T: 0.06
2022-06-20T07:59:47.332566629Z c [iter-simp] ------ Iteration 8
2022-06-20T07:59:47.385981735Z c [CNF-gen] Number of value assignments = 935
2022-06-20T07:59:47.386062644Z c Number of equiv assigments = 42
2022-06-20T07:59:49.766131035Z c [SAT] learnt 9 new facts in 2.43 seconds.
2022-06-20T07:59:49.766214333Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:49.824292292Z c [ANF prop] Left eqs: 894 T: 0.06
2022-06-20T07:59:49.825107979Z c [iter-simp] ------ Iteration 9
2022-06-20T07:59:49.825133936Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:50.357870207Z c [XL] Done. Learnt: 108 T: 0.53
2022-06-20T07:59:50.366334463Z c [XL] learnt 38 new facts in 0.54 seconds.
2022-06-20T07:59:50.366423621Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:50.416525014Z c [ANF prop] Left eqs: 910 T: 0.05
2022-06-20T07:59:50.416601681Z c [iter-simp] ------ Iteration 9
2022-06-20T07:59:50.416611980Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:53.273058749Z c [ElimLin] Done. Learnt: 112 T: 2.86
2022-06-20T07:59:53.275078584Z c [ElimLin] learnt 15 new facts in 2.86 seconds.
2022-06-20T07:59:53.275120226Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:53.339225501Z c [ANF prop] Left eqs: 917 T: 0.06
2022-06-20T07:59:53.339314830Z c [iter-simp] ------ Iteration 9
2022-06-20T07:59:53.412038897Z c [CNF-gen] Number of value assignments = 956
2022-06-20T07:59:53.412123888Z c Number of equiv assigments = 48
2022-06-20T07:59:55.507490488Z c [SAT] learnt 8 new facts in 2.16 seconds.
2022-06-20T07:59:55.507580500Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:55.567542990Z c [ANF prop] Left eqs: 902 T: 0.06
2022-06-20T07:59:55.568355624Z c [iter-simp] ------ Iteration 10
2022-06-20T07:59:55.568380533Z c [XL] Running XL... ring size: 1920
2022-06-20T07:59:56.034057014Z c [XL] Done. Learnt: 104 T: 0.46
2022-06-20T07:59:56.040183340Z c [XL] learnt 26 new facts in 0.47 seconds.
2022-06-20T07:59:56.040260846Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:56.067725858Z c [ANF prop] Left eqs: 901 T: 0.02
2022-06-20T07:59:56.067807139Z c [iter-simp] ------ Iteration 10
2022-06-20T07:59:56.067819223Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T07:59:59.645220405Z c [ElimLin] Done. Learnt: 128 T: 3.58
2022-06-20T07:59:59.647154176Z c [ElimLin] learnt 33 new facts in 3.58 seconds.
2022-06-20T07:59:59.647194462Z c [ANF prop] Running ANF propagation...
2022-06-20T07:59:59.718167267Z c [ANF prop] Left eqs: 911 T: 0.07
2022-06-20T07:59:59.718291005Z c [iter-simp] ------ Iteration 10
2022-06-20T07:59:59.765949081Z c [CNF-gen] Number of value assignments = 984
2022-06-20T07:59:59.766028518Z c Number of equiv assigments = 55
2022-06-20T08:00:01.826250829Z c [SAT] learnt 9 new facts in 2.11 seconds.
2022-06-20T08:00:01.826326359Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:01.891122043Z c [ANF prop] Left eqs: 902 T: 0.06
2022-06-20T08:00:01.892364967Z c [iter-simp] ------ Iteration 11
2022-06-20T08:00:01.892398426Z c [XL] Running XL... ring size: 1920
2022-06-20T08:00:02.524764928Z c [XL] Done. Learnt: 109 T: 0.63
2022-06-20T08:00:02.530938259Z c [XL] learnt 29 new facts in 0.64 seconds.
2022-06-20T08:00:02.531020246Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:02.557478092Z c [ANF prop] Left eqs: 917 T: 0.03
2022-06-20T08:00:02.557561234Z c [iter-simp] ------ Iteration 11
2022-06-20T08:00:02.557573516Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T08:00:05.511004820Z c [ElimLin] Done. Learnt: 130 T: 2.95
2022-06-20T08:00:05.512747579Z c [ElimLin] learnt 28 new facts in 2.95 seconds.
2022-06-20T08:00:05.512790493Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:05.592247821Z c [ANF prop] Left eqs: 898 T: 0.08
2022-06-20T08:00:05.592336615Z c [iter-simp] ------ Iteration 11
2022-06-20T08:00:05.635623341Z c [CNF-gen] Number of value assignments = 1008
2022-06-20T08:00:05.635709815Z c Number of equiv assigments = 68
2022-06-20T08:00:06.671523225Z c [SAT] learnt 1 new facts in 1.08 seconds.
2022-06-20T08:00:06.671610062Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:06.697521482Z c [ANF prop] Left eqs: 897 T: 0.03
2022-06-20T08:00:06.698409972Z c [iter-simp] ------ Iteration 12
2022-06-20T08:00:06.698438465Z c [XL] Running XL... ring size: 1920
2022-06-20T08:00:07.111982401Z c [XL] Done. Learnt: 121 T: 0.41
2022-06-20T08:00:07.116467059Z c [XL] learnt 51 new facts in 0.42 seconds.
2022-06-20T08:00:07.116541073Z c [ANF prop] Running ANF propagation...
2022-06-20T08:00:07.155870081Z c [ANF prop] Left eqs: 904 T: 0.04
2022-06-20T08:00:07.155961179Z c [iter-simp] ------ Iteration 12
2022-06-20T08:00:07.155972878Z c [ElimLin] Running ElimLin... ring size: 1920
2022-06-20T08:00:08.358255336Z c [GJ] UnSAT
2022-06-20T08:00:08.358341190Z c [ElimLin] learnt 0 new facts in 1.20 seconds.
2022-06-20T08:00:08.397669682Z c [ after 12.2 iteration(s) in 106.01 seconds.]
2022-06-20T08:00:08.397755334Z c Simplifying finished.
2022-06-20T08:00:08.397772071Z c ---- ANF stats -----
2022-06-20T08:00:08.397779898Z c Num total vars: 1920
2022-06-20T08:00:08.397826334Z c Num free vars: 862
2022-06-20T08:00:08.397834030Z c Num equations: 904
2022-06-20T08:00:08.401528820Z c Num monoms in eqs: 27752
2022-06-20T08:00:08.404940346Z c Max deg in eqs: 2
2022-06-20T08:00:08.404995352Z c Simple XORs: 256
2022-06-20T08:00:08.405005318Z c Num vars set: 1025
2022-06-20T08:00:08.405011921Z c Num vars replaced: 71
2022-06-20T08:00:08.405018350Z c --------------------
2022-06-20T08:00:08.427854447Z c [CNF-out] added UNSAT to CNF
2022-06-20T08:00:08.432458504Z c [CNF-gen] Number of value assignments = 1025
2022-06-20T08:00:08.432530241Z c Number of equiv assigments = 71
2022-06-20T08:00:08.871734367Z c [CNF conversion] in 0.44 seconds.
2022-06-20T08:00:08.871803920Z c ---- CNF stats -----
2022-06-20T08:00:08.871814251Z c Map sizes            : 15816/21627
2022-06-20T08:00:08.871823135Z c Clause Sets          : 15897
2022-06-20T08:00:08.871830112Z c Added as CNF         : 53
2022-06-20T08:00:08.871836314Z c Added as simple ANF  : 1352
2022-06-20T08:00:08.871842314Z c Added as complex  ANF: 595
2022-06-20T08:00:08.871848690Z c --------------------
2022-06-20T08:00:09.843517509Z s ANF-UNSATISFIABLE
2022-06-20T08:00:09.852624934Z c Learnt 918 fact(s) in 111.32 seconds using 172.41MB.
msoos commented 2 years ago

Hi, let me reopen this issue. I can't download the file round4rxoodooMess.anf. Can you please send it over or re-attach it? I'd love to see what happened here. Maybe there is a bug. I'm sorry for the very late response :( Can you please send me the file so I can debug?

Thank you in advance, and sorry again for the late response,

Mate

HuinaLi commented 2 years ago

Thanks, Mate. I have re-upload the complete file, please click this link. https://github.com/Lihuina/huina_bosphorus_sagemath/blob/main/huina_bosphorus/bosphorus_code/round4rxoodooMess.anf. But actually, the problem was gone when I rebuilt the latest Bosphorus, but I don't know whether it is because of my compilation problem or other reasons. My new log file is attached. bosphorus_code.zip round4rxoodooMess.log

msoos commented 2 years ago

Oh, OK, so maybe it was a linking issue. Thanks, I'll keep this in mind, maybe I'll fuzz the system a bit more to see if we can find some issues. Thank you again! And let us know how you think we could improve it :)

Is it faster than the the system in SageMath?

HuinaLi commented 2 years ago

Yes:), it is so cool!

For Sagemath, we takes 107.10 seconds on solving this problem, but for Bosphorus, only takes 13.25 seconds!

Bosphorus has been very useful on some problems I've been working on and has produced good results. Many thanks for your great work!

Huina

msoos commented 2 years ago

Great to hear! :smiley: Thanks for the kind feedback!