%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MSC014+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:33:24 EDT 2024
% Result : Satisfiable 0.98s 1.17s
% Output : Saturation 0.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : MSC014+1 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 13:57:07 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.98/1.17 % Version: 1.5
% 0.98/1.17 % SZS status Satisfiable
% 0.98/1.17 % SZS output start Saturation
% 0.98/1.17 fof(inject_f,axiom,(![X1]:(![X2]:(![X3]:(![X4]:(![Y1]:(![Y2]:(![Y3]:(![Y4]:(![Z]:((f(X1,X2,X3,X4,Z)&f(Y1,Y2,Y3,Y4,Z))=>(((equalish(X1,Y1)&equalish(X2,Y2))&equalish(X3,Y3))&equalish(X4,Y4)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', inject_f)).
% 0.98/1.17 fof(c0,plain,(![X1]:(![X2]:(![X3]:(![X4]:(![Y1]:(![Y2]:(![Y3]:(![Y4]:(![Z]:((~f(X1,X2,X3,X4,Z)|~f(Y1,Y2,Y3,Y4,Z))|(((equalish(X1,Y1)&equalish(X2,Y2))&equalish(X3,Y3))&equalish(X4,Y4)))))))))))),inference(fof_nnf,[status(thm)],[inject_f])).
% 0.98/1.17 fof(c1,plain,(![X1]:(![X2]:(![X3]:(![X4]:(![Y1]:(![Y2]:(![Y3]:(![Y4]:((![Z]:(~f(X1,X2,X3,X4,Z)|~f(Y1,Y2,Y3,Y4,Z)))|(((equalish(X1,Y1)&equalish(X2,Y2))&equalish(X3,Y3))&equalish(X4,Y4))))))))))),inference(shift_quantors,[status(thm)],[c0])).
% 0.98/1.17 fof(c3,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((~f(X2,X3,X4,X5,X10)|~f(X6,X7,X8,X9,X10))|(((equalish(X2,X6)&equalish(X3,X7))&equalish(X4,X8))&equalish(X5,X9)))))))))))),inference(shift_quantors,[status(thm)],[fof(c2,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((![X10]:(~f(X2,X3,X4,X5,X10)|~f(X6,X7,X8,X9,X10)))|(((equalish(X2,X6)&equalish(X3,X7))&equalish(X4,X8))&equalish(X5,X9))))))))))),inference(variable_rename,[status(thm)],[c1])).])).
% 0.98/1.17 fof(c4,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(((((~f(X2,X3,X4,X5,X10)|~f(X6,X7,X8,X9,X10))|equalish(X2,X6))&((~f(X2,X3,X4,X5,X10)|~f(X6,X7,X8,X9,X10))|equalish(X3,X7)))&((~f(X2,X3,X4,X5,X10)|~f(X6,X7,X8,X9,X10))|equalish(X4,X8)))&((~f(X2,X3,X4,X5,X10)|~f(X6,X7,X8,X9,X10))|equalish(X5,X9)))))))))))),inference(distribute,[status(thm)],[c3])).
% 0.98/1.17 cnf(c8,plain,~f(X66,X64,X61,X58,X65)|~f(X60,X59,X63,X62,X65)|equalish(X58,X62),inference(split_conjunct,[status(thm)],[c4])).
% 0.98/1.17 fof(n0_and_n1_reflexive,axiom,(equalish(n0,n0)&equalish(n1,n1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', n0_and_n1_reflexive)).
% 0.98/1.17 cnf(c17,plain,equalish(n1,n1),inference(split_conjunct,[status(thm)],[n0_and_n1_reflexive])).
% 0.98/1.17 cnf(c16,plain,equalish(n0,n0),inference(split_conjunct,[status(thm)],[n0_and_n1_reflexive])).
% 0.98/1.17 fof(exists_f,axiom,(![X1]:(![X2]:(![X3]:(![X4]:((((equalish(X1,X1)&equalish(X2,X2))&equalish(X3,X3))&equalish(X4,X4))=>(?[Z]:f(X1,X2,X3,X4,Z))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exists_f)).
% 0.98/1.17 fof(c9,plain,(![X1]:(![X2]:(![X3]:(![X4]:((((~equalish(X1,X1)|~equalish(X2,X2))|~equalish(X3,X3))|~equalish(X4,X4))|(?[Z]:f(X1,X2,X3,X4,Z))))))),inference(fof_nnf,[status(thm)],[exists_f])).
% 0.98/1.17 fof(c10,plain,(![X11]:(![X12]:(![X13]:(![X14]:((((~equalish(X11,X11)|~equalish(X12,X12))|~equalish(X13,X13))|~equalish(X14,X14))|(?[X15]:f(X11,X12,X13,X14,X15))))))),inference(variable_rename,[status(thm)],[c9])).
% 0.98/1.17 fof(c11,plain,(![X11]:(![X12]:(![X13]:(![X14]:((((~equalish(X11,X11)|~equalish(X12,X12))|~equalish(X13,X13))|~equalish(X14,X14))|f(X11,X12,X13,X14,skolem0001(X11,X12,X13,X14))))))),inference(skolemize,[status(esa)],[c10])).
% 0.98/1.17 cnf(c12,plain,~equalish(X68,X68)|~equalish(X67,X67)|~equalish(X69,X69)|~equalish(X70,X70)|f(X68,X67,X69,X70,skolem0001(X68,X67,X69,X70)),inference(split_conjunct,[status(thm)],[c11])).
% 0.98/1.17 cnf(c23,plain,~equalish(X83,X83)|~equalish(X85,X85)|~equalish(X84,X84)|f(X83,X85,X84,X85,skolem0001(X83,X85,X84,X85)),inference(factor,[status(thm)],[c12])).
% 0.98/1.17 cnf(c39,plain,~equalish(X105,X105)|~equalish(X106,X106)|f(X105,X106,X106,X106,skolem0001(X105,X106,X106,X106)),inference(factor,[status(thm)],[c23])).
% 0.98/1.17 cnf(c93,plain,~equalish(X222,X222)|f(X222,n0,n0,n0,skolem0001(X222,n0,n0,n0)),inference(resolution,[status(thm)],[c39, c16])).
% 0.98/1.17 cnf(c270,plain,f(n1,n0,n0,n0,skolem0001(n1,n0,n0,n0)),inference(resolution,[status(thm)],[c93, c17])).
% 0.98/1.17 cnf(c279,plain,~f(X433,X431,X434,X432,skolem0001(n1,n0,n0,n0))|equalish(X432,n0),inference(resolution,[status(thm)],[c270, c8])).
% 0.98/1.17 cnf(c5,plain,~f(X24,X22,X19,X16,X23)|~f(X18,X17,X21,X20,X23)|equalish(X24,X18),inference(split_conjunct,[status(thm)],[c4])).
% 0.98/1.17 cnf(c277,plain,~f(X428,X426,X427,X429,skolem0001(n1,n0,n0,n0))|equalish(X428,n1),inference(resolution,[status(thm)],[c270, c5])).
% 0.98/1.17 cnf(c7,plain,~f(X52,X50,X47,X44,X51)|~f(X46,X45,X49,X48,X51)|equalish(X47,X49),inference(split_conjunct,[status(thm)],[c4])).
% 0.98/1.17 cnf(c276,plain,~f(X424,X423,X425,X422,skolem0001(n1,n0,n0,n0))|equalish(X425,n0),inference(resolution,[status(thm)],[c270, c7])).
% 0.98/1.17 cnf(c6,plain,~f(X33,X31,X28,X25,X32)|~f(X27,X26,X30,X29,X32)|equalish(X31,X26),inference(split_conjunct,[status(thm)],[c4])).
% 0.98/1.17 cnf(c274,plain,~f(X420,X419,X418,X417,skolem0001(n1,n0,n0,n0))|equalish(X419,n0),inference(resolution,[status(thm)],[c270, c6])).
% 0.98/1.17 cnf(c92,plain,~equalish(X221,X221)|f(X221,n1,n1,n1,skolem0001(X221,n1,n1,n1)),inference(resolution,[status(thm)],[c39, c17])).
% 0.98/1.17 cnf(c261,plain,f(n0,n1,n1,n1,skolem0001(n0,n1,n1,n1)),inference(resolution,[status(thm)],[c92, c16])).
% 0.98/1.17 cnf(c269,plain,~f(X415,X413,X416,X414,skolem0001(n0,n1,n1,n1))|equalish(X414,n1),inference(resolution,[status(thm)],[c261, c8])).
% 0.98/1.17 cnf(c267,plain,~f(X411,X409,X410,X412,skolem0001(n0,n1,n1,n1))|equalish(X411,n0),inference(resolution,[status(thm)],[c261, c5])).
% 0.98/1.17 cnf(c266,plain,~f(X406,X405,X407,X404,skolem0001(n0,n1,n1,n1))|equalish(X407,n1),inference(resolution,[status(thm)],[c261, c7])).
% 0.98/1.17 cnf(c26,plain,~equalish(X96,X96)|~equalish(X98,X98)|~equalish(X97,X97)|f(X96,X98,X97,n0,skolem0001(X96,X98,X97,n0)),inference(resolution,[status(thm)],[c12, c16])).
% 0.98/1.17 cnf(c80,plain,~equalish(X202,X202)|~equalish(X201,X201)|f(X202,X201,X201,n0,skolem0001(X202,X201,X201,n0)),inference(factor,[status(thm)],[c26])).
% 0.98/1.17 cnf(c250,plain,~equalish(X403,X403)|f(X403,n1,n1,n0,skolem0001(X403,n1,n1,n0)),inference(resolution,[status(thm)],[c80, c17])).
% 0.98/1.17 cnf(c264,plain,~f(X402,X401,X400,X399,skolem0001(n0,n1,n1,n1))|equalish(X401,n1),inference(resolution,[status(thm)],[c261, c6])).
% 0.98/1.17 cnf(c79,plain,~equalish(X197,X197)|~equalish(X196,X196)|f(X197,X196,X197,n0,skolem0001(X197,X196,X197,n0)),inference(factor,[status(thm)],[c26])).
% 0.98/1.17 cnf(c234,plain,~equalish(X198,X198)|f(X198,X198,X198,n0,skolem0001(X198,X198,X198,n0)),inference(factor,[status(thm)],[c79])).
% 0.98/1.17 cnf(c237,plain,f(n1,n1,n1,n0,skolem0001(n1,n1,n1,n0)),inference(resolution,[status(thm)],[c234, c17])).
% 0.98/1.17 cnf(c247,plain,~f(X397,X396,X398,X395,skolem0001(n1,n1,n1,n0))|equalish(X398,n1),inference(resolution,[status(thm)],[c237, c7])).
% 0.98/1.17 cnf(c246,plain,~f(X393,X391,X394,X392,skolem0001(n1,n1,n1,n0))|equalish(X392,n0),inference(resolution,[status(thm)],[c237, c8])).
% 0.98/1.17 cnf(c245,plain,~f(X389,X387,X388,X390,skolem0001(n1,n1,n1,n0))|equalish(X389,n1),inference(resolution,[status(thm)],[c237, c5])).
% 0.98/1.17 cnf(c243,plain,~f(X386,X385,X384,X383,skolem0001(n1,n1,n1,n0))|equalish(X385,n1),inference(resolution,[status(thm)],[c237, c6])).
% 0.98/1.17 cnf(c24,plain,~equalish(X90,X90)|~equalish(X92,X92)|~equalish(X91,X91)|f(X90,X92,X91,X91,skolem0001(X90,X92,X91,X91)),inference(factor,[status(thm)],[c12])).
% 0.98/1.17 cnf(c58,plain,~equalish(X147,X147)|~equalish(X148,X148)|f(X147,X148,n0,n0,skolem0001(X147,X148,n0,n0)),inference(resolution,[status(thm)],[c24, c16])).
% 0.98/1.17 cnf(c156,plain,~equalish(X169,X169)|f(X169,X169,n0,n0,skolem0001(X169,X169,n0,n0)),inference(factor,[status(thm)],[c58])).
% 0.98/1.17 cnf(c194,plain,f(n1,n1,n0,n0,skolem0001(n1,n1,n0,n0)),inference(resolution,[status(thm)],[c156, c17])).
% 0.98/1.17 cnf(c226,plain,~f(X381,X380,X382,X379,skolem0001(n1,n1,n0,n0))|equalish(X382,n0),inference(resolution,[status(thm)],[c194, c7])).
% 0.98/1.17 cnf(c225,plain,~f(X376,X374,X377,X375,skolem0001(n1,n1,n0,n0))|equalish(X375,n0),inference(resolution,[status(thm)],[c194, c8])).
% 0.98/1.17 cnf(c224,plain,~f(X372,X370,X371,X373,skolem0001(n1,n1,n0,n0))|equalish(X372,n1),inference(resolution,[status(thm)],[c194, c5])).
% 0.98/1.17 cnf(c222,plain,~f(X368,X367,X366,X365,skolem0001(n1,n1,n0,n0))|equalish(X367,n1),inference(resolution,[status(thm)],[c194, c6])).
% 0.98/1.17 cnf(c57,plain,~equalish(X145,X145)|~equalish(X146,X146)|f(X145,X146,n1,n1,skolem0001(X145,X146,n1,n1)),inference(resolution,[status(thm)],[c24, c17])).
% 0.98/1.17 cnf(c145,plain,~equalish(X168,X168)|f(X168,X168,n1,n1,skolem0001(X168,X168,n1,n1)),inference(factor,[status(thm)],[c57])).
% 0.98/1.17 cnf(c193,plain,f(n0,n0,n1,n1,skolem0001(n0,n0,n1,n1)),inference(resolution,[status(thm)],[c145, c16])).
% 0.98/1.17 cnf(c215,plain,~f(X363,X362,X364,X361,skolem0001(n0,n0,n1,n1))|equalish(X364,n1),inference(resolution,[status(thm)],[c193, c7])).
% 0.98/1.17 cnf(c214,plain,~f(X359,X357,X360,X358,skolem0001(n0,n0,n1,n1))|equalish(X358,n1),inference(resolution,[status(thm)],[c193, c8])).
% 0.98/1.17 cnf(c213,plain,~f(X355,X353,X354,X356,skolem0001(n0,n0,n1,n1))|equalish(X355,n0),inference(resolution,[status(thm)],[c193, c5])).
% 0.98/1.17 cnf(c211,plain,~f(X352,X351,X350,X349,skolem0001(n0,n0,n1,n1))|equalish(X351,n0),inference(resolution,[status(thm)],[c193, c6])).
% 0.98/1.17 cnf(c25,plain,~equalish(X93,X93)|~equalish(X95,X95)|~equalish(X94,X94)|f(X93,X95,X94,n1,skolem0001(X93,X95,X94,n1)),inference(resolution,[status(thm)],[c12, c17])).
% 0.98/1.17 cnf(c68,plain,~equalish(X171,X171)|~equalish(X172,X172)|f(X171,X172,X172,n1,skolem0001(X171,X172,X172,n1)),inference(factor,[status(thm)],[c25])).
% 0.98/1.17 cnf(c198,plain,~equalish(X348,X348)|f(X348,n0,n0,n1,skolem0001(X348,n0,n0,n1)),inference(resolution,[status(thm)],[c68, c16])).
% 0.98/1.17 cnf(c67,plain,~equalish(X166,X166)|~equalish(X165,X165)|f(X166,X165,X166,n1,skolem0001(X166,X165,X166,n1)),inference(factor,[status(thm)],[c25])).
% 0.98/1.17 cnf(c187,plain,~equalish(X167,X167)|f(X167,X167,X167,n1,skolem0001(X167,X167,X167,n1)),inference(factor,[status(thm)],[c67])).
% 0.98/1.17 cnf(c191,plain,f(n0,n0,n0,n1,skolem0001(n0,n0,n0,n1)),inference(resolution,[status(thm)],[c187, c16])).
% 0.98/1.17 cnf(c207,plain,~f(X346,X345,X347,X344,skolem0001(n0,n0,n0,n1))|equalish(X347,n0),inference(resolution,[status(thm)],[c191, c7])).
% 0.98/1.17 cnf(c206,plain,~f(X342,X340,X343,X341,skolem0001(n0,n0,n0,n1))|equalish(X341,n1),inference(resolution,[status(thm)],[c191, c8])).
% 0.98/1.17 cnf(c205,plain,~f(X337,X335,X336,X338,skolem0001(n0,n0,n0,n1))|equalish(X337,n0),inference(resolution,[status(thm)],[c191, c5])).
% 0.98/1.17 cnf(c203,plain,~f(X334,X333,X332,X331,skolem0001(n0,n0,n0,n1))|equalish(X333,n0),inference(resolution,[status(thm)],[c191, c6])).
% 0.98/1.17 cnf(c38,plain,~equalish(X100,X100)|~equalish(X99,X99)|f(X100,X99,X100,X99,skolem0001(X100,X99,X100,X99)),inference(factor,[status(thm)],[c23])).
% 0.98/1.17 cnf(c85,plain,~equalish(X124,X124)|f(X124,n0,X124,n0,skolem0001(X124,n0,X124,n0)),inference(resolution,[status(thm)],[c38, c16])).
% 0.98/1.17 cnf(c119,plain,f(n1,n0,n1,n0,skolem0001(n1,n0,n1,n0)),inference(resolution,[status(thm)],[c85, c17])).
% 0.98/1.17 cnf(c183,plain,~f(X329,X328,X330,X327,skolem0001(n1,n0,n1,n0))|equalish(X330,n1),inference(resolution,[status(thm)],[c119, c7])).
% 0.98/1.17 cnf(c182,plain,~f(X325,X323,X326,X324,skolem0001(n1,n0,n1,n0))|equalish(X324,n0),inference(resolution,[status(thm)],[c119, c8])).
% 0.98/1.17 cnf(c181,plain,~f(X321,X319,X320,X322,skolem0001(n1,n0,n1,n0))|equalish(X321,n1),inference(resolution,[status(thm)],[c119, c5])).
% 0.98/1.17 cnf(c179,plain,~f(X318,X317,X316,X315,skolem0001(n1,n0,n1,n0))|equalish(X317,n0),inference(resolution,[status(thm)],[c119, c6])).
% 0.98/1.17 cnf(c84,plain,~equalish(X123,X123)|f(X123,n1,X123,n1,skolem0001(X123,n1,X123,n1)),inference(resolution,[status(thm)],[c38, c17])).
% 0.98/1.17 cnf(c118,plain,f(n0,n1,n0,n1,skolem0001(n0,n1,n0,n1)),inference(resolution,[status(thm)],[c84, c16])).
% 0.98/1.17 cnf(c174,plain,~f(X313,X312,X314,X311,skolem0001(n0,n1,n0,n1))|equalish(X314,n0),inference(resolution,[status(thm)],[c118, c7])).
% 0.98/1.17 cnf(c173,plain,~f(X309,X307,X310,X308,skolem0001(n0,n1,n0,n1))|equalish(X308,n1),inference(resolution,[status(thm)],[c118, c8])).
% 0.98/1.17 cnf(c172,plain,~f(X305,X303,X304,X306,skolem0001(n0,n1,n0,n1))|equalish(X305,n0),inference(resolution,[status(thm)],[c118, c5])).
% 0.98/1.17 cnf(c170,plain,~f(X302,X301,X300,X299,skolem0001(n0,n1,n0,n1))|equalish(X301,n1),inference(resolution,[status(thm)],[c118, c6])).
% 0.98/1.17 cnf(c22,plain,~equalish(X77,X77)|~equalish(X78,X78)|~equalish(X76,X76)|f(X77,X78,X76,X77,skolem0001(X77,X78,X76,X77)),inference(factor,[status(thm)],[c12])).
% 0.98/1.17 cnf(c28,plain,~equalish(X87,X87)|~equalish(X88,X88)|f(X87,X88,X88,X87,skolem0001(X87,X88,X88,X87)),inference(factor,[status(thm)],[c22])).
% 0.98/1.17 cnf(c46,plain,~equalish(X115,X115)|f(X115,n0,n0,X115,skolem0001(X115,n0,n0,X115)),inference(resolution,[status(thm)],[c28, c16])).
% 0.98/1.17 cnf(c112,plain,f(n1,n0,n0,n1,skolem0001(n1,n0,n0,n1)),inference(resolution,[status(thm)],[c46, c17])).
% 0.98/1.17 cnf(c165,plain,~f(X297,X296,X298,X295,skolem0001(n1,n0,n0,n1))|equalish(X298,n0),inference(resolution,[status(thm)],[c112, c7])).
% 0.98/1.17 cnf(c164,plain,~f(X293,X291,X294,X292,skolem0001(n1,n0,n0,n1))|equalish(X292,n1),inference(resolution,[status(thm)],[c112, c8])).
% 0.98/1.17 cnf(c163,plain,~f(X288,X286,X287,X289,skolem0001(n1,n0,n0,n1))|equalish(X288,n1),inference(resolution,[status(thm)],[c112, c5])).
% 0.98/1.17 cnf(c157,plain,~equalish(X285,X285)|f(X285,n1,n0,n0,skolem0001(X285,n1,n0,n0)),inference(resolution,[status(thm)],[c58, c17])).
% 0.98/1.17 cnf(c161,plain,~f(X284,X283,X282,X281,skolem0001(n1,n0,n0,n1))|equalish(X283,n0),inference(resolution,[status(thm)],[c112, c6])).
% 0.98/1.17 cnf(c45,plain,~equalish(X114,X114)|f(X114,n1,n1,X114,skolem0001(X114,n1,n1,X114)),inference(resolution,[status(thm)],[c28, c17])).
% 0.98/1.17 cnf(c111,plain,f(n0,n1,n1,n0,skolem0001(n0,n1,n1,n0)),inference(resolution,[status(thm)],[c45, c16])).
% 0.98/1.17 cnf(c154,plain,~f(X279,X278,X280,X277,skolem0001(n0,n1,n1,n0))|equalish(X280,n1),inference(resolution,[status(thm)],[c111, c7])).
% 0.98/1.17 cnf(c147,plain,~equalish(X276,X276)|f(X276,n0,n1,n1,skolem0001(X276,n0,n1,n1)),inference(resolution,[status(thm)],[c57, c16])).
% 0.98/1.17 cnf(c153,plain,~f(X274,X272,X275,X273,skolem0001(n0,n1,n1,n0))|equalish(X273,n0),inference(resolution,[status(thm)],[c111, c8])).
% 0.98/1.17 cnf(c152,plain,~f(X270,X268,X269,X271,skolem0001(n0,n1,n1,n0))|equalish(X270,n0),inference(resolution,[status(thm)],[c111, c5])).
% 0.98/1.17 cnf(c150,plain,~f(X266,X265,X264,X263,skolem0001(n0,n1,n1,n0))|equalish(X265,n1),inference(resolution,[status(thm)],[c111, c6])).
% 0.98/1.17 cnf(c30,plain,~equalish(X108,X108)|~equalish(X109,X109)|f(X108,X109,n0,X108,skolem0001(X108,X109,n0,X108)),inference(resolution,[status(thm)],[c22, c16])).
% 0.98/1.17 cnf(c102,plain,~equalish(X110,X110)|f(X110,X110,n0,X110,skolem0001(X110,X110,n0,X110)),inference(factor,[status(thm)],[c30])).
% 0.98/1.17 cnf(c105,plain,f(n1,n1,n0,n1,skolem0001(n1,n1,n0,n1)),inference(resolution,[status(thm)],[c102, c17])).
% 0.98/1.17 cnf(c142,plain,~f(X261,X260,X262,X259,skolem0001(n1,n1,n0,n1))|equalish(X262,n0),inference(resolution,[status(thm)],[c105, c7])).
% 0.98/1.17 cnf(c141,plain,~f(X257,X255,X258,X256,skolem0001(n1,n1,n0,n1))|equalish(X256,n1),inference(resolution,[status(thm)],[c105, c8])).
% 0.98/1.17 cnf(c140,plain,~f(X252,X250,X251,X253,skolem0001(n1,n1,n0,n1))|equalish(X252,n1),inference(resolution,[status(thm)],[c105, c5])).
% 0.98/1.17 cnf(c41,plain,~equalish(X118,X118)|~equalish(X119,X119)|f(X118,X119,n0,X119,skolem0001(X118,X119,n0,X119)),inference(resolution,[status(thm)],[c23, c16])).
% 0.98/1.17 cnf(c115,plain,~equalish(X249,X249)|f(X249,n1,n0,n1,skolem0001(X249,n1,n0,n1)),inference(resolution,[status(thm)],[c41, c17])).
% 0.98/1.17 cnf(c138,plain,~f(X248,X247,X246,X245,skolem0001(n1,n1,n0,n1))|equalish(X247,n1),inference(resolution,[status(thm)],[c105, c6])).
% 0.98/1.17 cnf(c29,plain,~equalish(X101,X101)|~equalish(X102,X102)|f(X101,X102,n1,X101,skolem0001(X101,X102,n1,X101)),inference(resolution,[status(thm)],[c22, c17])).
% 0.98/1.17 cnf(c86,plain,~equalish(X104,X104)|f(X104,X104,n1,X104,skolem0001(X104,X104,n1,X104)),inference(factor,[status(thm)],[c29])).
% 0.98/1.17 cnf(c90,plain,f(n0,n0,n1,n0,skolem0001(n0,n0,n1,n0)),inference(resolution,[status(thm)],[c86, c16])).
% 0.98/1.17 cnf(c130,plain,~f(X243,X242,X244,X241,skolem0001(n0,n0,n1,n0))|equalish(X244,n1),inference(resolution,[status(thm)],[c90, c7])).
% 0.98/1.17 cnf(c40,plain,~equalish(X111,X111)|~equalish(X112,X112)|f(X111,X112,n1,X112,skolem0001(X111,X112,n1,X112)),inference(resolution,[status(thm)],[c23, c17])).
% 0.98/1.17 cnf(c109,plain,~equalish(X240,X240)|f(X240,n0,n1,n0,skolem0001(X240,n0,n1,n0)),inference(resolution,[status(thm)],[c40, c16])).
% 0.98/1.17 cnf(c129,plain,~f(X238,X236,X239,X237,skolem0001(n0,n0,n1,n0))|equalish(X237,n0),inference(resolution,[status(thm)],[c90, c8])).
% 0.98/1.17 cnf(c128,plain,~f(X234,X232,X233,X235,skolem0001(n0,n0,n1,n0))|equalish(X234,n0),inference(resolution,[status(thm)],[c90, c5])).
% 0.98/1.17 cnf(c126,plain,~f(X230,X229,X228,X227,skolem0001(n0,n0,n1,n0))|equalish(X229,n0),inference(resolution,[status(thm)],[c90, c6])).
% 0.98/1.17 cnf(c27,plain,~equalish(X80,X80)|~equalish(X79,X79)|f(X80,X79,X80,X80,skolem0001(X80,X79,X80,X80)),inference(factor,[status(thm)],[c22])).
% 0.98/1.17 cnf(c33,plain,~equalish(X86,X86)|f(X86,n0,X86,X86,skolem0001(X86,n0,X86,X86)),inference(resolution,[status(thm)],[c27, c16])).
% 0.98/1.17 cnf(c42,plain,f(n1,n0,n1,n1,skolem0001(n1,n0,n1,n1)),inference(resolution,[status(thm)],[c33, c17])).
% 0.98/1.17 cnf(c100,plain,~f(X225,X224,X226,X223,skolem0001(n1,n0,n1,n1))|equalish(X226,n1),inference(resolution,[status(thm)],[c42, c7])).
% 0.98/1.17 cnf(c99,plain,~f(X219,X217,X220,X218,skolem0001(n1,n0,n1,n1))|equalish(X218,n1),inference(resolution,[status(thm)],[c42, c8])).
% 0.98/1.17 cnf(c98,plain,~f(X215,X213,X214,X216,skolem0001(n1,n0,n1,n1))|equalish(X215,n1),inference(resolution,[status(thm)],[c42, c5])).
% 0.98/1.17 cnf(c96,plain,~f(X212,X211,X210,X209,skolem0001(n1,n0,n1,n1))|equalish(X211,n0),inference(resolution,[status(thm)],[c42, c6])).
% 0.98/1.17 cnf(c81,plain,~equalish(X205,X205)|~equalish(X204,X204)|f(X205,X204,n1,n0,skolem0001(X205,X204,n1,n0)),inference(resolution,[status(thm)],[c26, c17])).
% 0.98/1.17 cnf(c252,plain,~equalish(X206,X206)|f(X206,X206,n1,n0,skolem0001(X206,X206,n1,n0)),inference(factor,[status(thm)],[c81])).
% 0.98/1.17 cnf(c235,plain,~equalish(X199,X199)|f(X199,n1,X199,n0,skolem0001(X199,n1,X199,n0)),inference(resolution,[status(thm)],[c79, c17])).
% 0.98/1.17 cnf(c32,plain,~equalish(X82,X82)|f(X82,n1,X82,X82,skolem0001(X82,n1,X82,X82)),inference(resolution,[status(thm)],[c27, c17])).
% 0.98/1.17 cnf(c37,plain,f(n0,n1,n0,n0,skolem0001(n0,n1,n0,n0)),inference(resolution,[status(thm)],[c32, c16])).
% 0.98/1.17 cnf(c77,plain,~f(X194,X193,X195,X192,skolem0001(n0,n1,n0,n0))|equalish(X195,n0),inference(resolution,[status(thm)],[c37, c7])).
% 0.98/1.17 cnf(c76,plain,~f(X190,X188,X191,X189,skolem0001(n0,n1,n0,n0))|equalish(X189,n0),inference(resolution,[status(thm)],[c37, c8])).
% 0.98/1.17 cnf(c70,plain,~equalish(X177,X177)|~equalish(X178,X178)|f(X177,X178,n0,n1,skolem0001(X177,X178,n0,n1)),inference(resolution,[status(thm)],[c25, c16])).
% 0.98/1.17 cnf(c217,plain,~equalish(X187,X187)|f(X187,X187,n0,n1,skolem0001(X187,X187,n0,n1)),inference(factor,[status(thm)],[c70])).
% 0.98/1.17 cnf(c75,plain,~f(X185,X183,X184,X186,skolem0001(n0,n1,n0,n0))|equalish(X185,n0),inference(resolution,[status(thm)],[c37, c5])).
% 0.98/1.17 cnf(c73,plain,~f(X182,X181,X180,X179,skolem0001(n0,n1,n0,n0))|equalish(X181,n1),inference(resolution,[status(thm)],[c37, c6])).
% 0.98/1.17 cnf(c189,plain,~equalish(X174,X174)|f(X174,n0,X174,n1,skolem0001(X174,n0,X174,n1)),inference(resolution,[status(thm)],[c67, c16])).
% 0.98/1.17 cnf(c31,plain,~equalish(X81,X81)|f(X81,X81,X81,X81,skolem0001(X81,X81,X81,X81)),inference(factor,[status(thm)],[c27])).
% 0.98/1.17 cnf(c35,plain,f(n0,n0,n0,n0,skolem0001(n0,n0,n0,n0)),inference(resolution,[status(thm)],[c31, c16])).
% 0.98/1.17 cnf(c65,plain,~f(X163,X162,X164,X161,skolem0001(n0,n0,n0,n0))|equalish(X164,n0),inference(resolution,[status(thm)],[c35, c7])).
% 0.98/1.17 cnf(c64,plain,~f(X159,X157,X160,X158,skolem0001(n0,n0,n0,n0))|equalish(X158,n0),inference(resolution,[status(thm)],[c35, c8])).
% 0.98/1.17 cnf(c63,plain,~f(X155,X153,X154,X156,skolem0001(n0,n0,n0,n0))|equalish(X155,n0),inference(resolution,[status(thm)],[c35, c5])).
% 0.98/1.17 cnf(c61,plain,~f(X152,X151,X150,X149,skolem0001(n0,n0,n0,n0))|equalish(X151,n0),inference(resolution,[status(thm)],[c35, c6])).
% 0.98/1.17 cnf(c34,plain,f(n1,n1,n1,n1,skolem0001(n1,n1,n1,n1)),inference(resolution,[status(thm)],[c31, c17])).
% 0.98/1.17 cnf(c53,plain,~f(X143,X142,X144,X141,skolem0001(n1,n1,n1,n1))|equalish(X144,n1),inference(resolution,[status(thm)],[c34, c7])).
% 0.98/1.17 cnf(c52,plain,~f(X138,X136,X139,X137,skolem0001(n1,n1,n1,n1))|equalish(X137,n1),inference(resolution,[status(thm)],[c34, c8])).
% 0.98/1.17 cnf(c103,plain,~equalish(X135,X135)|f(X135,n1,n0,X135,skolem0001(X135,n1,n0,X135)),inference(resolution,[status(thm)],[c30, c17])).
% 0.98/1.17 cnf(c51,plain,~f(X133,X131,X132,X134,skolem0001(n1,n1,n1,n1))|equalish(X133,n1),inference(resolution,[status(thm)],[c34, c5])).
% 0.98/1.17 cnf(c88,plain,~equalish(X130,X130)|f(X130,n0,n1,X130,skolem0001(X130,n0,n1,X130)),inference(resolution,[status(thm)],[c29, c16])).
% 0.98/1.17 cnf(c49,plain,~f(X129,X128,X127,X126,skolem0001(n1,n1,n1,n1))|equalish(X128,n1),inference(resolution,[status(thm)],[c34, c6])).
% 0.98/1.17 cnf(c21,plain,~f(X71,X73,X74,X72,X75)|equalish(X72,X72),inference(factor,[status(thm)],[c8])).
% 0.98/1.17 cnf(c20,plain,~f(X53,X57,X56,X54,X55)|equalish(X56,X56),inference(factor,[status(thm)],[c7])).
% 0.98/1.17 cnf(c19,plain,~f(X43,X42,X40,X39,X41)|equalish(X42,X42),inference(factor,[status(thm)],[c6])).
% 0.98/1.17 cnf(c18,plain,~f(X35,X36,X34,X37,X38)|equalish(X35,X35),inference(factor,[status(thm)],[c5])).
% 0.98/1.17 fof(n0_not_n1,axiom,((~equalish(n0,n1))&(~equalish(n1,n0))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', n0_not_n1)).
% 0.98/1.17 fof(c13,plain,(~equalish(n0,n1)&~equalish(n1,n0)),inference(fof_simplification,[status(thm)],[n0_not_n1])).
% 0.98/1.17 cnf(c15,plain,~equalish(n1,n0),inference(split_conjunct,[status(thm)],[c13])).
% 0.98/1.17 cnf(c14,plain,~equalish(n0,n1),inference(split_conjunct,[status(thm)],[c13])).
% 0.98/1.17 % SZS output end Saturation
% 0.98/1.17
% 0.98/1.17 % Initial clauses : 9
% 0.98/1.17 % Processed clauses : 141
% 0.98/1.17 % Factors computed : 33
% 0.98/1.17 % Resolvents computed: 290
% 0.98/1.17 % Tautologies deleted: 0
% 0.98/1.17 % Forward subsumed : 191
% 0.98/1.17 % Backward subsumed : 0
% 0.98/1.17 % -------- CPU Time ---------
% 0.98/1.17 % User time : 0.797 s
% 0.98/1.17 % System time : 0.024 s
% 0.98/1.17 % Total time : 0.821 s
%------------------------------------------------------------------------------