%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM016+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:43 EDT 2024
% Result : Theorem 0.60s 0.81s
% Output : Refutation 0.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : COM016+4 : TPTP v8.1.2. Released v4.0.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n005.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 07:08:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.60/0.81 % Version: 1.5
% 0.60/0.81 % SZS status Theorem
% 0.60/0.81 % SZS output start CNFRefutation
% 0.60/0.81 fof(m__731,plain,((aElement0(xa)&aElement0(xb))&aElement0(xc)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__731)).
% 0.60/0.81 cnf(c312,plain,aElement0(xb),inference(split_conjunct,[status(thm)],[m__731])).
% 0.60/0.81 cnf(reflexivity,axiom,X74=X74,theory(equality)).
% 0.60/0.81 fof(m__731_02,plain,((((aReductOfIn0(xb,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtplgtdt0(xa,xR,xb))&(aReductOfIn0(xc,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc)))))&sdtmndtplgtdt0(xa,xR,xc)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__731_02)).
% 0.60/0.81 fof(c20,plain,((((aReductOfIn0(xb,xa,xR)|(?[X4]:((aElement0(X4)&aReductOfIn0(X4,xa,xR))&sdtmndtplgtdt0(X4,xR,xb))))&sdtmndtplgtdt0(xa,xR,xb))&(aReductOfIn0(xc,xa,xR)|(?[X5]:((aElement0(X5)&aReductOfIn0(X5,xa,xR))&sdtmndtplgtdt0(X5,xR,xc)))))&sdtmndtplgtdt0(xa,xR,xc)),inference(variable_rename,[status(thm)],[m__731_02])).
% 0.60/0.81 fof(c21,plain,((((aReductOfIn0(xb,xa,xR)|((aElement0(skolem0001)&aReductOfIn0(skolem0001,xa,xR))&sdtmndtplgtdt0(skolem0001,xR,xb)))&sdtmndtplgtdt0(xa,xR,xb))&(aReductOfIn0(xc,xa,xR)|((aElement0(skolem0002)&aReductOfIn0(skolem0002,xa,xR))&sdtmndtplgtdt0(skolem0002,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc)),inference(skolemize,[status(esa)],[c20])).
% 0.60/0.81 fof(c22,plain,((((((aReductOfIn0(xb,xa,xR)|aElement0(skolem0001))&(aReductOfIn0(xb,xa,xR)|aReductOfIn0(skolem0001,xa,xR)))&(aReductOfIn0(xb,xa,xR)|sdtmndtplgtdt0(skolem0001,xR,xb)))&sdtmndtplgtdt0(xa,xR,xb))&(((aReductOfIn0(xc,xa,xR)|aElement0(skolem0002))&(aReductOfIn0(xc,xa,xR)|aReductOfIn0(skolem0002,xa,xR)))&(aReductOfIn0(xc,xa,xR)|sdtmndtplgtdt0(skolem0002,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc)),inference(distribute,[status(thm)],[c21])).
% 0.60/0.81 cnf(c23,plain,aReductOfIn0(xb,xa,xR)|aElement0(skolem0001),inference(split_conjunct,[status(thm)],[c22])).
% 0.60/0.81 fof(m__,conjecture,(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&((((W0=xb|aReductOfIn0(xb,W0,xR))|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,W0,xR))&sdtmndtplgtdt0(W1,xR,xb))))|sdtmndtplgtdt0(W0,xR,xb))|sdtmndtasgtdt0(W0,xR,xb)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 0.60/0.81 fof(c10,negated_conjecture,(~(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&((((W0=xb|aReductOfIn0(xb,W0,xR))|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,W0,xR))&sdtmndtplgtdt0(W1,xR,xb))))|sdtmndtplgtdt0(W0,xR,xb))|sdtmndtasgtdt0(W0,xR,xb))))),inference(assume_negation,[status(cth)],[m__])).
% 0.60/0.81 fof(c11,negated_conjecture,(![W0]:((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|((((W0!=xb&~aReductOfIn0(xb,W0,xR))&(![W1]:((~aElement0(W1)|~aReductOfIn0(W1,W0,xR))|~sdtmndtplgtdt0(W1,xR,xb))))&~sdtmndtplgtdt0(W0,xR,xb))&~sdtmndtasgtdt0(W0,xR,xb)))),inference(fof_nnf,[status(thm)],[c10])).
% 0.60/0.81 fof(c13,negated_conjecture,(![X2]:(![X3]:((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|((((X2!=xb&~aReductOfIn0(xb,X2,xR))&((~aElement0(X3)|~aReductOfIn0(X3,X2,xR))|~sdtmndtplgtdt0(X3,xR,xb)))&~sdtmndtplgtdt0(X2,xR,xb))&~sdtmndtasgtdt0(X2,xR,xb))))),inference(shift_quantors,[status(thm)],[fof(c12,negated_conjecture,(![X2]:((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|((((X2!=xb&~aReductOfIn0(xb,X2,xR))&(![X3]:((~aElement0(X3)|~aReductOfIn0(X3,X2,xR))|~sdtmndtplgtdt0(X3,xR,xb))))&~sdtmndtplgtdt0(X2,xR,xb))&~sdtmndtasgtdt0(X2,xR,xb)))),inference(variable_rename,[status(thm)],[c11])).])).
% 0.60/0.81 fof(c14,negated_conjecture,(![X2]:(![X3]:((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|X2!=xb)&((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~aReductOfIn0(xb,X2,xR)))&((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|((~aElement0(X3)|~aReductOfIn0(X3,X2,xR))|~sdtmndtplgtdt0(X3,xR,xb))))&((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb)))&((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtasgtdt0(X2,xR,xb))))),inference(distribute,[status(thm)],[c13])).
% 0.60/0.81 cnf(c15,negated_conjecture,~aElement0(X139)|~aReductOfIn0(X139,xa,xR)|X139!=xb,inference(split_conjunct,[status(thm)],[c14])).
% 0.60/0.81 cnf(c444,plain,~aElement0(xb)|xb!=xb|aElement0(skolem0001),inference(resolution,[status(thm)],[c15, c23])).
% 0.60/0.81 cnf(c447,plain,~aElement0(xb)|aElement0(skolem0001),inference(resolution,[status(thm)],[c444, reflexivity])).
% 0.60/0.81 cnf(c448,plain,aElement0(skolem0001),inference(resolution,[status(thm)],[c447, c312])).
% 0.60/0.81 cnf(c24,plain,aReductOfIn0(xb,xa,xR)|aReductOfIn0(skolem0001,xa,xR),inference(split_conjunct,[status(thm)],[c22])).
% 0.60/0.81 cnf(c19,negated_conjecture,~aElement0(X156)|~aReductOfIn0(X156,xa,xR)|~sdtmndtasgtdt0(X156,xR,xb),inference(split_conjunct,[status(thm)],[c14])).
% 0.60/0.81 fof(m__656,plain,aRewritingSystem0(xR),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__656)).
% 0.60/0.81 cnf(c335,plain,aRewritingSystem0(xR),inference(split_conjunct,[status(thm)],[m__656])).
% 0.60/0.81 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/sandbox2/benchmark/theBenchmark.p', mTCRDef)).
% 0.60/0.81 fof(c392,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])).
% 0.60/0.81 fof(c393,plain,(![X59]:(![X60]:(![X61]:(((~aElement0(X59)|~aRewritingSystem0(X60))|~aElement0(X61))|((~sdtmndtasgtdt0(X59,X60,X61)|(X59=X61|sdtmndtplgtdt0(X59,X60,X61)))&((X59!=X61&~sdtmndtplgtdt0(X59,X60,X61))|sdtmndtasgtdt0(X59,X60,X61))))))),inference(variable_rename,[status(thm)],[c392])).
% 0.60/0.81 fof(c394,plain,(![X59]:(![X60]:(![X61]:((((~aElement0(X59)|~aRewritingSystem0(X60))|~aElement0(X61))|(~sdtmndtasgtdt0(X59,X60,X61)|(X59=X61|sdtmndtplgtdt0(X59,X60,X61))))&((((~aElement0(X59)|~aRewritingSystem0(X60))|~aElement0(X61))|(X59!=X61|sdtmndtasgtdt0(X59,X60,X61)))&(((~aElement0(X59)|~aRewritingSystem0(X60))|~aElement0(X61))|(~sdtmndtplgtdt0(X59,X60,X61)|sdtmndtasgtdt0(X59,X60,X61)))))))),inference(distribute,[status(thm)],[c393])).
% 0.60/0.81 cnf(c396,plain,~aElement0(X201)|~aRewritingSystem0(X200)|~aElement0(X202)|X201!=X202|sdtmndtasgtdt0(X201,X200,X202),inference(split_conjunct,[status(thm)],[c394])).
% 0.60/0.81 cnf(c566,plain,~aElement0(X203)|~aRewritingSystem0(X204)|sdtmndtasgtdt0(X203,X204,X203),inference(resolution,[status(thm)],[c396, reflexivity])).
% 0.60/0.81 cnf(c567,plain,~aElement0(X208)|sdtmndtasgtdt0(X208,xR,X208),inference(resolution,[status(thm)],[c566, c335])).
% 0.60/0.81 cnf(c578,plain,sdtmndtasgtdt0(xb,xR,xb),inference(resolution,[status(thm)],[c567, c312])).
% 0.60/0.81 cnf(c584,plain,~aElement0(xb)|~aReductOfIn0(xb,xa,xR),inference(resolution,[status(thm)],[c578, c19])).
% 0.60/0.81 cnf(c590,plain,~aElement0(xb)|aReductOfIn0(skolem0001,xa,xR),inference(resolution,[status(thm)],[c584, c24])).
% 0.60/0.81 cnf(c596,plain,aReductOfIn0(skolem0001,xa,xR),inference(resolution,[status(thm)],[c590, c312])).
% 0.60/0.81 cnf(c18,negated_conjecture,~aElement0(X153)|~aReductOfIn0(X153,xa,xR)|~sdtmndtplgtdt0(X153,xR,xb),inference(split_conjunct,[status(thm)],[c14])).
% 0.60/0.81 cnf(c25,plain,aReductOfIn0(xb,xa,xR)|sdtmndtplgtdt0(skolem0001,xR,xb),inference(split_conjunct,[status(thm)],[c22])).
% 0.60/0.81 cnf(c589,plain,~aElement0(xb)|sdtmndtplgtdt0(skolem0001,xR,xb),inference(resolution,[status(thm)],[c584, c25])).
% 0.60/0.81 cnf(c591,plain,sdtmndtplgtdt0(skolem0001,xR,xb),inference(resolution,[status(thm)],[c589, c312])).
% 0.60/0.81 cnf(c592,plain,~aElement0(skolem0001)|~aReductOfIn0(skolem0001,xa,xR),inference(resolution,[status(thm)],[c591, c18])).
% 0.60/0.81 cnf(c604,plain,~aElement0(skolem0001),inference(resolution,[status(thm)],[c592, c596])).
% 0.60/0.81 cnf(c605,plain,$false,inference(resolution,[status(thm)],[c604, c448])).
% 0.60/0.81 % SZS output end CNFRefutation
% 0.60/0.81
% 0.60/0.81 % Initial clauses : 364
% 0.60/0.81 % Processed clauses : 124
% 0.60/0.81 % Factors computed : 1
% 0.60/0.81 % Resolvents computed: 182
% 0.60/0.81 % Tautologies deleted: 7
% 0.60/0.81 % Forward subsumed : 16
% 0.60/0.81 % Backward subsumed : 25
% 0.60/0.81 % -------- CPU Time ---------
% 0.60/0.81 % User time : 0.431 s
% 0.60/0.81 % System time : 0.010 s
% 0.60/0.81 % Total time : 0.441 s
%------------------------------------------------------------------------------