%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MSC013+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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 : 300s
% DateTime : Thu May 9 17:33:24 EDT 2024
% Result : CounterSatisfiable 4.21s 4.39s
% Output : Saturation 4.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : MSC013+1 : TPTP v8.1.2. Released v3.2.0.
% 0.00/0.09 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Wed May 8 13:54:52 EDT 2024
% 0.09/0.28 % CPUTime :
% 4.21/4.39 % Version: 1.5
% 4.21/4.39 % SZS status CounterSatisfiable
% 4.21/4.39 % SZS output start Saturation
% 4.21/4.39 fof(relation_injective,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![I]:(![J]:(![K]:((f(A,B,C,D,E,K)&f(F,G,H,I,J,K))=>((((equalish(A,F)&equalish(B,G))&equalish(C,H))&equalish(D,I))&equalish(E,J)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', relation_injective)).
% 4.21/4.39 fof(c3,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![I]:(![J]:(![K]:((~f(A,B,C,D,E,K)|~f(F,G,H,I,J,K))|((((equalish(A,F)&equalish(B,G))&equalish(C,H))&equalish(D,I))&equalish(E,J)))))))))))))),inference(fof_nnf,[status(thm)],[relation_injective])).
% 4.21/4.39 fof(c4,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![I]:(![J]:((![K]:(~f(A,B,C,D,E,K)|~f(F,G,H,I,J,K)))|((((equalish(A,F)&equalish(B,G))&equalish(C,H))&equalish(D,I))&equalish(E,J))))))))))))),inference(shift_quantors,[status(thm)],[c3])).
% 4.21/4.39 fof(c6,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((~f(X2,X3,X4,X5,X6,X12)|~f(X7,X8,X9,X10,X11,X12))|((((equalish(X2,X7)&equalish(X3,X8))&equalish(X4,X9))&equalish(X5,X10))&equalish(X6,X11)))))))))))))),inference(shift_quantors,[status(thm)],[fof(c5,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:((![X12]:(~f(X2,X3,X4,X5,X6,X12)|~f(X7,X8,X9,X10,X11,X12)))|((((equalish(X2,X7)&equalish(X3,X8))&equalish(X4,X9))&equalish(X5,X10))&equalish(X6,X11))))))))))))),inference(variable_rename,[status(thm)],[c4])).])).
% 4.21/4.39 fof(c7,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((((((~f(X2,X3,X4,X5,X6,X12)|~f(X7,X8,X9,X10,X11,X12))|equalish(X2,X7))&((~f(X2,X3,X4,X5,X6,X12)|~f(X7,X8,X9,X10,X11,X12))|equalish(X3,X8)))&((~f(X2,X3,X4,X5,X6,X12)|~f(X7,X8,X9,X10,X11,X12))|equalish(X4,X9)))&((~f(X2,X3,X4,X5,X6,X12)|~f(X7,X8,X9,X10,X11,X12))|equalish(X5,X10)))&((~f(X2,X3,X4,X5,X6,X12)|~f(X7,X8,X9,X10,X11,X12))|equalish(X6,X11)))))))))))))),inference(distribute,[status(thm)],[c6])).
% 4.21/4.39 cnf(c9,plain,~f(X45,X36,X41,X42,X39,X37)|~f(X38,X44,X46,X43,X40,X37)|equalish(X36,X44),inference(split_conjunct,[status(thm)],[c7])).
% 4.21/4.39 fof(n0_and_n1_reflexive,axiom,(equalish(n0,n0)&equalish(n1,n1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', n0_and_n1_reflexive)).
% 4.21/4.39 cnf(c22,plain,equalish(n1,n1),inference(split_conjunct,[status(thm)],[n0_and_n1_reflexive])).
% 4.21/4.39 cnf(c21,plain,equalish(n0,n0),inference(split_conjunct,[status(thm)],[n0_and_n1_reflexive])).
% 4.21/4.39 fof(relation_exists,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(((((equalish(A,A)&equalish(B,B))&equalish(C,C))&equalish(D,D))&equalish(E,E))=>(?[F]:f(A,B,C,D,E,F)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', relation_exists)).
% 4.21/4.39 fof(c13,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(((((~equalish(A,A)|~equalish(B,B))|~equalish(C,C))|~equalish(D,D))|~equalish(E,E))|(?[F]:f(A,B,C,D,E,F)))))))),inference(fof_nnf,[status(thm)],[relation_exists])).
% 4.21/4.39 fof(c14,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(((((~equalish(X13,X13)|~equalish(X14,X14))|~equalish(X15,X15))|~equalish(X16,X16))|~equalish(X17,X17))|(?[X18]:f(X13,X14,X15,X16,X17,X18)))))))),inference(variable_rename,[status(thm)],[c13])).
% 4.21/4.39 fof(c15,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(((((~equalish(X13,X13)|~equalish(X14,X14))|~equalish(X15,X15))|~equalish(X16,X16))|~equalish(X17,X17))|f(X13,X14,X15,X16,X17,skolem0001(X13,X14,X15,X16,X17)))))))),inference(skolemize,[status(esa)],[c14])).
% 4.21/4.39 cnf(c16,plain,~equalish(X104,X104)|~equalish(X107,X107)|~equalish(X105,X105)|~equalish(X108,X108)|~equalish(X106,X106)|f(X104,X107,X105,X108,X106,skolem0001(X104,X107,X105,X108,X106)),inference(split_conjunct,[status(thm)],[c15])).
% 4.21/4.39 cnf(c30,plain,~equalish(X126,X126)|~equalish(X128,X128)|~equalish(X125,X125)|~equalish(X127,X127)|f(X126,X128,X125,X127,X125,skolem0001(X126,X128,X125,X127,X125)),inference(factor,[status(thm)],[c16])).
% 4.21/4.39 cnf(c59,plain,~equalish(X227,X227)|~equalish(X228,X228)|~equalish(X229,X229)|f(X227,X228,X229,X229,X229,skolem0001(X227,X228,X229,X229,X229)),inference(factor,[status(thm)],[c30])).
% 4.21/4.39 cnf(c231,plain,~equalish(X596,X596)|~equalish(X597,X597)|f(X596,X597,n0,n0,n0,skolem0001(X596,X597,n0,n0,n0)),inference(resolution,[status(thm)],[c59, c21])).
% 4.21/4.39 cnf(c502,plain,~equalish(X847,X847)|f(X847,X847,n0,n0,n0,skolem0001(X847,X847,n0,n0,n0)),inference(factor,[status(thm)],[c231])).
% 4.21/4.39 cnf(c806,plain,f(n1,n1,n0,n0,n0,skolem0001(n1,n1,n0,n0,n0)),inference(resolution,[status(thm)],[c502, c22])).
% 4.21/4.39 cnf(c971,plain,~f(X1410,X1414,X1413,X1412,X1411,skolem0001(n1,n1,n0,n0,n0))|equalish(X1414,n1),inference(resolution,[status(thm)],[c806, c9])).
% 4.21/4.39 cnf(c8,plain,~f(X28,X19,X24,X25,X22,X20)|~f(X21,X27,X29,X26,X23,X20)|equalish(X28,X21),inference(split_conjunct,[status(thm)],[c7])).
% 4.21/4.39 cnf(c969,plain,~f(X1408,X1405,X1406,X1409,X1407,skolem0001(n1,n1,n0,n0,n0))|equalish(X1408,n1),inference(resolution,[status(thm)],[c806, c8])).
% 4.21/4.39 cnf(c10,plain,~f(X62,X53,X58,X59,X56,X54)|~f(X55,X61,X63,X60,X57,X54)|equalish(X58,X63),inference(split_conjunct,[status(thm)],[c7])).
% 4.21/4.39 cnf(c968,plain,~f(X1402,X1400,X1404,X1403,X1401,skolem0001(n1,n1,n0,n0,n0))|equalish(X1404,n0),inference(resolution,[status(thm)],[c806, c10])).
% 4.21/4.39 cnf(c12,plain,~f(X96,X87,X92,X93,X90,X88)|~f(X89,X95,X97,X94,X91,X88)|equalish(X90,X91),inference(split_conjunct,[status(thm)],[c7])).
% 4.21/4.39 cnf(c967,plain,~f(X1398,X1399,X1396,X1395,X1397,skolem0001(n1,n1,n0,n0,n0))|equalish(X1397,n0),inference(resolution,[status(thm)],[c806, c12])).
% 4.21/4.39 cnf(c11,plain,~f(X79,X70,X75,X76,X73,X71)|~f(X72,X78,X80,X77,X74,X71)|equalish(X76,X77),inference(split_conjunct,[status(thm)],[c7])).
% 4.21/4.39 cnf(c963,plain,~f(X1392,X1391,X1393,X1394,X1390,skolem0001(n1,n1,n0,n0,n0))|equalish(X1394,n0),inference(resolution,[status(thm)],[c806, c11])).
% 4.21/4.39 cnf(c230,plain,~equalish(X586,X586)|~equalish(X587,X587)|f(X586,X587,n1,n1,n1,skolem0001(X586,X587,n1,n1,n1)),inference(resolution,[status(thm)],[c59, c22])).
% 4.21/4.39 cnf(c493,plain,~equalish(X844,X844)|f(X844,X844,n1,n1,n1,skolem0001(X844,X844,n1,n1,n1)),inference(factor,[status(thm)],[c230])).
% 4.21/4.39 cnf(c791,plain,f(n0,n0,n1,n1,n1,skolem0001(n0,n0,n1,n1,n1)),inference(resolution,[status(thm)],[c493, c21])).
% 4.21/4.39 cnf(c956,plain,~f(X1385,X1389,X1388,X1387,X1386,skolem0001(n0,n0,n1,n1,n1))|equalish(X1389,n0),inference(resolution,[status(thm)],[c791, c9])).
% 4.21/4.39 cnf(c954,plain,~f(X1383,X1380,X1381,X1384,X1382,skolem0001(n0,n0,n1,n1,n1))|equalish(X1383,n0),inference(resolution,[status(thm)],[c791, c8])).
% 4.21/4.39 cnf(c953,plain,~f(X1377,X1375,X1379,X1378,X1376,skolem0001(n0,n0,n1,n1,n1))|equalish(X1379,n1),inference(resolution,[status(thm)],[c791, c10])).
% 4.21/4.39 cnf(c952,plain,~f(X1373,X1374,X1371,X1370,X1372,skolem0001(n0,n0,n1,n1,n1))|equalish(X1372,n1),inference(resolution,[status(thm)],[c791, c12])).
% 4.21/4.39 cnf(c948,plain,~f(X1367,X1366,X1368,X1369,X1365,skolem0001(n0,n0,n1,n1,n1))|equalish(X1369,n1),inference(resolution,[status(thm)],[c791, c11])).
% 4.21/4.39 cnf(c33,plain,~equalish(X153,X153)|~equalish(X155,X155)|~equalish(X152,X152)|~equalish(X154,X154)|f(X153,X155,X152,X154,n0,skolem0001(X153,X155,X152,X154,n0)),inference(resolution,[status(thm)],[c16, c21])).
% 4.21/4.39 cnf(c103,plain,~equalish(X333,X333)|~equalish(X335,X335)|~equalish(X334,X334)|f(X333,X335,X334,X333,n0,skolem0001(X333,X335,X334,X333,n0)),inference(factor,[status(thm)],[c33])).
% 4.21/4.39 cnf(c331,plain,~equalish(X695,X695)|~equalish(X696,X696)|f(X695,X696,X695,X695,n0,skolem0001(X695,X696,X695,X695,n0)),inference(factor,[status(thm)],[c103])).
% 4.21/4.39 cnf(c588,plain,~equalish(X697,X697)|f(X697,X697,X697,X697,n0,skolem0001(X697,X697,X697,X697,n0)),inference(factor,[status(thm)],[c331])).
% 4.21/4.39 cnf(c591,plain,f(n1,n1,n1,n1,n0,skolem0001(n1,n1,n1,n1,n0)),inference(resolution,[status(thm)],[c588, c22])).
% 4.21/4.39 cnf(c875,plain,~f(X1360,X1364,X1363,X1362,X1361,skolem0001(n1,n1,n1,n1,n0))|equalish(X1364,n1),inference(resolution,[status(thm)],[c591, c9])).
% 4.21/4.39 cnf(c873,plain,~f(X1358,X1355,X1356,X1359,X1357,skolem0001(n1,n1,n1,n1,n0))|equalish(X1358,n1),inference(resolution,[status(thm)],[c591, c8])).
% 4.21/4.39 cnf(c872,plain,~f(X1352,X1350,X1354,X1353,X1351,skolem0001(n1,n1,n1,n1,n0))|equalish(X1354,n1),inference(resolution,[status(thm)],[c591, c10])).
% 4.21/4.39 cnf(c871,plain,~f(X1348,X1349,X1346,X1345,X1347,skolem0001(n1,n1,n1,n1,n0))|equalish(X1347,n0),inference(resolution,[status(thm)],[c591, c12])).
% 4.21/4.39 cnf(c867,plain,~f(X1342,X1341,X1343,X1344,X1340,skolem0001(n1,n1,n1,n1,n0))|equalish(X1344,n1),inference(resolution,[status(thm)],[c591, c11])).
% 4.21/4.39 cnf(c31,plain,~equalish(X137,X137)|~equalish(X139,X139)|~equalish(X136,X136)|~equalish(X138,X138)|f(X137,X139,X136,X138,X138,skolem0001(X137,X139,X136,X138,X138)),inference(factor,[status(thm)],[c16])).
% 4.21/4.39 cnf(c76,plain,~equalish(X288,X288)|~equalish(X289,X289)|~equalish(X287,X287)|f(X288,X289,X287,n0,n0,skolem0001(X288,X289,X287,n0,n0)),inference(resolution,[status(thm)],[c31, c21])).
% 4.21/4.39 cnf(c271,plain,~equalish(X676,X676)|~equalish(X675,X675)|f(X676,X675,X676,n0,n0,skolem0001(X676,X675,X676,n0,n0)),inference(factor,[status(thm)],[c76])).
% 4.21/4.39 cnf(c565,plain,~equalish(X677,X677)|f(X677,X677,X677,n0,n0,skolem0001(X677,X677,X677,n0,n0)),inference(factor,[status(thm)],[c271])).
% 4.21/4.39 cnf(c568,plain,f(n1,n1,n1,n0,n0,skolem0001(n1,n1,n1,n0,n0)),inference(resolution,[status(thm)],[c565, c22])).
% 4.21/4.39 cnf(c853,plain,~f(X1338,X1339,X1336,X1335,X1337,skolem0001(n1,n1,n1,n0,n0))|equalish(X1337,n0),inference(resolution,[status(thm)],[c568, c12])).
% 4.21/4.39 cnf(c852,plain,~f(X1332,X1331,X1333,X1334,X1330,skolem0001(n1,n1,n1,n0,n0))|equalish(X1334,n0),inference(resolution,[status(thm)],[c568, c11])).
% 4.21/4.39 cnf(c849,plain,~f(X1328,X1325,X1326,X1329,X1327,skolem0001(n1,n1,n1,n0,n0))|equalish(X1328,n1),inference(resolution,[status(thm)],[c568, c8])).
% 4.21/4.39 cnf(c848,plain,~f(X1322,X1320,X1324,X1323,X1321,skolem0001(n1,n1,n1,n0,n0))|equalish(X1324,n1),inference(resolution,[status(thm)],[c568, c10])).
% 4.21/4.39 cnf(c847,plain,~f(X1315,X1319,X1318,X1317,X1316,skolem0001(n1,n1,n1,n0,n0))|equalish(X1319,n1),inference(resolution,[status(thm)],[c568, c9])).
% 4.21/4.39 cnf(c75,plain,~equalish(X275,X275)|~equalish(X276,X276)|~equalish(X274,X274)|f(X275,X276,X274,n1,n1,skolem0001(X275,X276,X274,n1,n1)),inference(resolution,[status(thm)],[c31, c22])).
% 4.21/4.39 cnf(c265,plain,~equalish(X621,X621)|~equalish(X622,X622)|f(X621,X622,X621,n1,n1,skolem0001(X621,X622,X621,n1,n1)),inference(factor,[status(thm)],[c75])).
% 4.21/4.39 cnf(c546,plain,~equalish(X623,X623)|f(X623,X623,X623,n1,n1,skolem0001(X623,X623,X623,n1,n1)),inference(factor,[status(thm)],[c265])).
% 4.21/4.39 cnf(c550,plain,f(n0,n0,n0,n1,n1,skolem0001(n0,n0,n0,n1,n1)),inference(resolution,[status(thm)],[c546, c21])).
% 4.21/4.39 cnf(c837,plain,~f(X1313,X1314,X1311,X1310,X1312,skolem0001(n0,n0,n0,n1,n1))|equalish(X1312,n1),inference(resolution,[status(thm)],[c550, c12])).
% 4.21/4.39 cnf(c836,plain,~f(X1307,X1306,X1308,X1309,X1305,skolem0001(n0,n0,n0,n1,n1))|equalish(X1309,n1),inference(resolution,[status(thm)],[c550, c11])).
% 4.21/4.39 cnf(c833,plain,~f(X1303,X1300,X1301,X1304,X1302,skolem0001(n0,n0,n0,n1,n1))|equalish(X1303,n0),inference(resolution,[status(thm)],[c550, c8])).
% 4.21/4.39 cnf(c832,plain,~f(X1297,X1295,X1299,X1298,X1296,skolem0001(n0,n0,n0,n1,n1))|equalish(X1299,n0),inference(resolution,[status(thm)],[c550, c10])).
% 4.21/4.39 cnf(c831,plain,~f(X1290,X1294,X1293,X1292,X1291,skolem0001(n0,n0,n0,n1,n1))|equalish(X1294,n0),inference(resolution,[status(thm)],[c550, c9])).
% 4.21/4.39 cnf(c32,plain,~equalish(X147,X147)|~equalish(X149,X149)|~equalish(X146,X146)|~equalish(X148,X148)|f(X147,X149,X146,X148,n1,skolem0001(X147,X149,X146,X148,n1)),inference(resolution,[status(thm)],[c16, c22])).
% 4.21/4.39 cnf(c86,plain,~equalish(X305,X305)|~equalish(X306,X306)|~equalish(X307,X307)|f(X305,X306,X307,X305,n1,skolem0001(X305,X306,X307,X305,n1)),inference(factor,[status(thm)],[c32])).
% 4.21/4.39 cnf(c278,plain,~equalish(X594,X594)|~equalish(X593,X593)|f(X594,X593,X594,X594,n1,skolem0001(X594,X593,X594,X594,n1)),inference(factor,[status(thm)],[c86])).
% 4.21/4.39 cnf(c497,plain,~equalish(X595,X595)|f(X595,X595,X595,X595,n1,skolem0001(X595,X595,X595,X595,n1)),inference(factor,[status(thm)],[c278])).
% 4.21/4.39 cnf(c501,plain,f(n0,n0,n0,n0,n1,skolem0001(n0,n0,n0,n0,n1)),inference(resolution,[status(thm)],[c497, c21])).
% 4.21/4.39 cnf(c801,plain,~f(X1288,X1289,X1286,X1285,X1287,skolem0001(n0,n0,n0,n0,n1))|equalish(X1287,n1),inference(resolution,[status(thm)],[c501, c12])).
% 4.21/4.39 cnf(c800,plain,~f(X1282,X1281,X1283,X1284,X1280,skolem0001(n0,n0,n0,n0,n1))|equalish(X1284,n0),inference(resolution,[status(thm)],[c501, c11])).
% 4.21/4.39 cnf(c797,plain,~f(X1278,X1275,X1276,X1279,X1277,skolem0001(n0,n0,n0,n0,n1))|equalish(X1278,n0),inference(resolution,[status(thm)],[c501, c8])).
% 4.21/4.39 cnf(c796,plain,~f(X1272,X1270,X1274,X1273,X1271,skolem0001(n0,n0,n0,n0,n1))|equalish(X1274,n0),inference(resolution,[status(thm)],[c501, c10])).
% 4.21/4.39 cnf(c795,plain,~f(X1265,X1269,X1268,X1267,X1266,skolem0001(n0,n0,n0,n0,n1))|equalish(X1269,n0),inference(resolution,[status(thm)],[c501, c9])).
% 4.21/4.39 cnf(c57,plain,~equalish(X214,X214)|~equalish(X213,X213)|~equalish(X215,X215)|f(X214,X213,X215,X214,X215,skolem0001(X214,X213,X215,X214,X215)),inference(factor,[status(thm)],[c30])).
% 4.21/4.39 cnf(c213,plain,~equalish(X550,X550)|~equalish(X549,X549)|f(X550,X549,n0,X550,n0,skolem0001(X550,X549,n0,X550,n0)),inference(resolution,[status(thm)],[c57, c21])).
% 4.21/4.39 cnf(c478,plain,~equalish(X551,X551)|f(X551,X551,n0,X551,n0,skolem0001(X551,X551,n0,X551,n0)),inference(factor,[status(thm)],[c213])).
% 4.21/4.39 cnf(c481,plain,f(n1,n1,n0,n1,n0,skolem0001(n1,n1,n0,n1,n0)),inference(resolution,[status(thm)],[c478, c22])).
% 4.21/4.39 cnf(c787,plain,~f(X1263,X1264,X1261,X1260,X1262,skolem0001(n1,n1,n0,n1,n0))|equalish(X1262,n0),inference(resolution,[status(thm)],[c481, c12])).
% 4.21/4.39 cnf(c786,plain,~f(X1257,X1256,X1258,X1259,X1255,skolem0001(n1,n1,n0,n1,n0))|equalish(X1259,n1),inference(resolution,[status(thm)],[c481, c11])).
% 4.21/4.39 cnf(c783,plain,~f(X1253,X1250,X1251,X1254,X1252,skolem0001(n1,n1,n0,n1,n0))|equalish(X1253,n1),inference(resolution,[status(thm)],[c481, c8])).
% 4.21/4.39 cnf(c782,plain,~f(X1247,X1245,X1249,X1248,X1246,skolem0001(n1,n1,n0,n1,n0))|equalish(X1249,n0),inference(resolution,[status(thm)],[c481, c10])).
% 4.21/4.39 cnf(c781,plain,~f(X1240,X1244,X1243,X1242,X1241,skolem0001(n1,n1,n0,n1,n0))|equalish(X1244,n1),inference(resolution,[status(thm)],[c481, c9])).
% 4.21/4.39 cnf(c212,plain,~equalish(X537,X537)|~equalish(X536,X536)|f(X537,X536,n1,X537,n1,skolem0001(X537,X536,n1,X537,n1)),inference(resolution,[status(thm)],[c57, c22])).
% 4.21/4.39 cnf(c471,plain,~equalish(X538,X538)|f(X538,X538,n1,X538,n1,skolem0001(X538,X538,n1,X538,n1)),inference(factor,[status(thm)],[c212])).
% 4.21/4.39 cnf(c475,plain,f(n0,n0,n1,n0,n1,skolem0001(n0,n0,n1,n0,n1)),inference(resolution,[status(thm)],[c471, c21])).
% 4.21/4.39 cnf(c773,plain,~f(X1238,X1239,X1236,X1235,X1237,skolem0001(n0,n0,n1,n0,n1))|equalish(X1237,n1),inference(resolution,[status(thm)],[c475, c12])).
% 4.21/4.39 cnf(c772,plain,~f(X1232,X1231,X1233,X1234,X1230,skolem0001(n0,n0,n1,n0,n1))|equalish(X1234,n0),inference(resolution,[status(thm)],[c475, c11])).
% 4.21/4.39 cnf(c769,plain,~f(X1228,X1225,X1226,X1229,X1227,skolem0001(n0,n0,n1,n0,n1))|equalish(X1228,n0),inference(resolution,[status(thm)],[c475, c8])).
% 4.21/4.39 cnf(c768,plain,~f(X1222,X1220,X1224,X1223,X1221,skolem0001(n0,n0,n1,n0,n1))|equalish(X1224,n1),inference(resolution,[status(thm)],[c475, c10])).
% 4.21/4.39 cnf(c767,plain,~f(X1215,X1219,X1218,X1217,X1216,skolem0001(n0,n0,n1,n0,n1))|equalish(X1219,n0),inference(resolution,[status(thm)],[c475, c9])).
% 4.21/4.39 cnf(c29,plain,~equalish(X114,X114)|~equalish(X113,X113)|~equalish(X115,X115)|~equalish(X116,X116)|f(X114,X113,X115,X116,X113,skolem0001(X114,X113,X115,X116,X113)),inference(factor,[status(thm)],[c16])).
% 4.21/4.39 cnf(c40,plain,~equalish(X183,X183)|~equalish(X185,X185)|~equalish(X184,X184)|f(X183,X185,X184,X185,X185,skolem0001(X183,X185,X184,X185,X185)),inference(factor,[status(thm)],[c29])).
% 4.21/4.39 cnf(c169,plain,~equalish(X199,X199)|~equalish(X198,X198)|f(X199,X198,X198,X198,X198,skolem0001(X199,X198,X198,X198,X198)),inference(factor,[status(thm)],[c40])).
% 4.21/4.39 cnf(c187,plain,~equalish(X469,X469)|f(X469,n0,n0,n0,n0,skolem0001(X469,n0,n0,n0,n0)),inference(resolution,[status(thm)],[c169, c21])).
% 4.21/4.39 cnf(c447,plain,f(n1,n0,n0,n0,n0,skolem0001(n1,n0,n0,n0,n0)),inference(resolution,[status(thm)],[c187, c22])).
% 4.21/4.39 cnf(c757,plain,~f(X1212,X1213,X1210,X1209,X1211,skolem0001(n1,n0,n0,n0,n0))|equalish(X1211,n0),inference(resolution,[status(thm)],[c447, c12])).
% 4.21/4.39 cnf(c756,plain,~f(X1205,X1204,X1206,X1207,X1203,skolem0001(n1,n0,n0,n0,n0))|equalish(X1207,n0),inference(resolution,[status(thm)],[c447, c11])).
% 4.21/4.39 cnf(c753,plain,~f(X1201,X1198,X1199,X1202,X1200,skolem0001(n1,n0,n0,n0,n0))|equalish(X1201,n1),inference(resolution,[status(thm)],[c447, c8])).
% 4.21/4.39 cnf(c752,plain,~f(X1195,X1193,X1197,X1196,X1194,skolem0001(n1,n0,n0,n0,n0))|equalish(X1197,n0),inference(resolution,[status(thm)],[c447, c10])).
% 4.21/4.39 cnf(c751,plain,~f(X1187,X1191,X1190,X1189,X1188,skolem0001(n1,n0,n0,n0,n0))|equalish(X1191,n0),inference(resolution,[status(thm)],[c447, c9])).
% 4.21/4.39 cnf(c186,plain,~equalish(X458,X458)|f(X458,n1,n1,n1,n1,skolem0001(X458,n1,n1,n1,n1)),inference(resolution,[status(thm)],[c169, c22])).
% 4.21/4.39 cnf(c444,plain,f(n0,n1,n1,n1,n1,skolem0001(n0,n1,n1,n1,n1)),inference(resolution,[status(thm)],[c186, c21])).
% 4.21/4.39 cnf(c747,plain,~f(X1185,X1186,X1183,X1182,X1184,skolem0001(n0,n1,n1,n1,n1))|equalish(X1184,n1),inference(resolution,[status(thm)],[c444, c12])).
% 4.21/4.39 cnf(c746,plain,~f(X1178,X1177,X1179,X1180,X1176,skolem0001(n0,n1,n1,n1,n1))|equalish(X1180,n1),inference(resolution,[status(thm)],[c444, c11])).
% 4.21/4.39 cnf(c743,plain,~f(X1174,X1171,X1172,X1175,X1173,skolem0001(n0,n1,n1,n1,n1))|equalish(X1174,n0),inference(resolution,[status(thm)],[c444, c8])).
% 4.21/4.39 cnf(c742,plain,~f(X1168,X1166,X1170,X1169,X1167,skolem0001(n0,n1,n1,n1,n1))|equalish(X1170,n1),inference(resolution,[status(thm)],[c444, c10])).
% 4.21/4.39 cnf(c741,plain,~f(X1160,X1164,X1163,X1162,X1161,skolem0001(n0,n1,n1,n1,n1))|equalish(X1164,n1),inference(resolution,[status(thm)],[c444, c9])).
% 4.21/4.39 cnf(c168,plain,~equalish(X192,X192)|~equalish(X193,X193)|f(X192,X193,X192,X193,X193,skolem0001(X192,X193,X192,X193,X193)),inference(factor,[status(thm)],[c40])).
% 4.21/4.39 cnf(c180,plain,~equalish(X435,X435)|f(X435,n0,X435,n0,n0,skolem0001(X435,n0,X435,n0,n0)),inference(resolution,[status(thm)],[c168, c21])).
% 4.21/4.39 cnf(c403,plain,f(n1,n0,n1,n0,n0,skolem0001(n1,n0,n1,n0,n0)),inference(resolution,[status(thm)],[c180, c22])).
% 4.21/4.39 cnf(c713,plain,~f(X1154,X1155,X1152,X1151,X1153,skolem0001(n1,n0,n1,n0,n0))|equalish(X1153,n0),inference(resolution,[status(thm)],[c403, c12])).
% 4.21/4.39 cnf(c712,plain,~f(X1147,X1146,X1148,X1149,X1145,skolem0001(n1,n0,n1,n0,n0))|equalish(X1149,n0),inference(resolution,[status(thm)],[c403, c11])).
% 4.21/4.39 cnf(c709,plain,~f(X1143,X1140,X1141,X1144,X1142,skolem0001(n1,n0,n1,n0,n0))|equalish(X1143,n1),inference(resolution,[status(thm)],[c403, c8])).
% 4.21/4.39 cnf(c708,plain,~f(X1137,X1135,X1139,X1138,X1136,skolem0001(n1,n0,n1,n0,n0))|equalish(X1139,n1),inference(resolution,[status(thm)],[c403, c10])).
% 4.21/4.39 cnf(c707,plain,~f(X1129,X1133,X1132,X1131,X1130,skolem0001(n1,n0,n1,n0,n0))|equalish(X1133,n0),inference(resolution,[status(thm)],[c403, c9])).
% 4.21/4.39 cnf(c105,plain,~equalish(X364,X364)|~equalish(X363,X363)|~equalish(X362,X362)|f(X364,X363,X362,X362,n0,skolem0001(X364,X363,X362,X362,n0)),inference(factor,[status(thm)],[c33])).
% 4.21/4.39 cnf(c348,plain,~equalish(X761,X761)|~equalish(X762,X762)|f(X761,X762,n1,n1,n0,skolem0001(X761,X762,n1,n1,n0)),inference(resolution,[status(thm)],[c105, c22])).
% 4.21/4.39 cnf(c703,plain,~equalish(X1128,X1128)|f(X1128,X1128,n1,n1,n0,skolem0001(X1128,X1128,n1,n1,n0)),inference(factor,[status(thm)],[c348])).
% 4.21/4.39 cnf(c179,plain,~equalish(X434,X434)|f(X434,n1,X434,n1,n1,skolem0001(X434,n1,X434,n1,n1)),inference(resolution,[status(thm)],[c168, c22])).
% 4.21/4.39 cnf(c402,plain,f(n0,n1,n0,n1,n1,skolem0001(n0,n1,n0,n1,n1)),inference(resolution,[status(thm)],[c179, c21])).
% 4.21/4.39 cnf(c700,plain,~f(X1126,X1127,X1124,X1123,X1125,skolem0001(n0,n1,n0,n1,n1))|equalish(X1125,n1),inference(resolution,[status(thm)],[c402, c12])).
% 4.21/4.39 cnf(c699,plain,~f(X1119,X1118,X1120,X1121,X1117,skolem0001(n0,n1,n0,n1,n1))|equalish(X1121,n1),inference(resolution,[status(thm)],[c402, c11])).
% 4.21/4.39 cnf(c696,plain,~f(X1115,X1112,X1113,X1116,X1114,skolem0001(n0,n1,n0,n1,n1))|equalish(X1115,n0),inference(resolution,[status(thm)],[c402, c8])).
% 4.21/4.39 cnf(c695,plain,~f(X1108,X1106,X1110,X1109,X1107,skolem0001(n0,n1,n0,n1,n1))|equalish(X1110,n0),inference(resolution,[status(thm)],[c402, c10])).
% 4.21/4.39 cnf(c694,plain,~f(X1101,X1105,X1104,X1103,X1102,skolem0001(n0,n1,n0,n1,n1))|equalish(X1105,n1),inference(resolution,[status(thm)],[c402, c9])).
% 4.21/4.39 cnf(c39,plain,~equalish(X182,X182)|~equalish(X180,X180)|~equalish(X181,X181)|f(X182,X180,X181,X182,X180,skolem0001(X182,X180,X181,X182,X180)),inference(factor,[status(thm)],[c29])).
% 4.21/4.39 cnf(c165,plain,~equalish(X190,X190)|~equalish(X189,X189)|f(X190,X189,X189,X190,X189,skolem0001(X190,X189,X189,X190,X189)),inference(factor,[status(thm)],[c39])).
% 4.21/4.39 cnf(c177,plain,~equalish(X430,X430)|f(X430,n0,n0,X430,n0,skolem0001(X430,n0,n0,X430,n0)),inference(resolution,[status(thm)],[c165, c21])).
% 4.21/4.39 cnf(c394,plain,f(n1,n0,n0,n1,n0,skolem0001(n1,n0,n0,n1,n0)),inference(resolution,[status(thm)],[c177, c22])).
% 4.21/4.39 cnf(c687,plain,~f(X1099,X1100,X1097,X1096,X1098,skolem0001(n1,n0,n0,n1,n0))|equalish(X1098,n0),inference(resolution,[status(thm)],[c394, c12])).
% 4.21/4.39 cnf(c686,plain,~f(X1092,X1091,X1093,X1094,X1090,skolem0001(n1,n0,n0,n1,n0))|equalish(X1094,n1),inference(resolution,[status(thm)],[c394, c11])).
% 4.21/4.39 cnf(c683,plain,~f(X1088,X1085,X1086,X1089,X1087,skolem0001(n1,n0,n0,n1,n0))|equalish(X1088,n1),inference(resolution,[status(thm)],[c394, c8])).
% 4.21/4.39 cnf(c682,plain,~f(X1081,X1079,X1083,X1082,X1080,skolem0001(n1,n0,n0,n1,n0))|equalish(X1083,n0),inference(resolution,[status(thm)],[c394, c10])).
% 4.21/4.39 cnf(c681,plain,~f(X1074,X1078,X1077,X1076,X1075,skolem0001(n1,n0,n0,n1,n0))|equalish(X1078,n0),inference(resolution,[status(thm)],[c394, c9])).
% 4.21/4.39 cnf(c104,plain,~equalish(X351,X351)|~equalish(X349,X349)|~equalish(X350,X350)|f(X351,X349,X350,X349,n0,skolem0001(X351,X349,X350,X349,n0)),inference(factor,[status(thm)],[c33])).
% 4.21/4.39 cnf(c341,plain,~equalish(X714,X714)|~equalish(X713,X713)|f(X714,X713,X713,X713,n0,skolem0001(X714,X713,X713,X713,n0)),inference(factor,[status(thm)],[c104])).
% 4.21/4.39 cnf(c609,plain,~equalish(X1073,X1073)|f(X1073,n1,n1,n1,n0,skolem0001(X1073,n1,n1,n1,n0)),inference(resolution,[status(thm)],[c341, c22])).
% 4.21/4.39 cnf(c176,plain,~equalish(X429,X429)|f(X429,n1,n1,X429,n1,skolem0001(X429,n1,n1,X429,n1)),inference(resolution,[status(thm)],[c165, c22])).
% 4.21/4.39 cnf(c393,plain,f(n0,n1,n1,n0,n1,skolem0001(n0,n1,n1,n0,n1)),inference(resolution,[status(thm)],[c176, c21])).
% 4.21/4.39 cnf(c672,plain,~f(X1069,X1070,X1067,X1066,X1068,skolem0001(n0,n1,n1,n0,n1))|equalish(X1068,n1),inference(resolution,[status(thm)],[c393, c12])).
% 4.21/4.39 cnf(c671,plain,~f(X1062,X1061,X1063,X1064,X1060,skolem0001(n0,n1,n1,n0,n1))|equalish(X1064,n0),inference(resolution,[status(thm)],[c393, c11])).
% 4.21/4.39 cnf(c668,plain,~f(X1058,X1055,X1056,X1059,X1057,skolem0001(n0,n1,n1,n0,n1))|equalish(X1058,n0),inference(resolution,[status(thm)],[c393, c8])).
% 4.21/4.39 cnf(c667,plain,~f(X1052,X1050,X1054,X1053,X1051,skolem0001(n0,n1,n1,n0,n1))|equalish(X1054,n1),inference(resolution,[status(thm)],[c393, c10])).
% 4.21/4.39 cnf(c666,plain,~f(X1044,X1048,X1047,X1046,X1045,skolem0001(n0,n1,n1,n0,n1))|equalish(X1048,n1),inference(resolution,[status(thm)],[c393, c9])).
% 4.21/4.39 cnf(c28,plain,~equalish(X110,X110)|~equalish(X112,X112)|~equalish(X109,X109)|~equalish(X111,X111)|f(X110,X112,X109,X111,X110,skolem0001(X110,X112,X109,X111,X110)),inference(factor,[status(thm)],[c16])).
% 4.21/4.39 cnf(c36,plain,~equalish(X161,X161)|~equalish(X162,X162)|~equalish(X163,X163)|f(X161,X162,X163,X163,X161,skolem0001(X161,X162,X163,X163,X161)),inference(factor,[status(thm)],[c28])).
% 4.21/4.39 cnf(c128,plain,~equalish(X414,X414)|~equalish(X415,X415)|f(X414,X415,n0,n0,X414,skolem0001(X414,X415,n0,n0,X414)),inference(resolution,[status(thm)],[c36, c21])).
% 4.21/4.39 cnf(c378,plain,~equalish(X417,X417)|f(X417,X417,n0,n0,X417,skolem0001(X417,X417,n0,n0,X417)),inference(factor,[status(thm)],[c128])).
% 4.21/4.39 cnf(c381,plain,f(n1,n1,n0,n0,n1,skolem0001(n1,n1,n0,n0,n1)),inference(resolution,[status(thm)],[c378, c22])).
% 4.21/4.39 cnf(c660,plain,~f(X1041,X1042,X1039,X1038,X1040,skolem0001(n1,n1,n0,n0,n1))|equalish(X1040,n1),inference(resolution,[status(thm)],[c381, c12])).
% 4.21/4.39 cnf(c659,plain,~f(X1035,X1034,X1036,X1037,X1033,skolem0001(n1,n1,n0,n0,n1))|equalish(X1037,n0),inference(resolution,[status(thm)],[c381, c11])).
% 4.21/4.39 cnf(c656,plain,~f(X1031,X1028,X1029,X1032,X1030,skolem0001(n1,n1,n0,n0,n1))|equalish(X1031,n1),inference(resolution,[status(thm)],[c381, c8])).
% 4.21/4.39 cnf(c272,plain,~equalish(X689,X689)|~equalish(X688,X688)|f(X689,X688,X688,n0,n0,skolem0001(X689,X688,X688,n0,n0)),inference(factor,[status(thm)],[c76])).
% 4.21/4.39 cnf(c573,plain,~equalish(X1027,X1027)|f(X1027,n1,n1,n0,n0,skolem0001(X1027,n1,n1,n0,n0)),inference(resolution,[status(thm)],[c272, c22])).
% 4.21/4.39 cnf(c655,plain,~f(X1024,X1022,X1026,X1025,X1023,skolem0001(n1,n1,n0,n0,n1))|equalish(X1026,n0),inference(resolution,[status(thm)],[c381, c10])).
% 4.21/4.39 cnf(c654,plain,~f(X1017,X1021,X1020,X1019,X1018,skolem0001(n1,n1,n0,n0,n1))|equalish(X1021,n1),inference(resolution,[status(thm)],[c381, c9])).
% 4.21/4.39 cnf(c127,plain,~equalish(X404,X404)|~equalish(X405,X405)|f(X404,X405,n1,n1,X404,skolem0001(X404,X405,n1,n1,X404)),inference(resolution,[status(thm)],[c36, c22])).
% 4.21/4.39 cnf(c369,plain,~equalish(X406,X406)|f(X406,X406,n1,n1,X406,skolem0001(X406,X406,n1,n1,X406)),inference(factor,[status(thm)],[c127])).
% 4.21/4.39 cnf(c373,plain,f(n0,n0,n1,n1,n0,skolem0001(n0,n0,n1,n1,n0)),inference(resolution,[status(thm)],[c369, c21])).
% 4.21/4.39 cnf(c638,plain,~f(X1011,X1012,X1009,X1008,X1010,skolem0001(n0,n0,n1,n1,n0))|equalish(X1010,n0),inference(resolution,[status(thm)],[c373, c12])).
% 4.21/4.39 cnf(c266,plain,~equalish(X635,X635)|~equalish(X634,X634)|f(X635,X634,X634,n1,n1,skolem0001(X635,X634,X634,n1,n1)),inference(factor,[status(thm)],[c75])).
% 4.21/4.39 cnf(c555,plain,~equalish(X1007,X1007)|f(X1007,n0,n0,n1,n1,skolem0001(X1007,n0,n0,n1,n1)),inference(resolution,[status(thm)],[c266, c21])).
% 4.21/4.39 cnf(c637,plain,~f(X1004,X1003,X1005,X1006,X1002,skolem0001(n0,n0,n1,n1,n0))|equalish(X1006,n1),inference(resolution,[status(thm)],[c373, c11])).
% 4.21/4.39 cnf(c634,plain,~f(X1000,X997,X998,X1001,X999,skolem0001(n0,n0,n1,n1,n0))|equalish(X1000,n0),inference(resolution,[status(thm)],[c373, c8])).
% 4.21/4.39 cnf(c633,plain,~f(X994,X992,X996,X995,X993,skolem0001(n0,n0,n1,n1,n0))|equalish(X996,n1),inference(resolution,[status(thm)],[c373, c10])).
% 4.21/4.39 cnf(c632,plain,~f(X986,X990,X989,X988,X987,skolem0001(n0,n0,n1,n1,n0))|equalish(X990,n0),inference(resolution,[status(thm)],[c373, c9])).
% 4.21/4.39 cnf(c88,plain,~equalish(X321,X321)|~equalish(X320,X320)|~equalish(X319,X319)|f(X321,X320,X319,X319,n1,skolem0001(X321,X320,X319,X319,n1)),inference(factor,[status(thm)],[c32])).
% 4.21/4.39 cnf(c309,plain,~equalish(X731,X731)|~equalish(X732,X732)|f(X731,X732,n0,n0,n1,skolem0001(X731,X732,n0,n0,n1)),inference(resolution,[status(thm)],[c88, c21])).
% 4.21/4.39 cnf(c628,plain,~equalish(X985,X985)|f(X985,X985,n0,n0,n1,skolem0001(X985,X985,n0,n0,n1)),inference(factor,[status(thm)],[c309])).
% 4.21/4.39 cnf(c38,plain,~equalish(X177,X177)|~equalish(X178,X178)|~equalish(X179,X179)|f(X177,X178,X179,n0,X177,skolem0001(X177,X178,X179,n0,X177)),inference(resolution,[status(thm)],[c28, c21])).
% 4.21/4.39 cnf(c150,plain,~equalish(X370,X370)|~equalish(X371,X371)|f(X370,X371,X370,n0,X370,skolem0001(X370,X371,X370,n0,X370)),inference(factor,[status(thm)],[c38])).
% 4.21/4.39 cnf(c351,plain,~equalish(X372,X372)|f(X372,X372,X372,n0,X372,skolem0001(X372,X372,X372,n0,X372)),inference(factor,[status(thm)],[c150])).
% 4.21/4.39 cnf(c354,plain,f(n1,n1,n1,n0,n1,skolem0001(n1,n1,n1,n0,n1)),inference(resolution,[status(thm)],[c351, c22])).
% 4.21/4.39 cnf(c618,plain,~f(X982,X983,X980,X979,X981,skolem0001(n1,n1,n1,n0,n1))|equalish(X981,n1),inference(resolution,[status(thm)],[c354, c12])).
% 4.21/4.39 cnf(c617,plain,~f(X975,X974,X976,X977,X973,skolem0001(n1,n1,n1,n0,n1))|equalish(X977,n0),inference(resolution,[status(thm)],[c354, c11])).
% 4.21/4.39 cnf(c614,plain,~f(X971,X968,X969,X972,X970,skolem0001(n1,n1,n1,n0,n1))|equalish(X971,n1),inference(resolution,[status(thm)],[c354, c8])).
% 4.21/4.39 cnf(c613,plain,~f(X965,X963,X967,X966,X964,skolem0001(n1,n1,n1,n0,n1))|equalish(X967,n1),inference(resolution,[status(thm)],[c354, c10])).
% 4.21/4.39 cnf(c87,plain,~equalish(X316,X316)|~equalish(X314,X314)|~equalish(X315,X315)|f(X316,X314,X315,X314,n1,skolem0001(X316,X314,X315,X314,n1)),inference(factor,[status(thm)],[c32])).
% 4.21/4.39 cnf(c289,plain,~equalish(X614,X614)|~equalish(X615,X615)|f(X614,X615,X615,X615,n1,skolem0001(X614,X615,X615,X615,n1)),inference(factor,[status(thm)],[c87])).
% 4.21/4.39 cnf(c522,plain,~equalish(X962,X962)|f(X962,n0,n0,n0,n1,skolem0001(X962,n0,n0,n0,n1)),inference(resolution,[status(thm)],[c289, c21])).
% 4.21/4.39 cnf(c612,plain,~f(X957,X961,X960,X959,X958,skolem0001(n1,n1,n1,n0,n1))|equalish(X961,n1),inference(resolution,[status(thm)],[c354, c9])).
% 4.21/4.39 cnf(c340,plain,~equalish(X707,X707)|~equalish(X708,X708)|f(X707,X708,X707,X708,n0,skolem0001(X707,X708,X707,X708,n0)),inference(factor,[status(thm)],[c104])).
% 4.21/4.39 cnf(c601,plain,~equalish(X952,X952)|f(X952,n1,X952,n1,n0,skolem0001(X952,n1,X952,n1,n0)),inference(resolution,[status(thm)],[c340, c22])).
% 4.21/4.39 cnf(c332,plain,~equalish(X703,X703)|~equalish(X702,X702)|f(X703,X702,X702,X703,n0,skolem0001(X703,X702,X702,X703,n0)),inference(factor,[status(thm)],[c103])).
% 4.21/4.39 cnf(c596,plain,~equalish(X949,X949)|f(X949,n1,n1,X949,n0,skolem0001(X949,n1,n1,X949,n0)),inference(resolution,[status(thm)],[c332, c22])).
% 4.21/4.39 cnf(c273,plain,~equalish(X692,X692)|~equalish(X691,X691)|f(X692,X691,n1,n0,n0,skolem0001(X692,X691,n1,n0,n0)),inference(resolution,[status(thm)],[c76, c22])).
% 4.21/4.39 cnf(c585,plain,~equalish(X946,X946)|f(X946,X946,n1,n0,n0,skolem0001(X946,X946,n1,n0,n0)),inference(factor,[status(thm)],[c273])).
% 4.21/4.39 cnf(c37,plain,~equalish(X170,X170)|~equalish(X171,X171)|~equalish(X172,X172)|f(X170,X171,X172,n1,X170,skolem0001(X170,X171,X172,n1,X170)),inference(resolution,[status(thm)],[c28, c22])).
% 4.21/4.39 cnf(c136,plain,~equalish(X329,X329)|~equalish(X328,X328)|f(X329,X328,X329,n1,X329,skolem0001(X329,X328,X329,n1,X329)),inference(factor,[status(thm)],[c37])).
% 4.21/4.39 cnf(c324,plain,~equalish(X330,X330)|f(X330,X330,X330,n1,X330,skolem0001(X330,X330,X330,n1,X330)),inference(factor,[status(thm)],[c136])).
% 4.21/4.39 cnf(c328,plain,f(n0,n0,n0,n1,n0,skolem0001(n0,n0,n0,n1,n0)),inference(resolution,[status(thm)],[c324, c21])).
% 4.21/4.39 cnf(c582,plain,~f(X944,X945,X942,X941,X943,skolem0001(n0,n0,n0,n1,n0))|equalish(X943,n0),inference(resolution,[status(thm)],[c328, c12])).
% 4.21/4.39 cnf(c503,plain,~equalish(X940,X940)|f(X940,n1,n0,n0,n0,skolem0001(X940,n1,n0,n0,n0)),inference(resolution,[status(thm)],[c231, c22])).
% 4.21/4.39 cnf(c581,plain,~f(X937,X936,X938,X939,X935,skolem0001(n0,n0,n0,n1,n0))|equalish(X939,n1),inference(resolution,[status(thm)],[c328, c11])).
% 4.21/4.39 cnf(c578,plain,~f(X933,X930,X931,X934,X932,skolem0001(n0,n0,n0,n1,n0))|equalish(X933,n0),inference(resolution,[status(thm)],[c328, c8])).
% 4.21/4.39 cnf(c577,plain,~f(X927,X925,X929,X928,X926,skolem0001(n0,n0,n0,n1,n0))|equalish(X929,n0),inference(resolution,[status(thm)],[c328, c10])).
% 4.21/4.39 cnf(c495,plain,~equalish(X924,X924)|f(X924,n0,n1,n1,n1,skolem0001(X924,n0,n1,n1,n1)),inference(resolution,[status(thm)],[c230, c21])).
% 4.21/4.39 cnf(c576,plain,~f(X919,X923,X922,X921,X920,skolem0001(n0,n0,n0,n1,n0))|equalish(X923,n0),inference(resolution,[status(thm)],[c328, c9])).
% 4.21/4.39 cnf(c566,plain,~equalish(X915,X915)|f(X915,n1,X915,n0,n0,skolem0001(X915,n1,X915,n0,n0)),inference(resolution,[status(thm)],[c271, c22])).
% 4.21/4.39 cnf(c268,plain,~equalish(X658,X658)|~equalish(X659,X659)|f(X658,X659,n0,n1,n1,skolem0001(X658,X659,n0,n1,n1)),inference(resolution,[status(thm)],[c75, c21])).
% 4.21/4.39 cnf(c559,plain,~equalish(X914,X914)|f(X914,X914,n0,n1,n1,skolem0001(X914,X914,n0,n1,n1)),inference(factor,[status(thm)],[c268])).
% 4.21/4.39 cnf(c58,plain,~equalish(X220,X220)|~equalish(X221,X221)|~equalish(X222,X222)|f(X220,X221,X222,X221,X222,skolem0001(X220,X221,X222,X221,X222)),inference(factor,[status(thm)],[c30])).
% 4.21/4.39 cnf(c227,plain,~equalish(X574,X574)|~equalish(X573,X573)|f(X574,X573,n0,X573,n0,skolem0001(X574,X573,n0,X573,n0)),inference(resolution,[status(thm)],[c58, c21])).
% 4.21/4.39 cnf(c489,plain,~equalish(X913,X913)|f(X913,n1,n0,n1,n0,skolem0001(X913,n1,n0,n1,n0)),inference(resolution,[status(thm)],[c227, c22])).
% 4.21/4.39 cnf(c548,plain,~equalish(X912,X912)|f(X912,n0,X912,n1,n1,skolem0001(X912,n0,X912,n1,n1)),inference(resolution,[status(thm)],[c265, c21])).
% 4.21/4.39 cnf(c226,plain,~equalish(X559,X559)|~equalish(X558,X558)|f(X559,X558,n1,X558,n1,skolem0001(X559,X558,n1,X558,n1)),inference(resolution,[status(thm)],[c58, c22])).
% 4.21/4.39 cnf(c485,plain,~equalish(X911,X911)|f(X911,n0,n1,n0,n1,skolem0001(X911,n0,n1,n0,n1)),inference(resolution,[status(thm)],[c226, c21])).
% 4.21/4.39 cnf(c35,plain,~equalish(X156,X156)|~equalish(X157,X157)|~equalish(X158,X158)|f(X156,X157,X158,X157,X156,skolem0001(X156,X157,X158,X157,X156)),inference(factor,[status(thm)],[c28])).
% 4.21/4.39 cnf(c119,plain,~equalish(X165,X165)|~equalish(X166,X166)|f(X165,X166,X166,X166,X165,skolem0001(X165,X166,X166,X166,X165)),inference(factor,[status(thm)],[c35])).
% 4.21/4.39 cnf(c131,plain,~equalish(X318,X318)|f(X318,n0,n0,n0,X318,skolem0001(X318,n0,n0,n0,X318)),inference(resolution,[status(thm)],[c119, c21])).
% 4.21/4.39 cnf(c294,plain,f(n1,n0,n0,n0,n1,skolem0001(n1,n0,n0,n0,n1)),inference(resolution,[status(thm)],[c131, c22])).
% 4.21/4.39 cnf(c543,plain,~f(X908,X909,X906,X905,X907,skolem0001(n1,n0,n0,n0,n1))|equalish(X907,n1),inference(resolution,[status(thm)],[c294, c12])).
% 4.21/4.39 cnf(c542,plain,~f(X902,X901,X903,X904,X900,skolem0001(n1,n0,n0,n0,n1))|equalish(X904,n0),inference(resolution,[status(thm)],[c294, c11])).
% 4.21/4.39 cnf(c539,plain,~f(X897,X894,X895,X898,X896,skolem0001(n1,n0,n0,n0,n1))|equalish(X897,n1),inference(resolution,[status(thm)],[c294, c8])).
% 4.21/4.40 cnf(c538,plain,~f(X891,X889,X893,X892,X890,skolem0001(n1,n0,n0,n0,n1))|equalish(X893,n0),inference(resolution,[status(thm)],[c294, c10])).
% 4.21/4.40 cnf(c537,plain,~f(X883,X887,X886,X885,X884,skolem0001(n1,n0,n0,n0,n1))|equalish(X887,n0),inference(resolution,[status(thm)],[c294, c9])).
% 4.21/4.40 cnf(c61,plain,~equalish(X237,X237)|~equalish(X238,X238)|~equalish(X239,X239)|f(X237,X238,X239,n0,X239,skolem0001(X237,X238,X239,n0,X239)),inference(resolution,[status(thm)],[c30, c21])).
% 4.21/4.40 cnf(c248,plain,~equalish(X618,X618)|~equalish(X617,X617)|f(X618,X617,n1,n0,n1,skolem0001(X618,X617,n1,n0,n1)),inference(resolution,[status(thm)],[c61, c22])).
% 4.21/4.40 cnf(c533,plain,~equalish(X882,X882)|f(X882,X882,n1,n0,n1,skolem0001(X882,X882,n1,n0,n1)),inference(factor,[status(thm)],[c248])).
% 4.21/4.40 cnf(c130,plain,~equalish(X317,X317)|f(X317,n1,n1,n1,X317,skolem0001(X317,n1,n1,n1,X317)),inference(resolution,[status(thm)],[c119, c22])).
% 4.21/4.40 cnf(c293,plain,f(n0,n1,n1,n1,n0,skolem0001(n0,n1,n1,n1,n0)),inference(resolution,[status(thm)],[c130, c21])).
% 4.21/4.40 cnf(c530,plain,~f(X880,X881,X878,X877,X879,skolem0001(n0,n1,n1,n1,n0))|equalish(X879,n0),inference(resolution,[status(thm)],[c293, c12])).
% 4.21/4.40 cnf(c529,plain,~f(X873,X872,X874,X875,X871,skolem0001(n0,n1,n1,n1,n0))|equalish(X875,n1),inference(resolution,[status(thm)],[c293, c11])).
% 4.21/4.40 cnf(c526,plain,~f(X869,X866,X867,X870,X868,skolem0001(n0,n1,n1,n1,n0))|equalish(X869,n0),inference(resolution,[status(thm)],[c293, c8])).
% 4.21/4.40 cnf(c525,plain,~f(X863,X861,X865,X864,X862,skolem0001(n0,n1,n1,n1,n0))|equalish(X865,n1),inference(resolution,[status(thm)],[c293, c10])).
% 4.21/4.40 cnf(c524,plain,~f(X855,X859,X858,X857,X856,skolem0001(n0,n1,n1,n1,n0))|equalish(X859,n1),inference(resolution,[status(thm)],[c293, c9])).
% 4.21/4.40 cnf(c60,plain,~equalish(X234,X234)|~equalish(X235,X235)|~equalish(X236,X236)|f(X234,X235,X236,n1,X236,skolem0001(X234,X235,X236,n1,X236)),inference(resolution,[status(thm)],[c30, c22])).
% 4.21/4.40 cnf(c245,plain,~equalish(X612,X612)|~equalish(X613,X613)|f(X612,X613,n0,n1,n0,skolem0001(X612,X613,n0,n1,n0)),inference(resolution,[status(thm)],[c60, c21])).
% 4.21/4.40 cnf(c517,plain,~equalish(X854,X854)|f(X854,X854,n0,n1,n0,skolem0001(X854,X854,n0,n1,n0)),inference(factor,[status(thm)],[c245])).
% 4.21/4.40 cnf(c288,plain,~equalish(X610,X610)|~equalish(X609,X609)|f(X610,X609,X610,X609,n1,skolem0001(X610,X609,X610,X609,n1)),inference(factor,[status(thm)],[c87])).
% 4.21/4.40 cnf(c516,plain,~equalish(X853,X853)|f(X853,n0,X853,n0,n1,skolem0001(X853,n0,X853,n0,n1)),inference(resolution,[status(thm)],[c288, c21])).
% 4.21/4.40 cnf(c279,plain,~equalish(X600,X600)|~equalish(X601,X601)|f(X600,X601,X601,X600,n1,skolem0001(X600,X601,X601,X600,n1)),inference(factor,[status(thm)],[c86])).
% 4.21/4.40 cnf(c509,plain,~equalish(X850,X850)|f(X850,n0,n0,X850,n1,skolem0001(X850,n0,n0,X850,n1)),inference(resolution,[status(thm)],[c279, c21])).
% 4.21/4.40 cnf(c43,plain,~equalish(X210,X210)|~equalish(X212,X212)|~equalish(X211,X211)|f(X210,X212,X211,n0,X212,skolem0001(X210,X212,X211,n0,X212)),inference(resolution,[status(thm)],[c29, c21])).
% 4.21/4.40 cnf(c207,plain,~equalish(X486,X486)|~equalish(X485,X485)|f(X486,X485,X485,n0,X485,skolem0001(X486,X485,X485,n0,X485)),inference(factor,[status(thm)],[c43])).
% 4.21/4.40 cnf(c455,plain,~equalish(X846,X846)|f(X846,n1,n1,n0,n1,skolem0001(X846,n1,n1,n0,n1)),inference(resolution,[status(thm)],[c207, c22])).
% 4.21/4.40 cnf(c42,plain,~equalish(X203,X203)|~equalish(X205,X205)|~equalish(X204,X204)|f(X203,X205,X204,n1,X205,skolem0001(X203,X205,X204,n1,X205)),inference(resolution,[status(thm)],[c29, c22])).
% 4.21/4.40 cnf(c193,plain,~equalish(X451,X451)|~equalish(X450,X450)|f(X451,X450,X450,n1,X450,skolem0001(X451,X450,X450,n1,X450)),inference(factor,[status(thm)],[c42])).
% 4.21/4.40 cnf(c441,plain,~equalish(X845,X845)|f(X845,n0,n0,n1,n0,skolem0001(X845,n0,n0,n1,n0)),inference(resolution,[status(thm)],[c193, c21])).
% 4.21/4.40 cnf(c479,plain,~equalish(X840,X840)|f(X840,n1,n0,X840,n0,skolem0001(X840,n1,n0,X840,n0)),inference(resolution,[status(thm)],[c213, c22])).
% 4.21/4.40 cnf(c41,plain,~equalish(X194,X194)|~equalish(X195,X195)|~equalish(X196,X196)|f(X194,X195,X196,X196,X195,skolem0001(X194,X195,X196,X196,X195)),inference(factor,[status(thm)],[c29])).
% 4.21/4.40 cnf(c184,plain,~equalish(X446,X446)|~equalish(X447,X447)|f(X446,X447,n0,n0,X447,skolem0001(X446,X447,n0,n0,X447)),inference(resolution,[status(thm)],[c41, c21])).
% 4.21/4.40 cnf(c437,plain,~equalish(X839,X839)|f(X839,n1,n0,n0,n1,skolem0001(X839,n1,n0,n0,n1)),inference(resolution,[status(thm)],[c184, c22])).
% 4.21/4.40 cnf(c473,plain,~equalish(X838,X838)|f(X838,n0,n1,X838,n1,skolem0001(X838,n0,n1,X838,n1)),inference(resolution,[status(thm)],[c212, c21])).
% 4.21/4.40 cnf(c183,plain,~equalish(X441,X441)|~equalish(X442,X442)|f(X441,X442,n1,n1,X442,skolem0001(X441,X442,n1,n1,X442)),inference(resolution,[status(thm)],[c41, c22])).
% 4.21/4.40 cnf(c432,plain,~equalish(X836,X836)|f(X836,n0,n1,n1,n0,skolem0001(X836,n0,n1,n1,n0)),inference(resolution,[status(thm)],[c183, c21])).
% 4.21/4.40 cnf(c206,plain,~equalish(X480,X480)|~equalish(X481,X481)|f(X480,X481,X480,n0,X481,skolem0001(X480,X481,X480,n0,X481)),inference(factor,[status(thm)],[c43])).
% 4.21/4.40 cnf(c452,plain,~equalish(X834,X834)|f(X834,n1,X834,n0,n1,skolem0001(X834,n1,X834,n0,n1)),inference(resolution,[status(thm)],[c206, c22])).
% 4.21/4.40 cnf(c171,plain,~equalish(X427,X427)|~equalish(X426,X426)|f(X427,X426,n0,X426,X426,skolem0001(X427,X426,n0,X426,X426)),inference(resolution,[status(thm)],[c40, c21])).
% 4.21/4.40 cnf(c390,plain,~equalish(X831,X831)|f(X831,n1,n0,n1,n1,skolem0001(X831,n1,n0,n1,n1)),inference(resolution,[status(thm)],[c171, c22])).
% 4.21/4.40 cnf(c192,plain,~equalish(X444,X444)|~equalish(X445,X445)|f(X444,X445,X444,n1,X445,skolem0001(X444,X445,X444,n1,X445)),inference(factor,[status(thm)],[c42])).
% 4.21/4.40 cnf(c435,plain,~equalish(X830,X830)|f(X830,n0,X830,n1,n0,skolem0001(X830,n0,X830,n1,n0)),inference(resolution,[status(thm)],[c192, c21])).
% 4.21/4.40 cnf(c164,plain,~equalish(X187,X187)|~equalish(X186,X186)|f(X187,X186,X187,X187,X186,skolem0001(X187,X186,X187,X187,X186)),inference(factor,[status(thm)],[c39])).
% 4.21/4.40 cnf(c174,plain,~equalish(X202,X202)|f(X202,n0,X202,X202,n0,skolem0001(X202,n0,X202,X202,n0)),inference(resolution,[status(thm)],[c164, c21])).
% 4.21/4.40 cnf(c190,plain,f(n1,n0,n1,n1,n0,skolem0001(n1,n0,n1,n1,n0)),inference(resolution,[status(thm)],[c174, c22])).
% 4.21/4.40 cnf(c427,plain,~f(X827,X828,X825,X824,X826,skolem0001(n1,n0,n1,n1,n0))|equalish(X826,n0),inference(resolution,[status(thm)],[c190, c12])).
% 4.21/4.40 cnf(c170,plain,~equalish(X422,X422)|~equalish(X421,X421)|f(X422,X421,n1,X421,X421,skolem0001(X422,X421,n1,X421,X421)),inference(resolution,[status(thm)],[c40, c22])).
% 4.21/4.40 cnf(c388,plain,~equalish(X823,X823)|f(X823,n0,n1,n0,n0,skolem0001(X823,n0,n1,n0,n0)),inference(resolution,[status(thm)],[c170, c21])).
% 4.21/4.40 cnf(c426,plain,~f(X820,X819,X821,X822,X818,skolem0001(n1,n0,n1,n1,n0))|equalish(X822,n1),inference(resolution,[status(thm)],[c190, c11])).
% 4.21/4.40 cnf(c423,plain,~f(X816,X813,X814,X817,X815,skolem0001(n1,n0,n1,n1,n0))|equalish(X816,n1),inference(resolution,[status(thm)],[c190, c8])).
% 4.21/4.40 cnf(c422,plain,~f(X809,X807,X811,X810,X808,skolem0001(n1,n0,n1,n1,n0))|equalish(X811,n1),inference(resolution,[status(thm)],[c190, c10])).
% 4.21/4.40 cnf(c421,plain,~f(X802,X806,X805,X804,X803,skolem0001(n1,n0,n1,n1,n0))|equalish(X806,n0),inference(resolution,[status(thm)],[c190, c9])).
% 4.21/4.40 cnf(c173,plain,~equalish(X201,X201)|f(X201,n1,X201,X201,n1,skolem0001(X201,n1,X201,X201,n1)),inference(resolution,[status(thm)],[c164, c22])).
% 4.21/4.40 cnf(c189,plain,f(n0,n1,n0,n0,n1,skolem0001(n0,n1,n0,n0,n1)),inference(resolution,[status(thm)],[c173, c21])).
% 4.21/4.40 cnf(c412,plain,~f(X796,X797,X794,X793,X795,skolem0001(n0,n1,n0,n0,n1))|equalish(X795,n1),inference(resolution,[status(thm)],[c189, c12])).
% 4.21/4.40 cnf(c411,plain,~f(X788,X787,X789,X790,X786,skolem0001(n0,n1,n0,n0,n1))|equalish(X790,n0),inference(resolution,[status(thm)],[c189, c11])).
% 4.21/4.40 cnf(c408,plain,~f(X784,X781,X782,X785,X783,skolem0001(n0,n1,n0,n0,n1))|equalish(X784,n0),inference(resolution,[status(thm)],[c189, c8])).
% 4.21/4.40 cnf(c106,plain,~equalish(X376,X376)|~equalish(X375,X375)|~equalish(X374,X374)|f(X376,X375,X374,n1,n0,skolem0001(X376,X375,X374,n1,n0)),inference(resolution,[status(thm)],[c33, c22])).
% 4.21/4.40 cnf(c359,plain,~equalish(X779,X779)|~equalish(X778,X778)|f(X779,X778,X778,n1,n0,skolem0001(X779,X778,X778,n1,n0)),inference(factor,[status(thm)],[c106])).
% 4.21/4.40 cnf(c407,plain,~f(X775,X773,X777,X776,X774,skolem0001(n0,n1,n0,n0,n1))|equalish(X777,n0),inference(resolution,[status(thm)],[c189, c10])).
% 4.21/4.40 cnf(c406,plain,~f(X768,X772,X771,X770,X769,skolem0001(n0,n1,n0,n0,n1))|equalish(X772,n1),inference(resolution,[status(thm)],[c189, c9])).
% 4.21/4.40 cnf(c358,plain,~equalish(X765,X765)|~equalish(X766,X766)|f(X765,X766,X765,n1,n0,skolem0001(X765,X766,X765,n1,n0)),inference(factor,[status(thm)],[c106])).
% 4.21/4.40 cnf(c716,plain,~equalish(X767,X767)|f(X767,X767,X767,n1,n0,skolem0001(X767,X767,X767,n1,n0)),inference(factor,[status(thm)],[c358])).
% 4.21/4.40 cnf(c342,plain,~equalish(X754,X754)|~equalish(X755,X755)|f(X754,X755,n1,X755,n0,skolem0001(X754,X755,n1,X755,n0)),inference(resolution,[status(thm)],[c104, c22])).
% 4.21/4.40 cnf(c333,plain,~equalish(X750,X750)|~equalish(X749,X749)|f(X750,X749,n1,X750,n0,skolem0001(X750,X749,n1,X750,n0)),inference(resolution,[status(thm)],[c103, c22])).
% 4.21/4.40 cnf(c675,plain,~equalish(X751,X751)|f(X751,X751,n1,X751,n0,skolem0001(X751,X751,n1,X751,n0)),inference(factor,[status(thm)],[c333])).
% 4.21/4.40 cnf(c167,plain,~equalish(X419,X419)|~equalish(X418,X418)|f(X419,X418,n0,X419,X418,skolem0001(X419,X418,n0,X419,X418)),inference(resolution,[status(thm)],[c39, c21])).
% 4.21/4.40 cnf(c384,plain,~equalish(X747,X747)|f(X747,n1,n0,X747,n1,skolem0001(X747,n1,n0,X747,n1)),inference(resolution,[status(thm)],[c167, c22])).
% 4.21/4.40 cnf(c379,plain,~equalish(X741,X741)|f(X741,n1,n0,n0,X741,skolem0001(X741,n1,n0,n0,X741)),inference(resolution,[status(thm)],[c128, c22])).
% 4.21/4.40 cnf(c90,plain,~equalish(X326,X326)|~equalish(X325,X325)|~equalish(X327,X327)|f(X326,X325,X327,n0,n1,skolem0001(X326,X325,X327,n0,n1)),inference(resolution,[status(thm)],[c32, c21])).
% 4.21/4.40 cnf(c321,plain,~equalish(X739,X739)|~equalish(X738,X738)|f(X739,X738,X738,n0,n1,skolem0001(X739,X738,X738,n0,n1)),inference(factor,[status(thm)],[c90])).
% 4.21/4.40 cnf(c166,plain,~equalish(X413,X413)|~equalish(X412,X412)|f(X413,X412,n1,X413,X412,skolem0001(X413,X412,n1,X413,X412)),inference(resolution,[status(thm)],[c39, c22])).
% 4.21/4.40 cnf(c377,plain,~equalish(X737,X737)|f(X737,n0,n1,X737,n0,skolem0001(X737,n0,n1,X737,n0)),inference(resolution,[status(thm)],[c166, c21])).
% 4.21/4.40 cnf(c320,plain,~equalish(X733,X733)|~equalish(X734,X734)|f(X733,X734,X733,n0,n1,skolem0001(X733,X734,X733,n0,n1)),inference(factor,[status(thm)],[c90])).
% 4.21/4.40 cnf(c641,plain,~equalish(X735,X735)|f(X735,X735,X735,n0,n1,skolem0001(X735,X735,X735,n0,n1)),inference(factor,[status(thm)],[c320])).
% 4.21/4.40 cnf(c371,plain,~equalish(X730,X730)|f(X730,n0,n1,n1,X730,skolem0001(X730,n0,n1,n1,X730)),inference(resolution,[status(thm)],[c127, c21])).
% 4.21/4.40 cnf(c151,plain,~equalish(X379,X379)|~equalish(X378,X378)|f(X379,X378,X378,n0,X379,skolem0001(X379,X378,X378,n0,X379)),inference(factor,[status(thm)],[c38])).
% 4.21/4.40 cnf(c363,plain,~equalish(X727,X727)|f(X727,n1,n1,n0,X727,skolem0001(X727,n1,n1,n0,X727)),inference(resolution,[status(thm)],[c151, c22])).
% 4.21/4.40 cnf(c291,plain,~equalish(X723,X723)|~equalish(X722,X722)|f(X723,X722,n0,X722,n1,skolem0001(X723,X722,n0,X722,n1)),inference(resolution,[status(thm)],[c87, c21])).
% 4.21/4.40 cnf(c281,plain,~equalish(X709,X709)|~equalish(X710,X710)|f(X709,X710,n0,X709,n1,skolem0001(X709,X710,n0,X709,n1)),inference(resolution,[status(thm)],[c86, c21])).
% 4.21/4.40 cnf(c603,plain,~equalish(X712,X712)|f(X712,X712,n0,X712,n1,skolem0001(X712,X712,n0,X712,n1)),inference(factor,[status(thm)],[c281])).
% 4.21/4.40 cnf(c137,plain,~equalish(X336,X336)|~equalish(X337,X337)|f(X336,X337,X337,n1,X336,skolem0001(X336,X337,X337,n1,X336)),inference(factor,[status(thm)],[c37])).
% 4.21/4.40 cnf(c337,plain,~equalish(X706,X706)|f(X706,n0,n0,n1,X706,skolem0001(X706,n0,n0,n1,X706)),inference(resolution,[status(thm)],[c137, c21])).
% 4.21/4.40 cnf(c589,plain,~equalish(X698,X698)|f(X698,n1,X698,X698,n0,skolem0001(X698,n1,X698,X698,n0)),inference(resolution,[status(thm)],[c331, c22])).
% 4.21/4.40 cnf(c118,plain,~equalish(X159,X159)|~equalish(X160,X160)|f(X159,X160,X159,X160,X159,skolem0001(X159,X160,X159,X160,X159)),inference(factor,[status(thm)],[c35])).
% 4.21/4.40 cnf(c124,plain,~equalish(X169,X169)|f(X169,n0,X169,n0,X169,skolem0001(X169,n0,X169,n0,X169)),inference(resolution,[status(thm)],[c118, c21])).
% 4.21/4.40 cnf(c134,plain,f(n1,n0,n1,n0,n1,skolem0001(n1,n0,n1,n0,n1)),inference(resolution,[status(thm)],[c124, c22])).
% 4.21/4.40 cnf(c318,plain,~f(X686,X683,X684,X687,X685,skolem0001(n1,n0,n1,n0,n1))|equalish(X686,n1),inference(resolution,[status(thm)],[c134, c8])).
% 4.21/4.40 cnf(c317,plain,~f(X680,X678,X682,X681,X679,skolem0001(n1,n0,n1,n0,n1))|equalish(X682,n1),inference(resolution,[status(thm)],[c134, c10])).
% 4.21/4.40 cnf(c316,plain,~f(X670,X674,X673,X672,X671,skolem0001(n1,n0,n1,n0,n1))|equalish(X674,n0),inference(resolution,[status(thm)],[c134, c9])).
% 4.21/4.40 cnf(c314,plain,~f(X667,X666,X668,X669,X665,skolem0001(n1,n0,n1,n0,n1))|equalish(X669,n0),inference(resolution,[status(thm)],[c134, c11])).
% 4.21/4.40 cnf(c310,plain,~f(X663,X664,X661,X660,X662,skolem0001(n1,n0,n1,n0,n1))|equalish(X662,n1),inference(resolution,[status(thm)],[c134, c12])).
% 4.21/4.40 cnf(c123,plain,~equalish(X168,X168)|f(X168,n1,X168,n1,X168,skolem0001(X168,n1,X168,n1,X168)),inference(resolution,[status(thm)],[c118, c22])).
% 4.21/4.40 cnf(c133,plain,f(n0,n1,n0,n1,n0,skolem0001(n0,n1,n0,n1,n0)),inference(resolution,[status(thm)],[c123, c21])).
% 4.21/4.40 cnf(c304,plain,~f(X652,X649,X650,X653,X651,skolem0001(n0,n1,n0,n1,n0))|equalish(X652,n0),inference(resolution,[status(thm)],[c133, c8])).
% 4.21/4.40 cnf(c303,plain,~f(X644,X642,X646,X645,X643,skolem0001(n0,n1,n0,n1,n0))|equalish(X646,n0),inference(resolution,[status(thm)],[c133, c10])).
% 4.21/4.40 cnf(c302,plain,~f(X637,X641,X640,X639,X638,skolem0001(n0,n1,n0,n1,n0))|equalish(X641,n1),inference(resolution,[status(thm)],[c133, c9])).
% 4.21/4.40 cnf(c300,plain,~f(X631,X630,X632,X633,X629,skolem0001(n0,n1,n0,n1,n0))|equalish(X633,n1),inference(resolution,[status(thm)],[c133, c11])).
% 4.21/4.40 cnf(c296,plain,~f(X627,X628,X625,X624,X626,skolem0001(n0,n1,n0,n1,n0))|equalish(X626,n0),inference(resolution,[status(thm)],[c133, c12])).
% 4.21/4.40 cnf(c121,plain,~equalish(X311,X311)|~equalish(X312,X312)|f(X311,X312,n0,X312,X311,skolem0001(X311,X312,n0,X312,X311)),inference(resolution,[status(thm)],[c35, c21])).
% 4.21/4.40 cnf(c286,plain,~equalish(X607,X607)|f(X607,n1,n0,n1,X607,skolem0001(X607,n1,n0,n1,X607)),inference(resolution,[status(thm)],[c121, c22])).
% 4.21/4.40 cnf(c120,plain,~equalish(X308,X308)|~equalish(X309,X309)|f(X308,X309,n1,X309,X308,skolem0001(X308,X309,n1,X309,X308)),inference(resolution,[status(thm)],[c35, c22])).
% 4.21/4.40 cnf(c284,plain,~equalish(X606,X606)|f(X606,n0,n1,n0,X606,skolem0001(X606,n0,n1,n0,X606)),inference(resolution,[status(thm)],[c120, c21])).
% 4.21/4.40 cnf(c499,plain,~equalish(X599,X599)|f(X599,n0,X599,X599,n1,skolem0001(X599,n0,X599,X599,n1)),inference(resolution,[status(thm)],[c278, c21])).
% 4.21/4.40 cnf(c34,plain,~equalish(X119,X119)|~equalish(X118,X118)|~equalish(X117,X117)|f(X119,X118,X117,X119,X119,skolem0001(X119,X118,X117,X119,X119)),inference(factor,[status(thm)],[c28])).
% 4.21/4.40 cnf(c47,plain,~equalish(X143,X143)|~equalish(X144,X144)|f(X143,X144,n0,X143,X143,skolem0001(X143,X144,n0,X143,X143)),inference(resolution,[status(thm)],[c34, c21])).
% 4.21/4.40 cnf(c81,plain,~equalish(X145,X145)|f(X145,X145,n0,X145,X145,skolem0001(X145,X145,n0,X145,X145)),inference(factor,[status(thm)],[c47])).
% 4.21/4.40 cnf(c84,plain,f(n1,n1,n0,n1,n1,skolem0001(n1,n1,n0,n1,n1)),inference(resolution,[status(thm)],[c81, c22])).
% 4.21/4.40 cnf(c258,plain,~f(X591,X588,X589,X592,X590,skolem0001(n1,n1,n0,n1,n1))|equalish(X591,n1),inference(resolution,[status(thm)],[c84, c8])).
% 4.21/4.40 cnf(c257,plain,~f(X583,X581,X585,X584,X582,skolem0001(n1,n1,n0,n1,n1))|equalish(X585,n0),inference(resolution,[status(thm)],[c84, c10])).
% 4.21/4.40 cnf(c256,plain,~f(X576,X580,X579,X578,X577,skolem0001(n1,n1,n0,n1,n1))|equalish(X580,n1),inference(resolution,[status(thm)],[c84, c9])).
% 4.21/4.40 cnf(c254,plain,~f(X570,X569,X571,X572,X568,skolem0001(n1,n1,n0,n1,n1))|equalish(X572,n1),inference(resolution,[status(thm)],[c84, c11])).
% 4.21/4.40 cnf(c250,plain,~f(X566,X567,X564,X563,X565,skolem0001(n1,n1,n0,n1,n1))|equalish(X565,n1),inference(resolution,[status(thm)],[c84, c12])).
% 4.21/4.40 cnf(c46,plain,~equalish(X134,X134)|~equalish(X135,X135)|f(X134,X135,n1,X134,X134,skolem0001(X134,X135,n1,X134,X134)),inference(resolution,[status(thm)],[c34, c22])).
% 4.21/4.40 cnf(c69,plain,~equalish(X140,X140)|f(X140,X140,n1,X140,X140,skolem0001(X140,X140,n1,X140,X140)),inference(factor,[status(thm)],[c46])).
% 4.21/4.40 cnf(c78,plain,f(n0,n0,n1,n0,n0,skolem0001(n0,n0,n1,n0,n0)),inference(resolution,[status(thm)],[c69, c21])).
% 4.21/4.40 cnf(c240,plain,~f(X547,X544,X545,X548,X546,skolem0001(n0,n0,n1,n0,n0))|equalish(X547,n0),inference(resolution,[status(thm)],[c78, c8])).
% 4.21/4.40 cnf(c239,plain,~f(X541,X539,X543,X542,X540,skolem0001(n0,n0,n1,n0,n0))|equalish(X543,n1),inference(resolution,[status(thm)],[c78, c10])).
% 4.21/4.40 cnf(c238,plain,~f(X531,X535,X534,X533,X532,skolem0001(n0,n0,n1,n0,n0))|equalish(X535,n0),inference(resolution,[status(thm)],[c78, c9])).
% 4.21/4.40 cnf(c236,plain,~f(X528,X527,X529,X530,X526,skolem0001(n0,n0,n1,n0,n0))|equalish(X530,n0),inference(resolution,[status(thm)],[c78, c11])).
% 4.21/4.40 cnf(c232,plain,~f(X524,X525,X522,X521,X523,skolem0001(n0,n0,n1,n0,n0))|equalish(X523,n0),inference(resolution,[status(thm)],[c78, c12])).
% 4.21/4.40 cnf(c45,plain,~equalish(X129,X129)|~equalish(X130,X130)|f(X129,X130,X130,X129,X129,skolem0001(X129,X130,X130,X129,X129)),inference(factor,[status(thm)],[c34])).
% 4.21/4.40 cnf(c64,plain,~equalish(X133,X133)|f(X133,n0,n0,X133,X133,skolem0001(X133,n0,n0,X133,X133)),inference(resolution,[status(thm)],[c45, c21])).
% 4.21/4.40 cnf(c67,plain,f(n1,n0,n0,n1,n1,skolem0001(n1,n0,n0,n1,n1)),inference(resolution,[status(thm)],[c64, c22])).
% 4.21/4.40 cnf(c222,plain,~f(X517,X514,X515,X518,X516,skolem0001(n1,n0,n0,n1,n1))|equalish(X517,n1),inference(resolution,[status(thm)],[c67, c8])).
% 4.21/4.40 cnf(c221,plain,~f(X511,X509,X513,X512,X510,skolem0001(n1,n0,n0,n1,n1))|equalish(X513,n0),inference(resolution,[status(thm)],[c67, c10])).
% 4.21/4.40 cnf(c208,plain,~equalish(X506,X506)|~equalish(X507,X507)|f(X506,X507,n1,n0,X507,skolem0001(X506,X507,n1,n0,X507)),inference(resolution,[status(thm)],[c43, c22])).
% 4.21/4.40 cnf(c220,plain,~f(X501,X505,X504,X503,X502,skolem0001(n1,n0,n0,n1,n1))|equalish(X505,n0),inference(resolution,[status(thm)],[c67, c9])).
% 4.21/4.40 cnf(c218,plain,~f(X498,X497,X499,X500,X496,skolem0001(n1,n0,n0,n1,n1))|equalish(X500,n1),inference(resolution,[status(thm)],[c67, c11])).
% 4.21/4.40 cnf(c195,plain,~equalish(X493,X493)|~equalish(X494,X494)|f(X493,X494,n0,n1,X494,skolem0001(X493,X494,n0,n1,X494)),inference(resolution,[status(thm)],[c42, c21])).
% 4.21/4.40 cnf(c214,plain,~f(X491,X492,X489,X488,X490,skolem0001(n1,n0,n0,n1,n1))|equalish(X490,n1),inference(resolution,[status(thm)],[c67, c12])).
% 4.21/4.40 cnf(c63,plain,~equalish(X132,X132)|f(X132,n1,n1,X132,X132,skolem0001(X132,n1,n1,X132,X132)),inference(resolution,[status(thm)],[c45, c22])).
% 4.21/4.40 cnf(c66,plain,f(n0,n1,n1,n0,n0,skolem0001(n0,n1,n1,n0,n0)),inference(resolution,[status(thm)],[c63, c21])).
% 4.21/4.40 cnf(c204,plain,~f(X478,X475,X476,X479,X477,skolem0001(n0,n1,n1,n0,n0))|equalish(X478,n0),inference(resolution,[status(thm)],[c66, c8])).
% 4.21/4.40 cnf(c203,plain,~f(X472,X470,X474,X473,X471,skolem0001(n0,n1,n1,n0,n0))|equalish(X474,n1),inference(resolution,[status(thm)],[c66, c10])).
% 4.21/4.40 cnf(c202,plain,~f(X464,X468,X467,X466,X465,skolem0001(n0,n1,n1,n0,n0))|equalish(X468,n1),inference(resolution,[status(thm)],[c66, c9])).
% 4.21/4.40 cnf(c200,plain,~f(X461,X460,X462,X463,X459,skolem0001(n0,n1,n1,n0,n0))|equalish(X463,n0),inference(resolution,[status(thm)],[c66, c11])).
% 4.21/4.40 cnf(c196,plain,~f(X456,X457,X454,X453,X455,skolem0001(n0,n1,n1,n0,n0))|equalish(X455,n0),inference(resolution,[status(thm)],[c66, c12])).
% 4.21/4.40 cnf(c152,plain,~equalish(X437,X437)|~equalish(X436,X436)|f(X437,X436,n1,n0,X437,skolem0001(X437,X436,n1,n0,X437)),inference(resolution,[status(thm)],[c38, c22])).
% 4.21/4.40 cnf(c415,plain,~equalish(X440,X440)|f(X440,X440,n1,n0,X440,skolem0001(X440,X440,n1,n0,X440)),inference(factor,[status(thm)],[c152])).
% 4.21/4.40 cnf(c139,plain,~equalish(X431,X431)|~equalish(X432,X432)|f(X431,X432,n0,n1,X431,skolem0001(X431,X432,n0,n1,X431)),inference(resolution,[status(thm)],[c37, c21])).
% 4.21/4.40 cnf(c396,plain,~equalish(X433,X433)|f(X433,X433,n0,n1,X433,skolem0001(X433,X433,n0,n1,X433)),inference(factor,[status(thm)],[c139])).
% 4.21/4.40 cnf(c44,plain,~equalish(X121,X121)|~equalish(X120,X120)|f(X121,X120,X121,X121,X121,skolem0001(X121,X120,X121,X121,X121)),inference(factor,[status(thm)],[c34])).
% 4.21/4.40 cnf(c50,plain,~equalish(X124,X124)|f(X124,n0,X124,X124,X124,skolem0001(X124,n0,X124,X124,X124)),inference(resolution,[status(thm)],[c44, c21])).
% 4.21/4.40 cnf(c55,plain,f(n1,n0,n1,n1,n1,skolem0001(n1,n0,n1,n1,n1)),inference(resolution,[status(thm)],[c50, c22])).
% 4.21/4.40 cnf(c162,plain,~f(X410,X407,X408,X411,X409,skolem0001(n1,n0,n1,n1,n1))|equalish(X410,n1),inference(resolution,[status(thm)],[c55, c8])).
% 4.21/4.40 cnf(c161,plain,~f(X401,X399,X403,X402,X400,skolem0001(n1,n0,n1,n1,n1))|equalish(X403,n1),inference(resolution,[status(thm)],[c55, c10])).
% 4.21/4.40 cnf(c160,plain,~f(X394,X398,X397,X396,X395,skolem0001(n1,n0,n1,n1,n1))|equalish(X398,n0),inference(resolution,[status(thm)],[c55, c9])).
% 4.21/4.40 cnf(c158,plain,~f(X391,X390,X392,X393,X389,skolem0001(n1,n0,n1,n1,n1))|equalish(X393,n1),inference(resolution,[status(thm)],[c55, c11])).
% 4.21/4.40 cnf(c154,plain,~f(X384,X385,X382,X381,X383,skolem0001(n1,n0,n1,n1,n1))|equalish(X383,n1),inference(resolution,[status(thm)],[c55, c12])).
% 4.21/4.40 cnf(c352,plain,~equalish(X373,X373)|f(X373,n1,X373,n0,X373,skolem0001(X373,n1,X373,n0,X373)),inference(resolution,[status(thm)],[c150, c22])).
% 4.21/4.40 cnf(c49,plain,~equalish(X123,X123)|f(X123,n1,X123,X123,X123,skolem0001(X123,n1,X123,X123,X123)),inference(resolution,[status(thm)],[c44, c22])).
% 4.21/4.40 cnf(c54,plain,f(n0,n1,n0,n0,n0,skolem0001(n0,n1,n0,n0,n0)),inference(resolution,[status(thm)],[c49, c21])).
% 4.21/4.40 cnf(c148,plain,~f(X368,X365,X366,X369,X367,skolem0001(n0,n1,n0,n0,n0))|equalish(X368,n0),inference(resolution,[status(thm)],[c54, c8])).
% 4.21/4.40 cnf(c147,plain,~f(X359,X357,X361,X360,X358,skolem0001(n0,n1,n0,n0,n0))|equalish(X361,n0),inference(resolution,[status(thm)],[c54, c10])).
% 4.21/4.40 cnf(c146,plain,~f(X352,X356,X355,X354,X353,skolem0001(n0,n1,n0,n0,n0))|equalish(X356,n1),inference(resolution,[status(thm)],[c54, c9])).
% 4.21/4.40 cnf(c144,plain,~f(X346,X345,X347,X348,X344,skolem0001(n0,n1,n0,n0,n0))|equalish(X348,n0),inference(resolution,[status(thm)],[c54, c11])).
% 4.21/4.40 cnf(c140,plain,~f(X342,X343,X340,X339,X341,skolem0001(n0,n1,n0,n0,n0))|equalish(X341,n0),inference(resolution,[status(thm)],[c54, c12])).
% 4.21/4.40 cnf(c326,plain,~equalish(X332,X332)|f(X332,n0,X332,n1,X332,skolem0001(X332,n0,X332,n1,X332)),inference(resolution,[status(thm)],[c136, c21])).
% 4.21/4.40 cnf(c48,plain,~equalish(X122,X122)|f(X122,X122,X122,X122,X122,skolem0001(X122,X122,X122,X122,X122)),inference(factor,[status(thm)],[c44])).
% 4.21/4.40 cnf(c52,plain,f(n0,n0,n0,n0,n0,skolem0001(n0,n0,n0,n0,n0)),inference(resolution,[status(thm)],[c48, c21])).
% 4.21/4.40 cnf(c116,plain,~f(X303,X300,X301,X304,X302,skolem0001(n0,n0,n0,n0,n0))|equalish(X303,n0),inference(resolution,[status(thm)],[c52, c8])).
% 4.21/4.40 cnf(c115,plain,~f(X297,X295,X299,X298,X296,skolem0001(n0,n0,n0,n0,n0))|equalish(X299,n0),inference(resolution,[status(thm)],[c52, c10])).
% 4.21/4.40 cnf(c114,plain,~f(X290,X294,X293,X292,X291,skolem0001(n0,n0,n0,n0,n0))|equalish(X294,n0),inference(resolution,[status(thm)],[c52, c9])).
% 4.21/4.40 cnf(c112,plain,~f(X284,X283,X285,X286,X282,skolem0001(n0,n0,n0,n0,n0))|equalish(X286,n0),inference(resolution,[status(thm)],[c52, c11])).
% 4.21/4.40 cnf(c108,plain,~f(X280,X281,X278,X277,X279,skolem0001(n0,n0,n0,n0,n0))|equalish(X279,n0),inference(resolution,[status(thm)],[c52, c12])).
% 4.21/4.40 cnf(c51,plain,f(n1,n1,n1,n1,n1,skolem0001(n1,n1,n1,n1,n1)),inference(resolution,[status(thm)],[c48, c22])).
% 4.21/4.40 cnf(c101,plain,~f(X272,X269,X270,X273,X271,skolem0001(n1,n1,n1,n1,n1))|equalish(X272,n1),inference(resolution,[status(thm)],[c51, c8])).
% 4.21/4.40 cnf(c100,plain,~f(X266,X264,X268,X267,X265,skolem0001(n1,n1,n1,n1,n1))|equalish(X268,n1),inference(resolution,[status(thm)],[c51, c10])).
% 4.21/4.40 cnf(c99,plain,~f(X259,X263,X262,X261,X260,skolem0001(n1,n1,n1,n1,n1))|equalish(X263,n1),inference(resolution,[status(thm)],[c51, c9])).
% 4.21/4.40 cnf(c97,plain,~f(X253,X252,X254,X255,X251,skolem0001(n1,n1,n1,n1,n1))|equalish(X255,n1),inference(resolution,[status(thm)],[c51, c11])).
% 4.21/4.40 cnf(c93,plain,~f(X249,X250,X247,X246,X248,skolem0001(n1,n1,n1,n1,n1))|equalish(X248,n1),inference(resolution,[status(thm)],[c51, c12])).
% 4.21/4.40 cnf(c82,plain,~equalish(X150,X150)|f(X150,n1,n0,X150,X150,skolem0001(X150,n1,n0,X150,X150)),inference(resolution,[status(thm)],[c47, c22])).
% 4.21/4.40 cnf(c71,plain,~equalish(X142,X142)|f(X142,n0,n1,X142,X142,skolem0001(X142,n0,n1,X142,X142)),inference(resolution,[status(thm)],[c46, c21])).
% 4.21/4.40 cnf(c27,plain,~f(X99,X103,X101,X100,X102,X98)|equalish(X102,X102),inference(factor,[status(thm)],[c12])).
% 4.21/4.40 cnf(c26,plain,~f(X84,X86,X82,X83,X81,X85)|equalish(X83,X83),inference(factor,[status(thm)],[c11])).
% 4.21/4.40 cnf(c25,plain,~f(X64,X67,X65,X68,X66,X69)|equalish(X65,X65),inference(factor,[status(thm)],[c10])).
% 4.21/4.40 cnf(c24,plain,~f(X50,X51,X47,X49,X48,X52)|equalish(X51,X51),inference(factor,[status(thm)],[c9])).
% 4.21/4.40 cnf(c23,plain,~f(X32,X31,X33,X30,X34,X35)|equalish(X32,X32),inference(factor,[status(thm)],[c8])).
% 4.21/4.40 fof(n0_equal_n1,axiom,(equalish(n0,n1)=>goal),file('/export/starexec/sandbox/benchmark/theBenchmark.p', n0_equal_n1)).
% 4.21/4.40 fof(c19,plain,(~equalish(n0,n1)|goal),inference(fof_nnf,[status(thm)],[n0_equal_n1])).
% 4.21/4.40 cnf(c20,plain,~equalish(n0,n1)|goal,inference(split_conjunct,[status(thm)],[c19])).
% 4.21/4.40 fof(n1_equal_n0,axiom,(equalish(n1,n0)=>goal),file('/export/starexec/sandbox/benchmark/theBenchmark.p', n1_equal_n0)).
% 4.21/4.40 fof(c17,plain,(~equalish(n1,n0)|goal),inference(fof_nnf,[status(thm)],[n1_equal_n0])).
% 4.21/4.40 cnf(c18,plain,~equalish(n1,n0)|goal,inference(split_conjunct,[status(thm)],[c17])).
% 4.21/4.40 fof(goal_to_be_proved,conjecture,goal,file('/export/starexec/sandbox/benchmark/theBenchmark.p', goal_to_be_proved)).
% 4.21/4.40 fof(c0,negated_conjecture,(~goal),inference(assume_negation,[status(cth)],[goal_to_be_proved])).
% 4.21/4.40 fof(c1,negated_conjecture,~goal,inference(fof_simplification,[status(thm)],[c0])).
% 4.21/4.40 cnf(c2,negated_conjecture,~goal,inference(split_conjunct,[status(thm)],[c1])).
% 4.21/4.40 % SZS output end Saturation
% 4.21/4.40
% 4.21/4.40 % Initial clauses : 11
% 4.21/4.40 % Processed clauses : 384
% 4.21/4.40 % Factors computed : 141
% 4.21/4.40 % Resolvents computed: 834
% 4.21/4.40 % Tautologies deleted: 0
% 4.21/4.40 % Forward subsumed : 602
% 4.21/4.40 % Backward subsumed : 0
% 4.21/4.40 % -------- CPU Time ---------
% 4.21/4.40 % User time : 4.093 s
% 4.21/4.40 % System time : 0.018 s
% 4.21/4.40 % Total time : 4.111 s
%------------------------------------------------------------------------------