%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM022+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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:17:45 EDT 2024
% Result : Theorem 1.69s 1.93s
% Output : Refutation 1.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : COM022+1 : TPTP v8.1.2. Released v4.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n002.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 07:12:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.69/1.93 % Version: 1.5
% 1.69/1.93 % SZS status Theorem
% 1.69/1.93 % SZS output start CNFRefutation
% 1.69/1.93 fof(m__731,plain,((aElement0(xa)&aElement0(xb))&aElement0(xc)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__731)).
% 1.69/1.93 cnf(c39,plain,aElement0(xb),inference(split_conjunct,[status(thm)],[m__731])).
% 1.69/1.93 fof(m__656,plain,aRewritingSystem0(xR),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__656)).
% 1.69/1.93 cnf(c43,plain,aRewritingSystem0(xR),inference(split_conjunct,[status(thm)],[m__656])).
% 1.69/1.93 cnf(reflexivity,axiom,X62=X62,theory(equality)).
% 1.69/1.93 fof(mTCRDef,plain,(![W0]:(![W1]:(![W2]:(((aElement0(W0)&aRewritingSystem0(W1))&aElement0(W2))=>(sdtmndtasgtdt0(W0,W1,W2)<=>(W0=W2|sdtmndtplgtdt0(W0,W1,W2))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mTCRDef)).
% 1.69/1.93 fof(c100,plain,(![W0]:(![W1]:(![W2]:(((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|((~sdtmndtasgtdt0(W0,W1,W2)|(W0=W2|sdtmndtplgtdt0(W0,W1,W2)))&((W0!=W2&~sdtmndtplgtdt0(W0,W1,W2))|sdtmndtasgtdt0(W0,W1,W2))))))),inference(fof_nnf,[status(thm)],[mTCRDef])).
% 1.69/1.93 fof(c101,plain,(![X47]:(![X48]:(![X49]:(((~aElement0(X47)|~aRewritingSystem0(X48))|~aElement0(X49))|((~sdtmndtasgtdt0(X47,X48,X49)|(X47=X49|sdtmndtplgtdt0(X47,X48,X49)))&((X47!=X49&~sdtmndtplgtdt0(X47,X48,X49))|sdtmndtasgtdt0(X47,X48,X49))))))),inference(variable_rename,[status(thm)],[c100])).
% 1.69/1.93 fof(c102,plain,(![X47]:(![X48]:(![X49]:((((~aElement0(X47)|~aRewritingSystem0(X48))|~aElement0(X49))|(~sdtmndtasgtdt0(X47,X48,X49)|(X47=X49|sdtmndtplgtdt0(X47,X48,X49))))&((((~aElement0(X47)|~aRewritingSystem0(X48))|~aElement0(X49))|(X47!=X49|sdtmndtasgtdt0(X47,X48,X49)))&(((~aElement0(X47)|~aRewritingSystem0(X48))|~aElement0(X49))|(~sdtmndtplgtdt0(X47,X48,X49)|sdtmndtasgtdt0(X47,X48,X49)))))))),inference(distribute,[status(thm)],[c101])).
% 1.69/1.93 cnf(c104,plain,~aElement0(X148)|~aRewritingSystem0(X149)|~aElement0(X150)|X148!=X150|sdtmndtasgtdt0(X148,X149,X150),inference(split_conjunct,[status(thm)],[c102])).
% 1.69/1.93 cnf(c186,plain,~aElement0(X152)|~aRewritingSystem0(X151)|sdtmndtasgtdt0(X152,X151,X152),inference(resolution,[status(thm)],[c104, reflexivity])).
% 1.69/1.93 cnf(c187,plain,~aElement0(X153)|sdtmndtasgtdt0(X153,xR,X153),inference(resolution,[status(thm)],[c186, c43])).
% 1.69/1.93 cnf(c196,plain,sdtmndtasgtdt0(xb,xR,xb),inference(resolution,[status(thm)],[c187, c39])).
% 1.69/1.93 fof(m__,conjecture,(((sdtmndtplgtdt0(xa,xR,xb)&sdtmndtplgtdt0(xa,xR,xc))=>(?[W0]:(((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]:(((aElement0(W1)&aReductOfIn0(W1,xa,xR))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]:(((aElement0(W2)&sdtmndtasgtdt0(W0,xR,W2))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]:((aNormalFormOfIn0(W3,W2,xR)&sdtmndtasgtdt0(xb,xR,W3))&sdtmndtasgtdt0(xc,xR,W3))))))))))=>((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))=>(?[W0]:((aElement0(W0)&sdtmndtasgtdt0(xb,xR,W0))&sdtmndtasgtdt0(xc,xR,W0))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 1.69/1.93 fof(c10,negated_conjecture,(~(((sdtmndtplgtdt0(xa,xR,xb)&sdtmndtplgtdt0(xa,xR,xc))=>(?[W0]:(((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]:(((aElement0(W1)&aReductOfIn0(W1,xa,xR))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]:(((aElement0(W2)&sdtmndtasgtdt0(W0,xR,W2))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]:((aNormalFormOfIn0(W3,W2,xR)&sdtmndtasgtdt0(xb,xR,W3))&sdtmndtasgtdt0(xc,xR,W3))))))))))=>((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))=>(?[W0]:((aElement0(W0)&sdtmndtasgtdt0(xb,xR,W0))&sdtmndtasgtdt0(xc,xR,W0)))))),inference(assume_negation,[status(cth)],[m__])).
% 1.69/1.93 fof(c11,negated_conjecture,(((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(?[W0]:(((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]:(((aElement0(W1)&aReductOfIn0(W1,xa,xR))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]:(((aElement0(W2)&sdtmndtasgtdt0(W0,xR,W2))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]:((aNormalFormOfIn0(W3,W2,xR)&sdtmndtasgtdt0(xb,xR,W3))&sdtmndtasgtdt0(xc,xR,W3))))))))))&((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))&(![W0]:((~aElement0(W0)|~sdtmndtasgtdt0(xb,xR,W0))|~sdtmndtasgtdt0(xc,xR,W0))))),inference(fof_nnf,[status(thm)],[c10])).
% 1.69/1.93 fof(c12,negated_conjecture,(((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(?[X2]:(((aElement0(X2)&aReductOfIn0(X2,xa,xR))&sdtmndtasgtdt0(X2,xR,xb))&(?[X3]:(((aElement0(X3)&aReductOfIn0(X3,xa,xR))&sdtmndtasgtdt0(X3,xR,xc))&(?[X4]:(((aElement0(X4)&sdtmndtasgtdt0(X2,xR,X4))&sdtmndtasgtdt0(X3,xR,X4))&(?[X5]:((aNormalFormOfIn0(X5,X4,xR)&sdtmndtasgtdt0(xb,xR,X5))&sdtmndtasgtdt0(xc,xR,X5))))))))))&((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))&(![X6]:((~aElement0(X6)|~sdtmndtasgtdt0(xb,xR,X6))|~sdtmndtasgtdt0(xc,xR,X6))))),inference(variable_rename,[status(thm)],[c11])).
% 1.69/1.93 fof(c14,negated_conjecture,(![X6]:(((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(((aElement0(skolem0001)&aReductOfIn0(skolem0001,xa,xR))&sdtmndtasgtdt0(skolem0001,xR,xb))&(((aElement0(skolem0002)&aReductOfIn0(skolem0002,xa,xR))&sdtmndtasgtdt0(skolem0002,xR,xc))&(((aElement0(skolem0003)&sdtmndtasgtdt0(skolem0001,xR,skolem0003))&sdtmndtasgtdt0(skolem0002,xR,skolem0003))&((aNormalFormOfIn0(skolem0004,skolem0003,xR)&sdtmndtasgtdt0(xb,xR,skolem0004))&sdtmndtasgtdt0(xc,xR,skolem0004))))))&((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))&((~aElement0(X6)|~sdtmndtasgtdt0(xb,xR,X6))|~sdtmndtasgtdt0(xc,xR,X6))))),inference(shift_quantors,[status(thm)],[fof(c13,negated_conjecture,(((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(((aElement0(skolem0001)&aReductOfIn0(skolem0001,xa,xR))&sdtmndtasgtdt0(skolem0001,xR,xb))&(((aElement0(skolem0002)&aReductOfIn0(skolem0002,xa,xR))&sdtmndtasgtdt0(skolem0002,xR,xc))&(((aElement0(skolem0003)&sdtmndtasgtdt0(skolem0001,xR,skolem0003))&sdtmndtasgtdt0(skolem0002,xR,skolem0003))&((aNormalFormOfIn0(skolem0004,skolem0003,xR)&sdtmndtasgtdt0(xb,xR,skolem0004))&sdtmndtasgtdt0(xc,xR,skolem0004))))))&((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))&(![X6]:((~aElement0(X6)|~sdtmndtasgtdt0(xb,xR,X6))|~sdtmndtasgtdt0(xc,xR,X6))))),inference(skolemize,[status(esa)],[c12])).])).
% 1.69/1.93 fof(c15,negated_conjecture,(![X6]:((((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0001))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aReductOfIn0(skolem0001,xa,xR)))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0001,xR,xb)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0002))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aReductOfIn0(skolem0002,xa,xR)))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0002,xR,xc)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0003))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0001,xR,skolem0003)))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0002,xR,skolem0003)))&((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aNormalFormOfIn0(skolem0004,skolem0003,xR))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(xb,xR,skolem0004)))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(xc,xR,skolem0004))))))&((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))&((~aElement0(X6)|~sdtmndtasgtdt0(xb,xR,X6))|~sdtmndtasgtdt0(xc,xR,X6))))),inference(distribute,[status(thm)],[c14])).
% 1.69/1.93 cnf(c30,negated_conjecture,~aElement0(X142)|~sdtmndtasgtdt0(xb,xR,X142)|~sdtmndtasgtdt0(xc,xR,X142),inference(split_conjunct,[status(thm)],[c15])).
% 1.69/1.93 cnf(c28,negated_conjecture,sdtmndtasgtdt0(xa,xR,xb),inference(split_conjunct,[status(thm)],[c15])).
% 1.69/1.93 cnf(c5,axiom,X108!=X109|X110!=X113|X111!=X112|~sdtmndtasgtdt0(X108,X110,X111)|sdtmndtasgtdt0(X109,X113,X112),theory(equality)).
% 1.69/1.93 cnf(c144,plain,xa!=X161|xR!=X162|xb!=X160|sdtmndtasgtdt0(X161,X162,X160),inference(resolution,[status(thm)],[c5, c28])).
% 1.69/1.93 cnf(c207,plain,xa!=X163|xR!=X164|sdtmndtasgtdt0(X163,X164,xb),inference(resolution,[status(thm)],[c144, reflexivity])).
% 1.69/1.93 cnf(c208,plain,xa!=X165|sdtmndtasgtdt0(X165,xR,xb),inference(resolution,[status(thm)],[c207, reflexivity])).
% 1.69/1.93 cnf(c40,plain,aElement0(xc),inference(split_conjunct,[status(thm)],[m__731])).
% 1.69/1.93 cnf(c189,plain,sdtmndtasgtdt0(xc,xR,xc),inference(resolution,[status(thm)],[c187, c40])).
% 1.69/1.93 cnf(c198,plain,~aElement0(xc)|~sdtmndtasgtdt0(xb,xR,xc),inference(resolution,[status(thm)],[c189, c30])).
% 1.69/1.93 cnf(c29,negated_conjecture,sdtmndtasgtdt0(xa,xR,xc),inference(split_conjunct,[status(thm)],[c15])).
% 1.69/1.93 cnf(c145,plain,xa!=X167|xR!=X168|xc!=X166|sdtmndtasgtdt0(X167,X168,X166),inference(resolution,[status(thm)],[c5, c29])).
% 1.69/1.93 cnf(c210,plain,xa!=X170|xR!=X169|sdtmndtasgtdt0(X170,X169,xc),inference(resolution,[status(thm)],[c145, reflexivity])).
% 1.69/1.93 cnf(c211,plain,xa!=X171|sdtmndtasgtdt0(X171,xR,xc),inference(resolution,[status(thm)],[c210, reflexivity])).
% 1.69/1.93 cnf(c38,plain,aElement0(xa),inference(split_conjunct,[status(thm)],[m__731])).
% 1.69/1.93 cnf(c103,plain,~aElement0(X222)|~aRewritingSystem0(X223)|~aElement0(X224)|~sdtmndtasgtdt0(X222,X223,X224)|X222=X224|sdtmndtplgtdt0(X222,X223,X224),inference(split_conjunct,[status(thm)],[c102])).
% 1.69/1.93 cnf(c310,plain,~aElement0(xa)|~aRewritingSystem0(xR)|~aElement0(xb)|xa=xb|sdtmndtplgtdt0(xa,xR,xb),inference(resolution,[status(thm)],[c103, c28])).
% 1.69/1.93 cnf(c885,plain,~aElement0(xa)|~aRewritingSystem0(xR)|xa=xb|sdtmndtplgtdt0(xa,xR,xb),inference(resolution,[status(thm)],[c310, c39])).
% 1.69/1.93 cnf(c886,plain,~aElement0(xa)|xa=xb|sdtmndtplgtdt0(xa,xR,xb),inference(resolution,[status(thm)],[c885, c43])).
% 1.69/1.93 cnf(c889,plain,xa=xb|sdtmndtplgtdt0(xa,xR,xb),inference(resolution,[status(thm)],[c886, c38])).
% 1.69/1.93 cnf(c894,plain,sdtmndtplgtdt0(xa,xR,xb)|sdtmndtasgtdt0(xb,xR,xc),inference(resolution,[status(thm)],[c889, c211])).
% 1.69/1.93 cnf(c971,plain,sdtmndtplgtdt0(xa,xR,xb)|~aElement0(xc),inference(resolution,[status(thm)],[c894, c198])).
% 1.69/1.93 cnf(c979,plain,sdtmndtplgtdt0(xa,xR,xb),inference(resolution,[status(thm)],[c971, c40])).
% 1.69/1.93 cnf(c22,negated_conjecture,~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|aElement0(skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 1.69/1.93 cnf(c312,plain,~aElement0(xa)|~aRewritingSystem0(xR)|~aElement0(xc)|xa=xc|sdtmndtplgtdt0(xa,xR,xc),inference(resolution,[status(thm)],[c103, c29])).
% 1.69/1.93 cnf(c1092,plain,~aElement0(xa)|~aRewritingSystem0(xR)|xa=xc|sdtmndtplgtdt0(xa,xR,xc),inference(resolution,[status(thm)],[c312, c40])).
% 1.69/1.93 cnf(c1093,plain,~aElement0(xa)|xa=xc|sdtmndtplgtdt0(xa,xR,xc),inference(resolution,[status(thm)],[c1092, c43])).
% 1.69/1.93 cnf(c1098,plain,xa=xc|sdtmndtplgtdt0(xa,xR,xc),inference(resolution,[status(thm)],[c1093, c38])).
% 1.69/1.93 cnf(c1121,plain,xa=xc|~sdtmndtplgtdt0(xa,xR,xb)|aElement0(skolem0003),inference(resolution,[status(thm)],[c1098, c22])).
% 1.69/1.93 cnf(c1716,plain,xa=xc|aElement0(skolem0003),inference(resolution,[status(thm)],[c1121, c979])).
% 1.69/1.93 cnf(c1728,plain,aElement0(skolem0003)|sdtmndtasgtdt0(xc,xR,xb),inference(resolution,[status(thm)],[c1716, c208])).
% 1.69/1.93 cnf(c1801,plain,aElement0(skolem0003)|~aElement0(xb)|~sdtmndtasgtdt0(xb,xR,xb),inference(resolution,[status(thm)],[c1728, c30])).
% 1.69/1.93 cnf(c2060,plain,aElement0(skolem0003)|~aElement0(xb),inference(resolution,[status(thm)],[c1801, c196])).
% 1.69/1.93 cnf(c2061,plain,aElement0(skolem0003),inference(resolution,[status(thm)],[c2060, c39])).
% 1.69/1.93 fof(mNFRDef,plain,(![W0]:(![W1]:((aElement0(W0)&aRewritingSystem0(W1))=>(![W2]:(aNormalFormOfIn0(W2,W0,W1)<=>((aElement0(W2)&sdtmndtasgtdt0(W0,W1,W2))&(~(?[W3]:aReductOfIn0(W3,W2,W1))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mNFRDef)).
% 1.69/1.93 fof(c49,plain,(![W0]:(![W1]:((~aElement0(W0)|~aRewritingSystem0(W1))|(![W2]:((~aNormalFormOfIn0(W2,W0,W1)|((aElement0(W2)&sdtmndtasgtdt0(W0,W1,W2))&(![W3]:~aReductOfIn0(W3,W2,W1))))&(((~aElement0(W2)|~sdtmndtasgtdt0(W0,W1,W2))|(?[W3]:aReductOfIn0(W3,W2,W1)))|aNormalFormOfIn0(W2,W0,W1))))))),inference(fof_nnf,[status(thm)],[mNFRDef])).
% 1.69/1.93 fof(c50,plain,(![W0]:(![W1]:((~aElement0(W0)|~aRewritingSystem0(W1))|((![W2]:(~aNormalFormOfIn0(W2,W0,W1)|((aElement0(W2)&sdtmndtasgtdt0(W0,W1,W2))&(![W3]:~aReductOfIn0(W3,W2,W1)))))&(![W2]:(((~aElement0(W2)|~sdtmndtasgtdt0(W0,W1,W2))|(?[W3]:aReductOfIn0(W3,W2,W1)))|aNormalFormOfIn0(W2,W0,W1))))))),inference(shift_quantors,[status(thm)],[c49])).
% 1.69/1.93 fof(c51,plain,(![X14]:(![X15]:((~aElement0(X14)|~aRewritingSystem0(X15))|((![X16]:(~aNormalFormOfIn0(X16,X14,X15)|((aElement0(X16)&sdtmndtasgtdt0(X14,X15,X16))&(![X17]:~aReductOfIn0(X17,X16,X15)))))&(![X18]:(((~aElement0(X18)|~sdtmndtasgtdt0(X14,X15,X18))|(?[X19]:aReductOfIn0(X19,X18,X15)))|aNormalFormOfIn0(X18,X14,X15))))))),inference(variable_rename,[status(thm)],[c50])).
% 1.69/1.93 fof(c53,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((~aElement0(X14)|~aRewritingSystem0(X15))|((~aNormalFormOfIn0(X16,X14,X15)|((aElement0(X16)&sdtmndtasgtdt0(X14,X15,X16))&~aReductOfIn0(X17,X16,X15)))&(((~aElement0(X18)|~sdtmndtasgtdt0(X14,X15,X18))|aReductOfIn0(skolem0007(X14,X15,X18),X18,X15))|aNormalFormOfIn0(X18,X14,X15))))))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,(![X14]:(![X15]:((~aElement0(X14)|~aRewritingSystem0(X15))|((![X16]:(~aNormalFormOfIn0(X16,X14,X15)|((aElement0(X16)&sdtmndtasgtdt0(X14,X15,X16))&(![X17]:~aReductOfIn0(X17,X16,X15)))))&(![X18]:(((~aElement0(X18)|~sdtmndtasgtdt0(X14,X15,X18))|aReductOfIn0(skolem0007(X14,X15,X18),X18,X15))|aNormalFormOfIn0(X18,X14,X15))))))),inference(skolemize,[status(esa)],[c51])).])).
% 1.69/1.93 fof(c54,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(((((~aElement0(X14)|~aRewritingSystem0(X15))|(~aNormalFormOfIn0(X16,X14,X15)|aElement0(X16)))&((~aElement0(X14)|~aRewritingSystem0(X15))|(~aNormalFormOfIn0(X16,X14,X15)|sdtmndtasgtdt0(X14,X15,X16))))&((~aElement0(X14)|~aRewritingSystem0(X15))|(~aNormalFormOfIn0(X16,X14,X15)|~aReductOfIn0(X17,X16,X15))))&((~aElement0(X14)|~aRewritingSystem0(X15))|(((~aElement0(X18)|~sdtmndtasgtdt0(X14,X15,X18))|aReductOfIn0(skolem0007(X14,X15,X18),X18,X15))|aNormalFormOfIn0(X18,X14,X15))))))))),inference(distribute,[status(thm)],[c53])).
% 1.69/1.93 cnf(c55,plain,~aElement0(X124)|~aRewritingSystem0(X125)|~aNormalFormOfIn0(X123,X124,X125)|aElement0(X123),inference(split_conjunct,[status(thm)],[c54])).
% 1.69/1.93 cnf(c25,negated_conjecture,~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|aNormalFormOfIn0(skolem0004,skolem0003,xR),inference(split_conjunct,[status(thm)],[c15])).
% 1.69/1.93 cnf(c1112,plain,sdtmndtplgtdt0(xa,xR,xc)|sdtmndtasgtdt0(xc,xR,xb),inference(resolution,[status(thm)],[c1098, c208])).
% 1.69/1.93 cnf(c1266,plain,sdtmndtplgtdt0(xa,xR,xc)|~aElement0(xb)|~sdtmndtasgtdt0(xb,xR,xb),inference(resolution,[status(thm)],[c1112, c30])).
% 1.69/1.93 cnf(c2624,plain,sdtmndtplgtdt0(xa,xR,xc)|~aElement0(xb),inference(resolution,[status(thm)],[c1266, c196])).
% 1.69/1.93 cnf(c2625,plain,sdtmndtplgtdt0(xa,xR,xc),inference(resolution,[status(thm)],[c2624, c39])).
% 1.69/1.93 cnf(c2633,plain,~sdtmndtplgtdt0(xa,xR,xb)|aNormalFormOfIn0(skolem0004,skolem0003,xR),inference(resolution,[status(thm)],[c2625, c25])).
% 1.69/1.93 cnf(c2714,plain,aNormalFormOfIn0(skolem0004,skolem0003,xR),inference(resolution,[status(thm)],[c2633, c979])).
% 1.69/1.93 cnf(c2717,plain,~aElement0(skolem0003)|~aRewritingSystem0(xR)|aElement0(skolem0004),inference(resolution,[status(thm)],[c2714, c55])).
% 1.69/1.93 cnf(c2718,plain,~aElement0(skolem0003)|aElement0(skolem0004),inference(resolution,[status(thm)],[c2717, c43])).
% 1.69/1.93 cnf(c2719,plain,aElement0(skolem0004),inference(resolution,[status(thm)],[c2718, c2061])).
% 1.69/1.93 cnf(c26,negated_conjecture,~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|sdtmndtasgtdt0(xb,xR,skolem0004),inference(split_conjunct,[status(thm)],[c15])).
% 1.69/1.93 cnf(c2631,plain,~sdtmndtplgtdt0(xa,xR,xb)|sdtmndtasgtdt0(xb,xR,skolem0004),inference(resolution,[status(thm)],[c2625, c26])).
% 1.69/1.93 cnf(c2683,plain,sdtmndtasgtdt0(xb,xR,skolem0004),inference(resolution,[status(thm)],[c2631, c979])).
% 1.69/1.93 cnf(c27,negated_conjecture,~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|sdtmndtasgtdt0(xc,xR,skolem0004),inference(split_conjunct,[status(thm)],[c15])).
% 1.69/1.93 cnf(c2640,plain,~sdtmndtplgtdt0(xa,xR,xb)|sdtmndtasgtdt0(xc,xR,skolem0004),inference(resolution,[status(thm)],[c2625, c27])).
% 1.69/1.93 cnf(c2767,plain,sdtmndtasgtdt0(xc,xR,skolem0004),inference(resolution,[status(thm)],[c2640, c979])).
% 1.69/1.93 cnf(c2773,plain,~aElement0(skolem0004)|~sdtmndtasgtdt0(xb,xR,skolem0004),inference(resolution,[status(thm)],[c2767, c30])).
% 1.69/1.93 cnf(c2793,plain,~aElement0(skolem0004),inference(resolution,[status(thm)],[c2773, c2683])).
% 1.69/1.93 cnf(c2794,plain,$false,inference(resolution,[status(thm)],[c2793, c2719])).
% 1.69/1.93 % SZS output end CNFRefutation
% 1.69/1.93
% 1.69/1.93 % Initial clauses : 80
% 1.69/1.93 % Processed clauses : 554
% 1.69/1.93 % Factors computed : 21
% 1.69/1.93 % Resolvents computed: 2643
% 1.69/1.93 % Tautologies deleted: 15
% 1.69/1.93 % Forward subsumed : 231
% 1.69/1.93 % Backward subsumed : 215
% 1.69/1.93 % -------- CPU Time ---------
% 1.69/1.93 % User time : 1.558 s
% 1.69/1.93 % System time : 0.014 s
% 1.69/1.93 % Total time : 1.572 s
%------------------------------------------------------------------------------