%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM012+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:42 EDT 2024
% Result : Theorem 1.67s 1.91s
% Output : Refutation 1.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : COM012+3 : TPTP v8.1.2. Released v4.0.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n020.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 07:11:38 EDT 2024
% 0.15/0.37 % CPUTime :
% 1.67/1.91 % Version: 1.5
% 1.67/1.91 % SZS status Theorem
% 1.67/1.91 % SZS output start CNFRefutation
% 1.67/1.91 fof(m__,conjecture,(((((xx=xy|((aReductOfIn0(xy,xx,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xx,xR))&sdtmndtplgtdt0(W0,xR,xy))))&sdtmndtplgtdt0(xx,xR,xy)))&sdtmndtasgtdt0(xx,xR,xy))&(xy=xz|((aReductOfIn0(xz,xy,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xy,xR))&sdtmndtplgtdt0(W0,xR,xz))))&sdtmndtplgtdt0(xy,xR,xz))))&sdtmndtasgtdt0(xy,xR,xz))=>((((xx=xz|aReductOfIn0(xz,xx,xR))|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xx,xR))&sdtmndtplgtdt0(W0,xR,xz))))|sdtmndtplgtdt0(xx,xR,xz))|sdtmndtasgtdt0(xx,xR,xz))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 1.67/1.91 fof(c6,negated_conjecture,(~(((((xx=xy|((aReductOfIn0(xy,xx,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xx,xR))&sdtmndtplgtdt0(W0,xR,xy))))&sdtmndtplgtdt0(xx,xR,xy)))&sdtmndtasgtdt0(xx,xR,xy))&(xy=xz|((aReductOfIn0(xz,xy,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xy,xR))&sdtmndtplgtdt0(W0,xR,xz))))&sdtmndtplgtdt0(xy,xR,xz))))&sdtmndtasgtdt0(xy,xR,xz))=>((((xx=xz|aReductOfIn0(xz,xx,xR))|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xx,xR))&sdtmndtplgtdt0(W0,xR,xz))))|sdtmndtplgtdt0(xx,xR,xz))|sdtmndtasgtdt0(xx,xR,xz)))),inference(assume_negation,[status(cth)],[m__])).
% 1.67/1.91 fof(c7,negated_conjecture,(((((xx=xy|((aReductOfIn0(xy,xx,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xx,xR))&sdtmndtplgtdt0(W0,xR,xy))))&sdtmndtplgtdt0(xx,xR,xy)))&sdtmndtasgtdt0(xx,xR,xy))&(xy=xz|((aReductOfIn0(xz,xy,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xy,xR))&sdtmndtplgtdt0(W0,xR,xz))))&sdtmndtplgtdt0(xy,xR,xz))))&sdtmndtasgtdt0(xy,xR,xz))&((((xx!=xz&~aReductOfIn0(xz,xx,xR))&(![W0]:((~aElement0(W0)|~aReductOfIn0(W0,xx,xR))|~sdtmndtplgtdt0(W0,xR,xz))))&~sdtmndtplgtdt0(xx,xR,xz))&~sdtmndtasgtdt0(xx,xR,xz))),inference(fof_nnf,[status(thm)],[c6])).
% 1.67/1.91 fof(c8,negated_conjecture,(((((xx=xy|((aReductOfIn0(xy,xx,xR)|(?[X2]:((aElement0(X2)&aReductOfIn0(X2,xx,xR))&sdtmndtplgtdt0(X2,xR,xy))))&sdtmndtplgtdt0(xx,xR,xy)))&sdtmndtasgtdt0(xx,xR,xy))&(xy=xz|((aReductOfIn0(xz,xy,xR)|(?[X3]:((aElement0(X3)&aReductOfIn0(X3,xy,xR))&sdtmndtplgtdt0(X3,xR,xz))))&sdtmndtplgtdt0(xy,xR,xz))))&sdtmndtasgtdt0(xy,xR,xz))&((((xx!=xz&~aReductOfIn0(xz,xx,xR))&(![X4]:((~aElement0(X4)|~aReductOfIn0(X4,xx,xR))|~sdtmndtplgtdt0(X4,xR,xz))))&~sdtmndtplgtdt0(xx,xR,xz))&~sdtmndtasgtdt0(xx,xR,xz))),inference(variable_rename,[status(thm)],[c7])).
% 1.67/1.91 fof(c10,negated_conjecture,(![X4]:(((((xx=xy|((aReductOfIn0(xy,xx,xR)|((aElement0(skolem0001)&aReductOfIn0(skolem0001,xx,xR))&sdtmndtplgtdt0(skolem0001,xR,xy)))&sdtmndtplgtdt0(xx,xR,xy)))&sdtmndtasgtdt0(xx,xR,xy))&(xy=xz|((aReductOfIn0(xz,xy,xR)|((aElement0(skolem0002)&aReductOfIn0(skolem0002,xy,xR))&sdtmndtplgtdt0(skolem0002,xR,xz)))&sdtmndtplgtdt0(xy,xR,xz))))&sdtmndtasgtdt0(xy,xR,xz))&((((xx!=xz&~aReductOfIn0(xz,xx,xR))&((~aElement0(X4)|~aReductOfIn0(X4,xx,xR))|~sdtmndtplgtdt0(X4,xR,xz)))&~sdtmndtplgtdt0(xx,xR,xz))&~sdtmndtasgtdt0(xx,xR,xz)))),inference(shift_quantors,[status(thm)],[fof(c9,negated_conjecture,(((((xx=xy|((aReductOfIn0(xy,xx,xR)|((aElement0(skolem0001)&aReductOfIn0(skolem0001,xx,xR))&sdtmndtplgtdt0(skolem0001,xR,xy)))&sdtmndtplgtdt0(xx,xR,xy)))&sdtmndtasgtdt0(xx,xR,xy))&(xy=xz|((aReductOfIn0(xz,xy,xR)|((aElement0(skolem0002)&aReductOfIn0(skolem0002,xy,xR))&sdtmndtplgtdt0(skolem0002,xR,xz)))&sdtmndtplgtdt0(xy,xR,xz))))&sdtmndtasgtdt0(xy,xR,xz))&((((xx!=xz&~aReductOfIn0(xz,xx,xR))&(![X4]:((~aElement0(X4)|~aReductOfIn0(X4,xx,xR))|~sdtmndtplgtdt0(X4,xR,xz))))&~sdtmndtplgtdt0(xx,xR,xz))&~sdtmndtasgtdt0(xx,xR,xz))),inference(skolemize,[status(esa)],[c8])).])).
% 1.67/1.91 fof(c11,negated_conjecture,(![X4]:((((((((xx=xy|(aReductOfIn0(xy,xx,xR)|aElement0(skolem0001)))&(xx=xy|(aReductOfIn0(xy,xx,xR)|aReductOfIn0(skolem0001,xx,xR))))&(xx=xy|(aReductOfIn0(xy,xx,xR)|sdtmndtplgtdt0(skolem0001,xR,xy))))&(xx=xy|sdtmndtplgtdt0(xx,xR,xy)))&sdtmndtasgtdt0(xx,xR,xy))&((((xy=xz|(aReductOfIn0(xz,xy,xR)|aElement0(skolem0002)))&(xy=xz|(aReductOfIn0(xz,xy,xR)|aReductOfIn0(skolem0002,xy,xR))))&(xy=xz|(aReductOfIn0(xz,xy,xR)|sdtmndtplgtdt0(skolem0002,xR,xz))))&(xy=xz|sdtmndtplgtdt0(xy,xR,xz))))&sdtmndtasgtdt0(xy,xR,xz))&((((xx!=xz&~aReductOfIn0(xz,xx,xR))&((~aElement0(X4)|~aReductOfIn0(X4,xx,xR))|~sdtmndtplgtdt0(X4,xR,xz)))&~sdtmndtplgtdt0(xx,xR,xz))&~sdtmndtasgtdt0(xx,xR,xz)))),inference(distribute,[status(thm)],[c10])).
% 1.67/1.91 cnf(c25,negated_conjecture,~sdtmndtplgtdt0(xx,xR,xz),inference(split_conjunct,[status(thm)],[c11])).
% 1.67/1.91 fof(m__349,plain,(((aElement0(xx)&aRewritingSystem0(xR))&aElement0(xy))&aElement0(xz)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__349)).
% 1.67/1.91 cnf(c27,plain,aElement0(xx),inference(split_conjunct,[status(thm)],[m__349])).
% 1.67/1.91 cnf(c28,plain,aRewritingSystem0(xR),inference(split_conjunct,[status(thm)],[m__349])).
% 1.67/1.91 cnf(c29,plain,aElement0(xy),inference(split_conjunct,[status(thm)],[m__349])).
% 1.67/1.91 cnf(c30,plain,aElement0(xz),inference(split_conjunct,[status(thm)],[m__349])).
% 1.67/1.91 cnf(c26,negated_conjecture,~sdtmndtasgtdt0(xx,xR,xz),inference(split_conjunct,[status(thm)],[c11])).
% 1.67/1.91 cnf(symmetry,axiom,X22!=X21|X21=X22,theory(equality)).
% 1.67/1.91 cnf(c15,negated_conjecture,xx=xy|sdtmndtplgtdt0(xx,xR,xy),inference(split_conjunct,[status(thm)],[c11])).
% 1.67/1.91 cnf(c67,plain,sdtmndtplgtdt0(xx,xR,xy)|xy=xx,inference(resolution,[status(thm)],[c15, symmetry])).
% 1.67/1.91 cnf(reflexivity,axiom,X20=X20,theory(equality)).
% 1.67/1.91 cnf(c21,negated_conjecture,sdtmndtasgtdt0(xy,xR,xz),inference(split_conjunct,[status(thm)],[c11])).
% 1.67/1.91 cnf(c5,axiom,X59!=X57|X56!=X60|X55!=X58|~sdtmndtasgtdt0(X59,X56,X55)|sdtmndtasgtdt0(X57,X60,X58),theory(equality)).
% 1.67/1.91 cnf(c87,plain,xy!=X89|xR!=X87|xz!=X88|sdtmndtasgtdt0(X89,X87,X88),inference(resolution,[status(thm)],[c5, c21])).
% 1.67/1.91 cnf(c228,plain,xy!=X90|xR!=X91|sdtmndtasgtdt0(X90,X91,xz),inference(resolution,[status(thm)],[c87, reflexivity])).
% 1.67/1.91 cnf(c231,plain,xy!=X92|sdtmndtasgtdt0(X92,xR,xz),inference(resolution,[status(thm)],[c228, reflexivity])).
% 1.67/1.91 cnf(c235,plain,sdtmndtasgtdt0(xx,xR,xz)|sdtmndtplgtdt0(xx,xR,xy),inference(resolution,[status(thm)],[c231, c67])).
% 1.67/1.91 cnf(c247,plain,sdtmndtplgtdt0(xx,xR,xy),inference(resolution,[status(thm)],[c235, c26])).
% 1.67/1.91 fof(mTCTrans,axiom,(![W0]:(![W1]:(![W2]:(![W3]:((((aElement0(W0)&aRewritingSystem0(W1))&aElement0(W2))&aElement0(W3))=>((sdtmndtplgtdt0(W0,W1,W2)&sdtmndtplgtdt0(W2,W1,W3))=>sdtmndtplgtdt0(W0,W1,W3))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mTCTrans)).
% 1.67/1.91 fof(c37,plain,(![W0]:(![W1]:(![W2]:(![W3]:((((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|~aElement0(W3))|((~sdtmndtplgtdt0(W0,W1,W2)|~sdtmndtplgtdt0(W2,W1,W3))|sdtmndtplgtdt0(W0,W1,W3))))))),inference(fof_nnf,[status(thm)],[mTCTrans])).
% 1.67/1.91 fof(c38,plain,(![X8]:(![X9]:(![X10]:(![X11]:((((~aElement0(X8)|~aRewritingSystem0(X9))|~aElement0(X10))|~aElement0(X11))|((~sdtmndtplgtdt0(X8,X9,X10)|~sdtmndtplgtdt0(X10,X9,X11))|sdtmndtplgtdt0(X8,X9,X11))))))),inference(variable_rename,[status(thm)],[c37])).
% 1.67/1.91 cnf(c39,plain,~aElement0(X81)|~aRewritingSystem0(X83)|~aElement0(X84)|~aElement0(X82)|~sdtmndtplgtdt0(X81,X83,X84)|~sdtmndtplgtdt0(X84,X83,X82)|sdtmndtplgtdt0(X81,X83,X82),inference(split_conjunct,[status(thm)],[c38])).
% 1.67/1.91 cnf(c20,negated_conjecture,xy=xz|sdtmndtplgtdt0(xy,xR,xz),inference(split_conjunct,[status(thm)],[c11])).
% 1.67/1.91 cnf(c16,negated_conjecture,sdtmndtasgtdt0(xx,xR,xy),inference(split_conjunct,[status(thm)],[c11])).
% 1.67/1.91 cnf(c88,plain,xx!=X98|xR!=X96|xy!=X97|sdtmndtasgtdt0(X98,X96,X97),inference(resolution,[status(thm)],[c5, c16])).
% 1.67/1.91 cnf(c261,plain,xx!=X278|xR!=X277|sdtmndtasgtdt0(X278,X277,xz)|sdtmndtplgtdt0(xy,xR,xz),inference(resolution,[status(thm)],[c88, c20])).
% 1.67/1.91 cnf(c1823,plain,xx!=X279|sdtmndtasgtdt0(X279,xR,xz)|sdtmndtplgtdt0(xy,xR,xz),inference(resolution,[status(thm)],[c261, reflexivity])).
% 1.67/1.91 cnf(c1824,plain,sdtmndtasgtdt0(xx,xR,xz)|sdtmndtplgtdt0(xy,xR,xz),inference(resolution,[status(thm)],[c1823, reflexivity])).
% 1.67/1.91 cnf(c1827,plain,sdtmndtplgtdt0(xy,xR,xz),inference(resolution,[status(thm)],[c1824, c26])).
% 1.67/1.91 cnf(c1838,plain,~aElement0(X761)|~aRewritingSystem0(xR)|~aElement0(xy)|~aElement0(xz)|~sdtmndtplgtdt0(X761,xR,xy)|sdtmndtplgtdt0(X761,xR,xz),inference(resolution,[status(thm)],[c1827, c39])).
% 1.67/1.91 cnf(c2196,plain,~aElement0(xx)|~aRewritingSystem0(xR)|~aElement0(xy)|~aElement0(xz)|sdtmndtplgtdt0(xx,xR,xz),inference(resolution,[status(thm)],[c1838, c247])).
% 1.67/1.91 cnf(c2198,plain,~aElement0(xx)|~aRewritingSystem0(xR)|~aElement0(xy)|sdtmndtplgtdt0(xx,xR,xz),inference(resolution,[status(thm)],[c2196, c30])).
% 1.67/1.91 cnf(c2199,plain,~aElement0(xx)|~aRewritingSystem0(xR)|sdtmndtplgtdt0(xx,xR,xz),inference(resolution,[status(thm)],[c2198, c29])).
% 1.67/1.91 cnf(c2200,plain,~aElement0(xx)|sdtmndtplgtdt0(xx,xR,xz),inference(resolution,[status(thm)],[c2199, c28])).
% 1.67/1.91 cnf(c2201,plain,sdtmndtplgtdt0(xx,xR,xz),inference(resolution,[status(thm)],[c2200, c27])).
% 1.67/1.91 cnf(c2204,plain,$false,inference(resolution,[status(thm)],[c2201, c25])).
% 1.67/1.91 % SZS output end CNFRefutation
% 1.67/1.91
% 1.67/1.91 % Initial clauses : 42
% 1.67/1.91 % Processed clauses : 414
% 1.67/1.91 % Factors computed : 7
% 1.67/1.91 % Resolvents computed: 2142
% 1.67/1.91 % Tautologies deleted: 5
% 1.67/1.91 % Forward subsumed : 928
% 1.67/1.91 % Backward subsumed : 244
% 1.67/1.91 % -------- CPU Time ---------
% 1.67/1.91 % User time : 1.524 s
% 1.67/1.91 % System time : 0.012 s
% 1.67/1.91 % Total time : 1.536 s
%------------------------------------------------------------------------------