%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM020+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:44 EDT 2024
% Result : Theorem 220.24s 220.52s
% Output : Refutation 220.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.14 % Problem : COM020+1 : TPTP v8.1.2. Released v4.0.0.
% 0.05/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n029.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Thu May 9 07:11:53 EDT 2024
% 0.15/0.37 % CPUTime :
% 220.24/220.52 % Version: 1.5
% 220.24/220.52 % SZS status Theorem
% 220.24/220.52 % SZS output start CNFRefutation
% 220.24/220.52 fof(m__755,plain,((aElement0(xu)&aReductOfIn0(xu,xa,xR))&sdtmndtasgtdt0(xu,xR,xb)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__755)).
% 220.24/220.52 cnf(c21,plain,aElement0(xu),inference(split_conjunct,[status(thm)],[m__755])).
% 220.24/220.52 fof(m__799,plain,((aElement0(xw)&sdtmndtasgtdt0(xu,xR,xw))&sdtmndtasgtdt0(xv,xR,xw)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__799)).
% 220.24/220.52 cnf(c15,plain,aElement0(xw),inference(split_conjunct,[status(thm)],[m__799])).
% 220.24/220.52 fof(m__656,plain,aRewritingSystem0(xR),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__656)).
% 220.24/220.52 cnf(c38,plain,aRewritingSystem0(xR),inference(split_conjunct,[status(thm)],[m__656])).
% 220.24/220.52 fof(m__818,plain,aNormalFormOfIn0(xd,xw,xR),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__818)).
% 220.24/220.52 cnf(c14,plain,aNormalFormOfIn0(xd,xw,xR),inference(split_conjunct,[status(thm)],[m__818])).
% 220.24/220.52 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/sandbox2/benchmark/theBenchmark.p', mNFRDef)).
% 220.24/220.52 fof(c44,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])).
% 220.24/220.52 fof(c45,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)],[c44])).
% 220.24/220.52 fof(c46,plain,(![X10]:(![X11]:((~aElement0(X10)|~aRewritingSystem0(X11))|((![X12]:(~aNormalFormOfIn0(X12,X10,X11)|((aElement0(X12)&sdtmndtasgtdt0(X10,X11,X12))&(![X13]:~aReductOfIn0(X13,X12,X11)))))&(![X14]:(((~aElement0(X14)|~sdtmndtasgtdt0(X10,X11,X14))|(?[X15]:aReductOfIn0(X15,X14,X11)))|aNormalFormOfIn0(X14,X10,X11))))))),inference(variable_rename,[status(thm)],[c45])).
% 220.24/220.52 fof(c48,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((~aElement0(X10)|~aRewritingSystem0(X11))|((~aNormalFormOfIn0(X12,X10,X11)|((aElement0(X12)&sdtmndtasgtdt0(X10,X11,X12))&~aReductOfIn0(X13,X12,X11)))&(((~aElement0(X14)|~sdtmndtasgtdt0(X10,X11,X14))|aReductOfIn0(skolem0003(X10,X11,X14),X14,X11))|aNormalFormOfIn0(X14,X10,X11))))))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,(![X10]:(![X11]:((~aElement0(X10)|~aRewritingSystem0(X11))|((![X12]:(~aNormalFormOfIn0(X12,X10,X11)|((aElement0(X12)&sdtmndtasgtdt0(X10,X11,X12))&(![X13]:~aReductOfIn0(X13,X12,X11)))))&(![X14]:(((~aElement0(X14)|~sdtmndtasgtdt0(X10,X11,X14))|aReductOfIn0(skolem0003(X10,X11,X14),X14,X11))|aNormalFormOfIn0(X14,X10,X11))))))),inference(skolemize,[status(esa)],[c46])).])).
% 220.24/220.52 fof(c49,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(((((~aElement0(X10)|~aRewritingSystem0(X11))|(~aNormalFormOfIn0(X12,X10,X11)|aElement0(X12)))&((~aElement0(X10)|~aRewritingSystem0(X11))|(~aNormalFormOfIn0(X12,X10,X11)|sdtmndtasgtdt0(X10,X11,X12))))&((~aElement0(X10)|~aRewritingSystem0(X11))|(~aNormalFormOfIn0(X12,X10,X11)|~aReductOfIn0(X13,X12,X11))))&((~aElement0(X10)|~aRewritingSystem0(X11))|(((~aElement0(X14)|~sdtmndtasgtdt0(X10,X11,X14))|aReductOfIn0(skolem0003(X10,X11,X14),X14,X11))|aNormalFormOfIn0(X14,X10,X11))))))))),inference(distribute,[status(thm)],[c48])).
% 220.24/220.52 cnf(c50,plain,~aElement0(X122)|~aRewritingSystem0(X120)|~aNormalFormOfIn0(X121,X122,X120)|aElement0(X121),inference(split_conjunct,[status(thm)],[c49])).
% 220.24/220.52 cnf(c151,plain,~aElement0(xw)|~aRewritingSystem0(xR)|aElement0(xd),inference(resolution,[status(thm)],[c50, c14])).
% 220.24/220.52 cnf(c152,plain,~aElement0(xw)|aElement0(xd),inference(resolution,[status(thm)],[c151, c38])).
% 220.24/220.52 cnf(c153,plain,aElement0(xd),inference(resolution,[status(thm)],[c152, c15])).
% 220.24/220.52 fof(m__731,plain,((aElement0(xa)&aElement0(xb))&aElement0(xc)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__731)).
% 220.24/220.52 cnf(c34,plain,aElement0(xb),inference(split_conjunct,[status(thm)],[m__731])).
% 220.24/220.52 fof(m__656_01,plain,(isLocallyConfluent0(xR)&isTerminating0(xR)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__656_01)).
% 220.24/220.52 cnf(c37,plain,isTerminating0(xR),inference(split_conjunct,[status(thm)],[m__656_01])).
% 220.24/220.52 cnf(c33,plain,aElement0(xa),inference(split_conjunct,[status(thm)],[m__731])).
% 220.24/220.52 fof(mTermin,plain,(![W0]:(aRewritingSystem0(W0)=>(isTerminating0(W0)<=>(![W1]:(![W2]:((aElement0(W1)&aElement0(W2))=>(sdtmndtplgtdt0(W1,W0,W2)=>iLess0(W2,W1)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mTermin)).
% 220.24/220.52 fof(c54,plain,(![W0]:(~aRewritingSystem0(W0)|((~isTerminating0(W0)|(![W1]:(![W2]:((~aElement0(W1)|~aElement0(W2))|(~sdtmndtplgtdt0(W1,W0,W2)|iLess0(W2,W1))))))&((?[W1]:(?[W2]:((aElement0(W1)&aElement0(W2))&(sdtmndtplgtdt0(W1,W0,W2)&~iLess0(W2,W1)))))|isTerminating0(W0))))),inference(fof_nnf,[status(thm)],[mTermin])).
% 220.24/220.52 fof(c55,plain,(![X16]:(~aRewritingSystem0(X16)|((~isTerminating0(X16)|(![X17]:(![X18]:((~aElement0(X17)|~aElement0(X18))|(~sdtmndtplgtdt0(X17,X16,X18)|iLess0(X18,X17))))))&((?[X19]:(?[X20]:((aElement0(X19)&aElement0(X20))&(sdtmndtplgtdt0(X19,X16,X20)&~iLess0(X20,X19)))))|isTerminating0(X16))))),inference(variable_rename,[status(thm)],[c54])).
% 220.24/220.52 fof(c57,plain,(![X16]:(![X17]:(![X18]:(~aRewritingSystem0(X16)|((~isTerminating0(X16)|((~aElement0(X17)|~aElement0(X18))|(~sdtmndtplgtdt0(X17,X16,X18)|iLess0(X18,X17))))&(((aElement0(skolem0004(X16))&aElement0(skolem0005(X16)))&(sdtmndtplgtdt0(skolem0004(X16),X16,skolem0005(X16))&~iLess0(skolem0005(X16),skolem0004(X16))))|isTerminating0(X16))))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,(![X16]:(~aRewritingSystem0(X16)|((~isTerminating0(X16)|(![X17]:(![X18]:((~aElement0(X17)|~aElement0(X18))|(~sdtmndtplgtdt0(X17,X16,X18)|iLess0(X18,X17))))))&(((aElement0(skolem0004(X16))&aElement0(skolem0005(X16)))&(sdtmndtplgtdt0(skolem0004(X16),X16,skolem0005(X16))&~iLess0(skolem0005(X16),skolem0004(X16))))|isTerminating0(X16))))),inference(skolemize,[status(esa)],[c55])).])).
% 220.24/220.52 fof(c58,plain,(![X16]:(![X17]:(![X18]:((~aRewritingSystem0(X16)|(~isTerminating0(X16)|((~aElement0(X17)|~aElement0(X18))|(~sdtmndtplgtdt0(X17,X16,X18)|iLess0(X18,X17)))))&(((~aRewritingSystem0(X16)|(aElement0(skolem0004(X16))|isTerminating0(X16)))&(~aRewritingSystem0(X16)|(aElement0(skolem0005(X16))|isTerminating0(X16))))&((~aRewritingSystem0(X16)|(sdtmndtplgtdt0(skolem0004(X16),X16,skolem0005(X16))|isTerminating0(X16)))&(~aRewritingSystem0(X16)|(~iLess0(skolem0005(X16),skolem0004(X16))|isTerminating0(X16))))))))),inference(distribute,[status(thm)],[c57])).
% 220.24/220.52 cnf(c59,plain,~aRewritingSystem0(X160)|~isTerminating0(X160)|~aElement0(X162)|~aElement0(X161)|~sdtmndtplgtdt0(X162,X160,X161)|iLess0(X161,X162),inference(split_conjunct,[status(thm)],[c58])).
% 220.24/220.52 cnf(c22,plain,aReductOfIn0(xu,xa,xR),inference(split_conjunct,[status(thm)],[m__755])).
% 220.24/220.52 fof(mTCDef,plain,(![W0]:(![W1]:(![W2]:(((aElement0(W0)&aRewritingSystem0(W1))&aElement0(W2))=>(sdtmndtplgtdt0(W0,W1,W2)<=>(aReductOfIn0(W2,W0,W1)|(?[W3]:((aElement0(W3)&aReductOfIn0(W3,W0,W1))&sdtmndtplgtdt0(W3,W1,W2))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mTCDef)).
% 220.24/220.52 fof(c104,plain,(![W0]:(![W1]:(![W2]:(((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|((~sdtmndtplgtdt0(W0,W1,W2)|(aReductOfIn0(W2,W0,W1)|(?[W3]:((aElement0(W3)&aReductOfIn0(W3,W0,W1))&sdtmndtplgtdt0(W3,W1,W2)))))&((~aReductOfIn0(W2,W0,W1)&(![W3]:((~aElement0(W3)|~aReductOfIn0(W3,W0,W1))|~sdtmndtplgtdt0(W3,W1,W2))))|sdtmndtplgtdt0(W0,W1,W2))))))),inference(fof_nnf,[status(thm)],[mTCDef])).
% 220.24/220.52 fof(c105,plain,(![X50]:(![X51]:(![X52]:(((~aElement0(X50)|~aRewritingSystem0(X51))|~aElement0(X52))|((~sdtmndtplgtdt0(X50,X51,X52)|(aReductOfIn0(X52,X50,X51)|(?[X53]:((aElement0(X53)&aReductOfIn0(X53,X50,X51))&sdtmndtplgtdt0(X53,X51,X52)))))&((~aReductOfIn0(X52,X50,X51)&(![X54]:((~aElement0(X54)|~aReductOfIn0(X54,X50,X51))|~sdtmndtplgtdt0(X54,X51,X52))))|sdtmndtplgtdt0(X50,X51,X52))))))),inference(variable_rename,[status(thm)],[c104])).
% 220.24/220.52 fof(c107,plain,(![X50]:(![X51]:(![X52]:(![X54]:(((~aElement0(X50)|~aRewritingSystem0(X51))|~aElement0(X52))|((~sdtmndtplgtdt0(X50,X51,X52)|(aReductOfIn0(X52,X50,X51)|((aElement0(skolem0014(X50,X51,X52))&aReductOfIn0(skolem0014(X50,X51,X52),X50,X51))&sdtmndtplgtdt0(skolem0014(X50,X51,X52),X51,X52))))&((~aReductOfIn0(X52,X50,X51)&((~aElement0(X54)|~aReductOfIn0(X54,X50,X51))|~sdtmndtplgtdt0(X54,X51,X52)))|sdtmndtplgtdt0(X50,X51,X52)))))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,(![X50]:(![X51]:(![X52]:(((~aElement0(X50)|~aRewritingSystem0(X51))|~aElement0(X52))|((~sdtmndtplgtdt0(X50,X51,X52)|(aReductOfIn0(X52,X50,X51)|((aElement0(skolem0014(X50,X51,X52))&aReductOfIn0(skolem0014(X50,X51,X52),X50,X51))&sdtmndtplgtdt0(skolem0014(X50,X51,X52),X51,X52))))&((~aReductOfIn0(X52,X50,X51)&(![X54]:((~aElement0(X54)|~aReductOfIn0(X54,X50,X51))|~sdtmndtplgtdt0(X54,X51,X52))))|sdtmndtplgtdt0(X50,X51,X52))))))),inference(skolemize,[status(esa)],[c105])).])).
% 220.24/220.52 fof(c108,plain,(![X50]:(![X51]:(![X52]:(![X54]:((((((~aElement0(X50)|~aRewritingSystem0(X51))|~aElement0(X52))|(~sdtmndtplgtdt0(X50,X51,X52)|(aReductOfIn0(X52,X50,X51)|aElement0(skolem0014(X50,X51,X52)))))&(((~aElement0(X50)|~aRewritingSystem0(X51))|~aElement0(X52))|(~sdtmndtplgtdt0(X50,X51,X52)|(aReductOfIn0(X52,X50,X51)|aReductOfIn0(skolem0014(X50,X51,X52),X50,X51)))))&(((~aElement0(X50)|~aRewritingSystem0(X51))|~aElement0(X52))|(~sdtmndtplgtdt0(X50,X51,X52)|(aReductOfIn0(X52,X50,X51)|sdtmndtplgtdt0(skolem0014(X50,X51,X52),X51,X52)))))&((((~aElement0(X50)|~aRewritingSystem0(X51))|~aElement0(X52))|(~aReductOfIn0(X52,X50,X51)|sdtmndtplgtdt0(X50,X51,X52)))&(((~aElement0(X50)|~aRewritingSystem0(X51))|~aElement0(X52))|(((~aElement0(X54)|~aReductOfIn0(X54,X50,X51))|~sdtmndtplgtdt0(X54,X51,X52))|sdtmndtplgtdt0(X50,X51,X52))))))))),inference(distribute,[status(thm)],[c107])).
% 220.24/220.52 cnf(c112,plain,~aElement0(X212)|~aRewritingSystem0(X211)|~aElement0(X213)|~aReductOfIn0(X213,X212,X211)|sdtmndtplgtdt0(X212,X211,X213),inference(split_conjunct,[status(thm)],[c108])).
% 220.24/220.52 cnf(c509,plain,~aElement0(xa)|~aRewritingSystem0(xR)|~aElement0(xu)|sdtmndtplgtdt0(xa,xR,xu),inference(resolution,[status(thm)],[c112, c22])).
% 220.24/220.52 cnf(c821,plain,~aElement0(xa)|~aRewritingSystem0(xR)|sdtmndtplgtdt0(xa,xR,xu),inference(resolution,[status(thm)],[c509, c21])).
% 220.24/220.52 cnf(c822,plain,~aElement0(xa)|sdtmndtplgtdt0(xa,xR,xu),inference(resolution,[status(thm)],[c821, c38])).
% 220.24/220.52 cnf(c823,plain,sdtmndtplgtdt0(xa,xR,xu),inference(resolution,[status(thm)],[c822, c33])).
% 220.24/220.52 cnf(c832,plain,~aRewritingSystem0(xR)|~isTerminating0(xR)|~aElement0(xa)|~aElement0(xu)|iLess0(xu,xa),inference(resolution,[status(thm)],[c823, c59])).
% 220.24/220.52 cnf(c969,plain,~aRewritingSystem0(xR)|~isTerminating0(xR)|~aElement0(xa)|iLess0(xu,xa),inference(resolution,[status(thm)],[c832, c21])).
% 220.24/220.52 cnf(c971,plain,~aRewritingSystem0(xR)|~isTerminating0(xR)|iLess0(xu,xa),inference(resolution,[status(thm)],[c969, c33])).
% 220.24/220.52 cnf(c972,plain,~aRewritingSystem0(xR)|iLess0(xu,xa),inference(resolution,[status(thm)],[c971, c37])).
% 220.24/220.52 cnf(c973,plain,iLess0(xu,xa),inference(resolution,[status(thm)],[c972, c38])).
% 220.24/220.52 cnf(c23,plain,sdtmndtasgtdt0(xu,xR,xb),inference(split_conjunct,[status(thm)],[m__755])).
% 220.24/220.52 fof(m__715,plain,(![W0]:(![W1]:(![W2]:(((((aElement0(W0)&aElement0(W1))&aElement0(W2))&sdtmndtasgtdt0(W0,xR,W1))&sdtmndtasgtdt0(W0,xR,W2))=>(iLess0(W0,xa)=>(?[W3]:((aElement0(W3)&sdtmndtasgtdt0(W1,xR,W3))&sdtmndtasgtdt0(W2,xR,W3)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__715)).
% 220.24/220.52 fof(c26,plain,(![W0]:(![W1]:(![W2]:(((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|~sdtmndtasgtdt0(W0,xR,W1))|~sdtmndtasgtdt0(W0,xR,W2))|(~iLess0(W0,xa)|(?[W3]:((aElement0(W3)&sdtmndtasgtdt0(W1,xR,W3))&sdtmndtasgtdt0(W2,xR,W3)))))))),inference(fof_nnf,[status(thm)],[m__715])).
% 220.24/220.52 fof(c27,plain,(![X3]:(![X4]:(![X5]:(((((~aElement0(X3)|~aElement0(X4))|~aElement0(X5))|~sdtmndtasgtdt0(X3,xR,X4))|~sdtmndtasgtdt0(X3,xR,X5))|(~iLess0(X3,xa)|(?[X6]:((aElement0(X6)&sdtmndtasgtdt0(X4,xR,X6))&sdtmndtasgtdt0(X5,xR,X6)))))))),inference(variable_rename,[status(thm)],[c26])).
% 220.24/220.52 fof(c28,plain,(![X3]:(![X4]:(![X5]:(((((~aElement0(X3)|~aElement0(X4))|~aElement0(X5))|~sdtmndtasgtdt0(X3,xR,X4))|~sdtmndtasgtdt0(X3,xR,X5))|(~iLess0(X3,xa)|((aElement0(skolem0001(X3,X4,X5))&sdtmndtasgtdt0(X4,xR,skolem0001(X3,X4,X5)))&sdtmndtasgtdt0(X5,xR,skolem0001(X3,X4,X5)))))))),inference(skolemize,[status(esa)],[c27])).
% 220.24/220.52 fof(c29,plain,(![X3]:(![X4]:(![X5]:(((((((~aElement0(X3)|~aElement0(X4))|~aElement0(X5))|~sdtmndtasgtdt0(X3,xR,X4))|~sdtmndtasgtdt0(X3,xR,X5))|(~iLess0(X3,xa)|aElement0(skolem0001(X3,X4,X5))))&(((((~aElement0(X3)|~aElement0(X4))|~aElement0(X5))|~sdtmndtasgtdt0(X3,xR,X4))|~sdtmndtasgtdt0(X3,xR,X5))|(~iLess0(X3,xa)|sdtmndtasgtdt0(X4,xR,skolem0001(X3,X4,X5)))))&(((((~aElement0(X3)|~aElement0(X4))|~aElement0(X5))|~sdtmndtasgtdt0(X3,xR,X4))|~sdtmndtasgtdt0(X3,xR,X5))|(~iLess0(X3,xa)|sdtmndtasgtdt0(X5,xR,skolem0001(X3,X4,X5)))))))),inference(distribute,[status(thm)],[c28])).
% 220.24/220.52 cnf(c30,plain,~aElement0(X124)|~aElement0(X125)|~aElement0(X126)|~sdtmndtasgtdt0(X124,xR,X125)|~sdtmndtasgtdt0(X124,xR,X126)|~iLess0(X124,xa)|aElement0(skolem0001(X124,X125,X126)),inference(split_conjunct,[status(thm)],[c29])).
% 220.24/220.52 cnf(c155,plain,~aElement0(xu)|~aElement0(X295)|~aElement0(xb)|~sdtmndtasgtdt0(xu,xR,X295)|~iLess0(xu,xa)|aElement0(skolem0001(xu,X295,xb)),inference(resolution,[status(thm)],[c30, c23])).
% 220.24/220.52 cnf(c16,plain,sdtmndtasgtdt0(xu,xR,xw),inference(split_conjunct,[status(thm)],[m__799])).
% 220.24/220.52 cnf(c51,plain,~aElement0(X140)|~aRewritingSystem0(X138)|~aNormalFormOfIn0(X139,X140,X138)|sdtmndtasgtdt0(X140,X138,X139),inference(split_conjunct,[status(thm)],[c49])).
% 220.24/220.52 cnf(c171,plain,~aElement0(xw)|~aRewritingSystem0(xR)|sdtmndtasgtdt0(xw,xR,xd),inference(resolution,[status(thm)],[c51, c14])).
% 220.24/220.52 cnf(c197,plain,~aElement0(xw)|sdtmndtasgtdt0(xw,xR,xd),inference(resolution,[status(thm)],[c171, c38])).
% 220.24/220.52 cnf(c198,plain,sdtmndtasgtdt0(xw,xR,xd),inference(resolution,[status(thm)],[c197, c15])).
% 220.24/220.52 fof(mTCRTrans,axiom,(![W0]:(![W1]:(![W2]:(![W3]:((((aElement0(W0)&aRewritingSystem0(W1))&aElement0(W2))&aElement0(W3))=>((sdtmndtasgtdt0(W0,W1,W2)&sdtmndtasgtdt0(W2,W1,W3))=>sdtmndtasgtdt0(W0,W1,W3))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mTCRTrans)).
% 220.24/220.52 fof(c92,plain,(![W0]:(![W1]:(![W2]:(![W3]:((((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|~aElement0(W3))|((~sdtmndtasgtdt0(W0,W1,W2)|~sdtmndtasgtdt0(W2,W1,W3))|sdtmndtasgtdt0(W0,W1,W3))))))),inference(fof_nnf,[status(thm)],[mTCRTrans])).
% 220.24/220.52 fof(c93,plain,(![X39]:(![X40]:(![X41]:(![X42]:((((~aElement0(X39)|~aRewritingSystem0(X40))|~aElement0(X41))|~aElement0(X42))|((~sdtmndtasgtdt0(X39,X40,X41)|~sdtmndtasgtdt0(X41,X40,X42))|sdtmndtasgtdt0(X39,X40,X42))))))),inference(variable_rename,[status(thm)],[c92])).
% 220.24/220.52 cnf(c94,plain,~aElement0(X200)|~aRewritingSystem0(X202)|~aElement0(X199)|~aElement0(X201)|~sdtmndtasgtdt0(X200,X202,X199)|~sdtmndtasgtdt0(X199,X202,X201)|sdtmndtasgtdt0(X200,X202,X201),inference(split_conjunct,[status(thm)],[c93])).
% 220.24/220.52 cnf(c364,plain,~aElement0(X623)|~aRewritingSystem0(xR)|~aElement0(xw)|~aElement0(xd)|~sdtmndtasgtdt0(X623,xR,xw)|sdtmndtasgtdt0(X623,xR,xd),inference(resolution,[status(thm)],[c94, c198])).
% 220.24/220.52 cnf(c2787,plain,~aElement0(xu)|~aRewritingSystem0(xR)|~aElement0(xw)|~aElement0(xd)|sdtmndtasgtdt0(xu,xR,xd),inference(resolution,[status(thm)],[c364, c16])).
% 220.24/220.52 cnf(c3015,plain,~aElement0(xu)|~aRewritingSystem0(xR)|~aElement0(xw)|sdtmndtasgtdt0(xu,xR,xd),inference(resolution,[status(thm)],[c2787, c153])).
% 220.24/220.52 cnf(c3016,plain,~aElement0(xu)|~aRewritingSystem0(xR)|sdtmndtasgtdt0(xu,xR,xd),inference(resolution,[status(thm)],[c3015, c15])).
% 220.24/220.52 cnf(c3017,plain,~aElement0(xu)|sdtmndtasgtdt0(xu,xR,xd),inference(resolution,[status(thm)],[c3016, c38])).
% 220.24/220.52 cnf(c3018,plain,sdtmndtasgtdt0(xu,xR,xd),inference(resolution,[status(thm)],[c3017, c21])).
% 220.24/220.52 cnf(c3040,plain,~aElement0(xu)|~aElement0(xd)|~aElement0(xb)|~iLess0(xu,xa)|aElement0(skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c3018, c155])).
% 220.24/220.52 cnf(c27570,plain,~aElement0(xu)|~aElement0(xd)|~aElement0(xb)|aElement0(skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c3040, c973])).
% 220.24/220.52 cnf(c27571,plain,~aElement0(xu)|~aElement0(xd)|aElement0(skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c27570, c34])).
% 220.24/220.52 cnf(c27573,plain,~aElement0(xu)|aElement0(skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c27571, c153])).
% 220.24/220.52 cnf(c27574,plain,aElement0(skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c27573, c21])).
% 220.24/220.52 fof(m__,conjecture,(?[W0]:((aElement0(W0)&sdtmndtasgtdt0(xb,xR,W0))&sdtmndtasgtdt0(xd,xR,W0))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 220.24/220.52 fof(c10,negated_conjecture,(~(?[W0]:((aElement0(W0)&sdtmndtasgtdt0(xb,xR,W0))&sdtmndtasgtdt0(xd,xR,W0)))),inference(assume_negation,[status(cth)],[m__])).
% 220.24/220.52 fof(c11,negated_conjecture,(![W0]:((~aElement0(W0)|~sdtmndtasgtdt0(xb,xR,W0))|~sdtmndtasgtdt0(xd,xR,W0))),inference(fof_nnf,[status(thm)],[c10])).
% 220.24/220.52 fof(c12,negated_conjecture,(![X2]:((~aElement0(X2)|~sdtmndtasgtdt0(xb,xR,X2))|~sdtmndtasgtdt0(xd,xR,X2))),inference(variable_rename,[status(thm)],[c11])).
% 220.24/220.52 cnf(c13,negated_conjecture,~aElement0(X119)|~sdtmndtasgtdt0(xb,xR,X119)|~sdtmndtasgtdt0(xd,xR,X119),inference(split_conjunct,[status(thm)],[c12])).
% 220.24/220.52 cnf(c31,plain,~aElement0(X132)|~aElement0(X133)|~aElement0(X134)|~sdtmndtasgtdt0(X132,xR,X133)|~sdtmndtasgtdt0(X132,xR,X134)|~iLess0(X132,xa)|sdtmndtasgtdt0(X133,xR,skolem0001(X132,X133,X134)),inference(split_conjunct,[status(thm)],[c29])).
% 220.24/220.52 cnf(c164,plain,~aElement0(xu)|~aElement0(X309)|~aElement0(xb)|~sdtmndtasgtdt0(xu,xR,X309)|~iLess0(xu,xa)|sdtmndtasgtdt0(X309,xR,skolem0001(xu,X309,xb)),inference(resolution,[status(thm)],[c31, c23])).
% 220.24/220.52 cnf(c3032,plain,~aElement0(xu)|~aElement0(xd)|~aElement0(xb)|~iLess0(xu,xa)|sdtmndtasgtdt0(xd,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c3018, c164])).
% 220.24/220.52 cnf(c77725,plain,~aElement0(xu)|~aElement0(xd)|~aElement0(xb)|sdtmndtasgtdt0(xd,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c3032, c973])).
% 220.24/220.52 cnf(c84027,plain,~aElement0(xu)|~aElement0(xd)|sdtmndtasgtdt0(xd,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c77725, c34])).
% 220.24/220.52 cnf(c84028,plain,~aElement0(xu)|sdtmndtasgtdt0(xd,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c84027, c153])).
% 220.24/220.52 cnf(c84029,plain,sdtmndtasgtdt0(xd,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c84028, c21])).
% 220.24/220.52 cnf(c84032,plain,~aElement0(skolem0001(xu,xd,xb))|~sdtmndtasgtdt0(xb,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c84029, c13])).
% 220.24/220.52 cnf(c32,plain,~aElement0(X145)|~aElement0(X146)|~aElement0(X147)|~sdtmndtasgtdt0(X145,xR,X146)|~sdtmndtasgtdt0(X145,xR,X147)|~iLess0(X145,xa)|sdtmndtasgtdt0(X147,xR,skolem0001(X145,X146,X147)),inference(split_conjunct,[status(thm)],[c29])).
% 220.24/220.52 cnf(c175,plain,~aElement0(xu)|~aElement0(X348)|~aElement0(xb)|~sdtmndtasgtdt0(xu,xR,X348)|~iLess0(xu,xa)|sdtmndtasgtdt0(xb,xR,skolem0001(xu,X348,xb)),inference(resolution,[status(thm)],[c32, c23])).
% 220.24/220.52 cnf(c3039,plain,~aElement0(xu)|~aElement0(xd)|~aElement0(xb)|~iLess0(xu,xa)|sdtmndtasgtdt0(xb,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c3018, c175])).
% 220.24/220.52 cnf(c77977,plain,~aElement0(xu)|~aElement0(xd)|~aElement0(xb)|sdtmndtasgtdt0(xb,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c3039, c973])).
% 220.24/220.52 cnf(c84068,plain,~aElement0(xu)|~aElement0(xd)|sdtmndtasgtdt0(xb,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c77977, c34])).
% 220.24/220.52 cnf(c84069,plain,~aElement0(xu)|sdtmndtasgtdt0(xb,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c84068, c153])).
% 220.24/220.52 cnf(c84070,plain,sdtmndtasgtdt0(xb,xR,skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c84069, c21])).
% 220.24/220.52 cnf(c84082,plain,~aElement0(skolem0001(xu,xd,xb)),inference(resolution,[status(thm)],[c84070, c84032])).
% 220.24/220.52 cnf(c84098,plain,$false,inference(resolution,[status(thm)],[c84082, c27574])).
% 220.24/220.52 % SZS output end CNFRefutation
% 220.24/220.52
% 220.24/220.52 % Initial clauses : 78
% 220.24/220.52 % Processed clauses : 6174
% 220.24/220.52 % Factors computed : 107
% 220.24/220.52 % Resolvents computed: 83867
% 220.24/220.52 % Tautologies deleted: 154
% 220.24/220.52 % Forward subsumed : 6182
% 220.24/220.52 % Backward subsumed : 1525
% 220.24/220.52 % -------- CPU Time ---------
% 220.24/220.52 % User time : 219.798 s
% 220.24/220.52 % System time : 0.250 s
% 220.24/220.52 % Total time : 220.048 s
%------------------------------------------------------------------------------