%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM021+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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 2.41s 2.62s
% Output : Refutation 2.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : COM021+4 : TPTP v8.1.2. Released v4.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 07:07:38 EDT 2024
% 0.13/0.36 % CPUTime :
% 2.41/2.62 % Version: 1.5
% 2.41/2.62 % SZS status Theorem
% 2.41/2.62 % SZS output start CNFRefutation
% 2.41/2.62 fof(m__,conjecture,((((xb=xd|aReductOfIn0(xd,xb,xR))|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xb,xR))&sdtmndtplgtdt0(W0,xR,xd))))|sdtmndtplgtdt0(xb,xR,xd))|sdtmndtasgtdt0(xb,xR,xd)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 2.41/2.62 fof(c10,negated_conjecture,(~((((xb=xd|aReductOfIn0(xd,xb,xR))|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xb,xR))&sdtmndtplgtdt0(W0,xR,xd))))|sdtmndtplgtdt0(xb,xR,xd))|sdtmndtasgtdt0(xb,xR,xd))),inference(assume_negation,[status(cth)],[m__])).
% 2.41/2.62 fof(c11,negated_conjecture,((((xb!=xd&~aReductOfIn0(xd,xb,xR))&(![W0]:((~aElement0(W0)|~aReductOfIn0(W0,xb,xR))|~sdtmndtplgtdt0(W0,xR,xd))))&~sdtmndtplgtdt0(xb,xR,xd))&~sdtmndtasgtdt0(xb,xR,xd)),inference(fof_nnf,[status(thm)],[c10])).
% 2.41/2.62 fof(c13,negated_conjecture,(![X2]:((((xb!=xd&~aReductOfIn0(xd,xb,xR))&((~aElement0(X2)|~aReductOfIn0(X2,xb,xR))|~sdtmndtplgtdt0(X2,xR,xd)))&~sdtmndtplgtdt0(xb,xR,xd))&~sdtmndtasgtdt0(xb,xR,xd))),inference(shift_quantors,[status(thm)],[fof(c12,negated_conjecture,((((xb!=xd&~aReductOfIn0(xd,xb,xR))&(![X2]:((~aElement0(X2)|~aReductOfIn0(X2,xb,xR))|~sdtmndtplgtdt0(X2,xR,xd))))&~sdtmndtplgtdt0(xb,xR,xd))&~sdtmndtasgtdt0(xb,xR,xd)),inference(variable_rename,[status(thm)],[c11])).])).
% 2.41/2.62 cnf(c18,negated_conjecture,~sdtmndtasgtdt0(xb,xR,xd),inference(split_conjunct,[status(thm)],[c13])).
% 2.41/2.62 cnf(reflexivity,axiom,X81=X81,theory(equality)).
% 2.41/2.62 cnf(symmetry,axiom,X82!=X83|X83=X82,theory(equality)).
% 2.41/2.62 fof(m__818,plain,((((aElement0(xd)&(xw=xd|((aReductOfIn0(xd,xw,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xw,xR))&sdtmndtplgtdt0(W0,xR,xd))))&sdtmndtplgtdt0(xw,xR,xd))))&sdtmndtasgtdt0(xw,xR,xd))&(~(?[W0]:aReductOfIn0(W0,xd,xR))))&aNormalFormOfIn0(xd,xw,xR)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__818)).
% 2.41/2.62 fof(c33,plain,((((aElement0(xd)&(xw=xd|((aReductOfIn0(xd,xw,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xw,xR))&sdtmndtplgtdt0(W0,xR,xd))))&sdtmndtplgtdt0(xw,xR,xd))))&sdtmndtasgtdt0(xw,xR,xd))&(![W0]:~aReductOfIn0(W0,xd,xR)))&aNormalFormOfIn0(xd,xw,xR)),inference(fof_nnf,[status(thm)],[m__818])).
% 2.41/2.62 fof(c34,plain,((((aElement0(xd)&(xw=xd|((aReductOfIn0(xd,xw,xR)|(?[X5]:((aElement0(X5)&aReductOfIn0(X5,xw,xR))&sdtmndtplgtdt0(X5,xR,xd))))&sdtmndtplgtdt0(xw,xR,xd))))&sdtmndtasgtdt0(xw,xR,xd))&(![X6]:~aReductOfIn0(X6,xd,xR)))&aNormalFormOfIn0(xd,xw,xR)),inference(variable_rename,[status(thm)],[c33])).
% 2.41/2.62 fof(c36,plain,(![X6]:((((aElement0(xd)&(xw=xd|((aReductOfIn0(xd,xw,xR)|((aElement0(skolem0003)&aReductOfIn0(skolem0003,xw,xR))&sdtmndtplgtdt0(skolem0003,xR,xd)))&sdtmndtplgtdt0(xw,xR,xd))))&sdtmndtasgtdt0(xw,xR,xd))&~aReductOfIn0(X6,xd,xR))&aNormalFormOfIn0(xd,xw,xR))),inference(shift_quantors,[status(thm)],[fof(c35,plain,((((aElement0(xd)&(xw=xd|((aReductOfIn0(xd,xw,xR)|((aElement0(skolem0003)&aReductOfIn0(skolem0003,xw,xR))&sdtmndtplgtdt0(skolem0003,xR,xd)))&sdtmndtplgtdt0(xw,xR,xd))))&sdtmndtasgtdt0(xw,xR,xd))&(![X6]:~aReductOfIn0(X6,xd,xR)))&aNormalFormOfIn0(xd,xw,xR)),inference(skolemize,[status(esa)],[c34])).])).
% 2.41/2.62 fof(c37,plain,(![X6]:((((aElement0(xd)&((((xw=xd|(aReductOfIn0(xd,xw,xR)|aElement0(skolem0003)))&(xw=xd|(aReductOfIn0(xd,xw,xR)|aReductOfIn0(skolem0003,xw,xR))))&(xw=xd|(aReductOfIn0(xd,xw,xR)|sdtmndtplgtdt0(skolem0003,xR,xd))))&(xw=xd|sdtmndtplgtdt0(xw,xR,xd))))&sdtmndtasgtdt0(xw,xR,xd))&~aReductOfIn0(X6,xd,xR))&aNormalFormOfIn0(xd,xw,xR))),inference(distribute,[status(thm)],[c36])).
% 2.41/2.62 cnf(c44,plain,~aReductOfIn0(X91,xd,xR),inference(split_conjunct,[status(thm)],[c37])).
% 2.41/2.62 fof(m__850,plain,((((aElement0(xx)&(xb=xx|((aReductOfIn0(xx,xb,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xb,xR))&sdtmndtplgtdt0(W0,xR,xx))))&sdtmndtplgtdt0(xb,xR,xx))))&sdtmndtasgtdt0(xb,xR,xx))&(xd=xx|((aReductOfIn0(xx,xd,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xd,xR))&sdtmndtplgtdt0(W0,xR,xx))))&sdtmndtplgtdt0(xd,xR,xx))))&sdtmndtasgtdt0(xd,xR,xx)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__850)).
% 2.41/2.62 fof(c19,plain,((((aElement0(xx)&(xb=xx|((aReductOfIn0(xx,xb,xR)|(?[X3]:((aElement0(X3)&aReductOfIn0(X3,xb,xR))&sdtmndtplgtdt0(X3,xR,xx))))&sdtmndtplgtdt0(xb,xR,xx))))&sdtmndtasgtdt0(xb,xR,xx))&(xd=xx|((aReductOfIn0(xx,xd,xR)|(?[X4]:((aElement0(X4)&aReductOfIn0(X4,xd,xR))&sdtmndtplgtdt0(X4,xR,xx))))&sdtmndtplgtdt0(xd,xR,xx))))&sdtmndtasgtdt0(xd,xR,xx)),inference(variable_rename,[status(thm)],[m__850])).
% 2.41/2.62 fof(c20,plain,((((aElement0(xx)&(xb=xx|((aReductOfIn0(xx,xb,xR)|((aElement0(skolem0001)&aReductOfIn0(skolem0001,xb,xR))&sdtmndtplgtdt0(skolem0001,xR,xx)))&sdtmndtplgtdt0(xb,xR,xx))))&sdtmndtasgtdt0(xb,xR,xx))&(xd=xx|((aReductOfIn0(xx,xd,xR)|((aElement0(skolem0002)&aReductOfIn0(skolem0002,xd,xR))&sdtmndtplgtdt0(skolem0002,xR,xx)))&sdtmndtplgtdt0(xd,xR,xx))))&sdtmndtasgtdt0(xd,xR,xx)),inference(skolemize,[status(esa)],[c19])).
% 2.41/2.62 fof(c21,plain,((((aElement0(xx)&((((xb=xx|(aReductOfIn0(xx,xb,xR)|aElement0(skolem0001)))&(xb=xx|(aReductOfIn0(xx,xb,xR)|aReductOfIn0(skolem0001,xb,xR))))&(xb=xx|(aReductOfIn0(xx,xb,xR)|sdtmndtplgtdt0(skolem0001,xR,xx))))&(xb=xx|sdtmndtplgtdt0(xb,xR,xx))))&sdtmndtasgtdt0(xb,xR,xx))&((((xd=xx|(aReductOfIn0(xx,xd,xR)|aElement0(skolem0002)))&(xd=xx|(aReductOfIn0(xx,xd,xR)|aReductOfIn0(skolem0002,xd,xR))))&(xd=xx|(aReductOfIn0(xx,xd,xR)|sdtmndtplgtdt0(skolem0002,xR,xx))))&(xd=xx|sdtmndtplgtdt0(xd,xR,xx))))&sdtmndtasgtdt0(xd,xR,xx)),inference(distribute,[status(thm)],[c20])).
% 2.41/2.62 cnf(c29,plain,xd=xx|aReductOfIn0(xx,xd,xR)|aReductOfIn0(skolem0002,xd,xR),inference(split_conjunct,[status(thm)],[c21])).
% 2.41/2.62 cnf(c627,plain,xd=xx|aReductOfIn0(skolem0002,xd,xR),inference(resolution,[status(thm)],[c29, c44])).
% 2.41/2.62 cnf(c773,plain,xd=xx,inference(resolution,[status(thm)],[c627, c44])).
% 2.41/2.62 cnf(c780,plain,xx=xd,inference(resolution,[status(thm)],[c773, symmetry])).
% 2.41/2.62 cnf(c27,plain,sdtmndtasgtdt0(xb,xR,xx),inference(split_conjunct,[status(thm)],[c21])).
% 2.41/2.62 cnf(c5,axiom,X119!=X121|X122!=X118|X117!=X120|~sdtmndtasgtdt0(X119,X122,X117)|sdtmndtasgtdt0(X121,X118,X120),theory(equality)).
% 2.41/2.62 cnf(c499,plain,xb!=X558|xR!=X556|xx!=X557|sdtmndtasgtdt0(X558,X556,X557),inference(resolution,[status(thm)],[c5, c27])).
% 2.41/2.62 cnf(c5155,plain,xb!=X567|xR!=X566|sdtmndtasgtdt0(X567,X566,xd),inference(resolution,[status(thm)],[c499, c780])).
% 2.41/2.62 cnf(c5202,plain,xb!=X568|sdtmndtasgtdt0(X568,xR,xd),inference(resolution,[status(thm)],[c5155, reflexivity])).
% 2.41/2.62 cnf(c5204,plain,sdtmndtasgtdt0(xb,xR,xd),inference(resolution,[status(thm)],[c5202, reflexivity])).
% 2.41/2.62 cnf(c5217,plain,$false,inference(resolution,[status(thm)],[c5204, c18])).
% 2.41/2.62 % SZS output end CNFRefutation
% 2.41/2.62
% 2.41/2.62 % Initial clauses : 408
% 2.41/2.62 % Processed clauses : 471
% 2.41/2.62 % Factors computed : 12
% 2.41/2.62 % Resolvents computed: 4726
% 2.41/2.62 % Tautologies deleted: 7
% 2.41/2.62 % Forward subsumed : 192
% 2.41/2.62 % Backward subsumed : 64
% 2.41/2.62 % -------- CPU Time ---------
% 2.41/2.62 % User time : 2.242 s
% 2.41/2.62 % System time : 0.023 s
% 2.41/2.62 % Total time : 2.265 s
%------------------------------------------------------------------------------