%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN067+2 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:37:09 EDT 2024
% Result : Theorem 0.42s 0.59s
% Output : Refutation 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUN067+2 : TPTP v8.1.2. Released v7.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 22:30:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.42/0.59 % Version: 1.5
% 0.42/0.59 % SZS status Theorem
% 0.42/0.59 % SZS output start CNFRefutation
% 0.42/0.59 fof(nonzerosexist,conjecture,(?[Y1]:(![Y2]:((~r1(Y2))|Y1!=Y2))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', nonzerosexist)).
% 0.42/0.59 fof(c4,negated_conjecture,(~(?[Y1]:(![Y2]:((~r1(Y2))|Y1!=Y2)))),inference(assume_negation,[status(cth)],[nonzerosexist])).
% 0.42/0.59 fof(c5,negated_conjecture,(~(?[Y1]:(![Y2]:(~r1(Y2)|Y1!=Y2)))),inference(fof_simplification,[status(thm)],[c4])).
% 0.42/0.59 fof(c6,negated_conjecture,(![Y1]:(?[Y2]:(r1(Y2)&Y1=Y2))),inference(fof_nnf,[status(thm)],[c5])).
% 0.42/0.59 fof(c7,negated_conjecture,(![X2]:(?[X3]:(r1(X3)&X2=X3))),inference(variable_rename,[status(thm)],[c6])).
% 0.42/0.59 fof(c8,negated_conjecture,(![X2]:(r1(skolem0001(X2))&X2=skolem0001(X2))),inference(skolemize,[status(esa)],[c7])).
% 0.42/0.59 cnf(c9,negated_conjecture,r1(skolem0001(X48)),inference(split_conjunct,[status(thm)],[c8])).
% 0.42/0.59 cnf(symmetry,axiom,X52!=X53|X53=X52,theory(equality)).
% 0.42/0.59 cnf(c10,negated_conjecture,X55=skolem0001(X55),inference(split_conjunct,[status(thm)],[c8])).
% 0.42/0.59 cnf(c84,plain,skolem0001(X58)=X58,inference(resolution,[status(thm)],[c10, symmetry])).
% 0.42/0.59 cnf(c0,axiom,X70!=X69|~r1(X70)|r1(X69),theory(equality)).
% 0.42/0.59 cnf(c94,plain,~r1(skolem0001(X120))|r1(X120),inference(resolution,[status(thm)],[c0, c84])).
% 0.42/0.59 cnf(c148,plain,r1(X122),inference(resolution,[status(thm)],[c94, c9])).
% 0.42/0.59 fof(axiom_1,axiom,(?[Y24]:(![X19]:(((~r1(X19))&X19!=Y24)|(r1(X19)&X19=Y24)))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_1)).
% 0.42/0.59 fof(c75,plain,(?[Y24]:(![X19]:((~r1(X19)&X19!=Y24)|(r1(X19)&X19=Y24)))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.42/0.59 fof(c76,plain,(?[X45]:(![X46]:((~r1(X46)&X46!=X45)|(r1(X46)&X46=X45)))),inference(variable_rename,[status(thm)],[c75])).
% 0.42/0.59 fof(c77,plain,(![X46]:((~r1(X46)&X46!=skolem0021)|(r1(X46)&X46=skolem0021))),inference(skolemize,[status(esa)],[c76])).
% 0.42/0.59 fof(c78,plain,(![X46]:(((~r1(X46)|r1(X46))&(~r1(X46)|X46=skolem0021))&((X46!=skolem0021|r1(X46))&(X46!=skolem0021|X46=skolem0021)))),inference(distribute,[status(thm)],[c77])).
% 0.42/0.59 cnf(c80,plain,~r1(X83)|X83=skolem0021,inference(split_conjunct,[status(thm)],[c78])).
% 0.42/0.59 cnf(c153,plain,X123=skolem0021,inference(resolution,[status(thm)],[c148, c80])).
% 0.42/0.59 cnf(transitivity,axiom,X60!=X61|X61!=X59|X60=X59,theory(equality)).
% 0.42/0.59 cnf(c154,plain,skolem0021=X124,inference(resolution,[status(thm)],[c153, symmetry])).
% 0.42/0.59 cnf(c157,plain,X152!=skolem0021|X152=X151,inference(resolution,[status(thm)],[c154, transitivity])).
% 0.42/0.59 cnf(c175,plain,X153=X154,inference(resolution,[status(thm)],[c157, c153])).
% 0.42/0.59 fof(axiom_7a,axiom,(![X7]:(![Y10]:((![Y20]:((~r1(Y20))|Y20!=Y10))|(~r2(X7,Y10))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_7a)).
% 0.42/0.59 fof(c11,plain,(![X7]:(![Y10]:((![Y20]:(~r1(Y20)|Y20!=Y10))|~r2(X7,Y10)))),inference(fof_simplification,[status(thm)],[axiom_7a])).
% 0.42/0.59 fof(c13,plain,(![X4]:(![X5]:(![X6]:((~r1(X6)|X6!=X5)|~r2(X4,X5))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,(![X4]:(![X5]:((![X6]:(~r1(X6)|X6!=X5))|~r2(X4,X5)))),inference(variable_rename,[status(thm)],[c11])).])).
% 0.42/0.59 cnf(c14,plain,~r1(X111)|X111!=X109|~r2(X110,X109),inference(split_conjunct,[status(thm)],[c13])).
% 0.42/0.59 fof(axiom_2,axiom,(![X11]:(?[Y21]:(![X12]:(((~r2(X11,X12))&X12!=Y21)|(r2(X11,X12)&X12=Y21))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_2)).
% 0.42/0.59 fof(c67,plain,(![X11]:(?[Y21]:(![X12]:((~r2(X11,X12)&X12!=Y21)|(r2(X11,X12)&X12=Y21))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.42/0.59 fof(c68,plain,(![X42]:(?[X43]:(![X44]:((~r2(X42,X44)&X44!=X43)|(r2(X42,X44)&X44=X43))))),inference(variable_rename,[status(thm)],[c67])).
% 0.42/0.59 fof(c69,plain,(![X42]:(![X44]:((~r2(X42,X44)&X44!=skolem0020(X42))|(r2(X42,X44)&X44=skolem0020(X42))))),inference(skolemize,[status(esa)],[c68])).
% 0.42/0.59 fof(c70,plain,(![X42]:(![X44]:(((~r2(X42,X44)|r2(X42,X44))&(~r2(X42,X44)|X44=skolem0020(X42)))&((X44!=skolem0020(X42)|r2(X42,X44))&(X44!=skolem0020(X42)|X44=skolem0020(X42)))))),inference(distribute,[status(thm)],[c69])).
% 0.42/0.59 cnf(c73,plain,X176!=skolem0020(X175)|r2(X175,X176),inference(split_conjunct,[status(thm)],[c70])).
% 0.42/0.59 cnf(c183,plain,r2(X178,X177),inference(resolution,[status(thm)],[c73, c175])).
% 0.42/0.59 cnf(c184,plain,~r1(X180)|X180!=X179,inference(resolution,[status(thm)],[c183, c14])).
% 0.42/0.59 cnf(c185,plain,~r1(X183),inference(resolution,[status(thm)],[c184, c175])).
% 0.42/0.59 cnf(c187,plain,$false,inference(resolution,[status(thm)],[c185, c148])).
% 0.42/0.59 % SZS output end CNFRefutation
% 0.42/0.59
% 0.42/0.59 % Initial clauses : 48
% 0.42/0.59 % Processed clauses : 55
% 0.42/0.59 % Factors computed : 2
% 0.42/0.59 % Resolvents computed: 103
% 0.42/0.59 % Tautologies deleted: 7
% 0.42/0.59 % Forward subsumed : 35
% 0.42/0.59 % Backward subsumed : 42
% 0.42/0.59 % -------- CPU Time ---------
% 0.42/0.59 % User time : 0.234 s
% 0.42/0.59 % System time : 0.017 s
% 0.42/0.59 % Total time : 0.251 s
%------------------------------------------------------------------------------