%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN073+2 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:10 EDT 2024
% Result : Theorem 16.90s 17.15s
% Output : Refutation 16.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : NUN073+2 : TPTP v8.1.2. Released v7.3.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n011.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 : Wed May 8 22:31:23 EDT 2024
% 0.14/0.37 % CPUTime :
% 16.90/17.15 % Version: 1.5
% 16.90/17.15 % SZS status Theorem
% 16.90/17.15 % SZS output start CNFRefutation
% 16.90/17.15 cnf(reflexivity,axiom,X50=X50,theory(equality)).
% 16.90/17.15 fof(oneuneqtwo,conjecture,(![Y1]:((![Y2]:((![Y4]:((~r1(Y4))|(~r2(Y4,Y2))))|Y2!=Y1))|(![Y3]:((![Y5]:((~r1(Y5))|(~r2(Y5,Y3))))|(~r2(Y3,Y1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', oneuneqtwo)).
% 16.90/17.15 fof(c4,negated_conjecture,(~(![Y1]:((![Y2]:((![Y4]:((~r1(Y4))|(~r2(Y4,Y2))))|Y2!=Y1))|(![Y3]:((![Y5]:((~r1(Y5))|(~r2(Y5,Y3))))|(~r2(Y3,Y1))))))),inference(assume_negation,[status(cth)],[oneuneqtwo])).
% 16.90/17.15 fof(c5,negated_conjecture,(~(![Y1]:((![Y2]:((![Y4]:(~r1(Y4)|~r2(Y4,Y2)))|Y2!=Y1))|(![Y3]:((![Y5]:(~r1(Y5)|~r2(Y5,Y3)))|~r2(Y3,Y1)))))),inference(fof_simplification,[status(thm)],[c4])).
% 16.90/17.15 fof(c6,negated_conjecture,(?[Y1]:((?[Y2]:((?[Y4]:(r1(Y4)&r2(Y4,Y2)))&Y2=Y1))&(?[Y3]:((?[Y5]:(r1(Y5)&r2(Y5,Y3)))&r2(Y3,Y1))))),inference(fof_nnf,[status(thm)],[c5])).
% 16.90/17.15 fof(c7,negated_conjecture,(?[X2]:((?[X3]:((?[X4]:(r1(X4)&r2(X4,X3)))&X3=X2))&(?[X5]:((?[X6]:(r1(X6)&r2(X6,X5)))&r2(X5,X2))))),inference(variable_rename,[status(thm)],[c6])).
% 16.90/17.15 fof(c8,negated_conjecture,(((r1(skolem0003)&r2(skolem0003,skolem0002))&skolem0002=skolem0001)&((r1(skolem0005)&r2(skolem0005,skolem0004))&r2(skolem0004,skolem0001))),inference(skolemize,[status(esa)],[c7])).
% 16.90/17.15 cnf(c13,negated_conjecture,r2(skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c8])).
% 16.90/17.15 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)).
% 16.90/17.15 fof(c15,plain,(![X7]:(![Y10]:((![Y20]:(~r1(Y20)|Y20!=Y10))|~r2(X7,Y10)))),inference(fof_simplification,[status(thm)],[axiom_7a])).
% 16.90/17.15 fof(c17,plain,(![X7]:(![X8]:(![X9]:((~r1(X9)|X9!=X8)|~r2(X7,X8))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,(![X7]:(![X8]:((![X9]:(~r1(X9)|X9!=X8))|~r2(X7,X8)))),inference(variable_rename,[status(thm)],[c15])).])).
% 16.90/17.15 cnf(c18,plain,~r1(X100)|X100!=X99|~r2(X101,X99),inference(split_conjunct,[status(thm)],[c17])).
% 16.90/17.15 cnf(c142,plain,~r1(X133)|X133!=skolem0004,inference(resolution,[status(thm)],[c18, c13])).
% 16.90/17.15 cnf(c219,plain,~r1(skolem0004),inference(resolution,[status(thm)],[c142, reflexivity])).
% 16.90/17.15 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)).
% 16.90/17.15 fof(c79,plain,(?[Y24]:(![X19]:((~r1(X19)&X19!=Y24)|(r1(X19)&X19=Y24)))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 16.90/17.15 fof(c80,plain,(?[X48]:(![X49]:((~r1(X49)&X49!=X48)|(r1(X49)&X49=X48)))),inference(variable_rename,[status(thm)],[c79])).
% 16.90/17.15 fof(c81,plain,(![X49]:((~r1(X49)&X49!=skolem0025)|(r1(X49)&X49=skolem0025))),inference(skolemize,[status(esa)],[c80])).
% 16.90/17.15 fof(c82,plain,(![X49]:(((~r1(X49)|r1(X49))&(~r1(X49)|X49=skolem0025))&((X49!=skolem0025|r1(X49))&(X49!=skolem0025|X49=skolem0025)))),inference(distribute,[status(thm)],[c81])).
% 16.90/17.15 cnf(c85,plain,X108!=skolem0025|r1(X108),inference(split_conjunct,[status(thm)],[c82])).
% 16.90/17.15 cnf(transitivity,axiom,X57!=X59|X59!=X58|X57=X58,theory(equality)).
% 16.90/17.15 cnf(c12,negated_conjecture,r1(skolem0005),inference(split_conjunct,[status(thm)],[c8])).
% 16.90/17.15 cnf(c84,plain,~r1(X82)|X82=skolem0025,inference(split_conjunct,[status(thm)],[c82])).
% 16.90/17.15 cnf(c112,plain,skolem0005=skolem0025,inference(resolution,[status(thm)],[c84, c12])).
% 16.90/17.15 cnf(c121,plain,X272!=skolem0005|X272=skolem0025,inference(resolution,[status(thm)],[c112, transitivity])).
% 16.90/17.15 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)).
% 16.90/17.15 fof(c71,plain,(![X11]:(?[Y21]:(![X12]:((~r2(X11,X12)&X12!=Y21)|(r2(X11,X12)&X12=Y21))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 16.90/17.15 fof(c72,plain,(![X45]:(?[X46]:(![X47]:((~r2(X45,X47)&X47!=X46)|(r2(X45,X47)&X47=X46))))),inference(variable_rename,[status(thm)],[c71])).
% 16.90/17.15 fof(c73,plain,(![X45]:(![X47]:((~r2(X45,X47)&X47!=skolem0024(X45))|(r2(X45,X47)&X47=skolem0024(X45))))),inference(skolemize,[status(esa)],[c72])).
% 16.90/17.15 fof(c74,plain,(![X45]:(![X47]:(((~r2(X45,X47)|r2(X45,X47))&(~r2(X45,X47)|X47=skolem0024(X45)))&((X47!=skolem0024(X45)|r2(X45,X47))&(X47!=skolem0024(X45)|X47=skolem0024(X45)))))),inference(distribute,[status(thm)],[c73])).
% 16.90/17.15 cnf(c77,plain,X205!=skolem0024(X206)|r2(X206,X205),inference(split_conjunct,[status(thm)],[c74])).
% 16.90/17.15 cnf(c14,negated_conjecture,r2(skolem0004,skolem0001),inference(split_conjunct,[status(thm)],[c8])).
% 16.90/17.15 cnf(c76,plain,~r2(X194,X193)|X193=skolem0024(X194),inference(split_conjunct,[status(thm)],[c74])).
% 16.90/17.15 cnf(c304,plain,skolem0001=skolem0024(skolem0004),inference(resolution,[status(thm)],[c76, c14])).
% 16.90/17.15 cnf(c317,plain,X880!=skolem0001|X880=skolem0024(skolem0004),inference(resolution,[status(thm)],[c304, transitivity])).
% 16.90/17.15 cnf(symmetry,axiom,X53!=X54|X54=X53,theory(equality)).
% 16.90/17.15 cnf(c10,negated_conjecture,r2(skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c8])).
% 16.90/17.15 cnf(c303,plain,skolem0002=skolem0024(skolem0003),inference(resolution,[status(thm)],[c76, c10])).
% 16.90/17.15 cnf(c313,plain,skolem0024(skolem0003)=skolem0002,inference(resolution,[status(thm)],[c303, symmetry])).
% 16.90/17.15 cnf(c11,negated_conjecture,skolem0002=skolem0001,inference(split_conjunct,[status(thm)],[c8])).
% 16.90/17.15 cnf(c90,plain,X224!=skolem0002|X224=skolem0001,inference(resolution,[status(thm)],[transitivity, c11])).
% 16.90/17.15 cnf(c368,plain,skolem0024(skolem0003)=skolem0001,inference(resolution,[status(thm)],[c90, c313])).
% 16.90/17.15 cnf(c431,plain,X1077!=skolem0024(skolem0003)|X1077=skolem0001,inference(resolution,[status(thm)],[c368, transitivity])).
% 16.90/17.15 cnf(c9,negated_conjecture,r1(skolem0003),inference(split_conjunct,[status(thm)],[c8])).
% 16.90/17.15 cnf(c111,plain,skolem0003=skolem0025,inference(resolution,[status(thm)],[c84, c9])).
% 16.90/17.15 cnf(c117,plain,skolem0025=skolem0003,inference(resolution,[status(thm)],[c111, symmetry])).
% 16.90/17.15 cnf(c124,plain,X274!=skolem0025|X274=skolem0003,inference(resolution,[status(thm)],[c117, transitivity])).
% 16.90/17.15 cnf(c589,plain,skolem0005=skolem0003,inference(resolution,[status(thm)],[c124, c112])).
% 16.90/17.15 cnf(c1,axiom,X73!=X71|X72!=X74|~r2(X73,X72)|r2(X71,X74),theory(equality)).
% 16.90/17.15 cnf(c103,plain,skolem0005!=X242|skolem0004!=X243|r2(X242,X243),inference(resolution,[status(thm)],[c1, c13])).
% 16.90/17.15 cnf(c457,plain,skolem0005!=X1076|r2(X1076,skolem0004),inference(resolution,[status(thm)],[c103, reflexivity])).
% 16.90/17.15 cnf(c4504,plain,r2(skolem0003,skolem0004),inference(resolution,[status(thm)],[c457, c589])).
% 16.90/17.15 cnf(c4534,plain,skolem0004=skolem0024(skolem0003),inference(resolution,[status(thm)],[c4504, c76])).
% 16.90/17.15 cnf(c4626,plain,skolem0004=skolem0001,inference(resolution,[status(thm)],[c4534, c431])).
% 16.90/17.15 cnf(c4680,plain,skolem0004=skolem0024(skolem0004),inference(resolution,[status(thm)],[c4626, c317])).
% 16.90/17.15 cnf(c5004,plain,r2(skolem0004,skolem0004),inference(resolution,[status(thm)],[c4680, c77])).
% 16.90/17.15 fof(axiom_3a,axiom,(![X3]:(![X10]:((![Y12]:((![Y13]:((~r2(X3,Y13))|Y13!=Y12))|(~r2(X10,Y12))))|X3=X10))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_3a)).
% 16.90/17.15 fof(c37,plain,(![X3]:(![X10]:((![Y12]:((![Y13]:(~r2(X3,Y13)|Y13!=Y12))|~r2(X10,Y12)))|X3=X10))),inference(fof_simplification,[status(thm)],[axiom_3a])).
% 16.90/17.15 fof(c39,plain,(![X21]:(![X22]:(![X23]:(![X24]:(((~r2(X21,X24)|X24!=X23)|~r2(X22,X23))|X21=X22))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,(![X21]:(![X22]:((![X23]:((![X24]:(~r2(X21,X24)|X24!=X23))|~r2(X22,X23)))|X21=X22))),inference(variable_rename,[status(thm)],[c37])).])).
% 16.90/17.15 cnf(c40,plain,~r2(X130,X132)|X132!=X131|~r2(X129,X131)|X130=X129,inference(split_conjunct,[status(thm)],[c39])).
% 16.90/17.15 cnf(c211,plain,~r2(X487,X486)|X486!=skolem0004|X487=skolem0005,inference(resolution,[status(thm)],[c40, c13])).
% 16.90/17.15 cnf(c1842,plain,~r2(X2201,skolem0004)|X2201=skolem0005,inference(resolution,[status(thm)],[c211, reflexivity])).
% 16.90/17.15 cnf(c27839,plain,skolem0004=skolem0005,inference(resolution,[status(thm)],[c1842, c5004])).
% 16.90/17.15 cnf(c27937,plain,skolem0004=skolem0025,inference(resolution,[status(thm)],[c27839, c121])).
% 16.90/17.15 cnf(c28101,plain,r1(skolem0004),inference(resolution,[status(thm)],[c27937, c85])).
% 16.90/17.15 cnf(c28105,plain,$false,inference(resolution,[status(thm)],[c28101, c219])).
% 16.90/17.15 % SZS output end CNFRefutation
% 16.90/17.15
% 16.90/17.15 % Initial clauses : 52
% 16.90/17.15 % Processed clauses : 1023
% 16.90/17.15 % Factors computed : 18
% 16.90/17.15 % Resolvents computed: 28005
% 16.90/17.15 % Tautologies deleted: 11
% 16.90/17.15 % Forward subsumed : 1542
% 16.90/17.15 % Backward subsumed : 15
% 16.90/17.15 % -------- CPU Time ---------
% 16.90/17.15 % User time : 16.705 s
% 16.90/17.15 % System time : 0.064 s
% 16.90/17.15 % Total time : 16.769 s
%------------------------------------------------------------------------------