%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SWV497-1.040 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % Computer : n012.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 : Wed Jul 20 18:21:27 EDT 2022 % Result : Satisfiable 0.52s 0.70s % Output : CNFRefutation 0.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV497-1.040 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.12/0.33 % Computer : n012.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 : Thu Jun 16 01:24:39 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.40 # No SInE strategy applied % 0.19/0.40 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.19/0.40 # and selection function SelectComplexExceptUniqMaxHorn. % 0.19/0.40 # % 0.19/0.40 # Presaturation interreduction done % 0.19/0.40 # Number of axioms: 863 Number of unprocessed: 863 % 0.19/0.40 # Tableaux proof search. % 0.19/0.40 # APR header successfully linked. % 0.19/0.40 # Hello from C++ % 0.48/0.65 # The folding up rule is enabled... % 0.48/0.65 # Local unification is enabled... % 0.48/0.65 # Any saturation attempts will use folding labels... % 0.48/0.65 # 863 beginning clauses after preprocessing and clausification % 0.48/0.65 # Creating start rules for all 1 conjectures. % 0.48/0.65 # There are 1 start rule candidates: % 0.48/0.65 # Found 862 unit axioms. % 0.48/0.65 # 1 start rule tableaux created. % 0.48/0.65 # 1 extension rule candidate clauses % 0.48/0.65 # 862 unit axiom clauses % 0.48/0.65 % 0.48/0.65 # Requested 8, 32 cores available to the main process. % 0.48/0.65 # There are not enough tableaux to fork, creating more from the initial 1 % 0.48/0.65 # Creating equality axioms % 0.48/0.65 # Ran out of tableaux, making start rules for all clauses % 0.48/0.65 # Returning from population with 870 new_tableaux and 0 remaining starting tableaux. % 0.48/0.65 # We now have 870 tableaux to operate on % 0.52/0.70 # 21993 Satisfiable branch % 0.52/0.70 # Satisfiable branch found. % 0.52/0.70 # There were 1 total branch saturation attempts. % 0.52/0.70 # There were 0 of these attempts blocked. % 0.52/0.70 # There were 0 deferred branch saturation attempts. % 0.52/0.70 # There were 0 free duplicated saturations. % 0.52/0.70 # There were 0 total successful branch saturations. % 0.52/0.70 # There were 0 successful branch saturations in interreduction. % 0.52/0.70 # There were 0 successful branch saturations on the branch. % 0.52/0.70 # There were 0 successful branch saturations after the branch. % 0.52/0.70 # SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.52/0.70 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.52/0.70 # Begin clausification derivation % 0.52/0.70 % 0.52/0.70 # End clausification derivation % 0.52/0.70 # Begin listing active clauses obtained from FOF to CNF conversion % 0.52/0.70 cnf(i_0_905, hypothesis, (store(a_1397,i40,e40)=a_1398)). % 0.52/0.70 cnf(i_0_945, hypothesis, (store(a_1437,i19,e19)=a_1438)). % 0.52/0.70 cnf(i_0_866, hypothesis, (store(a1,i1,e1)=a_1359)). % 0.52/0.70 cnf(i_0_867, hypothesis, (store(a_1359,i2,e2)=a_1360)). % 0.52/0.70 cnf(i_0_868, hypothesis, (store(a_1360,i3,e3)=a_1361)). % 0.52/0.70 cnf(i_0_869, hypothesis, (store(a_1361,i4,e4)=a_1362)). % 0.52/0.70 cnf(i_0_870, hypothesis, (store(a_1362,i5,e5)=a_1363)). % 0.52/0.70 cnf(i_0_871, hypothesis, (store(a_1363,i6,e6)=a_1364)). % 0.52/0.70 cnf(i_0_872, hypothesis, (store(a_1364,i7,e7)=a_1365)). % 0.52/0.70 cnf(i_0_873, hypothesis, (store(a_1365,i8,e8)=a_1366)). % 0.52/0.70 cnf(i_0_874, hypothesis, (store(a_1366,i9,e9)=a_1367)). % 0.52/0.70 cnf(i_0_875, hypothesis, (store(a_1367,i10,e10)=a_1368)). % 0.52/0.70 cnf(i_0_876, hypothesis, (store(a_1368,i11,e11)=a_1369)). % 0.52/0.70 cnf(i_0_877, hypothesis, (store(a_1369,i12,e12)=a_1370)). % 0.52/0.70 cnf(i_0_878, hypothesis, (store(a_1370,i13,e13)=a_1371)). % 0.52/0.70 cnf(i_0_879, hypothesis, (store(a_1371,i14,e14)=a_1372)). % 0.52/0.70 cnf(i_0_880, hypothesis, (store(a_1372,i15,e15)=a_1373)). % 0.52/0.70 cnf(i_0_881, hypothesis, (store(a_1373,i16,e16)=a_1374)). % 0.52/0.70 cnf(i_0_882, hypothesis, (store(a_1374,i17,e17)=a_1375)). % 0.52/0.70 cnf(i_0_883, hypothesis, (store(a_1375,i18,e18)=a_1376)). % 0.52/0.70 cnf(i_0_884, hypothesis, (store(a_1376,i19,e19)=a_1377)). % 0.52/0.70 cnf(i_0_885, hypothesis, (store(a_1377,i20,e20)=a_1378)). % 0.52/0.70 cnf(i_0_886, hypothesis, (store(a_1378,i21,e21)=a_1379)). % 0.52/0.70 cnf(i_0_887, hypothesis, (store(a_1379,i22,e22)=a_1380)). % 0.52/0.70 cnf(i_0_888, hypothesis, (store(a_1380,i23,e23)=a_1381)). % 0.52/0.70 cnf(i_0_889, hypothesis, (store(a_1381,i24,e24)=a_1382)). % 0.52/0.70 cnf(i_0_890, hypothesis, (store(a_1382,i25,e25)=a_1383)). % 0.52/0.70 cnf(i_0_891, hypothesis, (store(a_1383,i26,e26)=a_1384)). % 0.52/0.70 cnf(i_0_892, hypothesis, (store(a_1384,i27,e27)=a_1385)). % 0.52/0.70 cnf(i_0_893, hypothesis, (store(a_1385,i28,e28)=a_1386)). % 0.52/0.70 cnf(i_0_894, hypothesis, (store(a_1386,i29,e29)=a_1387)). % 0.52/0.70 cnf(i_0_895, hypothesis, (store(a_1387,i30,e30)=a_1388)). % 0.52/0.70 cnf(i_0_896, hypothesis, (store(a_1388,i31,e31)=a_1389)). % 0.52/0.70 cnf(i_0_897, hypothesis, (store(a_1389,i32,e32)=a_1390)). % 0.52/0.70 cnf(i_0_898, hypothesis, (store(a_1390,i33,e33)=a_1391)). % 0.52/0.70 cnf(i_0_899, hypothesis, (store(a_1391,i34,e34)=a_1392)). % 0.52/0.70 cnf(i_0_900, hypothesis, (store(a_1392,i35,e35)=a_1393)). % 0.52/0.70 cnf(i_0_901, hypothesis, (store(a_1393,i36,e36)=a_1394)). % 0.52/0.70 cnf(i_0_902, hypothesis, (store(a_1394,i37,e37)=a_1395)). % 0.52/0.70 cnf(i_0_903, hypothesis, (store(a_1395,i38,e38)=a_1396)). % 0.52/0.70 cnf(i_0_904, hypothesis, (store(a_1396,i39,e39)=a_1397)). % 0.52/0.70 cnf(i_0_906, hypothesis, (store(a1,i16,e16)=a_1399)). % 0.52/0.70 cnf(i_0_907, hypothesis, (store(a_1399,i14,e14)=a_1400)). % 0.52/0.70 cnf(i_0_908, hypothesis, (store(a_1400,i24,e24)=a_1401)). % 0.52/0.70 cnf(i_0_909, hypothesis, (store(a_1401,i11,e11)=a_1402)). % 0.52/0.70 cnf(i_0_910, hypothesis, (store(a_1402,i25,e25)=a_1403)). % 0.52/0.70 cnf(i_0_911, hypothesis, (store(a_1403,i17,e17)=a_1404)). % 0.52/0.70 cnf(i_0_912, hypothesis, (store(a_1404,i7,e7)=a_1405)). % 0.52/0.70 cnf(i_0_913, hypothesis, (store(a_1405,i32,e32)=a_1406)). % 0.52/0.70 cnf(i_0_914, hypothesis, (store(a_1406,i6,e6)=a_1407)). % 0.52/0.70 cnf(i_0_915, hypothesis, (store(a_1407,i18,e18)=a_1408)). % 0.52/0.70 cnf(i_0_916, hypothesis, (store(a_1408,i37,e37)=a_1409)). % 0.52/0.70 cnf(i_0_917, hypothesis, (store(a_1409,i31,e31)=a_1410)). % 0.52/0.70 cnf(i_0_918, hypothesis, (store(a_1410,i13,e13)=a_1411)). % 0.52/0.70 cnf(i_0_919, hypothesis, (store(a_1411,i12,e12)=a_1412)). % 0.52/0.70 cnf(i_0_920, hypothesis, (store(a_1412,i36,e36)=a_1413)). % 0.52/0.70 cnf(i_0_921, hypothesis, (store(a_1413,i20,e20)=a_1414)). % 0.52/0.70 cnf(i_0_922, hypothesis, (store(a_1414,i35,e35)=a_1415)). % 0.52/0.70 cnf(i_0_923, hypothesis, (store(a_1415,i23,e23)=a_1416)). % 0.52/0.70 cnf(i_0_924, hypothesis, (store(a_1416,i26,e26)=a_1417)). % 0.52/0.70 cnf(i_0_925, hypothesis, (store(a_1417,i21,e21)=a_1418)). % 0.52/0.70 cnf(i_0_926, hypothesis, (store(a_1418,i27,e27)=a_1419)). % 0.52/0.70 cnf(i_0_927, hypothesis, (store(a_1419,i10,e10)=a_1420)). % 0.52/0.70 cnf(i_0_928, hypothesis, (store(a_1420,i22,e22)=a_1421)). % 0.52/0.70 cnf(i_0_929, hypothesis, (store(a_1421,i8,e8)=a_1422)). % 0.52/0.70 cnf(i_0_930, hypothesis, (store(a_1422,i33,e33)=a_1423)). % 0.52/0.70 cnf(i_0_931, hypothesis, (store(a_1423,i2,e2)=a_1424)). % 0.52/0.70 cnf(i_0_932, hypothesis, (store(a_1424,i40,e40)=a_1425)). % 0.52/0.70 cnf(i_0_933, hypothesis, (store(a_1425,i38,e38)=a_1426)). % 0.52/0.70 cnf(i_0_934, hypothesis, (store(a_1426,i39,e39)=a_1427)). % 0.52/0.70 cnf(i_0_935, hypothesis, (store(a_1427,i1,e1)=a_1428)). % 0.52/0.70 cnf(i_0_936, hypothesis, (store(a_1428,i9,e9)=a_1429)). % 0.52/0.70 cnf(i_0_937, hypothesis, (store(a_1429,i3,e3)=a_1430)). % 0.52/0.70 cnf(i_0_938, hypothesis, (store(a_1430,i5,e5)=a_1431)). % 0.52/0.70 cnf(i_0_939, hypothesis, (store(a_1431,i4,e4)=a_1432)). % 0.52/0.70 cnf(i_0_940, hypothesis, (store(a_1432,i30,e30)=a_1433)). % 0.52/0.70 cnf(i_0_941, hypothesis, (store(a_1433,i15,e15)=a_1434)). % 0.52/0.70 cnf(i_0_942, hypothesis, (store(a_1434,i34,e34)=a_1435)). % 0.52/0.70 cnf(i_0_943, hypothesis, (store(a_1435,i28,e28)=a_1436)). % 0.52/0.70 cnf(i_0_944, hypothesis, (store(a_1436,i29,e29)=a_1437)). % 0.52/0.70 cnf(i_0_864, plain, (select(store(X1,X2,X3),X2)=X3)). % 0.52/0.70 cnf(i_0_1726, negated_conjecture, (a_1438!=a_1398)). % 0.52/0.70 cnf(i_0_1725, hypothesis, (i2!=i1)). % 0.52/0.70 cnf(i_0_1724, hypothesis, (i3!=i1)). % 0.52/0.70 cnf(i_0_1686, hypothesis, (i3!=i2)). % 0.52/0.70 cnf(i_0_1723, hypothesis, (i4!=i1)). % 0.52/0.70 cnf(i_0_1685, hypothesis, (i4!=i2)). % 0.52/0.70 cnf(i_0_1648, hypothesis, (i4!=i3)). % 0.52/0.70 cnf(i_0_1722, hypothesis, (i5!=i1)). % 0.52/0.70 cnf(i_0_1684, hypothesis, (i5!=i2)). % 0.52/0.70 cnf(i_0_1647, hypothesis, (i5!=i3)). % 0.52/0.70 cnf(i_0_1611, hypothesis, (i5!=i4)). % 0.52/0.70 cnf(i_0_1721, hypothesis, (i6!=i1)). % 0.52/0.70 cnf(i_0_1683, hypothesis, (i6!=i2)). % 0.52/0.70 cnf(i_0_1646, hypothesis, (i6!=i3)). % 0.52/0.70 cnf(i_0_1610, hypothesis, (i6!=i4)). % 0.52/0.70 cnf(i_0_1575, hypothesis, (i6!=i5)). % 0.52/0.70 cnf(i_0_1720, hypothesis, (i7!=i1)). % 0.52/0.70 cnf(i_0_1682, hypothesis, (i7!=i2)). % 0.52/0.70 cnf(i_0_1645, hypothesis, (i7!=i3)). % 0.52/0.70 cnf(i_0_1609, hypothesis, (i7!=i4)). % 0.52/0.70 cnf(i_0_1574, hypothesis, (i7!=i5)). % 0.52/0.70 cnf(i_0_1540, hypothesis, (i7!=i6)). % 0.52/0.70 cnf(i_0_1719, hypothesis, (i8!=i1)). % 0.52/0.70 cnf(i_0_1681, hypothesis, (i8!=i2)). % 0.52/0.70 cnf(i_0_1644, hypothesis, (i8!=i3)). % 0.52/0.70 cnf(i_0_1608, hypothesis, (i8!=i4)). % 0.52/0.70 cnf(i_0_1573, hypothesis, (i8!=i5)). % 0.52/0.70 cnf(i_0_1539, hypothesis, (i8!=i6)). % 0.52/0.70 cnf(i_0_1506, hypothesis, (i8!=i7)). % 0.52/0.70 cnf(i_0_1718, hypothesis, (i9!=i1)). % 0.52/0.70 cnf(i_0_1680, hypothesis, (i9!=i2)). % 0.52/0.70 cnf(i_0_1643, hypothesis, (i9!=i3)). % 0.52/0.70 cnf(i_0_1607, hypothesis, (i9!=i4)). % 0.52/0.70 cnf(i_0_1572, hypothesis, (i9!=i5)). % 0.52/0.70 cnf(i_0_1538, hypothesis, (i9!=i6)). % 0.52/0.70 cnf(i_0_1505, hypothesis, (i9!=i7)). % 0.52/0.70 cnf(i_0_1473, hypothesis, (i9!=i8)). % 0.52/0.70 cnf(i_0_1717, hypothesis, (i10!=i1)). % 0.52/0.70 cnf(i_0_1679, hypothesis, (i10!=i2)). % 0.52/0.70 cnf(i_0_1642, hypothesis, (i10!=i3)). % 0.52/0.70 cnf(i_0_1606, hypothesis, (i10!=i4)). % 0.52/0.70 cnf(i_0_1571, hypothesis, (i10!=i5)). % 0.52/0.70 cnf(i_0_1537, hypothesis, (i10!=i6)). % 0.52/0.70 cnf(i_0_1504, hypothesis, (i10!=i7)). % 0.52/0.70 cnf(i_0_1472, hypothesis, (i10!=i8)). % 0.52/0.70 cnf(i_0_1441, hypothesis, (i10!=i9)). % 0.52/0.70 cnf(i_0_1716, hypothesis, (i11!=i1)). % 0.52/0.70 cnf(i_0_1678, hypothesis, (i11!=i2)). % 0.52/0.70 cnf(i_0_1641, hypothesis, (i11!=i3)). % 0.52/0.70 cnf(i_0_1605, hypothesis, (i11!=i4)). % 0.52/0.70 cnf(i_0_1570, hypothesis, (i11!=i5)). % 0.52/0.70 cnf(i_0_1536, hypothesis, (i11!=i6)). % 0.52/0.70 cnf(i_0_1503, hypothesis, (i11!=i7)). % 0.52/0.70 cnf(i_0_1471, hypothesis, (i11!=i8)). % 0.52/0.70 cnf(i_0_1440, hypothesis, (i11!=i9)). % 0.52/0.70 cnf(i_0_1410, hypothesis, (i11!=i10)). % 0.52/0.70 cnf(i_0_1715, hypothesis, (i12!=i1)). % 0.52/0.70 cnf(i_0_1677, hypothesis, (i12!=i2)). % 0.52/0.70 cnf(i_0_1640, hypothesis, (i12!=i3)). % 0.52/0.70 cnf(i_0_1604, hypothesis, (i12!=i4)). % 0.52/0.70 cnf(i_0_1569, hypothesis, (i12!=i5)). % 0.52/0.70 cnf(i_0_1535, hypothesis, (i12!=i6)). % 0.52/0.70 cnf(i_0_1502, hypothesis, (i12!=i7)). % 0.52/0.70 cnf(i_0_1470, hypothesis, (i12!=i8)). % 0.52/0.70 cnf(i_0_1439, hypothesis, (i12!=i9)). % 0.52/0.70 cnf(i_0_1409, hypothesis, (i12!=i10)). % 0.52/0.70 cnf(i_0_1380, hypothesis, (i12!=i11)). % 0.52/0.70 cnf(i_0_1714, hypothesis, (i13!=i1)). % 0.52/0.70 cnf(i_0_1676, hypothesis, (i13!=i2)). % 0.52/0.70 cnf(i_0_1639, hypothesis, (i13!=i3)). % 0.52/0.70 cnf(i_0_1603, hypothesis, (i13!=i4)). % 0.52/0.70 cnf(i_0_1568, hypothesis, (i13!=i5)). % 0.52/0.70 cnf(i_0_1534, hypothesis, (i13!=i6)). % 0.52/0.70 cnf(i_0_1501, hypothesis, (i13!=i7)). % 0.52/0.70 cnf(i_0_1469, hypothesis, (i13!=i8)). % 0.52/0.70 cnf(i_0_1438, hypothesis, (i13!=i9)). % 0.52/0.70 cnf(i_0_1408, hypothesis, (i13!=i10)). % 0.52/0.70 cnf(i_0_1379, hypothesis, (i13!=i11)). % 0.52/0.70 cnf(i_0_1351, hypothesis, (i13!=i12)). % 0.52/0.70 cnf(i_0_1713, hypothesis, (i14!=i1)). % 0.52/0.70 cnf(i_0_1675, hypothesis, (i14!=i2)). % 0.52/0.70 cnf(i_0_1638, hypothesis, (i14!=i3)). % 0.52/0.70 cnf(i_0_1602, hypothesis, (i14!=i4)). % 0.52/0.70 cnf(i_0_1567, hypothesis, (i14!=i5)). % 0.52/0.70 cnf(i_0_1533, hypothesis, (i14!=i6)). % 0.52/0.70 cnf(i_0_1500, hypothesis, (i14!=i7)). % 0.52/0.70 cnf(i_0_1468, hypothesis, (i14!=i8)). % 0.52/0.70 cnf(i_0_1437, hypothesis, (i14!=i9)). % 0.52/0.70 cnf(i_0_1407, hypothesis, (i14!=i10)). % 0.52/0.70 cnf(i_0_1378, hypothesis, (i14!=i11)). % 0.52/0.70 cnf(i_0_1350, hypothesis, (i14!=i12)). % 0.52/0.70 cnf(i_0_1323, hypothesis, (i14!=i13)). % 0.52/0.70 cnf(i_0_1712, hypothesis, (i15!=i1)). % 0.52/0.70 cnf(i_0_1674, hypothesis, (i15!=i2)). % 0.52/0.70 cnf(i_0_1637, hypothesis, (i15!=i3)). % 0.52/0.70 cnf(i_0_1601, hypothesis, (i15!=i4)). % 0.52/0.70 cnf(i_0_1566, hypothesis, (i15!=i5)). % 0.52/0.70 cnf(i_0_1532, hypothesis, (i15!=i6)). % 0.52/0.70 cnf(i_0_1499, hypothesis, (i15!=i7)). % 0.52/0.70 cnf(i_0_1467, hypothesis, (i15!=i8)). % 0.52/0.70 cnf(i_0_1436, hypothesis, (i15!=i9)). % 0.52/0.70 cnf(i_0_1406, hypothesis, (i15!=i10)). % 0.52/0.70 cnf(i_0_1377, hypothesis, (i15!=i11)). % 0.52/0.70 cnf(i_0_1349, hypothesis, (i15!=i12)). % 0.52/0.70 cnf(i_0_1322, hypothesis, (i15!=i13)). % 0.52/0.70 cnf(i_0_1296, hypothesis, (i15!=i14)). % 0.52/0.70 cnf(i_0_1711, hypothesis, (i16!=i1)). % 0.52/0.70 cnf(i_0_1673, hypothesis, (i16!=i2)). % 0.52/0.70 cnf(i_0_1636, hypothesis, (i16!=i3)). % 0.52/0.70 cnf(i_0_1600, hypothesis, (i16!=i4)). % 0.52/0.70 cnf(i_0_1565, hypothesis, (i16!=i5)). % 0.52/0.70 cnf(i_0_1531, hypothesis, (i16!=i6)). % 0.52/0.70 cnf(i_0_1498, hypothesis, (i16!=i7)). % 0.52/0.70 cnf(i_0_1466, hypothesis, (i16!=i8)). % 0.52/0.70 cnf(i_0_1435, hypothesis, (i16!=i9)). % 0.52/0.70 cnf(i_0_1405, hypothesis, (i16!=i10)). % 0.52/0.70 cnf(i_0_1376, hypothesis, (i16!=i11)). % 0.52/0.70 cnf(i_0_1348, hypothesis, (i16!=i12)). % 0.52/0.70 cnf(i_0_1321, hypothesis, (i16!=i13)). % 0.52/0.70 cnf(i_0_1295, hypothesis, (i16!=i14)). % 0.52/0.70 cnf(i_0_1270, hypothesis, (i16!=i15)). % 0.52/0.70 cnf(i_0_1710, hypothesis, (i17!=i1)). % 0.52/0.70 cnf(i_0_1672, hypothesis, (i17!=i2)). % 0.52/0.70 cnf(i_0_1635, hypothesis, (i17!=i3)). % 0.52/0.70 cnf(i_0_1599, hypothesis, (i17!=i4)). % 0.52/0.70 cnf(i_0_1564, hypothesis, (i17!=i5)). % 0.52/0.70 cnf(i_0_1530, hypothesis, (i17!=i6)). % 0.52/0.70 cnf(i_0_1497, hypothesis, (i17!=i7)). % 0.52/0.70 cnf(i_0_1465, hypothesis, (i17!=i8)). % 0.52/0.70 cnf(i_0_1434, hypothesis, (i17!=i9)). % 0.52/0.70 cnf(i_0_1404, hypothesis, (i17!=i10)). % 0.52/0.70 cnf(i_0_1375, hypothesis, (i17!=i11)). % 0.52/0.70 cnf(i_0_1347, hypothesis, (i17!=i12)). % 0.52/0.70 cnf(i_0_1320, hypothesis, (i17!=i13)). % 0.52/0.70 cnf(i_0_1294, hypothesis, (i17!=i14)). % 0.52/0.70 cnf(i_0_1269, hypothesis, (i17!=i15)). % 0.52/0.70 cnf(i_0_1245, hypothesis, (i17!=i16)). % 0.52/0.70 cnf(i_0_1709, hypothesis, (i18!=i1)). % 0.52/0.70 cnf(i_0_1671, hypothesis, (i18!=i2)). % 0.52/0.70 cnf(i_0_1634, hypothesis, (i18!=i3)). % 0.52/0.70 cnf(i_0_1598, hypothesis, (i18!=i4)). % 0.52/0.70 cnf(i_0_1563, hypothesis, (i18!=i5)). % 0.52/0.70 cnf(i_0_1529, hypothesis, (i18!=i6)). % 0.52/0.70 cnf(i_0_1496, hypothesis, (i18!=i7)). % 0.52/0.70 cnf(i_0_1464, hypothesis, (i18!=i8)). % 0.52/0.70 cnf(i_0_1433, hypothesis, (i18!=i9)). % 0.52/0.70 cnf(i_0_1403, hypothesis, (i18!=i10)). % 0.52/0.70 cnf(i_0_1374, hypothesis, (i18!=i11)). % 0.52/0.70 cnf(i_0_1346, hypothesis, (i18!=i12)). % 0.52/0.70 cnf(i_0_1319, hypothesis, (i18!=i13)). % 0.52/0.70 cnf(i_0_1293, hypothesis, (i18!=i14)). % 0.52/0.70 cnf(i_0_1268, hypothesis, (i18!=i15)). % 0.52/0.70 cnf(i_0_1244, hypothesis, (i18!=i16)). % 0.52/0.70 cnf(i_0_1221, hypothesis, (i18!=i17)). % 0.52/0.70 cnf(i_0_1708, hypothesis, (i19!=i1)). % 0.52/0.70 cnf(i_0_1670, hypothesis, (i19!=i2)). % 0.52/0.70 cnf(i_0_1633, hypothesis, (i19!=i3)). % 0.52/0.70 cnf(i_0_1597, hypothesis, (i19!=i4)). % 0.52/0.70 cnf(i_0_1562, hypothesis, (i19!=i5)). % 0.52/0.70 cnf(i_0_1528, hypothesis, (i19!=i6)). % 0.52/0.70 cnf(i_0_1495, hypothesis, (i19!=i7)). % 0.52/0.70 cnf(i_0_1463, hypothesis, (i19!=i8)). % 0.52/0.70 cnf(i_0_1432, hypothesis, (i19!=i9)). % 0.52/0.70 cnf(i_0_1402, hypothesis, (i19!=i10)). % 0.52/0.70 cnf(i_0_1373, hypothesis, (i19!=i11)). % 0.52/0.70 cnf(i_0_1345, hypothesis, (i19!=i12)). % 0.52/0.70 cnf(i_0_1318, hypothesis, (i19!=i13)). % 0.52/0.70 cnf(i_0_1292, hypothesis, (i19!=i14)). % 0.52/0.70 cnf(i_0_1267, hypothesis, (i19!=i15)). % 0.52/0.70 cnf(i_0_1243, hypothesis, (i19!=i16)). % 0.52/0.70 cnf(i_0_1220, hypothesis, (i19!=i17)). % 0.52/0.70 cnf(i_0_1198, hypothesis, (i19!=i18)). % 0.52/0.70 cnf(i_0_1707, hypothesis, (i20!=i1)). % 0.52/0.70 cnf(i_0_1669, hypothesis, (i20!=i2)). % 0.52/0.70 cnf(i_0_1632, hypothesis, (i20!=i3)). % 0.52/0.70 cnf(i_0_1596, hypothesis, (i20!=i4)). % 0.52/0.70 cnf(i_0_1561, hypothesis, (i20!=i5)). % 0.52/0.70 cnf(i_0_1527, hypothesis, (i20!=i6)). % 0.52/0.70 cnf(i_0_1494, hypothesis, (i20!=i7)). % 0.52/0.70 cnf(i_0_1462, hypothesis, (i20!=i8)). % 0.52/0.70 cnf(i_0_1431, hypothesis, (i20!=i9)). % 0.52/0.70 cnf(i_0_1401, hypothesis, (i20!=i10)). % 0.52/0.70 cnf(i_0_1372, hypothesis, (i20!=i11)). % 0.52/0.70 cnf(i_0_1344, hypothesis, (i20!=i12)). % 0.52/0.70 cnf(i_0_1317, hypothesis, (i20!=i13)). % 0.52/0.70 cnf(i_0_1291, hypothesis, (i20!=i14)). % 0.52/0.70 cnf(i_0_1266, hypothesis, (i20!=i15)). % 0.52/0.70 cnf(i_0_1242, hypothesis, (i20!=i16)). % 0.52/0.70 cnf(i_0_1219, hypothesis, (i20!=i17)). % 0.52/0.70 cnf(i_0_1197, hypothesis, (i20!=i18)). % 0.52/0.70 cnf(i_0_1176, hypothesis, (i20!=i19)). % 0.52/0.70 cnf(i_0_1706, hypothesis, (i21!=i1)). % 0.52/0.70 cnf(i_0_1668, hypothesis, (i21!=i2)). % 0.52/0.70 cnf(i_0_1631, hypothesis, (i21!=i3)). % 0.52/0.70 cnf(i_0_1595, hypothesis, (i21!=i4)). % 0.52/0.70 cnf(i_0_1560, hypothesis, (i21!=i5)). % 0.52/0.70 cnf(i_0_1526, hypothesis, (i21!=i6)). % 0.52/0.70 cnf(i_0_1493, hypothesis, (i21!=i7)). % 0.52/0.70 cnf(i_0_1461, hypothesis, (i21!=i8)). % 0.52/0.70 cnf(i_0_1430, hypothesis, (i21!=i9)). % 0.52/0.70 cnf(i_0_1400, hypothesis, (i21!=i10)). % 0.52/0.70 cnf(i_0_1371, hypothesis, (i21!=i11)). % 0.52/0.70 cnf(i_0_1343, hypothesis, (i21!=i12)). % 0.52/0.70 cnf(i_0_1316, hypothesis, (i21!=i13)). % 0.52/0.70 cnf(i_0_1290, hypothesis, (i21!=i14)). % 0.52/0.70 cnf(i_0_1265, hypothesis, (i21!=i15)). % 0.52/0.70 cnf(i_0_1241, hypothesis, (i21!=i16)). % 0.52/0.70 cnf(i_0_1218, hypothesis, (i21!=i17)). % 0.52/0.70 cnf(i_0_1196, hypothesis, (i21!=i18)). % 0.52/0.70 cnf(i_0_1175, hypothesis, (i21!=i19)). % 0.52/0.70 cnf(i_0_1155, hypothesis, (i21!=i20)). % 0.52/0.70 cnf(i_0_1705, hypothesis, (i22!=i1)). % 0.52/0.70 cnf(i_0_1667, hypothesis, (i22!=i2)). % 0.52/0.70 cnf(i_0_1630, hypothesis, (i22!=i3)). % 0.52/0.70 cnf(i_0_1594, hypothesis, (i22!=i4)). % 0.52/0.70 cnf(i_0_1559, hypothesis, (i22!=i5)). % 0.52/0.70 cnf(i_0_1525, hypothesis, (i22!=i6)). % 0.52/0.70 cnf(i_0_1492, hypothesis, (i22!=i7)). % 0.52/0.70 cnf(i_0_1460, hypothesis, (i22!=i8)). % 0.52/0.70 cnf(i_0_1429, hypothesis, (i22!=i9)). % 0.52/0.70 cnf(i_0_1399, hypothesis, (i22!=i10)). % 0.52/0.70 cnf(i_0_1370, hypothesis, (i22!=i11)). % 0.52/0.70 cnf(i_0_1342, hypothesis, (i22!=i12)). % 0.52/0.70 cnf(i_0_1315, hypothesis, (i22!=i13)). % 0.52/0.70 cnf(i_0_1289, hypothesis, (i22!=i14)). % 0.52/0.70 cnf(i_0_1264, hypothesis, (i22!=i15)). % 0.52/0.70 cnf(i_0_1240, hypothesis, (i22!=i16)). % 0.52/0.70 cnf(i_0_1217, hypothesis, (i22!=i17)). % 0.52/0.70 cnf(i_0_1195, hypothesis, (i22!=i18)). % 0.52/0.70 cnf(i_0_1174, hypothesis, (i22!=i19)). % 0.52/0.70 cnf(i_0_1154, hypothesis, (i22!=i20)). % 0.52/0.70 cnf(i_0_1135, hypothesis, (i22!=i21)). % 0.52/0.70 cnf(i_0_1704, hypothesis, (i23!=i1)). % 0.52/0.70 cnf(i_0_1666, hypothesis, (i23!=i2)). % 0.52/0.70 cnf(i_0_1629, hypothesis, (i23!=i3)). % 0.52/0.70 cnf(i_0_1593, hypothesis, (i23!=i4)). % 0.52/0.70 cnf(i_0_1558, hypothesis, (i23!=i5)). % 0.52/0.70 cnf(i_0_1524, hypothesis, (i23!=i6)). % 0.52/0.70 cnf(i_0_1491, hypothesis, (i23!=i7)). % 0.52/0.70 cnf(i_0_1459, hypothesis, (i23!=i8)). % 0.52/0.70 cnf(i_0_1428, hypothesis, (i23!=i9)). % 0.52/0.70 cnf(i_0_1398, hypothesis, (i23!=i10)). % 0.52/0.70 cnf(i_0_1369, hypothesis, (i23!=i11)). % 0.52/0.70 cnf(i_0_1341, hypothesis, (i23!=i12)). % 0.52/0.70 cnf(i_0_1314, hypothesis, (i23!=i13)). % 0.52/0.70 cnf(i_0_1288, hypothesis, (i23!=i14)). % 0.52/0.70 cnf(i_0_1263, hypothesis, (i23!=i15)). % 0.52/0.70 cnf(i_0_1239, hypothesis, (i23!=i16)). % 0.52/0.70 cnf(i_0_1216, hypothesis, (i23!=i17)). % 0.52/0.70 cnf(i_0_1194, hypothesis, (i23!=i18)). % 0.52/0.70 cnf(i_0_1173, hypothesis, (i23!=i19)). % 0.52/0.70 cnf(i_0_1153, hypothesis, (i23!=i20)). % 0.52/0.70 cnf(i_0_1134, hypothesis, (i23!=i21)). % 0.52/0.70 cnf(i_0_1116, hypothesis, (i23!=i22)). % 0.52/0.70 cnf(i_0_1703, hypothesis, (i24!=i1)). % 0.52/0.70 cnf(i_0_1665, hypothesis, (i24!=i2)). % 0.52/0.70 cnf(i_0_1628, hypothesis, (i24!=i3)). % 0.52/0.70 cnf(i_0_1592, hypothesis, (i24!=i4)). % 0.52/0.70 cnf(i_0_1557, hypothesis, (i24!=i5)). % 0.52/0.70 cnf(i_0_1523, hypothesis, (i24!=i6)). % 0.52/0.70 cnf(i_0_1490, hypothesis, (i24!=i7)). % 0.52/0.70 cnf(i_0_1458, hypothesis, (i24!=i8)). % 0.52/0.70 cnf(i_0_1427, hypothesis, (i24!=i9)). % 0.52/0.70 cnf(i_0_1397, hypothesis, (i24!=i10)). % 0.52/0.70 cnf(i_0_1368, hypothesis, (i24!=i11)). % 0.52/0.70 cnf(i_0_1340, hypothesis, (i24!=i12)). % 0.52/0.70 cnf(i_0_1313, hypothesis, (i24!=i13)). % 0.52/0.70 cnf(i_0_1287, hypothesis, (i24!=i14)). % 0.52/0.70 cnf(i_0_1262, hypothesis, (i24!=i15)). % 0.52/0.70 cnf(i_0_1238, hypothesis, (i24!=i16)). % 0.52/0.70 cnf(i_0_1215, hypothesis, (i24!=i17)). % 0.52/0.70 cnf(i_0_1193, hypothesis, (i24!=i18)). % 0.52/0.70 cnf(i_0_1172, hypothesis, (i24!=i19)). % 0.52/0.70 cnf(i_0_1152, hypothesis, (i24!=i20)). % 0.52/0.70 cnf(i_0_1133, hypothesis, (i24!=i21)). % 0.52/0.70 cnf(i_0_1115, hypothesis, (i24!=i22)). % 0.52/0.70 cnf(i_0_1098, hypothesis, (i24!=i23)). % 0.52/0.70 cnf(i_0_1702, hypothesis, (i25!=i1)). % 0.52/0.70 cnf(i_0_1664, hypothesis, (i25!=i2)). % 0.52/0.70 cnf(i_0_1627, hypothesis, (i25!=i3)). % 0.52/0.70 cnf(i_0_1591, hypothesis, (i25!=i4)). % 0.52/0.70 cnf(i_0_1556, hypothesis, (i25!=i5)). % 0.52/0.70 cnf(i_0_1522, hypothesis, (i25!=i6)). % 0.52/0.70 cnf(i_0_1489, hypothesis, (i25!=i7)). % 0.52/0.70 cnf(i_0_1457, hypothesis, (i25!=i8)). % 0.52/0.70 cnf(i_0_1426, hypothesis, (i25!=i9)). % 0.52/0.70 cnf(i_0_1396, hypothesis, (i25!=i10)). % 0.52/0.70 cnf(i_0_1367, hypothesis, (i25!=i11)). % 0.52/0.70 cnf(i_0_1339, hypothesis, (i25!=i12)). % 0.52/0.70 cnf(i_0_1312, hypothesis, (i25!=i13)). % 0.52/0.70 cnf(i_0_1286, hypothesis, (i25!=i14)). % 0.52/0.70 cnf(i_0_1261, hypothesis, (i25!=i15)). % 0.52/0.70 cnf(i_0_1237, hypothesis, (i25!=i16)). % 0.52/0.70 cnf(i_0_1214, hypothesis, (i25!=i17)). % 0.52/0.70 cnf(i_0_1192, hypothesis, (i25!=i18)). % 0.52/0.70 cnf(i_0_1171, hypothesis, (i25!=i19)). % 0.52/0.70 cnf(i_0_1151, hypothesis, (i25!=i20)). % 0.52/0.70 cnf(i_0_1132, hypothesis, (i25!=i21)). % 0.52/0.70 cnf(i_0_1114, hypothesis, (i25!=i22)). % 0.52/0.70 cnf(i_0_1097, hypothesis, (i25!=i23)). % 0.52/0.70 cnf(i_0_1081, hypothesis, (i25!=i24)). % 0.52/0.70 cnf(i_0_1701, hypothesis, (i26!=i1)). % 0.52/0.70 cnf(i_0_1663, hypothesis, (i26!=i2)). % 0.52/0.70 cnf(i_0_1626, hypothesis, (i26!=i3)). % 0.52/0.70 cnf(i_0_1590, hypothesis, (i26!=i4)). % 0.52/0.70 cnf(i_0_1555, hypothesis, (i26!=i5)). % 0.52/0.70 cnf(i_0_1521, hypothesis, (i26!=i6)). % 0.52/0.70 cnf(i_0_1488, hypothesis, (i26!=i7)). % 0.52/0.70 cnf(i_0_1456, hypothesis, (i26!=i8)). % 0.52/0.70 cnf(i_0_1425, hypothesis, (i26!=i9)). % 0.52/0.70 cnf(i_0_1395, hypothesis, (i26!=i10)). % 0.52/0.70 cnf(i_0_1366, hypothesis, (i26!=i11)). % 0.52/0.70 cnf(i_0_1338, hypothesis, (i26!=i12)). % 0.52/0.70 cnf(i_0_1311, hypothesis, (i26!=i13)). % 0.52/0.70 cnf(i_0_1285, hypothesis, (i26!=i14)). % 0.52/0.70 cnf(i_0_1260, hypothesis, (i26!=i15)). % 0.52/0.70 cnf(i_0_1236, hypothesis, (i26!=i16)). % 0.52/0.70 cnf(i_0_1213, hypothesis, (i26!=i17)). % 0.52/0.70 cnf(i_0_1191, hypothesis, (i26!=i18)). % 0.52/0.70 cnf(i_0_1170, hypothesis, (i26!=i19)). % 0.52/0.70 cnf(i_0_1150, hypothesis, (i26!=i20)). % 0.52/0.70 cnf(i_0_1131, hypothesis, (i26!=i21)). % 0.52/0.70 cnf(i_0_1113, hypothesis, (i26!=i22)). % 0.52/0.70 cnf(i_0_1096, hypothesis, (i26!=i23)). % 0.52/0.70 cnf(i_0_1080, hypothesis, (i26!=i24)). % 0.52/0.70 cnf(i_0_1065, hypothesis, (i26!=i25)). % 0.52/0.70 cnf(i_0_1700, hypothesis, (i27!=i1)). % 0.52/0.70 cnf(i_0_1662, hypothesis, (i27!=i2)). % 0.52/0.70 cnf(i_0_1625, hypothesis, (i27!=i3)). % 0.52/0.70 cnf(i_0_1589, hypothesis, (i27!=i4)). % 0.52/0.70 cnf(i_0_1554, hypothesis, (i27!=i5)). % 0.52/0.70 cnf(i_0_1520, hypothesis, (i27!=i6)). % 0.52/0.70 cnf(i_0_1487, hypothesis, (i27!=i7)). % 0.52/0.70 cnf(i_0_1455, hypothesis, (i27!=i8)). % 0.52/0.70 cnf(i_0_1424, hypothesis, (i27!=i9)). % 0.52/0.70 cnf(i_0_1394, hypothesis, (i27!=i10)). % 0.52/0.70 cnf(i_0_1365, hypothesis, (i27!=i11)). % 0.52/0.70 cnf(i_0_1337, hypothesis, (i27!=i12)). % 0.52/0.70 cnf(i_0_1310, hypothesis, (i27!=i13)). % 0.52/0.70 cnf(i_0_1284, hypothesis, (i27!=i14)). % 0.52/0.70 cnf(i_0_1259, hypothesis, (i27!=i15)). % 0.52/0.70 cnf(i_0_1235, hypothesis, (i27!=i16)). % 0.52/0.70 cnf(i_0_1212, hypothesis, (i27!=i17)). % 0.52/0.70 cnf(i_0_1190, hypothesis, (i27!=i18)). % 0.52/0.70 cnf(i_0_1169, hypothesis, (i27!=i19)). % 0.52/0.70 cnf(i_0_1149, hypothesis, (i27!=i20)). % 0.52/0.70 cnf(i_0_1130, hypothesis, (i27!=i21)). % 0.52/0.70 cnf(i_0_1112, hypothesis, (i27!=i22)). % 0.52/0.70 cnf(i_0_1095, hypothesis, (i27!=i23)). % 0.52/0.70 cnf(i_0_1079, hypothesis, (i27!=i24)). % 0.52/0.70 cnf(i_0_1064, hypothesis, (i27!=i25)). % 0.52/0.70 cnf(i_0_1050, hypothesis, (i27!=i26)). % 0.52/0.70 cnf(i_0_1699, hypothesis, (i28!=i1)). % 0.52/0.70 cnf(i_0_1661, hypothesis, (i28!=i2)). % 0.52/0.70 cnf(i_0_1624, hypothesis, (i28!=i3)). % 0.52/0.70 cnf(i_0_1588, hypothesis, (i28!=i4)). % 0.52/0.70 cnf(i_0_1553, hypothesis, (i28!=i5)). % 0.52/0.70 cnf(i_0_1519, hypothesis, (i28!=i6)). % 0.52/0.70 cnf(i_0_1486, hypothesis, (i28!=i7)). % 0.52/0.70 cnf(i_0_1454, hypothesis, (i28!=i8)). % 0.52/0.70 cnf(i_0_1423, hypothesis, (i28!=i9)). % 0.52/0.70 cnf(i_0_1393, hypothesis, (i28!=i10)). % 0.52/0.70 cnf(i_0_1364, hypothesis, (i28!=i11)). % 0.52/0.70 cnf(i_0_1336, hypothesis, (i28!=i12)). % 0.52/0.70 cnf(i_0_1309, hypothesis, (i28!=i13)). % 0.52/0.70 cnf(i_0_1283, hypothesis, (i28!=i14)). % 0.52/0.70 cnf(i_0_1258, hypothesis, (i28!=i15)). % 0.52/0.70 cnf(i_0_1234, hypothesis, (i28!=i16)). % 0.52/0.70 cnf(i_0_1211, hypothesis, (i28!=i17)). % 0.52/0.70 cnf(i_0_1189, hypothesis, (i28!=i18)). % 0.52/0.70 cnf(i_0_1168, hypothesis, (i28!=i19)). % 0.52/0.70 cnf(i_0_1148, hypothesis, (i28!=i20)). % 0.52/0.70 cnf(i_0_1129, hypothesis, (i28!=i21)). % 0.52/0.70 cnf(i_0_1111, hypothesis, (i28!=i22)). % 0.52/0.70 cnf(i_0_1094, hypothesis, (i28!=i23)). % 0.52/0.70 cnf(i_0_1078, hypothesis, (i28!=i24)). % 0.52/0.70 cnf(i_0_1063, hypothesis, (i28!=i25)). % 0.52/0.70 cnf(i_0_1049, hypothesis, (i28!=i26)). % 0.52/0.70 cnf(i_0_1036, hypothesis, (i28!=i27)). % 0.52/0.70 cnf(i_0_1698, hypothesis, (i29!=i1)). % 0.52/0.70 cnf(i_0_1660, hypothesis, (i29!=i2)). % 0.52/0.70 cnf(i_0_1623, hypothesis, (i29!=i3)). % 0.52/0.70 cnf(i_0_1587, hypothesis, (i29!=i4)). % 0.52/0.70 cnf(i_0_1552, hypothesis, (i29!=i5)). % 0.52/0.70 cnf(i_0_1518, hypothesis, (i29!=i6)). % 0.52/0.70 cnf(i_0_1485, hypothesis, (i29!=i7)). % 0.52/0.70 cnf(i_0_1453, hypothesis, (i29!=i8)). % 0.52/0.70 cnf(i_0_1422, hypothesis, (i29!=i9)). % 0.52/0.70 cnf(i_0_1392, hypothesis, (i29!=i10)). % 0.52/0.70 cnf(i_0_1363, hypothesis, (i29!=i11)). % 0.52/0.70 cnf(i_0_1335, hypothesis, (i29!=i12)). % 0.52/0.70 cnf(i_0_1308, hypothesis, (i29!=i13)). % 0.52/0.70 cnf(i_0_1282, hypothesis, (i29!=i14)). % 0.52/0.70 cnf(i_0_1257, hypothesis, (i29!=i15)). % 0.52/0.70 cnf(i_0_1233, hypothesis, (i29!=i16)). % 0.52/0.70 cnf(i_0_1210, hypothesis, (i29!=i17)). % 0.52/0.70 cnf(i_0_1188, hypothesis, (i29!=i18)). % 0.52/0.70 cnf(i_0_1167, hypothesis, (i29!=i19)). % 0.52/0.70 cnf(i_0_1147, hypothesis, (i29!=i20)). % 0.52/0.70 cnf(i_0_1128, hypothesis, (i29!=i21)). % 0.52/0.70 cnf(i_0_1110, hypothesis, (i29!=i22)). % 0.52/0.70 cnf(i_0_1093, hypothesis, (i29!=i23)). % 0.52/0.70 cnf(i_0_1077, hypothesis, (i29!=i24)). % 0.52/0.70 cnf(i_0_1062, hypothesis, (i29!=i25)). % 0.52/0.70 cnf(i_0_1048, hypothesis, (i29!=i26)). % 0.52/0.70 cnf(i_0_1035, hypothesis, (i29!=i27)). % 0.52/0.70 cnf(i_0_1023, hypothesis, (i29!=i28)). % 0.52/0.70 cnf(i_0_1697, hypothesis, (i30!=i1)). % 0.52/0.70 cnf(i_0_1659, hypothesis, (i30!=i2)). % 0.52/0.70 cnf(i_0_1622, hypothesis, (i30!=i3)). % 0.52/0.70 cnf(i_0_1586, hypothesis, (i30!=i4)). % 0.52/0.70 cnf(i_0_1551, hypothesis, (i30!=i5)). % 0.52/0.70 cnf(i_0_1517, hypothesis, (i30!=i6)). % 0.52/0.70 cnf(i_0_1484, hypothesis, (i30!=i7)). % 0.52/0.70 cnf(i_0_1452, hypothesis, (i30!=i8)). % 0.52/0.70 cnf(i_0_1421, hypothesis, (i30!=i9)). % 0.52/0.70 cnf(i_0_1391, hypothesis, (i30!=i10)). % 0.52/0.70 cnf(i_0_1362, hypothesis, (i30!=i11)). % 0.52/0.70 cnf(i_0_1334, hypothesis, (i30!=i12)). % 0.52/0.70 cnf(i_0_1307, hypothesis, (i30!=i13)). % 0.52/0.70 cnf(i_0_1281, hypothesis, (i30!=i14)). % 0.52/0.70 cnf(i_0_1256, hypothesis, (i30!=i15)). % 0.52/0.70 cnf(i_0_1232, hypothesis, (i30!=i16)). % 0.52/0.70 cnf(i_0_1209, hypothesis, (i30!=i17)). % 0.52/0.70 cnf(i_0_1187, hypothesis, (i30!=i18)). % 0.52/0.70 cnf(i_0_1166, hypothesis, (i30!=i19)). % 0.52/0.70 cnf(i_0_1146, hypothesis, (i30!=i20)). % 0.52/0.70 cnf(i_0_1127, hypothesis, (i30!=i21)). % 0.52/0.70 cnf(i_0_1109, hypothesis, (i30!=i22)). % 0.52/0.70 cnf(i_0_1092, hypothesis, (i30!=i23)). % 0.52/0.70 cnf(i_0_1076, hypothesis, (i30!=i24)). % 0.52/0.70 cnf(i_0_1061, hypothesis, (i30!=i25)). % 0.52/0.70 cnf(i_0_1047, hypothesis, (i30!=i26)). % 0.52/0.70 cnf(i_0_1034, hypothesis, (i30!=i27)). % 0.52/0.70 cnf(i_0_1022, hypothesis, (i30!=i28)). % 0.52/0.70 cnf(i_0_1011, hypothesis, (i30!=i29)). % 0.52/0.70 cnf(i_0_1696, hypothesis, (i31!=i1)). % 0.52/0.70 cnf(i_0_1658, hypothesis, (i31!=i2)). % 0.52/0.70 cnf(i_0_1621, hypothesis, (i31!=i3)). % 0.52/0.70 cnf(i_0_1585, hypothesis, (i31!=i4)). % 0.52/0.70 cnf(i_0_1550, hypothesis, (i31!=i5)). % 0.52/0.70 cnf(i_0_1516, hypothesis, (i31!=i6)). % 0.52/0.70 cnf(i_0_1483, hypothesis, (i31!=i7)). % 0.52/0.70 cnf(i_0_1451, hypothesis, (i31!=i8)). % 0.52/0.70 cnf(i_0_1420, hypothesis, (i31!=i9)). % 0.52/0.70 cnf(i_0_1390, hypothesis, (i31!=i10)). % 0.52/0.70 cnf(i_0_1361, hypothesis, (i31!=i11)). % 0.52/0.70 cnf(i_0_1333, hypothesis, (i31!=i12)). % 0.52/0.70 cnf(i_0_1306, hypothesis, (i31!=i13)). % 0.52/0.70 cnf(i_0_1280, hypothesis, (i31!=i14)). % 0.52/0.70 cnf(i_0_1255, hypothesis, (i31!=i15)). % 0.52/0.70 cnf(i_0_1231, hypothesis, (i31!=i16)). % 0.52/0.70 cnf(i_0_1208, hypothesis, (i31!=i17)). % 0.52/0.70 cnf(i_0_1186, hypothesis, (i31!=i18)). % 0.52/0.70 cnf(i_0_1165, hypothesis, (i31!=i19)). % 0.52/0.70 cnf(i_0_1145, hypothesis, (i31!=i20)). % 0.52/0.70 cnf(i_0_1126, hypothesis, (i31!=i21)). % 0.52/0.70 cnf(i_0_1108, hypothesis, (i31!=i22)). % 0.52/0.70 cnf(i_0_1091, hypothesis, (i31!=i23)). % 0.52/0.70 cnf(i_0_1075, hypothesis, (i31!=i24)). % 0.52/0.70 cnf(i_0_1060, hypothesis, (i31!=i25)). % 0.52/0.70 cnf(i_0_1046, hypothesis, (i31!=i26)). % 0.52/0.70 cnf(i_0_1033, hypothesis, (i31!=i27)). % 0.52/0.70 cnf(i_0_1021, hypothesis, (i31!=i28)). % 0.52/0.70 cnf(i_0_1010, hypothesis, (i31!=i29)). % 0.52/0.70 cnf(i_0_1000, hypothesis, (i31!=i30)). % 0.52/0.70 cnf(i_0_1695, hypothesis, (i32!=i1)). % 0.52/0.70 cnf(i_0_1657, hypothesis, (i32!=i2)). % 0.52/0.70 cnf(i_0_1620, hypothesis, (i32!=i3)). % 0.52/0.70 cnf(i_0_1584, hypothesis, (i32!=i4)). % 0.52/0.70 cnf(i_0_1549, hypothesis, (i32!=i5)). % 0.52/0.70 cnf(i_0_1515, hypothesis, (i32!=i6)). % 0.52/0.70 cnf(i_0_1482, hypothesis, (i32!=i7)). % 0.52/0.70 cnf(i_0_1450, hypothesis, (i32!=i8)). % 0.52/0.70 cnf(i_0_1419, hypothesis, (i32!=i9)). % 0.52/0.70 cnf(i_0_1389, hypothesis, (i32!=i10)). % 0.52/0.70 cnf(i_0_1360, hypothesis, (i32!=i11)). % 0.52/0.70 cnf(i_0_1332, hypothesis, (i32!=i12)). % 0.52/0.70 cnf(i_0_1305, hypothesis, (i32!=i13)). % 0.52/0.70 cnf(i_0_1279, hypothesis, (i32!=i14)). % 0.52/0.70 cnf(i_0_1254, hypothesis, (i32!=i15)). % 0.52/0.70 cnf(i_0_1230, hypothesis, (i32!=i16)). % 0.52/0.70 cnf(i_0_1207, hypothesis, (i32!=i17)). % 0.52/0.70 cnf(i_0_1185, hypothesis, (i32!=i18)). % 0.52/0.70 cnf(i_0_1164, hypothesis, (i32!=i19)). % 0.52/0.70 cnf(i_0_1144, hypothesis, (i32!=i20)). % 0.52/0.70 cnf(i_0_1125, hypothesis, (i32!=i21)). % 0.52/0.70 cnf(i_0_1107, hypothesis, (i32!=i22)). % 0.52/0.70 cnf(i_0_1090, hypothesis, (i32!=i23)). % 0.52/0.70 cnf(i_0_1074, hypothesis, (i32!=i24)). % 0.52/0.70 cnf(i_0_1059, hypothesis, (i32!=i25)). % 0.52/0.70 cnf(i_0_1045, hypothesis, (i32!=i26)). % 0.52/0.70 cnf(i_0_1032, hypothesis, (i32!=i27)). % 0.52/0.70 cnf(i_0_1020, hypothesis, (i32!=i28)). % 0.52/0.70 cnf(i_0_1009, hypothesis, (i32!=i29)). % 0.52/0.70 cnf(i_0_999, hypothesis, (i32!=i30)). % 0.52/0.70 cnf(i_0_990, hypothesis, (i32!=i31)). % 0.52/0.70 cnf(i_0_1694, hypothesis, (i33!=i1)). % 0.52/0.70 cnf(i_0_1656, hypothesis, (i33!=i2)). % 0.52/0.70 cnf(i_0_1619, hypothesis, (i33!=i3)). % 0.52/0.70 cnf(i_0_1583, hypothesis, (i33!=i4)). % 0.52/0.70 cnf(i_0_1548, hypothesis, (i33!=i5)). % 0.52/0.70 cnf(i_0_1514, hypothesis, (i33!=i6)). % 0.52/0.70 cnf(i_0_1481, hypothesis, (i33!=i7)). % 0.52/0.70 cnf(i_0_1449, hypothesis, (i33!=i8)). % 0.52/0.70 cnf(i_0_1418, hypothesis, (i33!=i9)). % 0.52/0.70 cnf(i_0_1388, hypothesis, (i33!=i10)). % 0.52/0.70 cnf(i_0_1359, hypothesis, (i33!=i11)). % 0.52/0.70 cnf(i_0_1331, hypothesis, (i33!=i12)). % 0.52/0.70 cnf(i_0_1304, hypothesis, (i33!=i13)). % 0.52/0.70 cnf(i_0_1278, hypothesis, (i33!=i14)). % 0.52/0.70 cnf(i_0_1253, hypothesis, (i33!=i15)). % 0.52/0.70 cnf(i_0_1229, hypothesis, (i33!=i16)). % 0.52/0.70 cnf(i_0_1206, hypothesis, (i33!=i17)). % 0.52/0.70 cnf(i_0_1184, hypothesis, (i33!=i18)). % 0.52/0.70 cnf(i_0_1163, hypothesis, (i33!=i19)). % 0.52/0.70 cnf(i_0_1143, hypothesis, (i33!=i20)). % 0.52/0.70 cnf(i_0_1124, hypothesis, (i33!=i21)). % 0.52/0.70 cnf(i_0_1106, hypothesis, (i33!=i22)). % 0.52/0.70 cnf(i_0_1089, hypothesis, (i33!=i23)). % 0.52/0.70 cnf(i_0_1073, hypothesis, (i33!=i24)). % 0.52/0.70 cnf(i_0_1058, hypothesis, (i33!=i25)). % 0.52/0.70 cnf(i_0_1044, hypothesis, (i33!=i26)). % 0.52/0.70 cnf(i_0_1031, hypothesis, (i33!=i27)). % 0.52/0.70 cnf(i_0_1019, hypothesis, (i33!=i28)). % 0.52/0.70 cnf(i_0_1008, hypothesis, (i33!=i29)). % 0.52/0.70 cnf(i_0_998, hypothesis, (i33!=i30)). % 0.52/0.70 cnf(i_0_989, hypothesis, (i33!=i31)). % 0.52/0.70 cnf(i_0_981, hypothesis, (i33!=i32)). % 0.52/0.70 cnf(i_0_1693, hypothesis, (i34!=i1)). % 0.52/0.70 cnf(i_0_1655, hypothesis, (i34!=i2)). % 0.52/0.70 cnf(i_0_1618, hypothesis, (i34!=i3)). % 0.52/0.70 cnf(i_0_1582, hypothesis, (i34!=i4)). % 0.52/0.70 cnf(i_0_1547, hypothesis, (i34!=i5)). % 0.52/0.70 cnf(i_0_1513, hypothesis, (i34!=i6)). % 0.52/0.70 cnf(i_0_1480, hypothesis, (i34!=i7)). % 0.52/0.70 cnf(i_0_1448, hypothesis, (i34!=i8)). % 0.52/0.70 cnf(i_0_1417, hypothesis, (i34!=i9)). % 0.52/0.70 cnf(i_0_1387, hypothesis, (i34!=i10)). % 0.52/0.70 cnf(i_0_1358, hypothesis, (i34!=i11)). % 0.52/0.70 cnf(i_0_1330, hypothesis, (i34!=i12)). % 0.52/0.70 cnf(i_0_1303, hypothesis, (i34!=i13)). % 0.52/0.70 cnf(i_0_1277, hypothesis, (i34!=i14)). % 0.52/0.70 cnf(i_0_1252, hypothesis, (i34!=i15)). % 0.52/0.70 cnf(i_0_1228, hypothesis, (i34!=i16)). % 0.52/0.70 cnf(i_0_1205, hypothesis, (i34!=i17)). % 0.52/0.70 cnf(i_0_1183, hypothesis, (i34!=i18)). % 0.52/0.70 cnf(i_0_1162, hypothesis, (i34!=i19)). % 0.52/0.70 cnf(i_0_1142, hypothesis, (i34!=i20)). % 0.52/0.70 cnf(i_0_1123, hypothesis, (i34!=i21)). % 0.52/0.70 cnf(i_0_1105, hypothesis, (i34!=i22)). % 0.52/0.70 cnf(i_0_1088, hypothesis, (i34!=i23)). % 0.52/0.70 cnf(i_0_1072, hypothesis, (i34!=i24)). % 0.52/0.70 cnf(i_0_1057, hypothesis, (i34!=i25)). % 0.52/0.70 cnf(i_0_1043, hypothesis, (i34!=i26)). % 0.52/0.70 cnf(i_0_1030, hypothesis, (i34!=i27)). % 0.52/0.70 cnf(i_0_1018, hypothesis, (i34!=i28)). % 0.52/0.70 cnf(i_0_1007, hypothesis, (i34!=i29)). % 0.52/0.70 cnf(i_0_997, hypothesis, (i34!=i30)). % 0.52/0.70 cnf(i_0_988, hypothesis, (i34!=i31)). % 0.52/0.70 cnf(i_0_980, hypothesis, (i34!=i32)). % 0.52/0.70 cnf(i_0_973, hypothesis, (i34!=i33)). % 0.52/0.70 cnf(i_0_1692, hypothesis, (i35!=i1)). % 0.52/0.70 cnf(i_0_1654, hypothesis, (i35!=i2)). % 0.52/0.70 cnf(i_0_1617, hypothesis, (i35!=i3)). % 0.52/0.70 cnf(i_0_1581, hypothesis, (i35!=i4)). % 0.52/0.70 cnf(i_0_1546, hypothesis, (i35!=i5)). % 0.52/0.70 cnf(i_0_1512, hypothesis, (i35!=i6)). % 0.52/0.70 cnf(i_0_1479, hypothesis, (i35!=i7)). % 0.52/0.70 cnf(i_0_1447, hypothesis, (i35!=i8)). % 0.52/0.70 cnf(i_0_1416, hypothesis, (i35!=i9)). % 0.52/0.70 cnf(i_0_1386, hypothesis, (i35!=i10)). % 0.52/0.70 cnf(i_0_1357, hypothesis, (i35!=i11)). % 0.52/0.70 cnf(i_0_1329, hypothesis, (i35!=i12)). % 0.52/0.70 cnf(i_0_1302, hypothesis, (i35!=i13)). % 0.52/0.70 cnf(i_0_1276, hypothesis, (i35!=i14)). % 0.52/0.70 cnf(i_0_1251, hypothesis, (i35!=i15)). % 0.52/0.70 cnf(i_0_1227, hypothesis, (i35!=i16)). % 0.52/0.70 cnf(i_0_1204, hypothesis, (i35!=i17)). % 0.52/0.70 cnf(i_0_1182, hypothesis, (i35!=i18)). % 0.52/0.70 cnf(i_0_1161, hypothesis, (i35!=i19)). % 0.52/0.70 cnf(i_0_1141, hypothesis, (i35!=i20)). % 0.52/0.70 cnf(i_0_1122, hypothesis, (i35!=i21)). % 0.52/0.70 cnf(i_0_1104, hypothesis, (i35!=i22)). % 0.52/0.70 cnf(i_0_1087, hypothesis, (i35!=i23)). % 0.52/0.70 cnf(i_0_1071, hypothesis, (i35!=i24)). % 0.52/0.70 cnf(i_0_1056, hypothesis, (i35!=i25)). % 0.52/0.70 cnf(i_0_1042, hypothesis, (i35!=i26)). % 0.52/0.70 cnf(i_0_1029, hypothesis, (i35!=i27)). % 0.52/0.70 cnf(i_0_1017, hypothesis, (i35!=i28)). % 0.52/0.70 cnf(i_0_1006, hypothesis, (i35!=i29)). % 0.52/0.70 cnf(i_0_996, hypothesis, (i35!=i30)). % 0.52/0.70 cnf(i_0_987, hypothesis, (i35!=i31)). % 0.52/0.70 cnf(i_0_979, hypothesis, (i35!=i32)). % 0.52/0.70 cnf(i_0_972, hypothesis, (i35!=i33)). % 0.52/0.70 cnf(i_0_966, hypothesis, (i35!=i34)). % 0.52/0.70 cnf(i_0_1691, hypothesis, (i36!=i1)). % 0.52/0.70 cnf(i_0_1653, hypothesis, (i36!=i2)). % 0.52/0.70 cnf(i_0_1616, hypothesis, (i36!=i3)). % 0.52/0.70 cnf(i_0_1580, hypothesis, (i36!=i4)). % 0.52/0.70 cnf(i_0_1545, hypothesis, (i36!=i5)). % 0.52/0.70 cnf(i_0_1511, hypothesis, (i36!=i6)). % 0.52/0.70 cnf(i_0_1478, hypothesis, (i36!=i7)). % 0.52/0.70 cnf(i_0_1446, hypothesis, (i36!=i8)). % 0.52/0.70 cnf(i_0_1415, hypothesis, (i36!=i9)). % 0.52/0.70 cnf(i_0_1385, hypothesis, (i36!=i10)). % 0.52/0.70 cnf(i_0_1356, hypothesis, (i36!=i11)). % 0.52/0.70 cnf(i_0_1328, hypothesis, (i36!=i12)). % 0.52/0.70 cnf(i_0_1301, hypothesis, (i36!=i13)). % 0.52/0.70 cnf(i_0_1275, hypothesis, (i36!=i14)). % 0.52/0.70 cnf(i_0_1250, hypothesis, (i36!=i15)). % 0.52/0.70 cnf(i_0_1226, hypothesis, (i36!=i16)). % 0.52/0.70 cnf(i_0_1203, hypothesis, (i36!=i17)). % 0.52/0.70 cnf(i_0_1181, hypothesis, (i36!=i18)). % 0.52/0.70 cnf(i_0_1160, hypothesis, (i36!=i19)). % 0.52/0.70 cnf(i_0_1140, hypothesis, (i36!=i20)). % 0.52/0.70 cnf(i_0_1121, hypothesis, (i36!=i21)). % 0.52/0.70 cnf(i_0_1103, hypothesis, (i36!=i22)). % 0.52/0.70 cnf(i_0_1086, hypothesis, (i36!=i23)). % 0.52/0.70 cnf(i_0_1070, hypothesis, (i36!=i24)). % 0.52/0.70 cnf(i_0_1055, hypothesis, (i36!=i25)). % 0.52/0.70 cnf(i_0_1041, hypothesis, (i36!=i26)). % 0.52/0.70 cnf(i_0_1028, hypothesis, (i36!=i27)). % 0.52/0.70 cnf(i_0_1016, hypothesis, (i36!=i28)). % 0.52/0.70 cnf(i_0_1005, hypothesis, (i36!=i29)). % 0.52/0.70 cnf(i_0_995, hypothesis, (i36!=i30)). % 0.52/0.70 cnf(i_0_986, hypothesis, (i36!=i31)). % 0.52/0.70 cnf(i_0_978, hypothesis, (i36!=i32)). % 0.52/0.70 cnf(i_0_971, hypothesis, (i36!=i33)). % 0.52/0.70 cnf(i_0_965, hypothesis, (i36!=i34)). % 0.52/0.70 cnf(i_0_960, hypothesis, (i36!=i35)). % 0.52/0.70 cnf(i_0_1690, hypothesis, (i37!=i1)). % 0.52/0.70 cnf(i_0_1652, hypothesis, (i37!=i2)). % 0.52/0.70 cnf(i_0_1615, hypothesis, (i37!=i3)). % 0.52/0.70 cnf(i_0_1579, hypothesis, (i37!=i4)). % 0.52/0.70 cnf(i_0_1544, hypothesis, (i37!=i5)). % 0.52/0.70 cnf(i_0_1510, hypothesis, (i37!=i6)). % 0.52/0.70 cnf(i_0_1477, hypothesis, (i37!=i7)). % 0.52/0.70 cnf(i_0_1445, hypothesis, (i37!=i8)). % 0.52/0.70 cnf(i_0_1414, hypothesis, (i37!=i9)). % 0.52/0.70 cnf(i_0_1384, hypothesis, (i37!=i10)). % 0.52/0.70 cnf(i_0_1355, hypothesis, (i37!=i11)). % 0.52/0.70 cnf(i_0_1327, hypothesis, (i37!=i12)). % 0.52/0.70 cnf(i_0_1300, hypothesis, (i37!=i13)). % 0.52/0.70 cnf(i_0_1274, hypothesis, (i37!=i14)). % 0.52/0.70 cnf(i_0_1249, hypothesis, (i37!=i15)). % 0.52/0.70 cnf(i_0_1225, hypothesis, (i37!=i16)). % 0.52/0.70 cnf(i_0_1202, hypothesis, (i37!=i17)). % 0.52/0.70 cnf(i_0_1180, hypothesis, (i37!=i18)). % 0.52/0.70 cnf(i_0_1159, hypothesis, (i37!=i19)). % 0.52/0.70 cnf(i_0_1139, hypothesis, (i37!=i20)). % 0.52/0.70 cnf(i_0_1120, hypothesis, (i37!=i21)). % 0.52/0.70 cnf(i_0_1102, hypothesis, (i37!=i22)). % 0.52/0.70 cnf(i_0_1085, hypothesis, (i37!=i23)). % 0.52/0.70 cnf(i_0_1069, hypothesis, (i37!=i24)). % 0.52/0.70 cnf(i_0_1054, hypothesis, (i37!=i25)). % 0.52/0.70 cnf(i_0_1040, hypothesis, (i37!=i26)). % 0.52/0.70 cnf(i_0_1027, hypothesis, (i37!=i27)). % 0.52/0.70 cnf(i_0_1015, hypothesis, (i37!=i28)). % 0.52/0.70 cnf(i_0_1004, hypothesis, (i37!=i29)). % 0.52/0.70 cnf(i_0_994, hypothesis, (i37!=i30)). % 0.52/0.70 cnf(i_0_985, hypothesis, (i37!=i31)). % 0.52/0.70 cnf(i_0_977, hypothesis, (i37!=i32)). % 0.52/0.70 cnf(i_0_970, hypothesis, (i37!=i33)). % 0.52/0.70 cnf(i_0_964, hypothesis, (i37!=i34)). % 0.52/0.70 cnf(i_0_959, hypothesis, (i37!=i35)). % 0.52/0.70 cnf(i_0_955, hypothesis, (i37!=i36)). % 0.52/0.70 cnf(i_0_1689, hypothesis, (i38!=i1)). % 0.52/0.70 cnf(i_0_1651, hypothesis, (i38!=i2)). % 0.52/0.70 cnf(i_0_1614, hypothesis, (i38!=i3)). % 0.52/0.70 cnf(i_0_1578, hypothesis, (i38!=i4)). % 0.52/0.70 cnf(i_0_1543, hypothesis, (i38!=i5)). % 0.52/0.70 cnf(i_0_1509, hypothesis, (i38!=i6)). % 0.52/0.70 cnf(i_0_1476, hypothesis, (i38!=i7)). % 0.52/0.70 cnf(i_0_1444, hypothesis, (i38!=i8)). % 0.52/0.70 cnf(i_0_1413, hypothesis, (i38!=i9)). % 0.52/0.70 cnf(i_0_1383, hypothesis, (i38!=i10)). % 0.52/0.70 cnf(i_0_1354, hypothesis, (i38!=i11)). % 0.52/0.70 cnf(i_0_1326, hypothesis, (i38!=i12)). % 0.52/0.70 cnf(i_0_1299, hypothesis, (i38!=i13)). % 0.52/0.70 cnf(i_0_1273, hypothesis, (i38!=i14)). % 0.52/0.70 cnf(i_0_1248, hypothesis, (i38!=i15)). % 0.52/0.70 cnf(i_0_1224, hypothesis, (i38!=i16)). % 0.52/0.70 cnf(i_0_1201, hypothesis, (i38!=i17)). % 0.52/0.70 cnf(i_0_1179, hypothesis, (i38!=i18)). % 0.52/0.70 cnf(i_0_1158, hypothesis, (i38!=i19)). % 0.52/0.70 cnf(i_0_1138, hypothesis, (i38!=i20)). % 0.52/0.70 cnf(i_0_1119, hypothesis, (i38!=i21)). % 0.52/0.70 cnf(i_0_1101, hypothesis, (i38!=i22)). % 0.52/0.70 cnf(i_0_1084, hypothesis, (i38!=i23)). % 0.52/0.70 cnf(i_0_1068, hypothesis, (i38!=i24)). % 0.52/0.70 cnf(i_0_1053, hypothesis, (i38!=i25)). % 0.52/0.70 cnf(i_0_1039, hypothesis, (i38!=i26)). % 0.52/0.70 cnf(i_0_1026, hypothesis, (i38!=i27)). % 0.52/0.70 cnf(i_0_1014, hypothesis, (i38!=i28)). % 0.52/0.70 cnf(i_0_1003, hypothesis, (i38!=i29)). % 0.52/0.70 cnf(i_0_993, hypothesis, (i38!=i30)). % 0.52/0.70 cnf(i_0_984, hypothesis, (i38!=i31)). % 0.52/0.70 cnf(i_0_976, hypothesis, (i38!=i32)). % 0.52/0.70 cnf(i_0_969, hypothesis, (i38!=i33)). % 0.52/0.70 cnf(i_0_963, hypothesis, (i38!=i34)). % 0.52/0.70 cnf(i_0_958, hypothesis, (i38!=i35)). % 0.52/0.70 cnf(i_0_954, hypothesis, (i38!=i36)). % 0.52/0.70 cnf(i_0_951, hypothesis, (i38!=i37)). % 0.52/0.70 cnf(i_0_1688, hypothesis, (i39!=i1)). % 0.52/0.70 cnf(i_0_1650, hypothesis, (i39!=i2)). % 0.52/0.70 cnf(i_0_1613, hypothesis, (i39!=i3)). % 0.52/0.70 cnf(i_0_1577, hypothesis, (i39!=i4)). % 0.52/0.70 cnf(i_0_1542, hypothesis, (i39!=i5)). % 0.52/0.70 cnf(i_0_1508, hypothesis, (i39!=i6)). % 0.52/0.70 cnf(i_0_1475, hypothesis, (i39!=i7)). % 0.52/0.70 cnf(i_0_1443, hypothesis, (i39!=i8)). % 0.52/0.70 cnf(i_0_1412, hypothesis, (i39!=i9)). % 0.52/0.70 cnf(i_0_1382, hypothesis, (i39!=i10)). % 0.52/0.70 cnf(i_0_1353, hypothesis, (i39!=i11)). % 0.52/0.70 cnf(i_0_1325, hypothesis, (i39!=i12)). % 0.52/0.70 cnf(i_0_1298, hypothesis, (i39!=i13)). % 0.52/0.70 cnf(i_0_1272, hypothesis, (i39!=i14)). % 0.52/0.70 cnf(i_0_1247, hypothesis, (i39!=i15)). % 0.52/0.70 cnf(i_0_1223, hypothesis, (i39!=i16)). % 0.52/0.70 cnf(i_0_1200, hypothesis, (i39!=i17)). % 0.52/0.70 cnf(i_0_1178, hypothesis, (i39!=i18)). % 0.52/0.70 cnf(i_0_1157, hypothesis, (i39!=i19)). % 0.52/0.70 cnf(i_0_1137, hypothesis, (i39!=i20)). % 0.52/0.70 cnf(i_0_1118, hypothesis, (i39!=i21)). % 0.52/0.70 cnf(i_0_1100, hypothesis, (i39!=i22)). % 0.52/0.70 cnf(i_0_1083, hypothesis, (i39!=i23)). % 0.52/0.70 cnf(i_0_1067, hypothesis, (i39!=i24)). % 0.52/0.70 cnf(i_0_1052, hypothesis, (i39!=i25)). % 0.52/0.70 cnf(i_0_1038, hypothesis, (i39!=i26)). % 0.52/0.70 cnf(i_0_1025, hypothesis, (i39!=i27)). % 0.52/0.70 cnf(i_0_1013, hypothesis, (i39!=i28)). % 0.52/0.70 cnf(i_0_1002, hypothesis, (i39!=i29)). % 0.52/0.70 cnf(i_0_992, hypothesis, (i39!=i30)). % 0.52/0.70 cnf(i_0_983, hypothesis, (i39!=i31)). % 0.52/0.70 cnf(i_0_975, hypothesis, (i39!=i32)). % 0.52/0.70 cnf(i_0_968, hypothesis, (i39!=i33)). % 0.52/0.70 cnf(i_0_962, hypothesis, (i39!=i34)). % 0.52/0.70 cnf(i_0_957, hypothesis, (i39!=i35)). % 0.52/0.70 cnf(i_0_953, hypothesis, (i39!=i36)). % 0.52/0.70 cnf(i_0_950, hypothesis, (i39!=i37)). % 0.52/0.70 cnf(i_0_948, hypothesis, (i39!=i38)). % 0.52/0.70 cnf(i_0_1687, hypothesis, (i40!=i1)). % 0.52/0.70 cnf(i_0_1649, hypothesis, (i40!=i2)). % 0.52/0.70 cnf(i_0_1612, hypothesis, (i40!=i3)). % 0.52/0.70 cnf(i_0_1576, hypothesis, (i40!=i4)). % 0.52/0.70 cnf(i_0_1541, hypothesis, (i40!=i5)). % 0.52/0.70 cnf(i_0_1507, hypothesis, (i40!=i6)). % 0.52/0.70 cnf(i_0_1474, hypothesis, (i40!=i7)). % 0.52/0.70 cnf(i_0_1442, hypothesis, (i40!=i8)). % 0.52/0.70 cnf(i_0_1411, hypothesis, (i40!=i9)). % 0.52/0.70 cnf(i_0_1381, hypothesis, (i40!=i10)). % 0.52/0.70 cnf(i_0_1352, hypothesis, (i40!=i11)). % 0.52/0.70 cnf(i_0_1324, hypothesis, (i40!=i12)). % 0.52/0.70 cnf(i_0_1297, hypothesis, (i40!=i13)). % 0.52/0.70 cnf(i_0_1271, hypothesis, (i40!=i14)). % 0.52/0.70 cnf(i_0_1246, hypothesis, (i40!=i15)). % 0.52/0.70 cnf(i_0_1222, hypothesis, (i40!=i16)). % 0.52/0.70 cnf(i_0_1199, hypothesis, (i40!=i17)). % 0.52/0.70 cnf(i_0_1177, hypothesis, (i40!=i18)). % 0.52/0.70 cnf(i_0_1156, hypothesis, (i40!=i19)). % 0.52/0.70 cnf(i_0_1136, hypothesis, (i40!=i20)). % 0.52/0.70 cnf(i_0_1117, hypothesis, (i40!=i21)). % 0.52/0.70 cnf(i_0_1099, hypothesis, (i40!=i22)). % 0.52/0.70 cnf(i_0_1082, hypothesis, (i40!=i23)). % 0.52/0.70 cnf(i_0_1066, hypothesis, (i40!=i24)). % 0.52/0.70 cnf(i_0_1051, hypothesis, (i40!=i25)). % 0.52/0.70 cnf(i_0_1037, hypothesis, (i40!=i26)). % 0.52/0.70 cnf(i_0_1024, hypothesis, (i40!=i27)). % 0.52/0.70 cnf(i_0_1012, hypothesis, (i40!=i28)). % 0.52/0.70 cnf(i_0_1001, hypothesis, (i40!=i29)). % 0.52/0.70 cnf(i_0_991, hypothesis, (i40!=i30)). % 0.52/0.70 cnf(i_0_982, hypothesis, (i40!=i31)). % 0.52/0.70 cnf(i_0_974, hypothesis, (i40!=i32)). % 0.52/0.70 cnf(i_0_967, hypothesis, (i40!=i33)). % 0.52/0.70 cnf(i_0_961, hypothesis, (i40!=i34)). % 0.52/0.70 cnf(i_0_956, hypothesis, (i40!=i35)). % 0.52/0.70 cnf(i_0_952, hypothesis, (i40!=i36)). % 0.52/0.70 cnf(i_0_949, hypothesis, (i40!=i37)). % 0.52/0.70 cnf(i_0_947, hypothesis, (i40!=i38)). % 0.52/0.70 cnf(i_0_946, hypothesis, (i40!=i39)). % 0.52/0.70 cnf(i_0_865, plain, (select(store(X1,X2,X3),X4)=select(X1,X4)|X2=X4)). % 0.52/0.70 cnf(i_0_1732, plain, (X5=X5)). % 0.52/0.70 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 0.52/0.70 # Begin printing tableau % 0.52/0.70 # Found 6 steps % 0.52/0.70 cnf(i_0_945, hypothesis, (store(a_1437,i19,e19)=a_1438), inference(start_rule)). % 0.52/0.70 cnf(i_0_1739, plain, (store(a_1437,i19,e19)=a_1438), inference(extension_rule, [i_0_1735])). % 0.52/0.70 cnf(i_0_2627, plain, (store(a_1437,i19,e19)!=a_1438), inference(closure_rule, [i_0_945])). % 0.52/0.70 cnf(i_0_2625, plain, (store(a_1437,i19,e19)=store(a_1437,i19,e19)), inference(extension_rule, [i_0_1736])). % 0.52/0.70 cnf(i_0_2636, plain, (store(a_1397,i40,e40)!=a_1398), inference(closure_rule, [i_0_905])). % 0.52/0.70 cnf(i_0_2637, plain, (store(a_1397,i40,e40)!=a_1398), inference(closure_rule, [i_0_905])). % 0.52/0.70 # End printing tableau % 0.52/0.70 # SZS output end % 0.52/0.70 # Branches closed with saturation will be marked with an "s" % 0.52/0.72 # 21983 Satisfiable branch % 0.52/0.72 # 21988 Satisfiable branch % 0.52/0.72 # 21985 Satisfiable branch % 0.52/0.72 # 21984 Satisfiable branch % 0.52/0.72 # Satisfiable branch found. % 0.52/0.72 # There were 1 total branch saturation attempts. % 0.52/0.72 # There were 0 of these attempts blocked. % 0.52/0.72 # There were 0 deferred branch saturation attempts. % 0.52/0.72 # There were 0 free duplicated saturations. % 0.52/0.72 # There were 0 total successful branch saturations. % 0.52/0.72 # There were 0 successful branch saturations in interreduction. % 0.52/0.72 # There were 0 successful branch saturations on the branch. % 0.52/0.72 # There were 0 successful branch saturations after the branch. % 0.52/0.72 # Child (21993) has found a proof. % 0.52/0.72 % 0.61/0.77 # Proof search is over... % 0.61/0.77 # Freeing feature tree %------------------------------------------------------------------------------