%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWV494-1.050 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:55:46 PM UTC 2026
% Result : Satisfiable 0.33s 0.76s
% Output : Saturation 0.33s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named a2ERROR: Could not build tree for root c_0_2454ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_2454,axiom,
( select(store(X3,X1,X4),X2) = select(X3,X2)
| X1 = X2 ),
a2,
[final] ).
cnf(c_0_2455,negated_conjecture,
store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),i31,e31),i32,e32),i33,e33),i34,e34),i35,e35),i36,e36),i37,e37),i38,e38),i39,e39),i40,e40),i41,e41),i42,e42),i43,e43),i44,e44),i45,e45),i46,e46),i47,e47),i48,e48),i49,e49),i1,e1) != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i41,e41),i30,e30),i45,e45),i43,e43),i28,e28),i19,e19),i22,e22),i39,e39),i20,e20),i40,e40),i16,e16),i8,e8),i49,e49),i14,e14),i13,e13),i6,e6),i27,e27),i15,e15),i7,e7),i33,e33),i9,e9),i17,e17),i42,e42),i47,e47),i18,e18),i26,e26),i34,e34),i11,e11),i36,e36),i44,e44),i38,e38),i23,e23),i25,e25),i46,e46),i35,e35),i50,e50),i2,e2),i10,e10),i48,e48),i29,e29),i3,e3),i37,e37),i12,e12),i5,e5),i32,e32),i4,e4),i24,e24),i21,e21),i31,e31),i1,e1),
c_0_1228,
[final] ).
cnf(c_0_2456,hypothesis,
i1 != i2,
c_0_1229,
[final] ).
cnf(c_0_2457,hypothesis,
i1 != i3,
c_0_1230,
[final] ).
cnf(c_0_2458,hypothesis,
i1 != i4,
c_0_1231,
[final] ).
cnf(c_0_2459,hypothesis,
i1 != i5,
c_0_1232,
[final] ).
cnf(c_0_2460,hypothesis,
i1 != i6,
c_0_1233,
[final] ).
cnf(c_0_2461,hypothesis,
i1 != i7,
c_0_1234,
[final] ).
cnf(c_0_2462,hypothesis,
i1 != i8,
c_0_1235,
[final] ).
cnf(c_0_2463,hypothesis,
i1 != i9,
c_0_1236,
[final] ).
cnf(c_0_2464,hypothesis,
i1 != i10,
c_0_1237,
[final] ).
cnf(c_0_2465,hypothesis,
i1 != i11,
c_0_1238,
[final] ).
cnf(c_0_2466,hypothesis,
i1 != i12,
c_0_1239,
[final] ).
cnf(c_0_2467,hypothesis,
i1 != i13,
c_0_1240,
[final] ).
cnf(c_0_2468,hypothesis,
i1 != i14,
c_0_1241,
[final] ).
cnf(c_0_2469,hypothesis,
i1 != i15,
c_0_1242,
[final] ).
cnf(c_0_2470,hypothesis,
i1 != i16,
c_0_1243,
[final] ).
cnf(c_0_2471,hypothesis,
i1 != i17,
c_0_1244,
[final] ).
cnf(c_0_2472,hypothesis,
i1 != i18,
c_0_1245,
[final] ).
cnf(c_0_2473,hypothesis,
i1 != i19,
c_0_1246,
[final] ).
cnf(c_0_2474,hypothesis,
i1 != i20,
c_0_1247,
[final] ).
cnf(c_0_2475,hypothesis,
i1 != i21,
c_0_1248,
[final] ).
cnf(c_0_2476,hypothesis,
i1 != i22,
c_0_1249,
[final] ).
cnf(c_0_2477,hypothesis,
i1 != i23,
c_0_1250,
[final] ).
cnf(c_0_2478,hypothesis,
i1 != i24,
c_0_1251,
[final] ).
cnf(c_0_2479,hypothesis,
i1 != i25,
c_0_1252,
[final] ).
cnf(c_0_2480,hypothesis,
i1 != i26,
c_0_1253,
[final] ).
cnf(c_0_2481,hypothesis,
i1 != i27,
c_0_1254,
[final] ).
cnf(c_0_2482,hypothesis,
i1 != i28,
c_0_1255,
[final] ).
cnf(c_0_2483,hypothesis,
i1 != i29,
c_0_1256,
[final] ).
cnf(c_0_2484,hypothesis,
i1 != i30,
c_0_1257,
[final] ).
cnf(c_0_2485,hypothesis,
i1 != i31,
c_0_1258,
[final] ).
cnf(c_0_2486,hypothesis,
i1 != i32,
c_0_1259,
[final] ).
cnf(c_0_2487,hypothesis,
i1 != i33,
c_0_1260,
[final] ).
cnf(c_0_2488,hypothesis,
i1 != i34,
c_0_1261,
[final] ).
cnf(c_0_2489,hypothesis,
i1 != i35,
c_0_1262,
[final] ).
cnf(c_0_2490,hypothesis,
i1 != i36,
c_0_1263,
[final] ).
cnf(c_0_2491,hypothesis,
i1 != i37,
c_0_1264,
[final] ).
cnf(c_0_2492,hypothesis,
i1 != i38,
c_0_1265,
[final] ).
cnf(c_0_2493,hypothesis,
i1 != i39,
c_0_1266,
[final] ).
cnf(c_0_2494,hypothesis,
i1 != i40,
c_0_1267,
[final] ).
cnf(c_0_2495,hypothesis,
i1 != i41,
c_0_1268,
[final] ).
cnf(c_0_2496,hypothesis,
i1 != i42,
c_0_1269,
[final] ).
cnf(c_0_2497,hypothesis,
i1 != i43,
c_0_1270,
[final] ).
cnf(c_0_2498,hypothesis,
i1 != i44,
c_0_1271,
[final] ).
cnf(c_0_2499,hypothesis,
i1 != i45,
c_0_1272,
[final] ).
cnf(c_0_2500,hypothesis,
i1 != i46,
c_0_1273,
[final] ).
cnf(c_0_2501,hypothesis,
i1 != i47,
c_0_1274,
[final] ).
cnf(c_0_2502,hypothesis,
i1 != i48,
c_0_1275,
[final] ).
cnf(c_0_2503,hypothesis,
i1 != i50,
c_0_1276,
[final] ).
cnf(c_0_2504,hypothesis,
i1 != i49,
c_0_1277,
[final] ).
cnf(c_0_2505,hypothesis,
i2 != i3,
c_0_1278,
[final] ).
cnf(c_0_2506,hypothesis,
i2 != i4,
c_0_1279,
[final] ).
cnf(c_0_2507,hypothesis,
i2 != i5,
c_0_1280,
[final] ).
cnf(c_0_2508,hypothesis,
i2 != i6,
c_0_1281,
[final] ).
cnf(c_0_2509,hypothesis,
i2 != i7,
c_0_1282,
[final] ).
cnf(c_0_2510,hypothesis,
i2 != i8,
c_0_1283,
[final] ).
cnf(c_0_2511,hypothesis,
i2 != i9,
c_0_1284,
[final] ).
cnf(c_0_2512,hypothesis,
i2 != i10,
c_0_1285,
[final] ).
cnf(c_0_2513,hypothesis,
i2 != i11,
c_0_1286,
[final] ).
cnf(c_0_2514,hypothesis,
i2 != i12,
c_0_1287,
[final] ).
cnf(c_0_2515,hypothesis,
i2 != i13,
c_0_1288,
[final] ).
cnf(c_0_2516,hypothesis,
i2 != i14,
c_0_1289,
[final] ).
cnf(c_0_2517,hypothesis,
i2 != i15,
c_0_1290,
[final] ).
cnf(c_0_2518,hypothesis,
i2 != i16,
c_0_1291,
[final] ).
cnf(c_0_2519,hypothesis,
i2 != i17,
c_0_1292,
[final] ).
cnf(c_0_2520,hypothesis,
i2 != i18,
c_0_1293,
[final] ).
cnf(c_0_2521,hypothesis,
i2 != i19,
c_0_1294,
[final] ).
cnf(c_0_2522,hypothesis,
i2 != i20,
c_0_1295,
[final] ).
cnf(c_0_2523,hypothesis,
i2 != i21,
c_0_1296,
[final] ).
cnf(c_0_2524,hypothesis,
i2 != i22,
c_0_1297,
[final] ).
cnf(c_0_2525,hypothesis,
i2 != i23,
c_0_1298,
[final] ).
cnf(c_0_2526,hypothesis,
i2 != i24,
c_0_1299,
[final] ).
cnf(c_0_2527,hypothesis,
i2 != i25,
c_0_1300,
[final] ).
cnf(c_0_2528,hypothesis,
i2 != i26,
c_0_1301,
[final] ).
cnf(c_0_2529,hypothesis,
i2 != i27,
c_0_1302,
[final] ).
cnf(c_0_2530,hypothesis,
i2 != i28,
c_0_1303,
[final] ).
cnf(c_0_2531,hypothesis,
i2 != i29,
c_0_1304,
[final] ).
cnf(c_0_2532,hypothesis,
i2 != i30,
c_0_1305,
[final] ).
cnf(c_0_2533,hypothesis,
i2 != i31,
c_0_1306,
[final] ).
cnf(c_0_2534,hypothesis,
i2 != i32,
c_0_1307,
[final] ).
cnf(c_0_2535,hypothesis,
i2 != i33,
c_0_1308,
[final] ).
cnf(c_0_2536,hypothesis,
i2 != i34,
c_0_1309,
[final] ).
cnf(c_0_2537,hypothesis,
i2 != i35,
c_0_1310,
[final] ).
cnf(c_0_2538,hypothesis,
i2 != i36,
c_0_1311,
[final] ).
cnf(c_0_2539,hypothesis,
i2 != i37,
c_0_1312,
[final] ).
cnf(c_0_2540,hypothesis,
i2 != i38,
c_0_1313,
[final] ).
cnf(c_0_2541,hypothesis,
i2 != i39,
c_0_1314,
[final] ).
cnf(c_0_2542,hypothesis,
i2 != i40,
c_0_1315,
[final] ).
cnf(c_0_2543,hypothesis,
i2 != i41,
c_0_1316,
[final] ).
cnf(c_0_2544,hypothesis,
i2 != i42,
c_0_1317,
[final] ).
cnf(c_0_2545,hypothesis,
i2 != i43,
c_0_1318,
[final] ).
cnf(c_0_2546,hypothesis,
i2 != i44,
c_0_1319,
[final] ).
cnf(c_0_2547,hypothesis,
i2 != i45,
c_0_1320,
[final] ).
cnf(c_0_2548,hypothesis,
i2 != i46,
c_0_1321,
[final] ).
cnf(c_0_2549,hypothesis,
i2 != i47,
c_0_1322,
[final] ).
cnf(c_0_2550,hypothesis,
i2 != i48,
c_0_1323,
[final] ).
cnf(c_0_2551,hypothesis,
i2 != i50,
c_0_1324,
[final] ).
cnf(c_0_2552,hypothesis,
i2 != i49,
c_0_1325,
[final] ).
cnf(c_0_2553,hypothesis,
i3 != i4,
c_0_1326,
[final] ).
cnf(c_0_2554,hypothesis,
i3 != i5,
c_0_1327,
[final] ).
cnf(c_0_2555,hypothesis,
i3 != i6,
c_0_1328,
[final] ).
cnf(c_0_2556,hypothesis,
i3 != i7,
c_0_1329,
[final] ).
cnf(c_0_2557,hypothesis,
i3 != i8,
c_0_1330,
[final] ).
cnf(c_0_2558,hypothesis,
i3 != i9,
c_0_1331,
[final] ).
cnf(c_0_2559,hypothesis,
i3 != i10,
c_0_1332,
[final] ).
cnf(c_0_2560,hypothesis,
i3 != i11,
c_0_1333,
[final] ).
cnf(c_0_2561,hypothesis,
i3 != i12,
c_0_1334,
[final] ).
cnf(c_0_2562,hypothesis,
i3 != i13,
c_0_1335,
[final] ).
cnf(c_0_2563,hypothesis,
i3 != i14,
c_0_1336,
[final] ).
cnf(c_0_2564,hypothesis,
i3 != i15,
c_0_1337,
[final] ).
cnf(c_0_2565,hypothesis,
i3 != i16,
c_0_1338,
[final] ).
cnf(c_0_2566,hypothesis,
i3 != i17,
c_0_1339,
[final] ).
cnf(c_0_2567,hypothesis,
i3 != i18,
c_0_1340,
[final] ).
cnf(c_0_2568,hypothesis,
i3 != i19,
c_0_1341,
[final] ).
cnf(c_0_2569,hypothesis,
i3 != i20,
c_0_1342,
[final] ).
cnf(c_0_2570,hypothesis,
i3 != i21,
c_0_1343,
[final] ).
cnf(c_0_2571,hypothesis,
i3 != i22,
c_0_1344,
[final] ).
cnf(c_0_2572,hypothesis,
i3 != i23,
c_0_1345,
[final] ).
cnf(c_0_2573,hypothesis,
i3 != i24,
c_0_1346,
[final] ).
cnf(c_0_2574,hypothesis,
i3 != i25,
c_0_1347,
[final] ).
cnf(c_0_2575,hypothesis,
i3 != i26,
c_0_1348,
[final] ).
cnf(c_0_2576,hypothesis,
i3 != i27,
c_0_1349,
[final] ).
cnf(c_0_2577,hypothesis,
i3 != i28,
c_0_1350,
[final] ).
cnf(c_0_2578,hypothesis,
i3 != i29,
c_0_1351,
[final] ).
cnf(c_0_2579,hypothesis,
i3 != i30,
c_0_1352,
[final] ).
cnf(c_0_2580,hypothesis,
i3 != i31,
c_0_1353,
[final] ).
cnf(c_0_2581,hypothesis,
i3 != i32,
c_0_1354,
[final] ).
cnf(c_0_2582,hypothesis,
i3 != i33,
c_0_1355,
[final] ).
cnf(c_0_2583,hypothesis,
i3 != i34,
c_0_1356,
[final] ).
cnf(c_0_2584,hypothesis,
i3 != i35,
c_0_1357,
[final] ).
cnf(c_0_2585,hypothesis,
i3 != i36,
c_0_1358,
[final] ).
cnf(c_0_2586,hypothesis,
i3 != i37,
c_0_1359,
[final] ).
cnf(c_0_2587,hypothesis,
i3 != i38,
c_0_1360,
[final] ).
cnf(c_0_2588,hypothesis,
i3 != i39,
c_0_1361,
[final] ).
cnf(c_0_2589,hypothesis,
i3 != i40,
c_0_1362,
[final] ).
cnf(c_0_2590,hypothesis,
i3 != i41,
c_0_1363,
[final] ).
cnf(c_0_2591,hypothesis,
i3 != i42,
c_0_1364,
[final] ).
cnf(c_0_2592,hypothesis,
i3 != i43,
c_0_1365,
[final] ).
cnf(c_0_2593,hypothesis,
i3 != i44,
c_0_1366,
[final] ).
cnf(c_0_2594,hypothesis,
i3 != i45,
c_0_1367,
[final] ).
cnf(c_0_2595,hypothesis,
i3 != i46,
c_0_1368,
[final] ).
cnf(c_0_2596,hypothesis,
i3 != i47,
c_0_1369,
[final] ).
cnf(c_0_2597,hypothesis,
i3 != i48,
c_0_1370,
[final] ).
cnf(c_0_2598,hypothesis,
i3 != i50,
c_0_1371,
[final] ).
cnf(c_0_2599,hypothesis,
i3 != i49,
c_0_1372,
[final] ).
cnf(c_0_2600,hypothesis,
i4 != i5,
c_0_1373,
[final] ).
cnf(c_0_2601,hypothesis,
i4 != i6,
c_0_1374,
[final] ).
cnf(c_0_2602,hypothesis,
i4 != i7,
c_0_1375,
[final] ).
cnf(c_0_2603,hypothesis,
i4 != i8,
c_0_1376,
[final] ).
cnf(c_0_2604,hypothesis,
i4 != i9,
c_0_1377,
[final] ).
cnf(c_0_2605,hypothesis,
i4 != i10,
c_0_1378,
[final] ).
cnf(c_0_2606,hypothesis,
i4 != i11,
c_0_1379,
[final] ).
cnf(c_0_2607,hypothesis,
i4 != i12,
c_0_1380,
[final] ).
cnf(c_0_2608,hypothesis,
i4 != i13,
c_0_1381,
[final] ).
cnf(c_0_2609,hypothesis,
i4 != i14,
c_0_1382,
[final] ).
cnf(c_0_2610,hypothesis,
i4 != i15,
c_0_1383,
[final] ).
cnf(c_0_2611,hypothesis,
i4 != i16,
c_0_1384,
[final] ).
cnf(c_0_2612,hypothesis,
i4 != i17,
c_0_1385,
[final] ).
cnf(c_0_2613,hypothesis,
i4 != i18,
c_0_1386,
[final] ).
cnf(c_0_2614,hypothesis,
i4 != i19,
c_0_1387,
[final] ).
cnf(c_0_2615,hypothesis,
i4 != i20,
c_0_1388,
[final] ).
cnf(c_0_2616,hypothesis,
i4 != i21,
c_0_1389,
[final] ).
cnf(c_0_2617,hypothesis,
i4 != i22,
c_0_1390,
[final] ).
cnf(c_0_2618,hypothesis,
i4 != i23,
c_0_1391,
[final] ).
cnf(c_0_2619,hypothesis,
i4 != i24,
c_0_1392,
[final] ).
cnf(c_0_2620,hypothesis,
i4 != i25,
c_0_1393,
[final] ).
cnf(c_0_2621,hypothesis,
i4 != i26,
c_0_1394,
[final] ).
cnf(c_0_2622,hypothesis,
i4 != i27,
c_0_1395,
[final] ).
cnf(c_0_2623,hypothesis,
i4 != i28,
c_0_1396,
[final] ).
cnf(c_0_2624,hypothesis,
i4 != i29,
c_0_1397,
[final] ).
cnf(c_0_2625,hypothesis,
i4 != i30,
c_0_1398,
[final] ).
cnf(c_0_2626,hypothesis,
i4 != i31,
c_0_1399,
[final] ).
cnf(c_0_2627,hypothesis,
i4 != i32,
c_0_1400,
[final] ).
cnf(c_0_2628,hypothesis,
i4 != i33,
c_0_1401,
[final] ).
cnf(c_0_2629,hypothesis,
i4 != i34,
c_0_1402,
[final] ).
cnf(c_0_2630,hypothesis,
i4 != i35,
c_0_1403,
[final] ).
cnf(c_0_2631,hypothesis,
i4 != i36,
c_0_1404,
[final] ).
cnf(c_0_2632,hypothesis,
i4 != i37,
c_0_1405,
[final] ).
cnf(c_0_2633,hypothesis,
i4 != i38,
c_0_1406,
[final] ).
cnf(c_0_2634,hypothesis,
i4 != i39,
c_0_1407,
[final] ).
cnf(c_0_2635,hypothesis,
i4 != i40,
c_0_1408,
[final] ).
cnf(c_0_2636,hypothesis,
i4 != i41,
c_0_1409,
[final] ).
cnf(c_0_2637,hypothesis,
i4 != i42,
c_0_1410,
[final] ).
cnf(c_0_2638,hypothesis,
i4 != i43,
c_0_1411,
[final] ).
cnf(c_0_2639,hypothesis,
i4 != i44,
c_0_1412,
[final] ).
cnf(c_0_2640,hypothesis,
i4 != i45,
c_0_1413,
[final] ).
cnf(c_0_2641,hypothesis,
i4 != i46,
c_0_1414,
[final] ).
cnf(c_0_2642,hypothesis,
i4 != i47,
c_0_1415,
[final] ).
cnf(c_0_2643,hypothesis,
i4 != i48,
c_0_1416,
[final] ).
cnf(c_0_2644,hypothesis,
i4 != i50,
c_0_1417,
[final] ).
cnf(c_0_2645,hypothesis,
i4 != i49,
c_0_1418,
[final] ).
cnf(c_0_2646,hypothesis,
i5 != i6,
c_0_1419,
[final] ).
cnf(c_0_2647,hypothesis,
i5 != i7,
c_0_1420,
[final] ).
cnf(c_0_2648,hypothesis,
i5 != i8,
c_0_1421,
[final] ).
cnf(c_0_2649,hypothesis,
i5 != i9,
c_0_1422,
[final] ).
cnf(c_0_2650,hypothesis,
i5 != i10,
c_0_1423,
[final] ).
cnf(c_0_2651,hypothesis,
i5 != i11,
c_0_1424,
[final] ).
cnf(c_0_2652,hypothesis,
i5 != i12,
c_0_1425,
[final] ).
cnf(c_0_2653,hypothesis,
i5 != i13,
c_0_1426,
[final] ).
cnf(c_0_2654,hypothesis,
i5 != i14,
c_0_1427,
[final] ).
cnf(c_0_2655,hypothesis,
i5 != i15,
c_0_1428,
[final] ).
cnf(c_0_2656,hypothesis,
i5 != i16,
c_0_1429,
[final] ).
cnf(c_0_2657,hypothesis,
i5 != i17,
c_0_1430,
[final] ).
cnf(c_0_2658,hypothesis,
i5 != i18,
c_0_1431,
[final] ).
cnf(c_0_2659,hypothesis,
i5 != i19,
c_0_1432,
[final] ).
cnf(c_0_2660,hypothesis,
i5 != i20,
c_0_1433,
[final] ).
cnf(c_0_2661,hypothesis,
i5 != i21,
c_0_1434,
[final] ).
cnf(c_0_2662,hypothesis,
i5 != i22,
c_0_1435,
[final] ).
cnf(c_0_2663,hypothesis,
i5 != i23,
c_0_1436,
[final] ).
cnf(c_0_2664,hypothesis,
i5 != i24,
c_0_1437,
[final] ).
cnf(c_0_2665,hypothesis,
i5 != i25,
c_0_1438,
[final] ).
cnf(c_0_2666,hypothesis,
i5 != i26,
c_0_1439,
[final] ).
cnf(c_0_2667,hypothesis,
i5 != i27,
c_0_1440,
[final] ).
cnf(c_0_2668,hypothesis,
i5 != i28,
c_0_1441,
[final] ).
cnf(c_0_2669,hypothesis,
i5 != i29,
c_0_1442,
[final] ).
cnf(c_0_2670,hypothesis,
i5 != i30,
c_0_1443,
[final] ).
cnf(c_0_2671,hypothesis,
i5 != i31,
c_0_1444,
[final] ).
cnf(c_0_2672,hypothesis,
i5 != i32,
c_0_1445,
[final] ).
cnf(c_0_2673,hypothesis,
i5 != i33,
c_0_1446,
[final] ).
cnf(c_0_2674,hypothesis,
i5 != i34,
c_0_1447,
[final] ).
cnf(c_0_2675,hypothesis,
i5 != i35,
c_0_1448,
[final] ).
cnf(c_0_2676,hypothesis,
i5 != i36,
c_0_1449,
[final] ).
cnf(c_0_2677,hypothesis,
i5 != i37,
c_0_1450,
[final] ).
cnf(c_0_2678,hypothesis,
i5 != i38,
c_0_1451,
[final] ).
cnf(c_0_2679,hypothesis,
i5 != i39,
c_0_1452,
[final] ).
cnf(c_0_2680,hypothesis,
i5 != i40,
c_0_1453,
[final] ).
cnf(c_0_2681,hypothesis,
i5 != i41,
c_0_1454,
[final] ).
cnf(c_0_2682,hypothesis,
i5 != i42,
c_0_1455,
[final] ).
cnf(c_0_2683,hypothesis,
i5 != i43,
c_0_1456,
[final] ).
cnf(c_0_2684,hypothesis,
i5 != i44,
c_0_1457,
[final] ).
cnf(c_0_2685,hypothesis,
i5 != i45,
c_0_1458,
[final] ).
cnf(c_0_2686,hypothesis,
i5 != i46,
c_0_1459,
[final] ).
cnf(c_0_2687,hypothesis,
i5 != i47,
c_0_1460,
[final] ).
cnf(c_0_2688,hypothesis,
i5 != i48,
c_0_1461,
[final] ).
cnf(c_0_2689,hypothesis,
i5 != i50,
c_0_1462,
[final] ).
cnf(c_0_2690,hypothesis,
i5 != i49,
c_0_1463,
[final] ).
cnf(c_0_2691,hypothesis,
i6 != i7,
c_0_1464,
[final] ).
cnf(c_0_2692,hypothesis,
i6 != i8,
c_0_1465,
[final] ).
cnf(c_0_2693,hypothesis,
i6 != i9,
c_0_1466,
[final] ).
cnf(c_0_2694,hypothesis,
i6 != i10,
c_0_1467,
[final] ).
cnf(c_0_2695,hypothesis,
i6 != i11,
c_0_1468,
[final] ).
cnf(c_0_2696,hypothesis,
i6 != i12,
c_0_1469,
[final] ).
cnf(c_0_2697,hypothesis,
i6 != i13,
c_0_1470,
[final] ).
cnf(c_0_2698,hypothesis,
i6 != i14,
c_0_1471,
[final] ).
cnf(c_0_2699,hypothesis,
i6 != i15,
c_0_1472,
[final] ).
cnf(c_0_2700,hypothesis,
i6 != i16,
c_0_1473,
[final] ).
cnf(c_0_2701,hypothesis,
i6 != i17,
c_0_1474,
[final] ).
cnf(c_0_2702,hypothesis,
i6 != i18,
c_0_1475,
[final] ).
cnf(c_0_2703,hypothesis,
i6 != i19,
c_0_1476,
[final] ).
cnf(c_0_2704,hypothesis,
i6 != i20,
c_0_1477,
[final] ).
cnf(c_0_2705,hypothesis,
i6 != i21,
c_0_1478,
[final] ).
cnf(c_0_2706,hypothesis,
i6 != i22,
c_0_1479,
[final] ).
cnf(c_0_2707,hypothesis,
i6 != i23,
c_0_1480,
[final] ).
cnf(c_0_2708,hypothesis,
i6 != i24,
c_0_1481,
[final] ).
cnf(c_0_2709,hypothesis,
i6 != i25,
c_0_1482,
[final] ).
cnf(c_0_2710,hypothesis,
i6 != i26,
c_0_1483,
[final] ).
cnf(c_0_2711,hypothesis,
i6 != i27,
c_0_1484,
[final] ).
cnf(c_0_2712,hypothesis,
i6 != i28,
c_0_1485,
[final] ).
cnf(c_0_2713,hypothesis,
i6 != i29,
c_0_1486,
[final] ).
cnf(c_0_2714,hypothesis,
i6 != i30,
c_0_1487,
[final] ).
cnf(c_0_2715,hypothesis,
i6 != i31,
c_0_1488,
[final] ).
cnf(c_0_2716,hypothesis,
i6 != i32,
c_0_1489,
[final] ).
cnf(c_0_2717,hypothesis,
i6 != i33,
c_0_1490,
[final] ).
cnf(c_0_2718,hypothesis,
i6 != i34,
c_0_1491,
[final] ).
cnf(c_0_2719,hypothesis,
i6 != i35,
c_0_1492,
[final] ).
cnf(c_0_2720,hypothesis,
i6 != i36,
c_0_1493,
[final] ).
cnf(c_0_2721,hypothesis,
i6 != i37,
c_0_1494,
[final] ).
cnf(c_0_2722,hypothesis,
i6 != i38,
c_0_1495,
[final] ).
cnf(c_0_2723,hypothesis,
i6 != i39,
c_0_1496,
[final] ).
cnf(c_0_2724,hypothesis,
i6 != i40,
c_0_1497,
[final] ).
cnf(c_0_2725,hypothesis,
i6 != i41,
c_0_1498,
[final] ).
cnf(c_0_2726,hypothesis,
i6 != i42,
c_0_1499,
[final] ).
cnf(c_0_2727,hypothesis,
i6 != i43,
c_0_1500,
[final] ).
cnf(c_0_2728,hypothesis,
i6 != i44,
c_0_1501,
[final] ).
cnf(c_0_2729,hypothesis,
i6 != i45,
c_0_1502,
[final] ).
cnf(c_0_2730,hypothesis,
i6 != i46,
c_0_1503,
[final] ).
cnf(c_0_2731,hypothesis,
i6 != i47,
c_0_1504,
[final] ).
cnf(c_0_2732,hypothesis,
i6 != i48,
c_0_1505,
[final] ).
cnf(c_0_2733,hypothesis,
i6 != i50,
c_0_1506,
[final] ).
cnf(c_0_2734,hypothesis,
i6 != i49,
c_0_1507,
[final] ).
cnf(c_0_2735,hypothesis,
i7 != i8,
c_0_1508,
[final] ).
cnf(c_0_2736,hypothesis,
i7 != i9,
c_0_1509,
[final] ).
cnf(c_0_2737,hypothesis,
i7 != i10,
c_0_1510,
[final] ).
cnf(c_0_2738,hypothesis,
i7 != i11,
c_0_1511,
[final] ).
cnf(c_0_2739,hypothesis,
i7 != i12,
c_0_1512,
[final] ).
cnf(c_0_2740,hypothesis,
i7 != i13,
c_0_1513,
[final] ).
cnf(c_0_2741,hypothesis,
i7 != i14,
c_0_1514,
[final] ).
cnf(c_0_2742,hypothesis,
i7 != i15,
c_0_1515,
[final] ).
cnf(c_0_2743,hypothesis,
i7 != i16,
c_0_1516,
[final] ).
cnf(c_0_2744,hypothesis,
i7 != i17,
c_0_1517,
[final] ).
cnf(c_0_2745,hypothesis,
i7 != i18,
c_0_1518,
[final] ).
cnf(c_0_2746,hypothesis,
i7 != i19,
c_0_1519,
[final] ).
cnf(c_0_2747,hypothesis,
i7 != i20,
c_0_1520,
[final] ).
cnf(c_0_2748,hypothesis,
i7 != i21,
c_0_1521,
[final] ).
cnf(c_0_2749,hypothesis,
i7 != i22,
c_0_1522,
[final] ).
cnf(c_0_2750,hypothesis,
i7 != i23,
c_0_1523,
[final] ).
cnf(c_0_2751,hypothesis,
i7 != i24,
c_0_1524,
[final] ).
cnf(c_0_2752,hypothesis,
i7 != i25,
c_0_1525,
[final] ).
cnf(c_0_2753,hypothesis,
i7 != i26,
c_0_1526,
[final] ).
cnf(c_0_2754,hypothesis,
i7 != i27,
c_0_1527,
[final] ).
cnf(c_0_2755,hypothesis,
i7 != i28,
c_0_1528,
[final] ).
cnf(c_0_2756,hypothesis,
i7 != i29,
c_0_1529,
[final] ).
cnf(c_0_2757,hypothesis,
i7 != i30,
c_0_1530,
[final] ).
cnf(c_0_2758,hypothesis,
i7 != i31,
c_0_1531,
[final] ).
cnf(c_0_2759,hypothesis,
i7 != i32,
c_0_1532,
[final] ).
cnf(c_0_2760,hypothesis,
i7 != i33,
c_0_1533,
[final] ).
cnf(c_0_2761,hypothesis,
i7 != i34,
c_0_1534,
[final] ).
cnf(c_0_2762,hypothesis,
i7 != i35,
c_0_1535,
[final] ).
cnf(c_0_2763,hypothesis,
i7 != i36,
c_0_1536,
[final] ).
cnf(c_0_2764,hypothesis,
i7 != i37,
c_0_1537,
[final] ).
cnf(c_0_2765,hypothesis,
i7 != i38,
c_0_1538,
[final] ).
cnf(c_0_2766,hypothesis,
i7 != i39,
c_0_1539,
[final] ).
cnf(c_0_2767,hypothesis,
i7 != i40,
c_0_1540,
[final] ).
cnf(c_0_2768,hypothesis,
i7 != i41,
c_0_1541,
[final] ).
cnf(c_0_2769,hypothesis,
i7 != i42,
c_0_1542,
[final] ).
cnf(c_0_2770,hypothesis,
i7 != i43,
c_0_1543,
[final] ).
cnf(c_0_2771,hypothesis,
i7 != i44,
c_0_1544,
[final] ).
cnf(c_0_2772,hypothesis,
i7 != i45,
c_0_1545,
[final] ).
cnf(c_0_2773,hypothesis,
i7 != i46,
c_0_1546,
[final] ).
cnf(c_0_2774,hypothesis,
i7 != i47,
c_0_1547,
[final] ).
cnf(c_0_2775,hypothesis,
i7 != i48,
c_0_1548,
[final] ).
cnf(c_0_2776,hypothesis,
i7 != i50,
c_0_1549,
[final] ).
cnf(c_0_2777,hypothesis,
i7 != i49,
c_0_1550,
[final] ).
cnf(c_0_2778,hypothesis,
i8 != i9,
c_0_1551,
[final] ).
cnf(c_0_2779,hypothesis,
i8 != i10,
c_0_1552,
[final] ).
cnf(c_0_2780,hypothesis,
i8 != i11,
c_0_1553,
[final] ).
cnf(c_0_2781,hypothesis,
i8 != i12,
c_0_1554,
[final] ).
cnf(c_0_2782,hypothesis,
i8 != i13,
c_0_1555,
[final] ).
cnf(c_0_2783,hypothesis,
i8 != i14,
c_0_1556,
[final] ).
cnf(c_0_2784,hypothesis,
i8 != i15,
c_0_1557,
[final] ).
cnf(c_0_2785,hypothesis,
i8 != i16,
c_0_1558,
[final] ).
cnf(c_0_2786,hypothesis,
i8 != i17,
c_0_1559,
[final] ).
cnf(c_0_2787,hypothesis,
i8 != i18,
c_0_1560,
[final] ).
cnf(c_0_2788,hypothesis,
i8 != i19,
c_0_1561,
[final] ).
cnf(c_0_2789,hypothesis,
i8 != i20,
c_0_1562,
[final] ).
cnf(c_0_2790,hypothesis,
i8 != i21,
c_0_1563,
[final] ).
cnf(c_0_2791,hypothesis,
i8 != i22,
c_0_1564,
[final] ).
cnf(c_0_2792,hypothesis,
i8 != i23,
c_0_1565,
[final] ).
cnf(c_0_2793,hypothesis,
i8 != i24,
c_0_1566,
[final] ).
cnf(c_0_2794,hypothesis,
i8 != i25,
c_0_1567,
[final] ).
cnf(c_0_2795,hypothesis,
i8 != i26,
c_0_1568,
[final] ).
cnf(c_0_2796,hypothesis,
i8 != i27,
c_0_1569,
[final] ).
cnf(c_0_2797,hypothesis,
i8 != i28,
c_0_1570,
[final] ).
cnf(c_0_2798,hypothesis,
i8 != i29,
c_0_1571,
[final] ).
cnf(c_0_2799,hypothesis,
i8 != i30,
c_0_1572,
[final] ).
cnf(c_0_2800,hypothesis,
i8 != i31,
c_0_1573,
[final] ).
cnf(c_0_2801,hypothesis,
i8 != i32,
c_0_1574,
[final] ).
cnf(c_0_2802,hypothesis,
i8 != i33,
c_0_1575,
[final] ).
cnf(c_0_2803,hypothesis,
i8 != i34,
c_0_1576,
[final] ).
cnf(c_0_2804,hypothesis,
i8 != i35,
c_0_1577,
[final] ).
cnf(c_0_2805,hypothesis,
i8 != i36,
c_0_1578,
[final] ).
cnf(c_0_2806,hypothesis,
i8 != i37,
c_0_1579,
[final] ).
cnf(c_0_2807,hypothesis,
i8 != i38,
c_0_1580,
[final] ).
cnf(c_0_2808,hypothesis,
i8 != i39,
c_0_1581,
[final] ).
cnf(c_0_2809,hypothesis,
i8 != i40,
c_0_1582,
[final] ).
cnf(c_0_2810,hypothesis,
i8 != i41,
c_0_1583,
[final] ).
cnf(c_0_2811,hypothesis,
i8 != i42,
c_0_1584,
[final] ).
cnf(c_0_2812,hypothesis,
i8 != i43,
c_0_1585,
[final] ).
cnf(c_0_2813,hypothesis,
i8 != i44,
c_0_1586,
[final] ).
cnf(c_0_2814,hypothesis,
i8 != i45,
c_0_1587,
[final] ).
cnf(c_0_2815,hypothesis,
i8 != i46,
c_0_1588,
[final] ).
cnf(c_0_2816,hypothesis,
i8 != i47,
c_0_1589,
[final] ).
cnf(c_0_2817,hypothesis,
i8 != i48,
c_0_1590,
[final] ).
cnf(c_0_2818,hypothesis,
i8 != i50,
c_0_1591,
[final] ).
cnf(c_0_2819,hypothesis,
i8 != i49,
c_0_1592,
[final] ).
cnf(c_0_2820,hypothesis,
i9 != i10,
c_0_1593,
[final] ).
cnf(c_0_2821,hypothesis,
i9 != i11,
c_0_1594,
[final] ).
cnf(c_0_2822,hypothesis,
i9 != i12,
c_0_1595,
[final] ).
cnf(c_0_2823,hypothesis,
i9 != i13,
c_0_1596,
[final] ).
cnf(c_0_2824,hypothesis,
i9 != i14,
c_0_1597,
[final] ).
cnf(c_0_2825,hypothesis,
i9 != i15,
c_0_1598,
[final] ).
cnf(c_0_2826,hypothesis,
i9 != i16,
c_0_1599,
[final] ).
cnf(c_0_2827,hypothesis,
i9 != i17,
c_0_1600,
[final] ).
cnf(c_0_2828,hypothesis,
i9 != i18,
c_0_1601,
[final] ).
cnf(c_0_2829,hypothesis,
i9 != i19,
c_0_1602,
[final] ).
cnf(c_0_2830,hypothesis,
i9 != i20,
c_0_1603,
[final] ).
cnf(c_0_2831,hypothesis,
i9 != i21,
c_0_1604,
[final] ).
cnf(c_0_2832,hypothesis,
i9 != i22,
c_0_1605,
[final] ).
cnf(c_0_2833,hypothesis,
i9 != i23,
c_0_1606,
[final] ).
cnf(c_0_2834,hypothesis,
i9 != i24,
c_0_1607,
[final] ).
cnf(c_0_2835,hypothesis,
i9 != i25,
c_0_1608,
[final] ).
cnf(c_0_2836,hypothesis,
i9 != i26,
c_0_1609,
[final] ).
cnf(c_0_2837,hypothesis,
i9 != i27,
c_0_1610,
[final] ).
cnf(c_0_2838,hypothesis,
i9 != i28,
c_0_1611,
[final] ).
cnf(c_0_2839,hypothesis,
i9 != i29,
c_0_1612,
[final] ).
cnf(c_0_2840,hypothesis,
i9 != i30,
c_0_1613,
[final] ).
cnf(c_0_2841,hypothesis,
i9 != i31,
c_0_1614,
[final] ).
cnf(c_0_2842,hypothesis,
i9 != i32,
c_0_1615,
[final] ).
cnf(c_0_2843,hypothesis,
i9 != i33,
c_0_1616,
[final] ).
cnf(c_0_2844,hypothesis,
i9 != i34,
c_0_1617,
[final] ).
cnf(c_0_2845,hypothesis,
i9 != i35,
c_0_1618,
[final] ).
cnf(c_0_2846,hypothesis,
i9 != i36,
c_0_1619,
[final] ).
cnf(c_0_2847,hypothesis,
i9 != i37,
c_0_1620,
[final] ).
cnf(c_0_2848,hypothesis,
i9 != i38,
c_0_1621,
[final] ).
cnf(c_0_2849,hypothesis,
i9 != i39,
c_0_1622,
[final] ).
cnf(c_0_2850,hypothesis,
i9 != i40,
c_0_1623,
[final] ).
cnf(c_0_2851,hypothesis,
i9 != i41,
c_0_1624,
[final] ).
cnf(c_0_2852,hypothesis,
i9 != i42,
c_0_1625,
[final] ).
cnf(c_0_2853,hypothesis,
i9 != i43,
c_0_1626,
[final] ).
cnf(c_0_2854,hypothesis,
i9 != i44,
c_0_1627,
[final] ).
cnf(c_0_2855,hypothesis,
i9 != i45,
c_0_1628,
[final] ).
cnf(c_0_2856,hypothesis,
i9 != i46,
c_0_1629,
[final] ).
cnf(c_0_2857,hypothesis,
i9 != i47,
c_0_1630,
[final] ).
cnf(c_0_2858,hypothesis,
i9 != i48,
c_0_1631,
[final] ).
cnf(c_0_2859,hypothesis,
i9 != i50,
c_0_1632,
[final] ).
cnf(c_0_2860,hypothesis,
i9 != i49,
c_0_1633,
[final] ).
cnf(c_0_2861,hypothesis,
i10 != i11,
c_0_1634,
[final] ).
cnf(c_0_2862,hypothesis,
i10 != i12,
c_0_1635,
[final] ).
cnf(c_0_2863,hypothesis,
i10 != i13,
c_0_1636,
[final] ).
cnf(c_0_2864,hypothesis,
i10 != i14,
c_0_1637,
[final] ).
cnf(c_0_2865,hypothesis,
i10 != i15,
c_0_1638,
[final] ).
cnf(c_0_2866,hypothesis,
i10 != i16,
c_0_1639,
[final] ).
cnf(c_0_2867,hypothesis,
i10 != i17,
c_0_1640,
[final] ).
cnf(c_0_2868,hypothesis,
i10 != i18,
c_0_1641,
[final] ).
cnf(c_0_2869,hypothesis,
i10 != i19,
c_0_1642,
[final] ).
cnf(c_0_2870,hypothesis,
i10 != i20,
c_0_1643,
[final] ).
cnf(c_0_2871,hypothesis,
i10 != i21,
c_0_1644,
[final] ).
cnf(c_0_2872,hypothesis,
i10 != i22,
c_0_1645,
[final] ).
cnf(c_0_2873,hypothesis,
i10 != i23,
c_0_1646,
[final] ).
cnf(c_0_2874,hypothesis,
i10 != i24,
c_0_1647,
[final] ).
cnf(c_0_2875,hypothesis,
i10 != i25,
c_0_1648,
[final] ).
cnf(c_0_2876,hypothesis,
i10 != i26,
c_0_1649,
[final] ).
cnf(c_0_2877,hypothesis,
i10 != i27,
c_0_1650,
[final] ).
cnf(c_0_2878,hypothesis,
i10 != i28,
c_0_1651,
[final] ).
cnf(c_0_2879,hypothesis,
i10 != i29,
c_0_1652,
[final] ).
cnf(c_0_2880,hypothesis,
i10 != i30,
c_0_1653,
[final] ).
cnf(c_0_2881,hypothesis,
i10 != i31,
c_0_1654,
[final] ).
cnf(c_0_2882,hypothesis,
i10 != i32,
c_0_1655,
[final] ).
cnf(c_0_2883,hypothesis,
i10 != i33,
c_0_1656,
[final] ).
cnf(c_0_2884,hypothesis,
i10 != i34,
c_0_1657,
[final] ).
cnf(c_0_2885,hypothesis,
i10 != i35,
c_0_1658,
[final] ).
cnf(c_0_2886,hypothesis,
i10 != i36,
c_0_1659,
[final] ).
cnf(c_0_2887,hypothesis,
i10 != i37,
c_0_1660,
[final] ).
cnf(c_0_2888,hypothesis,
i10 != i38,
c_0_1661,
[final] ).
cnf(c_0_2889,hypothesis,
i10 != i39,
c_0_1662,
[final] ).
cnf(c_0_2890,hypothesis,
i10 != i40,
c_0_1663,
[final] ).
cnf(c_0_2891,hypothesis,
i10 != i41,
c_0_1664,
[final] ).
cnf(c_0_2892,hypothesis,
i10 != i42,
c_0_1665,
[final] ).
cnf(c_0_2893,hypothesis,
i10 != i43,
c_0_1666,
[final] ).
cnf(c_0_2894,hypothesis,
i10 != i44,
c_0_1667,
[final] ).
cnf(c_0_2895,hypothesis,
i10 != i45,
c_0_1668,
[final] ).
cnf(c_0_2896,hypothesis,
i10 != i46,
c_0_1669,
[final] ).
cnf(c_0_2897,hypothesis,
i10 != i47,
c_0_1670,
[final] ).
cnf(c_0_2898,hypothesis,
i10 != i48,
c_0_1671,
[final] ).
cnf(c_0_2899,hypothesis,
i10 != i50,
c_0_1672,
[final] ).
cnf(c_0_2900,hypothesis,
i10 != i49,
c_0_1673,
[final] ).
cnf(c_0_2901,hypothesis,
i11 != i12,
c_0_1674,
[final] ).
cnf(c_0_2902,hypothesis,
i11 != i13,
c_0_1675,
[final] ).
cnf(c_0_2903,hypothesis,
i11 != i14,
c_0_1676,
[final] ).
cnf(c_0_2904,hypothesis,
i11 != i15,
c_0_1677,
[final] ).
cnf(c_0_2905,hypothesis,
i11 != i16,
c_0_1678,
[final] ).
cnf(c_0_2906,hypothesis,
i11 != i17,
c_0_1679,
[final] ).
cnf(c_0_2907,hypothesis,
i11 != i18,
c_0_1680,
[final] ).
cnf(c_0_2908,hypothesis,
i11 != i19,
c_0_1681,
[final] ).
cnf(c_0_2909,hypothesis,
i11 != i20,
c_0_1682,
[final] ).
cnf(c_0_2910,hypothesis,
i11 != i21,
c_0_1683,
[final] ).
cnf(c_0_2911,hypothesis,
i11 != i22,
c_0_1684,
[final] ).
cnf(c_0_2912,hypothesis,
i11 != i23,
c_0_1685,
[final] ).
cnf(c_0_2913,hypothesis,
i11 != i24,
c_0_1686,
[final] ).
cnf(c_0_2914,hypothesis,
i11 != i25,
c_0_1687,
[final] ).
cnf(c_0_2915,hypothesis,
i11 != i26,
c_0_1688,
[final] ).
cnf(c_0_2916,hypothesis,
i11 != i27,
c_0_1689,
[final] ).
cnf(c_0_2917,hypothesis,
i11 != i28,
c_0_1690,
[final] ).
cnf(c_0_2918,hypothesis,
i11 != i29,
c_0_1691,
[final] ).
cnf(c_0_2919,hypothesis,
i11 != i30,
c_0_1692,
[final] ).
cnf(c_0_2920,hypothesis,
i11 != i31,
c_0_1693,
[final] ).
cnf(c_0_2921,hypothesis,
i11 != i32,
c_0_1694,
[final] ).
cnf(c_0_2922,hypothesis,
i11 != i33,
c_0_1695,
[final] ).
cnf(c_0_2923,hypothesis,
i11 != i34,
c_0_1696,
[final] ).
cnf(c_0_2924,hypothesis,
i11 != i35,
c_0_1697,
[final] ).
cnf(c_0_2925,hypothesis,
i11 != i36,
c_0_1698,
[final] ).
cnf(c_0_2926,hypothesis,
i11 != i37,
c_0_1699,
[final] ).
cnf(c_0_2927,hypothesis,
i11 != i38,
c_0_1700,
[final] ).
cnf(c_0_2928,hypothesis,
i11 != i39,
c_0_1701,
[final] ).
cnf(c_0_2929,hypothesis,
i11 != i40,
c_0_1702,
[final] ).
cnf(c_0_2930,hypothesis,
i11 != i41,
c_0_1703,
[final] ).
cnf(c_0_2931,hypothesis,
i11 != i42,
c_0_1704,
[final] ).
cnf(c_0_2932,hypothesis,
i11 != i43,
c_0_1705,
[final] ).
cnf(c_0_2933,hypothesis,
i11 != i44,
c_0_1706,
[final] ).
cnf(c_0_2934,hypothesis,
i11 != i45,
c_0_1707,
[final] ).
cnf(c_0_2935,hypothesis,
i11 != i46,
c_0_1708,
[final] ).
cnf(c_0_2936,hypothesis,
i11 != i47,
c_0_1709,
[final] ).
cnf(c_0_2937,hypothesis,
i11 != i48,
c_0_1710,
[final] ).
cnf(c_0_2938,hypothesis,
i11 != i50,
c_0_1711,
[final] ).
cnf(c_0_2939,hypothesis,
i11 != i49,
c_0_1712,
[final] ).
cnf(c_0_2940,hypothesis,
i12 != i13,
c_0_1713,
[final] ).
cnf(c_0_2941,hypothesis,
i12 != i14,
c_0_1714,
[final] ).
cnf(c_0_2942,hypothesis,
i12 != i15,
c_0_1715,
[final] ).
cnf(c_0_2943,hypothesis,
i12 != i16,
c_0_1716,
[final] ).
cnf(c_0_2944,hypothesis,
i12 != i17,
c_0_1717,
[final] ).
cnf(c_0_2945,hypothesis,
i12 != i18,
c_0_1718,
[final] ).
cnf(c_0_2946,hypothesis,
i12 != i19,
c_0_1719,
[final] ).
cnf(c_0_2947,hypothesis,
i12 != i20,
c_0_1720,
[final] ).
cnf(c_0_2948,hypothesis,
i12 != i21,
c_0_1721,
[final] ).
cnf(c_0_2949,hypothesis,
i12 != i22,
c_0_1722,
[final] ).
cnf(c_0_2950,hypothesis,
i12 != i23,
c_0_1723,
[final] ).
cnf(c_0_2951,hypothesis,
i12 != i24,
c_0_1724,
[final] ).
cnf(c_0_2952,hypothesis,
i12 != i25,
c_0_1725,
[final] ).
cnf(c_0_2953,hypothesis,
i12 != i26,
c_0_1726,
[final] ).
cnf(c_0_2954,hypothesis,
i12 != i27,
c_0_1727,
[final] ).
cnf(c_0_2955,hypothesis,
i12 != i28,
c_0_1728,
[final] ).
cnf(c_0_2956,hypothesis,
i12 != i29,
c_0_1729,
[final] ).
cnf(c_0_2957,hypothesis,
i12 != i30,
c_0_1730,
[final] ).
cnf(c_0_2958,hypothesis,
i12 != i31,
c_0_1731,
[final] ).
cnf(c_0_2959,hypothesis,
i12 != i32,
c_0_1732,
[final] ).
cnf(c_0_2960,hypothesis,
i12 != i33,
c_0_1733,
[final] ).
cnf(c_0_2961,hypothesis,
i12 != i34,
c_0_1734,
[final] ).
cnf(c_0_2962,hypothesis,
i12 != i35,
c_0_1735,
[final] ).
cnf(c_0_2963,hypothesis,
i12 != i36,
c_0_1736,
[final] ).
cnf(c_0_2964,hypothesis,
i12 != i37,
c_0_1737,
[final] ).
cnf(c_0_2965,hypothesis,
i12 != i38,
c_0_1738,
[final] ).
cnf(c_0_2966,hypothesis,
i12 != i39,
c_0_1739,
[final] ).
cnf(c_0_2967,hypothesis,
i12 != i40,
c_0_1740,
[final] ).
cnf(c_0_2968,hypothesis,
i12 != i41,
c_0_1741,
[final] ).
cnf(c_0_2969,hypothesis,
i12 != i42,
c_0_1742,
[final] ).
cnf(c_0_2970,hypothesis,
i12 != i43,
c_0_1743,
[final] ).
cnf(c_0_2971,hypothesis,
i12 != i44,
c_0_1744,
[final] ).
cnf(c_0_2972,hypothesis,
i12 != i45,
c_0_1745,
[final] ).
cnf(c_0_2973,hypothesis,
i12 != i46,
c_0_1746,
[final] ).
cnf(c_0_2974,hypothesis,
i12 != i47,
c_0_1747,
[final] ).
cnf(c_0_2975,hypothesis,
i12 != i48,
c_0_1748,
[final] ).
cnf(c_0_2976,hypothesis,
i12 != i50,
c_0_1749,
[final] ).
cnf(c_0_2977,hypothesis,
i12 != i49,
c_0_1750,
[final] ).
cnf(c_0_2978,hypothesis,
i13 != i14,
c_0_1751,
[final] ).
cnf(c_0_2979,hypothesis,
i13 != i15,
c_0_1752,
[final] ).
cnf(c_0_2980,hypothesis,
i13 != i16,
c_0_1753,
[final] ).
cnf(c_0_2981,hypothesis,
i13 != i17,
c_0_1754,
[final] ).
cnf(c_0_2982,hypothesis,
i13 != i18,
c_0_1755,
[final] ).
cnf(c_0_2983,hypothesis,
i13 != i19,
c_0_1756,
[final] ).
cnf(c_0_2984,hypothesis,
i13 != i20,
c_0_1757,
[final] ).
cnf(c_0_2985,hypothesis,
i13 != i21,
c_0_1758,
[final] ).
cnf(c_0_2986,hypothesis,
i13 != i22,
c_0_1759,
[final] ).
cnf(c_0_2987,hypothesis,
i13 != i23,
c_0_1760,
[final] ).
cnf(c_0_2988,hypothesis,
i13 != i24,
c_0_1761,
[final] ).
cnf(c_0_2989,hypothesis,
i13 != i25,
c_0_1762,
[final] ).
cnf(c_0_2990,hypothesis,
i13 != i26,
c_0_1763,
[final] ).
cnf(c_0_2991,hypothesis,
i13 != i27,
c_0_1764,
[final] ).
cnf(c_0_2992,hypothesis,
i13 != i28,
c_0_1765,
[final] ).
cnf(c_0_2993,hypothesis,
i13 != i29,
c_0_1766,
[final] ).
cnf(c_0_2994,hypothesis,
i13 != i30,
c_0_1767,
[final] ).
cnf(c_0_2995,hypothesis,
i13 != i31,
c_0_1768,
[final] ).
cnf(c_0_2996,hypothesis,
i13 != i32,
c_0_1769,
[final] ).
cnf(c_0_2997,hypothesis,
i13 != i33,
c_0_1770,
[final] ).
cnf(c_0_2998,hypothesis,
i13 != i34,
c_0_1771,
[final] ).
cnf(c_0_2999,hypothesis,
i13 != i35,
c_0_1772,
[final] ).
cnf(c_0_3000,hypothesis,
i13 != i36,
c_0_1773,
[final] ).
cnf(c_0_3001,hypothesis,
i13 != i37,
c_0_1774,
[final] ).
cnf(c_0_3002,hypothesis,
i13 != i38,
c_0_1775,
[final] ).
cnf(c_0_3003,hypothesis,
i13 != i39,
c_0_1776,
[final] ).
cnf(c_0_3004,hypothesis,
i13 != i40,
c_0_1777,
[final] ).
cnf(c_0_3005,hypothesis,
i13 != i41,
c_0_1778,
[final] ).
cnf(c_0_3006,hypothesis,
i13 != i42,
c_0_1779,
[final] ).
cnf(c_0_3007,hypothesis,
i13 != i43,
c_0_1780,
[final] ).
cnf(c_0_3008,hypothesis,
i13 != i44,
c_0_1781,
[final] ).
cnf(c_0_3009,hypothesis,
i13 != i45,
c_0_1782,
[final] ).
cnf(c_0_3010,hypothesis,
i13 != i46,
c_0_1783,
[final] ).
cnf(c_0_3011,hypothesis,
i13 != i47,
c_0_1784,
[final] ).
cnf(c_0_3012,hypothesis,
i13 != i48,
c_0_1785,
[final] ).
cnf(c_0_3013,hypothesis,
i13 != i50,
c_0_1786,
[final] ).
cnf(c_0_3014,hypothesis,
i13 != i49,
c_0_1787,
[final] ).
cnf(c_0_3015,hypothesis,
i14 != i15,
c_0_1788,
[final] ).
cnf(c_0_3016,hypothesis,
i14 != i16,
c_0_1789,
[final] ).
cnf(c_0_3017,hypothesis,
i14 != i17,
c_0_1790,
[final] ).
cnf(c_0_3018,hypothesis,
i14 != i18,
c_0_1791,
[final] ).
cnf(c_0_3019,hypothesis,
i14 != i19,
c_0_1792,
[final] ).
cnf(c_0_3020,hypothesis,
i14 != i20,
c_0_1793,
[final] ).
cnf(c_0_3021,hypothesis,
i14 != i21,
c_0_1794,
[final] ).
cnf(c_0_3022,hypothesis,
i14 != i22,
c_0_1795,
[final] ).
cnf(c_0_3023,hypothesis,
i14 != i23,
c_0_1796,
[final] ).
cnf(c_0_3024,hypothesis,
i14 != i24,
c_0_1797,
[final] ).
cnf(c_0_3025,hypothesis,
i14 != i25,
c_0_1798,
[final] ).
cnf(c_0_3026,hypothesis,
i14 != i26,
c_0_1799,
[final] ).
cnf(c_0_3027,hypothesis,
i14 != i27,
c_0_1800,
[final] ).
cnf(c_0_3028,hypothesis,
i14 != i28,
c_0_1801,
[final] ).
cnf(c_0_3029,hypothesis,
i14 != i29,
c_0_1802,
[final] ).
cnf(c_0_3030,hypothesis,
i14 != i30,
c_0_1803,
[final] ).
cnf(c_0_3031,hypothesis,
i14 != i31,
c_0_1804,
[final] ).
cnf(c_0_3032,hypothesis,
i14 != i32,
c_0_1805,
[final] ).
cnf(c_0_3033,hypothesis,
i14 != i33,
c_0_1806,
[final] ).
cnf(c_0_3034,hypothesis,
i14 != i34,
c_0_1807,
[final] ).
cnf(c_0_3035,hypothesis,
i14 != i35,
c_0_1808,
[final] ).
cnf(c_0_3036,hypothesis,
i14 != i36,
c_0_1809,
[final] ).
cnf(c_0_3037,hypothesis,
i14 != i37,
c_0_1810,
[final] ).
cnf(c_0_3038,hypothesis,
i14 != i38,
c_0_1811,
[final] ).
cnf(c_0_3039,hypothesis,
i14 != i39,
c_0_1812,
[final] ).
cnf(c_0_3040,hypothesis,
i14 != i40,
c_0_1813,
[final] ).
cnf(c_0_3041,hypothesis,
i14 != i41,
c_0_1814,
[final] ).
cnf(c_0_3042,hypothesis,
i14 != i42,
c_0_1815,
[final] ).
cnf(c_0_3043,hypothesis,
i14 != i43,
c_0_1816,
[final] ).
cnf(c_0_3044,hypothesis,
i14 != i44,
c_0_1817,
[final] ).
cnf(c_0_3045,hypothesis,
i14 != i45,
c_0_1818,
[final] ).
cnf(c_0_3046,hypothesis,
i14 != i46,
c_0_1819,
[final] ).
cnf(c_0_3047,hypothesis,
i14 != i47,
c_0_1820,
[final] ).
cnf(c_0_3048,hypothesis,
i14 != i48,
c_0_1821,
[final] ).
cnf(c_0_3049,hypothesis,
i14 != i50,
c_0_1822,
[final] ).
cnf(c_0_3050,hypothesis,
i14 != i49,
c_0_1823,
[final] ).
cnf(c_0_3051,hypothesis,
i15 != i16,
c_0_1824,
[final] ).
cnf(c_0_3052,hypothesis,
i15 != i17,
c_0_1825,
[final] ).
cnf(c_0_3053,hypothesis,
i15 != i18,
c_0_1826,
[final] ).
cnf(c_0_3054,hypothesis,
i15 != i19,
c_0_1827,
[final] ).
cnf(c_0_3055,hypothesis,
i15 != i20,
c_0_1828,
[final] ).
cnf(c_0_3056,hypothesis,
i15 != i21,
c_0_1829,
[final] ).
cnf(c_0_3057,hypothesis,
i15 != i22,
c_0_1830,
[final] ).
cnf(c_0_3058,hypothesis,
i15 != i23,
c_0_1831,
[final] ).
cnf(c_0_3059,hypothesis,
i15 != i24,
c_0_1832,
[final] ).
cnf(c_0_3060,hypothesis,
i15 != i25,
c_0_1833,
[final] ).
cnf(c_0_3061,hypothesis,
i15 != i26,
c_0_1834,
[final] ).
cnf(c_0_3062,hypothesis,
i15 != i27,
c_0_1835,
[final] ).
cnf(c_0_3063,hypothesis,
i15 != i28,
c_0_1836,
[final] ).
cnf(c_0_3064,hypothesis,
i15 != i29,
c_0_1837,
[final] ).
cnf(c_0_3065,hypothesis,
i15 != i30,
c_0_1838,
[final] ).
cnf(c_0_3066,hypothesis,
i15 != i31,
c_0_1839,
[final] ).
cnf(c_0_3067,hypothesis,
i15 != i32,
c_0_1840,
[final] ).
cnf(c_0_3068,hypothesis,
i15 != i33,
c_0_1841,
[final] ).
cnf(c_0_3069,hypothesis,
i15 != i34,
c_0_1842,
[final] ).
cnf(c_0_3070,hypothesis,
i15 != i35,
c_0_1843,
[final] ).
cnf(c_0_3071,hypothesis,
i15 != i36,
c_0_1844,
[final] ).
cnf(c_0_3072,hypothesis,
i15 != i37,
c_0_1845,
[final] ).
cnf(c_0_3073,hypothesis,
i15 != i38,
c_0_1846,
[final] ).
cnf(c_0_3074,hypothesis,
i15 != i39,
c_0_1847,
[final] ).
cnf(c_0_3075,hypothesis,
i15 != i40,
c_0_1848,
[final] ).
cnf(c_0_3076,hypothesis,
i15 != i41,
c_0_1849,
[final] ).
cnf(c_0_3077,hypothesis,
i15 != i42,
c_0_1850,
[final] ).
cnf(c_0_3078,hypothesis,
i15 != i43,
c_0_1851,
[final] ).
cnf(c_0_3079,hypothesis,
i15 != i44,
c_0_1852,
[final] ).
cnf(c_0_3080,hypothesis,
i15 != i45,
c_0_1853,
[final] ).
cnf(c_0_3081,hypothesis,
i15 != i46,
c_0_1854,
[final] ).
cnf(c_0_3082,hypothesis,
i15 != i47,
c_0_1855,
[final] ).
cnf(c_0_3083,hypothesis,
i15 != i48,
c_0_1856,
[final] ).
cnf(c_0_3084,hypothesis,
i15 != i50,
c_0_1857,
[final] ).
cnf(c_0_3085,hypothesis,
i15 != i49,
c_0_1858,
[final] ).
cnf(c_0_3086,hypothesis,
i16 != i17,
c_0_1859,
[final] ).
cnf(c_0_3087,hypothesis,
i16 != i18,
c_0_1860,
[final] ).
cnf(c_0_3088,hypothesis,
i16 != i19,
c_0_1861,
[final] ).
cnf(c_0_3089,hypothesis,
i16 != i20,
c_0_1862,
[final] ).
cnf(c_0_3090,hypothesis,
i16 != i21,
c_0_1863,
[final] ).
cnf(c_0_3091,hypothesis,
i16 != i22,
c_0_1864,
[final] ).
cnf(c_0_3092,hypothesis,
i16 != i23,
c_0_1865,
[final] ).
cnf(c_0_3093,hypothesis,
i16 != i24,
c_0_1866,
[final] ).
cnf(c_0_3094,hypothesis,
i16 != i25,
c_0_1867,
[final] ).
cnf(c_0_3095,hypothesis,
i16 != i26,
c_0_1868,
[final] ).
cnf(c_0_3096,hypothesis,
i16 != i27,
c_0_1869,
[final] ).
cnf(c_0_3097,hypothesis,
i16 != i28,
c_0_1870,
[final] ).
cnf(c_0_3098,hypothesis,
i16 != i29,
c_0_1871,
[final] ).
cnf(c_0_3099,hypothesis,
i16 != i30,
c_0_1872,
[final] ).
cnf(c_0_3100,hypothesis,
i16 != i31,
c_0_1873,
[final] ).
cnf(c_0_3101,hypothesis,
i16 != i32,
c_0_1874,
[final] ).
cnf(c_0_3102,hypothesis,
i16 != i33,
c_0_1875,
[final] ).
cnf(c_0_3103,hypothesis,
i16 != i34,
c_0_1876,
[final] ).
cnf(c_0_3104,hypothesis,
i16 != i35,
c_0_1877,
[final] ).
cnf(c_0_3105,hypothesis,
i16 != i36,
c_0_1878,
[final] ).
cnf(c_0_3106,hypothesis,
i16 != i37,
c_0_1879,
[final] ).
cnf(c_0_3107,hypothesis,
i16 != i38,
c_0_1880,
[final] ).
cnf(c_0_3108,hypothesis,
i16 != i39,
c_0_1881,
[final] ).
cnf(c_0_3109,hypothesis,
i16 != i40,
c_0_1882,
[final] ).
cnf(c_0_3110,hypothesis,
i16 != i41,
c_0_1883,
[final] ).
cnf(c_0_3111,hypothesis,
i16 != i42,
c_0_1884,
[final] ).
cnf(c_0_3112,hypothesis,
i16 != i43,
c_0_1885,
[final] ).
cnf(c_0_3113,hypothesis,
i16 != i44,
c_0_1886,
[final] ).
cnf(c_0_3114,hypothesis,
i16 != i45,
c_0_1887,
[final] ).
cnf(c_0_3115,hypothesis,
i16 != i46,
c_0_1888,
[final] ).
cnf(c_0_3116,hypothesis,
i16 != i47,
c_0_1889,
[final] ).
cnf(c_0_3117,hypothesis,
i16 != i48,
c_0_1890,
[final] ).
cnf(c_0_3118,hypothesis,
i16 != i50,
c_0_1891,
[final] ).
cnf(c_0_3119,hypothesis,
i16 != i49,
c_0_1892,
[final] ).
cnf(c_0_3120,hypothesis,
i17 != i18,
c_0_1893,
[final] ).
cnf(c_0_3121,hypothesis,
i17 != i19,
c_0_1894,
[final] ).
cnf(c_0_3122,hypothesis,
i17 != i20,
c_0_1895,
[final] ).
cnf(c_0_3123,hypothesis,
i17 != i21,
c_0_1896,
[final] ).
cnf(c_0_3124,hypothesis,
i17 != i22,
c_0_1897,
[final] ).
cnf(c_0_3125,hypothesis,
i17 != i23,
c_0_1898,
[final] ).
cnf(c_0_3126,hypothesis,
i17 != i24,
c_0_1899,
[final] ).
cnf(c_0_3127,hypothesis,
i17 != i25,
c_0_1900,
[final] ).
cnf(c_0_3128,hypothesis,
i17 != i26,
c_0_1901,
[final] ).
cnf(c_0_3129,hypothesis,
i17 != i27,
c_0_1902,
[final] ).
cnf(c_0_3130,hypothesis,
i17 != i28,
c_0_1903,
[final] ).
cnf(c_0_3131,hypothesis,
i17 != i29,
c_0_1904,
[final] ).
cnf(c_0_3132,hypothesis,
i17 != i30,
c_0_1905,
[final] ).
cnf(c_0_3133,hypothesis,
i17 != i31,
c_0_1906,
[final] ).
cnf(c_0_3134,hypothesis,
i17 != i32,
c_0_1907,
[final] ).
cnf(c_0_3135,hypothesis,
i17 != i33,
c_0_1908,
[final] ).
cnf(c_0_3136,hypothesis,
i17 != i34,
c_0_1909,
[final] ).
cnf(c_0_3137,hypothesis,
i17 != i35,
c_0_1910,
[final] ).
cnf(c_0_3138,hypothesis,
i17 != i36,
c_0_1911,
[final] ).
cnf(c_0_3139,hypothesis,
i17 != i37,
c_0_1912,
[final] ).
cnf(c_0_3140,hypothesis,
i17 != i38,
c_0_1913,
[final] ).
cnf(c_0_3141,hypothesis,
i17 != i39,
c_0_1914,
[final] ).
cnf(c_0_3142,hypothesis,
i17 != i40,
c_0_1915,
[final] ).
cnf(c_0_3143,hypothesis,
i17 != i41,
c_0_1916,
[final] ).
cnf(c_0_3144,hypothesis,
i17 != i42,
c_0_1917,
[final] ).
cnf(c_0_3145,hypothesis,
i17 != i43,
c_0_1918,
[final] ).
cnf(c_0_3146,hypothesis,
i17 != i44,
c_0_1919,
[final] ).
cnf(c_0_3147,hypothesis,
i17 != i45,
c_0_1920,
[final] ).
cnf(c_0_3148,hypothesis,
i17 != i46,
c_0_1921,
[final] ).
cnf(c_0_3149,hypothesis,
i17 != i47,
c_0_1922,
[final] ).
cnf(c_0_3150,hypothesis,
i17 != i48,
c_0_1923,
[final] ).
cnf(c_0_3151,hypothesis,
i17 != i50,
c_0_1924,
[final] ).
cnf(c_0_3152,hypothesis,
i17 != i49,
c_0_1925,
[final] ).
cnf(c_0_3153,hypothesis,
i18 != i19,
c_0_1926,
[final] ).
cnf(c_0_3154,hypothesis,
i18 != i20,
c_0_1927,
[final] ).
cnf(c_0_3155,hypothesis,
i18 != i21,
c_0_1928,
[final] ).
cnf(c_0_3156,hypothesis,
i18 != i22,
c_0_1929,
[final] ).
cnf(c_0_3157,hypothesis,
i18 != i23,
c_0_1930,
[final] ).
cnf(c_0_3158,hypothesis,
i18 != i24,
c_0_1931,
[final] ).
cnf(c_0_3159,hypothesis,
i18 != i25,
c_0_1932,
[final] ).
cnf(c_0_3160,hypothesis,
i18 != i26,
c_0_1933,
[final] ).
cnf(c_0_3161,hypothesis,
i18 != i27,
c_0_1934,
[final] ).
cnf(c_0_3162,hypothesis,
i18 != i28,
c_0_1935,
[final] ).
cnf(c_0_3163,hypothesis,
i18 != i29,
c_0_1936,
[final] ).
cnf(c_0_3164,hypothesis,
i18 != i30,
c_0_1937,
[final] ).
cnf(c_0_3165,hypothesis,
i18 != i31,
c_0_1938,
[final] ).
cnf(c_0_3166,hypothesis,
i18 != i32,
c_0_1939,
[final] ).
cnf(c_0_3167,hypothesis,
i18 != i33,
c_0_1940,
[final] ).
cnf(c_0_3168,hypothesis,
i18 != i34,
c_0_1941,
[final] ).
cnf(c_0_3169,hypothesis,
i18 != i35,
c_0_1942,
[final] ).
cnf(c_0_3170,hypothesis,
i18 != i36,
c_0_1943,
[final] ).
cnf(c_0_3171,hypothesis,
i18 != i37,
c_0_1944,
[final] ).
cnf(c_0_3172,hypothesis,
i18 != i38,
c_0_1945,
[final] ).
cnf(c_0_3173,hypothesis,
i18 != i39,
c_0_1946,
[final] ).
cnf(c_0_3174,hypothesis,
i18 != i40,
c_0_1947,
[final] ).
cnf(c_0_3175,hypothesis,
i18 != i41,
c_0_1948,
[final] ).
cnf(c_0_3176,hypothesis,
i18 != i42,
c_0_1949,
[final] ).
cnf(c_0_3177,hypothesis,
i18 != i43,
c_0_1950,
[final] ).
cnf(c_0_3178,hypothesis,
i18 != i44,
c_0_1951,
[final] ).
cnf(c_0_3179,hypothesis,
i18 != i45,
c_0_1952,
[final] ).
cnf(c_0_3180,hypothesis,
i18 != i46,
c_0_1953,
[final] ).
cnf(c_0_3181,hypothesis,
i18 != i47,
c_0_1954,
[final] ).
cnf(c_0_3182,hypothesis,
i18 != i48,
c_0_1955,
[final] ).
cnf(c_0_3183,hypothesis,
i18 != i50,
c_0_1956,
[final] ).
cnf(c_0_3184,hypothesis,
i18 != i49,
c_0_1957,
[final] ).
cnf(c_0_3185,hypothesis,
i19 != i20,
c_0_1958,
[final] ).
cnf(c_0_3186,hypothesis,
i19 != i21,
c_0_1959,
[final] ).
cnf(c_0_3187,hypothesis,
i19 != i22,
c_0_1960,
[final] ).
cnf(c_0_3188,hypothesis,
i19 != i23,
c_0_1961,
[final] ).
cnf(c_0_3189,hypothesis,
i19 != i24,
c_0_1962,
[final] ).
cnf(c_0_3190,hypothesis,
i19 != i25,
c_0_1963,
[final] ).
cnf(c_0_3191,hypothesis,
i19 != i26,
c_0_1964,
[final] ).
cnf(c_0_3192,hypothesis,
i19 != i27,
c_0_1965,
[final] ).
cnf(c_0_3193,hypothesis,
i19 != i28,
c_0_1966,
[final] ).
cnf(c_0_3194,hypothesis,
i19 != i29,
c_0_1967,
[final] ).
cnf(c_0_3195,hypothesis,
i19 != i30,
c_0_1968,
[final] ).
cnf(c_0_3196,hypothesis,
i19 != i31,
c_0_1969,
[final] ).
cnf(c_0_3197,hypothesis,
i19 != i32,
c_0_1970,
[final] ).
cnf(c_0_3198,hypothesis,
i19 != i33,
c_0_1971,
[final] ).
cnf(c_0_3199,hypothesis,
i19 != i34,
c_0_1972,
[final] ).
cnf(c_0_3200,hypothesis,
i19 != i35,
c_0_1973,
[final] ).
cnf(c_0_3201,hypothesis,
i19 != i36,
c_0_1974,
[final] ).
cnf(c_0_3202,hypothesis,
i19 != i37,
c_0_1975,
[final] ).
cnf(c_0_3203,hypothesis,
i19 != i38,
c_0_1976,
[final] ).
cnf(c_0_3204,hypothesis,
i19 != i39,
c_0_1977,
[final] ).
cnf(c_0_3205,hypothesis,
i19 != i40,
c_0_1978,
[final] ).
cnf(c_0_3206,hypothesis,
i19 != i41,
c_0_1979,
[final] ).
cnf(c_0_3207,hypothesis,
i19 != i42,
c_0_1980,
[final] ).
cnf(c_0_3208,hypothesis,
i19 != i43,
c_0_1981,
[final] ).
cnf(c_0_3209,hypothesis,
i19 != i44,
c_0_1982,
[final] ).
cnf(c_0_3210,hypothesis,
i19 != i45,
c_0_1983,
[final] ).
cnf(c_0_3211,hypothesis,
i19 != i46,
c_0_1984,
[final] ).
cnf(c_0_3212,hypothesis,
i19 != i47,
c_0_1985,
[final] ).
cnf(c_0_3213,hypothesis,
i19 != i48,
c_0_1986,
[final] ).
cnf(c_0_3214,hypothesis,
i19 != i50,
c_0_1987,
[final] ).
cnf(c_0_3215,hypothesis,
i19 != i49,
c_0_1988,
[final] ).
cnf(c_0_3216,hypothesis,
i20 != i21,
c_0_1989,
[final] ).
cnf(c_0_3217,hypothesis,
i20 != i22,
c_0_1990,
[final] ).
cnf(c_0_3218,hypothesis,
i20 != i23,
c_0_1991,
[final] ).
cnf(c_0_3219,hypothesis,
i20 != i24,
c_0_1992,
[final] ).
cnf(c_0_3220,hypothesis,
i20 != i25,
c_0_1993,
[final] ).
cnf(c_0_3221,hypothesis,
i20 != i26,
c_0_1994,
[final] ).
cnf(c_0_3222,hypothesis,
i20 != i27,
c_0_1995,
[final] ).
cnf(c_0_3223,hypothesis,
i20 != i28,
c_0_1996,
[final] ).
cnf(c_0_3224,hypothesis,
i20 != i29,
c_0_1997,
[final] ).
cnf(c_0_3225,hypothesis,
i20 != i30,
c_0_1998,
[final] ).
cnf(c_0_3226,hypothesis,
i20 != i31,
c_0_1999,
[final] ).
cnf(c_0_3227,hypothesis,
i20 != i32,
c_0_2000,
[final] ).
cnf(c_0_3228,hypothesis,
i20 != i33,
c_0_2001,
[final] ).
cnf(c_0_3229,hypothesis,
i20 != i34,
c_0_2002,
[final] ).
cnf(c_0_3230,hypothesis,
i20 != i35,
c_0_2003,
[final] ).
cnf(c_0_3231,hypothesis,
i20 != i36,
c_0_2004,
[final] ).
cnf(c_0_3232,hypothesis,
i20 != i37,
c_0_2005,
[final] ).
cnf(c_0_3233,hypothesis,
i20 != i38,
c_0_2006,
[final] ).
cnf(c_0_3234,hypothesis,
i20 != i39,
c_0_2007,
[final] ).
cnf(c_0_3235,hypothesis,
i20 != i40,
c_0_2008,
[final] ).
cnf(c_0_3236,hypothesis,
i20 != i41,
c_0_2009,
[final] ).
cnf(c_0_3237,hypothesis,
i20 != i42,
c_0_2010,
[final] ).
cnf(c_0_3238,hypothesis,
i20 != i43,
c_0_2011,
[final] ).
cnf(c_0_3239,hypothesis,
i20 != i44,
c_0_2012,
[final] ).
cnf(c_0_3240,hypothesis,
i20 != i45,
c_0_2013,
[final] ).
cnf(c_0_3241,hypothesis,
i20 != i46,
c_0_2014,
[final] ).
cnf(c_0_3242,hypothesis,
i20 != i47,
c_0_2015,
[final] ).
cnf(c_0_3243,hypothesis,
i20 != i48,
c_0_2016,
[final] ).
cnf(c_0_3244,hypothesis,
i20 != i50,
c_0_2017,
[final] ).
cnf(c_0_3245,hypothesis,
i20 != i49,
c_0_2018,
[final] ).
cnf(c_0_3246,hypothesis,
i21 != i22,
c_0_2019,
[final] ).
cnf(c_0_3247,hypothesis,
i21 != i23,
c_0_2020,
[final] ).
cnf(c_0_3248,hypothesis,
i21 != i24,
c_0_2021,
[final] ).
cnf(c_0_3249,hypothesis,
i21 != i25,
c_0_2022,
[final] ).
cnf(c_0_3250,hypothesis,
i21 != i26,
c_0_2023,
[final] ).
cnf(c_0_3251,hypothesis,
i21 != i27,
c_0_2024,
[final] ).
cnf(c_0_3252,hypothesis,
i21 != i28,
c_0_2025,
[final] ).
cnf(c_0_3253,hypothesis,
i21 != i29,
c_0_2026,
[final] ).
cnf(c_0_3254,hypothesis,
i21 != i30,
c_0_2027,
[final] ).
cnf(c_0_3255,hypothesis,
i21 != i31,
c_0_2028,
[final] ).
cnf(c_0_3256,hypothesis,
i21 != i32,
c_0_2029,
[final] ).
cnf(c_0_3257,hypothesis,
i21 != i33,
c_0_2030,
[final] ).
cnf(c_0_3258,hypothesis,
i21 != i34,
c_0_2031,
[final] ).
cnf(c_0_3259,hypothesis,
i21 != i35,
c_0_2032,
[final] ).
cnf(c_0_3260,hypothesis,
i21 != i36,
c_0_2033,
[final] ).
cnf(c_0_3261,hypothesis,
i21 != i37,
c_0_2034,
[final] ).
cnf(c_0_3262,hypothesis,
i21 != i38,
c_0_2035,
[final] ).
cnf(c_0_3263,hypothesis,
i21 != i39,
c_0_2036,
[final] ).
cnf(c_0_3264,hypothesis,
i21 != i40,
c_0_2037,
[final] ).
cnf(c_0_3265,hypothesis,
i21 != i41,
c_0_2038,
[final] ).
cnf(c_0_3266,hypothesis,
i21 != i42,
c_0_2039,
[final] ).
cnf(c_0_3267,hypothesis,
i21 != i43,
c_0_2040,
[final] ).
cnf(c_0_3268,hypothesis,
i21 != i44,
c_0_2041,
[final] ).
cnf(c_0_3269,hypothesis,
i21 != i45,
c_0_2042,
[final] ).
cnf(c_0_3270,hypothesis,
i21 != i46,
c_0_2043,
[final] ).
cnf(c_0_3271,hypothesis,
i21 != i47,
c_0_2044,
[final] ).
cnf(c_0_3272,hypothesis,
i21 != i48,
c_0_2045,
[final] ).
cnf(c_0_3273,hypothesis,
i21 != i50,
c_0_2046,
[final] ).
cnf(c_0_3274,hypothesis,
i21 != i49,
c_0_2047,
[final] ).
cnf(c_0_3275,hypothesis,
i22 != i23,
c_0_2048,
[final] ).
cnf(c_0_3276,hypothesis,
i22 != i24,
c_0_2049,
[final] ).
cnf(c_0_3277,hypothesis,
i22 != i25,
c_0_2050,
[final] ).
cnf(c_0_3278,hypothesis,
i22 != i26,
c_0_2051,
[final] ).
cnf(c_0_3279,hypothesis,
i22 != i27,
c_0_2052,
[final] ).
cnf(c_0_3280,hypothesis,
i22 != i28,
c_0_2053,
[final] ).
cnf(c_0_3281,hypothesis,
i22 != i29,
c_0_2054,
[final] ).
cnf(c_0_3282,hypothesis,
i22 != i30,
c_0_2055,
[final] ).
cnf(c_0_3283,hypothesis,
i22 != i31,
c_0_2056,
[final] ).
cnf(c_0_3284,hypothesis,
i22 != i32,
c_0_2057,
[final] ).
cnf(c_0_3285,hypothesis,
i22 != i33,
c_0_2058,
[final] ).
cnf(c_0_3286,hypothesis,
i22 != i34,
c_0_2059,
[final] ).
cnf(c_0_3287,hypothesis,
i22 != i35,
c_0_2060,
[final] ).
cnf(c_0_3288,hypothesis,
i22 != i36,
c_0_2061,
[final] ).
cnf(c_0_3289,hypothesis,
i22 != i37,
c_0_2062,
[final] ).
cnf(c_0_3290,hypothesis,
i22 != i38,
c_0_2063,
[final] ).
cnf(c_0_3291,hypothesis,
i22 != i39,
c_0_2064,
[final] ).
cnf(c_0_3292,hypothesis,
i22 != i40,
c_0_2065,
[final] ).
cnf(c_0_3293,hypothesis,
i22 != i41,
c_0_2066,
[final] ).
cnf(c_0_3294,hypothesis,
i22 != i42,
c_0_2067,
[final] ).
cnf(c_0_3295,hypothesis,
i22 != i43,
c_0_2068,
[final] ).
cnf(c_0_3296,hypothesis,
i22 != i44,
c_0_2069,
[final] ).
cnf(c_0_3297,hypothesis,
i22 != i45,
c_0_2070,
[final] ).
cnf(c_0_3298,hypothesis,
i22 != i46,
c_0_2071,
[final] ).
cnf(c_0_3299,hypothesis,
i22 != i47,
c_0_2072,
[final] ).
cnf(c_0_3300,hypothesis,
i22 != i48,
c_0_2073,
[final] ).
cnf(c_0_3301,hypothesis,
i22 != i50,
c_0_2074,
[final] ).
cnf(c_0_3302,hypothesis,
i22 != i49,
c_0_2075,
[final] ).
cnf(c_0_3303,hypothesis,
i23 != i24,
c_0_2076,
[final] ).
cnf(c_0_3304,hypothesis,
i23 != i25,
c_0_2077,
[final] ).
cnf(c_0_3305,hypothesis,
i23 != i26,
c_0_2078,
[final] ).
cnf(c_0_3306,hypothesis,
i23 != i27,
c_0_2079,
[final] ).
cnf(c_0_3307,hypothesis,
i23 != i28,
c_0_2080,
[final] ).
cnf(c_0_3308,hypothesis,
i23 != i29,
c_0_2081,
[final] ).
cnf(c_0_3309,hypothesis,
i23 != i30,
c_0_2082,
[final] ).
cnf(c_0_3310,hypothesis,
i23 != i31,
c_0_2083,
[final] ).
cnf(c_0_3311,hypothesis,
i23 != i32,
c_0_2084,
[final] ).
cnf(c_0_3312,hypothesis,
i23 != i33,
c_0_2085,
[final] ).
cnf(c_0_3313,hypothesis,
i23 != i34,
c_0_2086,
[final] ).
cnf(c_0_3314,hypothesis,
i23 != i35,
c_0_2087,
[final] ).
cnf(c_0_3315,hypothesis,
i23 != i36,
c_0_2088,
[final] ).
cnf(c_0_3316,hypothesis,
i23 != i37,
c_0_2089,
[final] ).
cnf(c_0_3317,hypothesis,
i23 != i38,
c_0_2090,
[final] ).
cnf(c_0_3318,hypothesis,
i23 != i39,
c_0_2091,
[final] ).
cnf(c_0_3319,hypothesis,
i23 != i40,
c_0_2092,
[final] ).
cnf(c_0_3320,hypothesis,
i23 != i41,
c_0_2093,
[final] ).
cnf(c_0_3321,hypothesis,
i23 != i42,
c_0_2094,
[final] ).
cnf(c_0_3322,hypothesis,
i23 != i43,
c_0_2095,
[final] ).
cnf(c_0_3323,hypothesis,
i23 != i44,
c_0_2096,
[final] ).
cnf(c_0_3324,hypothesis,
i23 != i45,
c_0_2097,
[final] ).
cnf(c_0_3325,hypothesis,
i23 != i46,
c_0_2098,
[final] ).
cnf(c_0_3326,hypothesis,
i23 != i47,
c_0_2099,
[final] ).
cnf(c_0_3327,hypothesis,
i23 != i48,
c_0_2100,
[final] ).
cnf(c_0_3328,hypothesis,
i23 != i50,
c_0_2101,
[final] ).
cnf(c_0_3329,hypothesis,
i23 != i49,
c_0_2102,
[final] ).
cnf(c_0_3330,hypothesis,
i24 != i25,
c_0_2103,
[final] ).
cnf(c_0_3331,hypothesis,
i24 != i26,
c_0_2104,
[final] ).
cnf(c_0_3332,hypothesis,
i24 != i27,
c_0_2105,
[final] ).
cnf(c_0_3333,hypothesis,
i24 != i28,
c_0_2106,
[final] ).
cnf(c_0_3334,hypothesis,
i24 != i29,
c_0_2107,
[final] ).
cnf(c_0_3335,hypothesis,
i24 != i30,
c_0_2108,
[final] ).
cnf(c_0_3336,hypothesis,
i24 != i31,
c_0_2109,
[final] ).
cnf(c_0_3337,hypothesis,
i24 != i32,
c_0_2110,
[final] ).
cnf(c_0_3338,hypothesis,
i24 != i33,
c_0_2111,
[final] ).
cnf(c_0_3339,hypothesis,
i24 != i34,
c_0_2112,
[final] ).
cnf(c_0_3340,hypothesis,
i24 != i35,
c_0_2113,
[final] ).
cnf(c_0_3341,hypothesis,
i24 != i36,
c_0_2114,
[final] ).
cnf(c_0_3342,hypothesis,
i24 != i37,
c_0_2115,
[final] ).
cnf(c_0_3343,hypothesis,
i24 != i38,
c_0_2116,
[final] ).
cnf(c_0_3344,hypothesis,
i24 != i39,
c_0_2117,
[final] ).
cnf(c_0_3345,hypothesis,
i24 != i40,
c_0_2118,
[final] ).
cnf(c_0_3346,hypothesis,
i24 != i41,
c_0_2119,
[final] ).
cnf(c_0_3347,hypothesis,
i24 != i42,
c_0_2120,
[final] ).
cnf(c_0_3348,hypothesis,
i24 != i43,
c_0_2121,
[final] ).
cnf(c_0_3349,hypothesis,
i24 != i44,
c_0_2122,
[final] ).
cnf(c_0_3350,hypothesis,
i24 != i45,
c_0_2123,
[final] ).
cnf(c_0_3351,hypothesis,
i24 != i46,
c_0_2124,
[final] ).
cnf(c_0_3352,hypothesis,
i24 != i47,
c_0_2125,
[final] ).
cnf(c_0_3353,hypothesis,
i24 != i48,
c_0_2126,
[final] ).
cnf(c_0_3354,hypothesis,
i24 != i50,
c_0_2127,
[final] ).
cnf(c_0_3355,hypothesis,
i24 != i49,
c_0_2128,
[final] ).
cnf(c_0_3356,hypothesis,
i25 != i26,
c_0_2129,
[final] ).
cnf(c_0_3357,hypothesis,
i25 != i27,
c_0_2130,
[final] ).
cnf(c_0_3358,hypothesis,
i25 != i28,
c_0_2131,
[final] ).
cnf(c_0_3359,hypothesis,
i25 != i29,
c_0_2132,
[final] ).
cnf(c_0_3360,hypothesis,
i25 != i30,
c_0_2133,
[final] ).
cnf(c_0_3361,hypothesis,
i25 != i31,
c_0_2134,
[final] ).
cnf(c_0_3362,hypothesis,
i25 != i32,
c_0_2135,
[final] ).
cnf(c_0_3363,hypothesis,
i25 != i33,
c_0_2136,
[final] ).
cnf(c_0_3364,hypothesis,
i25 != i34,
c_0_2137,
[final] ).
cnf(c_0_3365,hypothesis,
i25 != i35,
c_0_2138,
[final] ).
cnf(c_0_3366,hypothesis,
i25 != i36,
c_0_2139,
[final] ).
cnf(c_0_3367,hypothesis,
i25 != i37,
c_0_2140,
[final] ).
cnf(c_0_3368,hypothesis,
i25 != i38,
c_0_2141,
[final] ).
cnf(c_0_3369,hypothesis,
i25 != i39,
c_0_2142,
[final] ).
cnf(c_0_3370,hypothesis,
i25 != i40,
c_0_2143,
[final] ).
cnf(c_0_3371,hypothesis,
i25 != i41,
c_0_2144,
[final] ).
cnf(c_0_3372,hypothesis,
i25 != i42,
c_0_2145,
[final] ).
cnf(c_0_3373,hypothesis,
i25 != i43,
c_0_2146,
[final] ).
cnf(c_0_3374,hypothesis,
i25 != i44,
c_0_2147,
[final] ).
cnf(c_0_3375,hypothesis,
i25 != i45,
c_0_2148,
[final] ).
cnf(c_0_3376,hypothesis,
i25 != i46,
c_0_2149,
[final] ).
cnf(c_0_3377,hypothesis,
i25 != i47,
c_0_2150,
[final] ).
cnf(c_0_3378,hypothesis,
i25 != i48,
c_0_2151,
[final] ).
cnf(c_0_3379,hypothesis,
i25 != i50,
c_0_2152,
[final] ).
cnf(c_0_3380,hypothesis,
i25 != i49,
c_0_2153,
[final] ).
cnf(c_0_3381,hypothesis,
i26 != i27,
c_0_2154,
[final] ).
cnf(c_0_3382,hypothesis,
i26 != i28,
c_0_2155,
[final] ).
cnf(c_0_3383,hypothesis,
i26 != i29,
c_0_2156,
[final] ).
cnf(c_0_3384,hypothesis,
i26 != i30,
c_0_2157,
[final] ).
cnf(c_0_3385,hypothesis,
i26 != i31,
c_0_2158,
[final] ).
cnf(c_0_3386,hypothesis,
i26 != i32,
c_0_2159,
[final] ).
cnf(c_0_3387,hypothesis,
i26 != i33,
c_0_2160,
[final] ).
cnf(c_0_3388,hypothesis,
i26 != i34,
c_0_2161,
[final] ).
cnf(c_0_3389,hypothesis,
i26 != i35,
c_0_2162,
[final] ).
cnf(c_0_3390,hypothesis,
i26 != i36,
c_0_2163,
[final] ).
cnf(c_0_3391,hypothesis,
i26 != i37,
c_0_2164,
[final] ).
cnf(c_0_3392,hypothesis,
i26 != i38,
c_0_2165,
[final] ).
cnf(c_0_3393,hypothesis,
i26 != i39,
c_0_2166,
[final] ).
cnf(c_0_3394,hypothesis,
i26 != i40,
c_0_2167,
[final] ).
cnf(c_0_3395,hypothesis,
i26 != i41,
c_0_2168,
[final] ).
cnf(c_0_3396,hypothesis,
i26 != i42,
c_0_2169,
[final] ).
cnf(c_0_3397,hypothesis,
i26 != i43,
c_0_2170,
[final] ).
cnf(c_0_3398,hypothesis,
i26 != i44,
c_0_2171,
[final] ).
cnf(c_0_3399,hypothesis,
i26 != i45,
c_0_2172,
[final] ).
cnf(c_0_3400,hypothesis,
i26 != i46,
c_0_2173,
[final] ).
cnf(c_0_3401,hypothesis,
i26 != i47,
c_0_2174,
[final] ).
cnf(c_0_3402,hypothesis,
i26 != i48,
c_0_2175,
[final] ).
cnf(c_0_3403,hypothesis,
i26 != i50,
c_0_2176,
[final] ).
cnf(c_0_3404,hypothesis,
i26 != i49,
c_0_2177,
[final] ).
cnf(c_0_3405,hypothesis,
i27 != i28,
c_0_2178,
[final] ).
cnf(c_0_3406,hypothesis,
i27 != i29,
c_0_2179,
[final] ).
cnf(c_0_3407,hypothesis,
i27 != i30,
c_0_2180,
[final] ).
cnf(c_0_3408,hypothesis,
i27 != i31,
c_0_2181,
[final] ).
cnf(c_0_3409,hypothesis,
i27 != i32,
c_0_2182,
[final] ).
cnf(c_0_3410,hypothesis,
i27 != i33,
c_0_2183,
[final] ).
cnf(c_0_3411,hypothesis,
i27 != i34,
c_0_2184,
[final] ).
cnf(c_0_3412,hypothesis,
i27 != i35,
c_0_2185,
[final] ).
cnf(c_0_3413,hypothesis,
i27 != i36,
c_0_2186,
[final] ).
cnf(c_0_3414,hypothesis,
i27 != i37,
c_0_2187,
[final] ).
cnf(c_0_3415,hypothesis,
i27 != i38,
c_0_2188,
[final] ).
cnf(c_0_3416,hypothesis,
i27 != i39,
c_0_2189,
[final] ).
cnf(c_0_3417,hypothesis,
i27 != i40,
c_0_2190,
[final] ).
cnf(c_0_3418,hypothesis,
i27 != i41,
c_0_2191,
[final] ).
cnf(c_0_3419,hypothesis,
i27 != i42,
c_0_2192,
[final] ).
cnf(c_0_3420,hypothesis,
i27 != i43,
c_0_2193,
[final] ).
cnf(c_0_3421,hypothesis,
i27 != i44,
c_0_2194,
[final] ).
cnf(c_0_3422,hypothesis,
i27 != i45,
c_0_2195,
[final] ).
cnf(c_0_3423,hypothesis,
i27 != i46,
c_0_2196,
[final] ).
cnf(c_0_3424,hypothesis,
i27 != i47,
c_0_2197,
[final] ).
cnf(c_0_3425,hypothesis,
i27 != i48,
c_0_2198,
[final] ).
cnf(c_0_3426,hypothesis,
i27 != i50,
c_0_2199,
[final] ).
cnf(c_0_3427,hypothesis,
i27 != i49,
c_0_2200,
[final] ).
cnf(c_0_3428,hypothesis,
i28 != i29,
c_0_2201,
[final] ).
cnf(c_0_3429,hypothesis,
i28 != i30,
c_0_2202,
[final] ).
cnf(c_0_3430,hypothesis,
i28 != i31,
c_0_2203,
[final] ).
cnf(c_0_3431,hypothesis,
i28 != i32,
c_0_2204,
[final] ).
cnf(c_0_3432,hypothesis,
i28 != i33,
c_0_2205,
[final] ).
cnf(c_0_3433,hypothesis,
i28 != i34,
c_0_2206,
[final] ).
cnf(c_0_3434,hypothesis,
i28 != i35,
c_0_2207,
[final] ).
cnf(c_0_3435,hypothesis,
i28 != i36,
c_0_2208,
[final] ).
cnf(c_0_3436,hypothesis,
i28 != i37,
c_0_2209,
[final] ).
cnf(c_0_3437,hypothesis,
i28 != i38,
c_0_2210,
[final] ).
cnf(c_0_3438,hypothesis,
i28 != i39,
c_0_2211,
[final] ).
cnf(c_0_3439,hypothesis,
i28 != i40,
c_0_2212,
[final] ).
cnf(c_0_3440,hypothesis,
i28 != i41,
c_0_2213,
[final] ).
cnf(c_0_3441,hypothesis,
i28 != i42,
c_0_2214,
[final] ).
cnf(c_0_3442,hypothesis,
i28 != i43,
c_0_2215,
[final] ).
cnf(c_0_3443,hypothesis,
i28 != i44,
c_0_2216,
[final] ).
cnf(c_0_3444,hypothesis,
i28 != i45,
c_0_2217,
[final] ).
cnf(c_0_3445,hypothesis,
i28 != i46,
c_0_2218,
[final] ).
cnf(c_0_3446,hypothesis,
i28 != i47,
c_0_2219,
[final] ).
cnf(c_0_3447,hypothesis,
i28 != i48,
c_0_2220,
[final] ).
cnf(c_0_3448,hypothesis,
i28 != i50,
c_0_2221,
[final] ).
cnf(c_0_3449,hypothesis,
i28 != i49,
c_0_2222,
[final] ).
cnf(c_0_3450,hypothesis,
i29 != i30,
c_0_2223,
[final] ).
cnf(c_0_3451,hypothesis,
i29 != i31,
c_0_2224,
[final] ).
cnf(c_0_3452,hypothesis,
i29 != i32,
c_0_2225,
[final] ).
cnf(c_0_3453,hypothesis,
i29 != i33,
c_0_2226,
[final] ).
cnf(c_0_3454,hypothesis,
i29 != i34,
c_0_2227,
[final] ).
cnf(c_0_3455,hypothesis,
i29 != i35,
c_0_2228,
[final] ).
cnf(c_0_3456,hypothesis,
i29 != i36,
c_0_2229,
[final] ).
cnf(c_0_3457,hypothesis,
i29 != i37,
c_0_2230,
[final] ).
cnf(c_0_3458,hypothesis,
i29 != i38,
c_0_2231,
[final] ).
cnf(c_0_3459,hypothesis,
i29 != i39,
c_0_2232,
[final] ).
cnf(c_0_3460,hypothesis,
i29 != i40,
c_0_2233,
[final] ).
cnf(c_0_3461,hypothesis,
i29 != i41,
c_0_2234,
[final] ).
cnf(c_0_3462,hypothesis,
i29 != i42,
c_0_2235,
[final] ).
cnf(c_0_3463,hypothesis,
i29 != i43,
c_0_2236,
[final] ).
cnf(c_0_3464,hypothesis,
i29 != i44,
c_0_2237,
[final] ).
cnf(c_0_3465,hypothesis,
i29 != i45,
c_0_2238,
[final] ).
cnf(c_0_3466,hypothesis,
i29 != i46,
c_0_2239,
[final] ).
cnf(c_0_3467,hypothesis,
i29 != i47,
c_0_2240,
[final] ).
cnf(c_0_3468,hypothesis,
i29 != i48,
c_0_2241,
[final] ).
cnf(c_0_3469,hypothesis,
i29 != i50,
c_0_2242,
[final] ).
cnf(c_0_3470,hypothesis,
i29 != i49,
c_0_2243,
[final] ).
cnf(c_0_3471,hypothesis,
i30 != i31,
c_0_2244,
[final] ).
cnf(c_0_3472,hypothesis,
i30 != i32,
c_0_2245,
[final] ).
cnf(c_0_3473,hypothesis,
i30 != i33,
c_0_2246,
[final] ).
cnf(c_0_3474,hypothesis,
i30 != i34,
c_0_2247,
[final] ).
cnf(c_0_3475,hypothesis,
i30 != i35,
c_0_2248,
[final] ).
cnf(c_0_3476,hypothesis,
i30 != i36,
c_0_2249,
[final] ).
cnf(c_0_3477,hypothesis,
i30 != i37,
c_0_2250,
[final] ).
cnf(c_0_3478,hypothesis,
i30 != i38,
c_0_2251,
[final] ).
cnf(c_0_3479,hypothesis,
i30 != i39,
c_0_2252,
[final] ).
cnf(c_0_3480,hypothesis,
i30 != i40,
c_0_2253,
[final] ).
cnf(c_0_3481,hypothesis,
i30 != i41,
c_0_2254,
[final] ).
cnf(c_0_3482,hypothesis,
i30 != i42,
c_0_2255,
[final] ).
cnf(c_0_3483,hypothesis,
i30 != i43,
c_0_2256,
[final] ).
cnf(c_0_3484,hypothesis,
i30 != i44,
c_0_2257,
[final] ).
cnf(c_0_3485,hypothesis,
i30 != i45,
c_0_2258,
[final] ).
cnf(c_0_3486,hypothesis,
i30 != i46,
c_0_2259,
[final] ).
cnf(c_0_3487,hypothesis,
i30 != i47,
c_0_2260,
[final] ).
cnf(c_0_3488,hypothesis,
i30 != i48,
c_0_2261,
[final] ).
cnf(c_0_3489,hypothesis,
i30 != i50,
c_0_2262,
[final] ).
cnf(c_0_3490,hypothesis,
i30 != i49,
c_0_2263,
[final] ).
cnf(c_0_3491,hypothesis,
i31 != i32,
c_0_2264,
[final] ).
cnf(c_0_3492,hypothesis,
i31 != i33,
c_0_2265,
[final] ).
cnf(c_0_3493,hypothesis,
i31 != i34,
c_0_2266,
[final] ).
cnf(c_0_3494,hypothesis,
i31 != i35,
c_0_2267,
[final] ).
cnf(c_0_3495,hypothesis,
i31 != i36,
c_0_2268,
[final] ).
cnf(c_0_3496,hypothesis,
i31 != i37,
c_0_2269,
[final] ).
cnf(c_0_3497,hypothesis,
i31 != i38,
c_0_2270,
[final] ).
cnf(c_0_3498,hypothesis,
i31 != i39,
c_0_2271,
[final] ).
cnf(c_0_3499,hypothesis,
i31 != i40,
c_0_2272,
[final] ).
cnf(c_0_3500,hypothesis,
i31 != i41,
c_0_2273,
[final] ).
cnf(c_0_3501,hypothesis,
i31 != i42,
c_0_2274,
[final] ).
cnf(c_0_3502,hypothesis,
i31 != i43,
c_0_2275,
[final] ).
cnf(c_0_3503,hypothesis,
i31 != i44,
c_0_2276,
[final] ).
cnf(c_0_3504,hypothesis,
i31 != i45,
c_0_2277,
[final] ).
cnf(c_0_3505,hypothesis,
i31 != i46,
c_0_2278,
[final] ).
cnf(c_0_3506,hypothesis,
i31 != i47,
c_0_2279,
[final] ).
cnf(c_0_3507,hypothesis,
i31 != i48,
c_0_2280,
[final] ).
cnf(c_0_3508,hypothesis,
i31 != i50,
c_0_2281,
[final] ).
cnf(c_0_3509,hypothesis,
i31 != i49,
c_0_2282,
[final] ).
cnf(c_0_3510,hypothesis,
i32 != i33,
c_0_2283,
[final] ).
cnf(c_0_3511,hypothesis,
i32 != i34,
c_0_2284,
[final] ).
cnf(c_0_3512,hypothesis,
i32 != i35,
c_0_2285,
[final] ).
cnf(c_0_3513,hypothesis,
i32 != i36,
c_0_2286,
[final] ).
cnf(c_0_3514,hypothesis,
i32 != i37,
c_0_2287,
[final] ).
cnf(c_0_3515,hypothesis,
i32 != i38,
c_0_2288,
[final] ).
cnf(c_0_3516,hypothesis,
i32 != i39,
c_0_2289,
[final] ).
cnf(c_0_3517,hypothesis,
i32 != i40,
c_0_2290,
[final] ).
cnf(c_0_3518,hypothesis,
i32 != i41,
c_0_2291,
[final] ).
cnf(c_0_3519,hypothesis,
i32 != i42,
c_0_2292,
[final] ).
cnf(c_0_3520,hypothesis,
i32 != i43,
c_0_2293,
[final] ).
cnf(c_0_3521,hypothesis,
i32 != i44,
c_0_2294,
[final] ).
cnf(c_0_3522,hypothesis,
i32 != i45,
c_0_2295,
[final] ).
cnf(c_0_3523,hypothesis,
i32 != i46,
c_0_2296,
[final] ).
cnf(c_0_3524,hypothesis,
i32 != i47,
c_0_2297,
[final] ).
cnf(c_0_3525,hypothesis,
i32 != i48,
c_0_2298,
[final] ).
cnf(c_0_3526,hypothesis,
i32 != i50,
c_0_2299,
[final] ).
cnf(c_0_3527,hypothesis,
i32 != i49,
c_0_2300,
[final] ).
cnf(c_0_3528,hypothesis,
i33 != i34,
c_0_2301,
[final] ).
cnf(c_0_3529,hypothesis,
i33 != i35,
c_0_2302,
[final] ).
cnf(c_0_3530,hypothesis,
i33 != i36,
c_0_2303,
[final] ).
cnf(c_0_3531,hypothesis,
i33 != i37,
c_0_2304,
[final] ).
cnf(c_0_3532,hypothesis,
i33 != i38,
c_0_2305,
[final] ).
cnf(c_0_3533,hypothesis,
i33 != i39,
c_0_2306,
[final] ).
cnf(c_0_3534,hypothesis,
i33 != i40,
c_0_2307,
[final] ).
cnf(c_0_3535,hypothesis,
i33 != i41,
c_0_2308,
[final] ).
cnf(c_0_3536,hypothesis,
i33 != i42,
c_0_2309,
[final] ).
cnf(c_0_3537,hypothesis,
i33 != i43,
c_0_2310,
[final] ).
cnf(c_0_3538,hypothesis,
i33 != i44,
c_0_2311,
[final] ).
cnf(c_0_3539,hypothesis,
i33 != i45,
c_0_2312,
[final] ).
cnf(c_0_3540,hypothesis,
i33 != i46,
c_0_2313,
[final] ).
cnf(c_0_3541,hypothesis,
i33 != i47,
c_0_2314,
[final] ).
cnf(c_0_3542,hypothesis,
i33 != i48,
c_0_2315,
[final] ).
cnf(c_0_3543,hypothesis,
i33 != i50,
c_0_2316,
[final] ).
cnf(c_0_3544,hypothesis,
i33 != i49,
c_0_2317,
[final] ).
cnf(c_0_3545,hypothesis,
i34 != i35,
c_0_2318,
[final] ).
cnf(c_0_3546,hypothesis,
i34 != i36,
c_0_2319,
[final] ).
cnf(c_0_3547,hypothesis,
i34 != i37,
c_0_2320,
[final] ).
cnf(c_0_3548,hypothesis,
i34 != i38,
c_0_2321,
[final] ).
cnf(c_0_3549,hypothesis,
i34 != i39,
c_0_2322,
[final] ).
cnf(c_0_3550,hypothesis,
i34 != i40,
c_0_2323,
[final] ).
cnf(c_0_3551,hypothesis,
i34 != i41,
c_0_2324,
[final] ).
cnf(c_0_3552,hypothesis,
i34 != i42,
c_0_2325,
[final] ).
cnf(c_0_3553,hypothesis,
i34 != i43,
c_0_2326,
[final] ).
cnf(c_0_3554,hypothesis,
i34 != i44,
c_0_2327,
[final] ).
cnf(c_0_3555,hypothesis,
i34 != i45,
c_0_2328,
[final] ).
cnf(c_0_3556,hypothesis,
i34 != i46,
c_0_2329,
[final] ).
cnf(c_0_3557,hypothesis,
i34 != i47,
c_0_2330,
[final] ).
cnf(c_0_3558,hypothesis,
i34 != i48,
c_0_2331,
[final] ).
cnf(c_0_3559,hypothesis,
i34 != i50,
c_0_2332,
[final] ).
cnf(c_0_3560,hypothesis,
i34 != i49,
c_0_2333,
[final] ).
cnf(c_0_3561,hypothesis,
i35 != i36,
c_0_2334,
[final] ).
cnf(c_0_3562,hypothesis,
i35 != i37,
c_0_2335,
[final] ).
cnf(c_0_3563,hypothesis,
i35 != i38,
c_0_2336,
[final] ).
cnf(c_0_3564,hypothesis,
i35 != i39,
c_0_2337,
[final] ).
cnf(c_0_3565,hypothesis,
i35 != i40,
c_0_2338,
[final] ).
cnf(c_0_3566,hypothesis,
i35 != i41,
c_0_2339,
[final] ).
cnf(c_0_3567,hypothesis,
i35 != i42,
c_0_2340,
[final] ).
cnf(c_0_3568,hypothesis,
i35 != i43,
c_0_2341,
[final] ).
cnf(c_0_3569,hypothesis,
i35 != i44,
c_0_2342,
[final] ).
cnf(c_0_3570,hypothesis,
i35 != i45,
c_0_2343,
[final] ).
cnf(c_0_3571,hypothesis,
i35 != i46,
c_0_2344,
[final] ).
cnf(c_0_3572,hypothesis,
i35 != i47,
c_0_2345,
[final] ).
cnf(c_0_3573,hypothesis,
i35 != i48,
c_0_2346,
[final] ).
cnf(c_0_3574,hypothesis,
i35 != i50,
c_0_2347,
[final] ).
cnf(c_0_3575,hypothesis,
i35 != i49,
c_0_2348,
[final] ).
cnf(c_0_3576,hypothesis,
i36 != i37,
c_0_2349,
[final] ).
cnf(c_0_3577,hypothesis,
i36 != i38,
c_0_2350,
[final] ).
cnf(c_0_3578,hypothesis,
i36 != i39,
c_0_2351,
[final] ).
cnf(c_0_3579,hypothesis,
i36 != i40,
c_0_2352,
[final] ).
cnf(c_0_3580,hypothesis,
i36 != i41,
c_0_2353,
[final] ).
cnf(c_0_3581,hypothesis,
i36 != i42,
c_0_2354,
[final] ).
cnf(c_0_3582,hypothesis,
i36 != i43,
c_0_2355,
[final] ).
cnf(c_0_3583,hypothesis,
i36 != i44,
c_0_2356,
[final] ).
cnf(c_0_3584,hypothesis,
i36 != i45,
c_0_2357,
[final] ).
cnf(c_0_3585,hypothesis,
i36 != i46,
c_0_2358,
[final] ).
cnf(c_0_3586,hypothesis,
i36 != i47,
c_0_2359,
[final] ).
cnf(c_0_3587,hypothesis,
i36 != i48,
c_0_2360,
[final] ).
cnf(c_0_3588,hypothesis,
i36 != i50,
c_0_2361,
[final] ).
cnf(c_0_3589,hypothesis,
i36 != i49,
c_0_2362,
[final] ).
cnf(c_0_3590,hypothesis,
i37 != i38,
c_0_2363,
[final] ).
cnf(c_0_3591,hypothesis,
i37 != i39,
c_0_2364,
[final] ).
cnf(c_0_3592,hypothesis,
i37 != i40,
c_0_2365,
[final] ).
cnf(c_0_3593,hypothesis,
i37 != i41,
c_0_2366,
[final] ).
cnf(c_0_3594,hypothesis,
i37 != i42,
c_0_2367,
[final] ).
cnf(c_0_3595,hypothesis,
i37 != i43,
c_0_2368,
[final] ).
cnf(c_0_3596,hypothesis,
i37 != i44,
c_0_2369,
[final] ).
cnf(c_0_3597,hypothesis,
i37 != i45,
c_0_2370,
[final] ).
cnf(c_0_3598,hypothesis,
i37 != i46,
c_0_2371,
[final] ).
cnf(c_0_3599,hypothesis,
i37 != i47,
c_0_2372,
[final] ).
cnf(c_0_3600,hypothesis,
i37 != i48,
c_0_2373,
[final] ).
cnf(c_0_3601,hypothesis,
i37 != i50,
c_0_2374,
[final] ).
cnf(c_0_3602,hypothesis,
i37 != i49,
c_0_2375,
[final] ).
cnf(c_0_3603,hypothesis,
i38 != i39,
c_0_2376,
[final] ).
cnf(c_0_3604,hypothesis,
i38 != i40,
c_0_2377,
[final] ).
cnf(c_0_3605,hypothesis,
i38 != i41,
c_0_2378,
[final] ).
cnf(c_0_3606,hypothesis,
i38 != i42,
c_0_2379,
[final] ).
cnf(c_0_3607,hypothesis,
i38 != i43,
c_0_2380,
[final] ).
cnf(c_0_3608,hypothesis,
i38 != i44,
c_0_2381,
[final] ).
cnf(c_0_3609,hypothesis,
i38 != i45,
c_0_2382,
[final] ).
cnf(c_0_3610,hypothesis,
i38 != i46,
c_0_2383,
[final] ).
cnf(c_0_3611,hypothesis,
i38 != i47,
c_0_2384,
[final] ).
cnf(c_0_3612,hypothesis,
i38 != i48,
c_0_2385,
[final] ).
cnf(c_0_3613,hypothesis,
i38 != i50,
c_0_2386,
[final] ).
cnf(c_0_3614,hypothesis,
i38 != i49,
c_0_2387,
[final] ).
cnf(c_0_3615,hypothesis,
i39 != i40,
c_0_2388,
[final] ).
cnf(c_0_3616,hypothesis,
i39 != i41,
c_0_2389,
[final] ).
cnf(c_0_3617,hypothesis,
i39 != i42,
c_0_2390,
[final] ).
cnf(c_0_3618,hypothesis,
i39 != i43,
c_0_2391,
[final] ).
cnf(c_0_3619,hypothesis,
i39 != i44,
c_0_2392,
[final] ).
cnf(c_0_3620,hypothesis,
i39 != i45,
c_0_2393,
[final] ).
cnf(c_0_3621,hypothesis,
i39 != i46,
c_0_2394,
[final] ).
cnf(c_0_3622,hypothesis,
i39 != i47,
c_0_2395,
[final] ).
cnf(c_0_3623,hypothesis,
i39 != i48,
c_0_2396,
[final] ).
cnf(c_0_3624,hypothesis,
i39 != i50,
c_0_2397,
[final] ).
cnf(c_0_3625,hypothesis,
i39 != i49,
c_0_2398,
[final] ).
cnf(c_0_3626,hypothesis,
i40 != i41,
c_0_2399,
[final] ).
cnf(c_0_3627,hypothesis,
i40 != i42,
c_0_2400,
[final] ).
cnf(c_0_3628,hypothesis,
i40 != i43,
c_0_2401,
[final] ).
cnf(c_0_3629,hypothesis,
i40 != i44,
c_0_2402,
[final] ).
cnf(c_0_3630,hypothesis,
i40 != i45,
c_0_2403,
[final] ).
cnf(c_0_3631,hypothesis,
i40 != i46,
c_0_2404,
[final] ).
cnf(c_0_3632,hypothesis,
i40 != i47,
c_0_2405,
[final] ).
cnf(c_0_3633,hypothesis,
i40 != i48,
c_0_2406,
[final] ).
cnf(c_0_3634,hypothesis,
i40 != i50,
c_0_2407,
[final] ).
cnf(c_0_3635,hypothesis,
i40 != i49,
c_0_2408,
[final] ).
cnf(c_0_3636,hypothesis,
i41 != i42,
c_0_2409,
[final] ).
cnf(c_0_3637,hypothesis,
i41 != i43,
c_0_2410,
[final] ).
cnf(c_0_3638,hypothesis,
i41 != i44,
c_0_2411,
[final] ).
cnf(c_0_3639,hypothesis,
i41 != i45,
c_0_2412,
[final] ).
cnf(c_0_3640,hypothesis,
i41 != i46,
c_0_2413,
[final] ).
cnf(c_0_3641,hypothesis,
i41 != i47,
c_0_2414,
[final] ).
cnf(c_0_3642,hypothesis,
i41 != i48,
c_0_2415,
[final] ).
cnf(c_0_3643,hypothesis,
i41 != i50,
c_0_2416,
[final] ).
cnf(c_0_3644,hypothesis,
i41 != i49,
c_0_2417,
[final] ).
cnf(c_0_3645,hypothesis,
i42 != i43,
c_0_2418,
[final] ).
cnf(c_0_3646,hypothesis,
i42 != i44,
c_0_2419,
[final] ).
cnf(c_0_3647,hypothesis,
i42 != i45,
c_0_2420,
[final] ).
cnf(c_0_3648,hypothesis,
i42 != i46,
c_0_2421,
[final] ).
cnf(c_0_3649,hypothesis,
i42 != i47,
c_0_2422,
[final] ).
cnf(c_0_3650,hypothesis,
i42 != i48,
c_0_2423,
[final] ).
cnf(c_0_3651,hypothesis,
i42 != i50,
c_0_2424,
[final] ).
cnf(c_0_3652,hypothesis,
i42 != i49,
c_0_2425,
[final] ).
cnf(c_0_3653,hypothesis,
i43 != i44,
c_0_2426,
[final] ).
cnf(c_0_3654,hypothesis,
i43 != i45,
c_0_2427,
[final] ).
cnf(c_0_3655,hypothesis,
i43 != i46,
c_0_2428,
[final] ).
cnf(c_0_3656,hypothesis,
i43 != i47,
c_0_2429,
[final] ).
cnf(c_0_3657,hypothesis,
i43 != i48,
c_0_2430,
[final] ).
cnf(c_0_3658,hypothesis,
i43 != i50,
c_0_2431,
[final] ).
cnf(c_0_3659,hypothesis,
i43 != i49,
c_0_2432,
[final] ).
cnf(c_0_3660,hypothesis,
i44 != i45,
c_0_2433,
[final] ).
cnf(c_0_3661,hypothesis,
i44 != i46,
c_0_2434,
[final] ).
cnf(c_0_3662,hypothesis,
i44 != i47,
c_0_2435,
[final] ).
cnf(c_0_3663,hypothesis,
i44 != i48,
c_0_2436,
[final] ).
cnf(c_0_3664,hypothesis,
i44 != i50,
c_0_2437,
[final] ).
cnf(c_0_3665,hypothesis,
i44 != i49,
c_0_2438,
[final] ).
cnf(c_0_3666,hypothesis,
i45 != i46,
c_0_2439,
[final] ).
cnf(c_0_3667,hypothesis,
i45 != i47,
c_0_2440,
[final] ).
cnf(c_0_3668,hypothesis,
i45 != i48,
c_0_2441,
[final] ).
cnf(c_0_3669,hypothesis,
i45 != i50,
c_0_2442,
[final] ).
cnf(c_0_3670,hypothesis,
i45 != i49,
c_0_2443,
[final] ).
cnf(c_0_3671,hypothesis,
i46 != i47,
c_0_2444,
[final] ).
cnf(c_0_3672,hypothesis,
i46 != i48,
c_0_2445,
[final] ).
cnf(c_0_3673,hypothesis,
i46 != i50,
c_0_2446,
[final] ).
cnf(c_0_3674,hypothesis,
i46 != i49,
c_0_2447,
[final] ).
cnf(c_0_3675,hypothesis,
i47 != i48,
c_0_2448,
[final] ).
cnf(c_0_3676,hypothesis,
i47 != i50,
c_0_2449,
[final] ).
cnf(c_0_3677,hypothesis,
i47 != i49,
c_0_2450,
[final] ).
cnf(c_0_3678,hypothesis,
i48 != i50,
c_0_2451,
[final] ).
cnf(c_0_3679,hypothesis,
i48 != i49,
c_0_2452,
[final] ).
cnf(c_0_3680,hypothesis,
i49 != i50,
c_0_2453,
[final] ).
cnf(c_0_3681,axiom,
select(store(X1,X2,X3),X2) = X3,
a1,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV494-1.050 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.09 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.48 % Computer : n006.cluster.edu
% 0.22/0.48 % Model : x86_64 x86_64
% 0.22/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.48 % Memory : 8046.5625MB
% 0.22/0.48 % OS : Linux 6.8.0-71-generic
% 0.22/0.48 % CPULimit : 300
% 0.22/0.48 % WCLimit : 300
% 0.22/0.48 % DateTime : Mon Sep 21 08:53:57 UTC 2026
% 0.22/0.49 % CPUTime :
% 0.22/0.49 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.27/0.59 Running first-order theorem proving
% 0.27/0.59 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/0.76 % Version: 3.5.1
% 0.33/0.76 % Preprocessing class: FMLMSMSMSSSNFFN.
% 0.33/0.76 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.33/0.76 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.33/0.76 % Starting new_bool_3 with 300s (1) cores
% 0.33/0.76 % Starting new_bool_1 with 300s (1) cores
% 0.33/0.76 % Starting sh5l with 300s (1) cores
% 0.33/0.76 % new_bool_1 with pid 2478855 completed with status 1
% 0.33/0.76 % Result found by new_bool_1
% 0.33/0.76 % Preprocessing class: FMLMSMSMSSSNFFN.
% 0.33/0.76 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.33/0.76 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.33/0.76 % Starting new_bool_3 with 300s (1) cores
% 0.33/0.76 % Starting new_bool_1 with 300s (1) cores
% 0.33/0.76 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.33/0.76 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.33/0.76 % Search class: FGUPF-SSLF32-DFFFFFNN
% 0.33/0.76 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.33/0.76 % Starting SubtermCWHack with 31s (1) cores
% 0.33/0.76 % SubtermCWHack with pid 2478863 completed with status 1
% 0.33/0.76 % Result found by SubtermCWHack
% 0.33/0.76 % Preprocessing class: FMLMSMSMSSSNFFN.
% 0.33/0.76 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.33/0.76 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.33/0.76 % Starting new_bool_3 with 300s (1) cores
% 0.33/0.76 % Starting new_bool_1 with 300s (1) cores
% 0.33/0.76 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.33/0.76 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.33/0.76 % Search class: FGUPF-SSLF32-DFFFFFNN
% 0.33/0.76 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.33/0.76 % Starting SubtermCWHack with 31s (1) cores
% 0.33/0.76 % Preprocessing time : 0.010 s
% 0.33/0.76
% 0.33/0.76 % No proof found!
% 0.33/0.76 % SZS status Satisfiable
% 0.33/0.76 % SZS output start Saturation
% See solution above
% 0.33/0.77 % Parsed axioms : 1228
% 0.33/0.77 % Removed by relevancy pruning/SinE : 0
% 0.33/0.77 % Initial clauses : 1228
% 0.33/0.77 % Removed in clause preprocessing : 0
% 0.33/0.77 % Initial clauses in saturation : 1228
% 0.33/0.77 % Processed clauses : 1228
% 0.33/0.77 % ...of these trivial : 0
% 0.33/0.77 % ...subsumed : 0
% 0.33/0.77 % ...remaining for further processing : 1228
% 0.33/0.77 % Other redundant clauses eliminated : 0
% 0.33/0.77 % Clauses deleted for lack of memory : 0
% 0.33/0.77 % Backward-subsumed : 0
% 0.33/0.77 % Backward-rewritten : 0
% 0.33/0.77 % Generated clauses : 0
% 0.33/0.77 % ...of the previous two non-redundant : 0
% 0.33/0.77 % ...aggressively subsumed : 0
% 0.33/0.77 % Contextual simplify-reflections : 0
% 0.33/0.77 % Paramodulations : 0
% 0.33/0.77 % Factorizations : 0
% 0.33/0.77 % NegExts : 0
% 0.33/0.77 % Equation resolutions : 0
% 0.33/0.77 % Disequality decompositions : 0
% 0.33/0.77 % Total rewrite steps : 0
% 0.33/0.77 % ...of those cached : 0
% 0.33/0.77 % Propositional unsat checks : 0
% 0.33/0.77 % Propositional check models : 0
% 0.33/0.77 % Propositional check unsatisfiable : 0
% 0.33/0.77 % Propositional clauses : 0
% 0.33/0.77 % Propositional clauses after purity: 0
% 0.33/0.77 % Propositional unsat core size : 0
% 0.33/0.77 % Propositional preprocessing time : 0.000
% 0.33/0.77 % Propositional encoding time : 0.000
% 0.33/0.77 % Propositional solver time : 0.000
% 0.33/0.77 % Success case prop preproc time : 0.000
% 0.33/0.77 % Success case prop encoding time : 0.000
% 0.33/0.77 % Success case prop solver time : 0.000
% 0.33/0.77 % Current number of processed clauses : 1228
% 0.33/0.77 % Positive orientable unit clauses : 1
% 0.33/0.77 % Positive unorientable unit clauses: 0
% 0.33/0.77 % Negative unit clauses : 1226
% 0.33/0.77 % Non-unit-clauses : 1
% 0.33/0.77 % Current number of unprocessed clauses: 0
% 0.33/0.77 % ...number of literals in the above : 0
% 0.33/0.77 % Current number of archived formulas : 0
% 0.33/0.77 % Current number of archived clauses : 0
% 0.33/0.77 % Clause-clause subsumption calls (NU) : 0
% 0.33/0.77 % Rec. Clause-clause subsumption calls : 0
% 0.33/0.77 % Non-unit clause-clause subsumptions : 0
% 0.33/0.77 % Unit Clause-clause subsumption calls : 4608
% 0.33/0.77 % Rewrite failures with RHS unbound : 0
% 0.33/0.77 % BW rewrite match attempts : 0
% 0.33/0.77 % BW rewrite match successes : 0
% 0.33/0.77 % Condensation attempts : 0
% 0.33/0.77 % Condensation successes : 0
% 0.33/0.77 % Termbank termtop insertions : 11668
% 0.33/0.77 % Search garbage collected termcells : 2452
% 0.33/0.77
% 0.33/0.77 % -------------------------------------------------
% 0.33/0.77 % User time : 0.081 s
% 0.33/0.77 % System time : 0.015 s
% 0.33/0.77 % Total time : 0.096 s
% 0.33/0.77 % Maximum resident set size: 5940 pages
% 0.33/0.77
% 0.33/0.77 % -------------------------------------------------
% 0.33/0.77 % User time : 0.096 s
% 0.33/0.77 % System time : 0.030 s
% 0.33/0.77 % Total time : 0.126 s
% 0.33/0.77 % Maximum resident set size: 5632 pages
% 0.33/0.77 % E exiting
%------------------------------------------------------------------------------