%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN068+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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 271.13s 271.39s
% Output : Refutation 271.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : NUN068+1 : TPTP v8.1.2. Released v7.3.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n003.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 22:30:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 271.13/271.39 % Version: 1.5
% 271.13/271.39 % SZS status Theorem
% 271.13/271.39 % SZS output start CNFRefutation
% 271.13/271.39 fof(axiom_7a,axiom,(![X7]:(![Y10]:((![Y20]:((~id(Y20,Y10))|(~r1(Y20))))|(~r2(X7,Y10))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_7a)).
% 271.13/271.39 fof(c12,plain,(![X7]:(![Y10]:((![Y20]:(~id(Y20,Y10)|~r1(Y20)))|~r2(X7,Y10)))),inference(fof_simplification,[status(thm)],[axiom_7a])).
% 271.13/271.39 fof(c14,plain,(![X6]:(![X7]:(![X8]:((~id(X8,X7)|~r1(X8))|~r2(X6,X7))))),inference(shift_quantors,[status(thm)],[fof(c13,plain,(![X6]:(![X7]:((![X8]:(~id(X8,X7)|~r1(X8)))|~r2(X6,X7)))),inference(variable_rename,[status(thm)],[c12])).])).
% 271.13/271.39 cnf(c15,plain,~id(X117,X116)|~r1(X117)|~r2(X118,X116),inference(split_conjunct,[status(thm)],[c14])).
% 271.13/271.39 fof(axiom_1a,axiom,(![X1]:(![X8]:(?[Y4]:((?[Y5]:(id(Y5,Y4)&(?[Y15]:(r2(X8,Y15)&r3(X1,Y15,Y5)))))&(?[Y7]:(r2(Y7,Y4)&r3(X1,X8,Y7))))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_1a)).
% 271.13/271.39 fof(c45,plain,(![X30]:(![X31]:(?[X32]:((?[X33]:(id(X33,X32)&(?[X34]:(r2(X31,X34)&r3(X30,X34,X33)))))&(?[X35]:(r2(X35,X32)&r3(X30,X31,X35))))))),inference(variable_rename,[status(thm)],[axiom_1a])).
% 271.13/271.39 fof(c46,plain,(![X30]:(![X31]:((id(skolem0017(X30,X31),skolem0016(X30,X31))&(r2(X31,skolem0018(X30,X31))&r3(X30,skolem0018(X30,X31),skolem0017(X30,X31))))&(r2(skolem0019(X30,X31),skolem0016(X30,X31))&r3(X30,X31,skolem0019(X30,X31)))))),inference(skolemize,[status(esa)],[c45])).
% 271.13/271.39 cnf(c50,plain,r2(skolem0019(X127,X128),skolem0016(X127,X128)),inference(split_conjunct,[status(thm)],[c46])).
% 271.13/271.39 cnf(c159,plain,~id(X304,skolem0016(X302,X303))|~r1(X304),inference(resolution,[status(thm)],[c50, c15])).
% 271.13/271.39 fof(axiom_4a,axiom,(![X4]:(?[Y9]:(id(Y9,X4)&(?[Y16]:(r1(Y16)&r3(X4,Y16,Y9)))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_4a)).
% 271.13/271.39 fof(c29,plain,(![X17]:(?[X18]:(id(X18,X17)&(?[X19]:(r1(X19)&r3(X17,X19,X18)))))),inference(variable_rename,[status(thm)],[axiom_4a])).
% 271.13/271.39 fof(c30,plain,(![X17]:(id(skolem0010(X17),X17)&(r1(skolem0011(X17))&r3(X17,skolem0011(X17),skolem0010(X17))))),inference(skolemize,[status(esa)],[c29])).
% 271.13/271.39 cnf(c31,plain,id(skolem0010(X77),X77),inference(split_conjunct,[status(thm)],[c30])).
% 271.13/271.39 fof(axiom_7,axiom,(![X23]:(![X24]:(![X25]:(((~id(X23,X24))|id(X23,X25))|(~id(X24,X25)))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_7)).
% 271.13/271.39 fof(c80,plain,(![X23]:(![X24]:(![X25]:((~id(X23,X24)|id(X23,X25))|~id(X24,X25))))),inference(fof_simplification,[status(thm)],[axiom_7])).
% 271.13/271.39 fof(c81,plain,(![X54]:(![X55]:(![X56]:((~id(X54,X55)|id(X54,X56))|~id(X55,X56))))),inference(variable_rename,[status(thm)],[c80])).
% 271.13/271.39 cnf(c82,plain,~id(X339,X337)|id(X339,X338)|~id(X337,X338),inference(split_conjunct,[status(thm)],[c81])).
% 271.13/271.39 cnf(c387,plain,~id(X366,skolem0010(X367))|id(X366,X367),inference(resolution,[status(thm)],[c82, c31])).
% 271.13/271.39 cnf(c433,plain,id(skolem0010(skolem0010(X377)),X377),inference(resolution,[status(thm)],[c387, c31])).
% 271.13/271.39 cnf(c443,plain,id(skolem0010(skolem0010(skolem0010(X436))),X436),inference(resolution,[status(thm)],[c433, c387])).
% 271.13/271.39 cnf(c633,plain,~r1(skolem0010(skolem0010(skolem0010(skolem0016(X2801,X2802))))),inference(resolution,[status(thm)],[c443, c159])).
% 271.13/271.39 fof(axiom_1,axiom,(?[Y24]:(![X19]:((id(X19,Y24)&r1(X19))|((~r1(X19))&(~id(X19,Y24)))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_1)).
% 271.13/271.39 fof(c112,plain,(?[Y24]:(![X19]:((id(X19,Y24)&r1(X19))|(~r1(X19)&~id(X19,Y24))))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 271.13/271.39 fof(c113,plain,(?[X71]:(![X72]:((id(X72,X71)&r1(X72))|(~r1(X72)&~id(X72,X71))))),inference(variable_rename,[status(thm)],[c112])).
% 271.13/271.39 fof(c114,plain,(![X72]:((id(X72,skolem0023)&r1(X72))|(~r1(X72)&~id(X72,skolem0023)))),inference(skolemize,[status(esa)],[c113])).
% 271.13/271.39 fof(c115,plain,(![X72]:(((id(X72,skolem0023)|~r1(X72))&(id(X72,skolem0023)|~id(X72,skolem0023)))&((r1(X72)|~r1(X72))&(r1(X72)|~id(X72,skolem0023))))),inference(distribute,[status(thm)],[c114])).
% 271.13/271.39 cnf(c119,plain,r1(X110)|~id(X110,skolem0023),inference(split_conjunct,[status(thm)],[c115])).
% 271.13/271.39 cnf(c116,plain,id(X98,skolem0023)|~r1(X98),inference(split_conjunct,[status(thm)],[c115])).
% 271.13/271.39 fof(axiom_5,axiom,(![X20]:id(X20,X20)),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_5)).
% 271.13/271.39 fof(c86,plain,(![X59]:id(X59,X59)),inference(variable_rename,[status(thm)],[axiom_5])).
% 271.13/271.39 cnf(c87,plain,id(X73,X73),inference(split_conjunct,[status(thm)],[c86])).
% 271.13/271.39 fof(axiom_2,axiom,(![X11]:(?[Y21]:(![X12]:((id(X12,Y21)&r2(X11,X12))|((~r2(X11,X12))&(~id(X12,Y21))))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_2)).
% 271.13/271.39 fof(c104,plain,(![X11]:(?[Y21]:(![X12]:((id(X12,Y21)&r2(X11,X12))|(~r2(X11,X12)&~id(X12,Y21)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 271.13/271.39 fof(c105,plain,(![X68]:(?[X69]:(![X70]:((id(X70,X69)&r2(X68,X70))|(~r2(X68,X70)&~id(X70,X69)))))),inference(variable_rename,[status(thm)],[c104])).
% 271.13/271.39 fof(c106,plain,(![X68]:(![X70]:((id(X70,skolem0022(X68))&r2(X68,X70))|(~r2(X68,X70)&~id(X70,skolem0022(X68)))))),inference(skolemize,[status(esa)],[c105])).
% 271.13/271.39 fof(c107,plain,(![X68]:(![X70]:(((id(X70,skolem0022(X68))|~r2(X68,X70))&(id(X70,skolem0022(X68))|~id(X70,skolem0022(X68))))&((r2(X68,X70)|~r2(X68,X70))&(r2(X68,X70)|~id(X70,skolem0022(X68))))))),inference(distribute,[status(thm)],[c106])).
% 271.13/271.39 cnf(c111,plain,r2(X242,X243)|~id(X243,skolem0022(X242)),inference(split_conjunct,[status(thm)],[c107])).
% 271.13/271.39 cnf(c298,plain,r2(X244,skolem0022(X244)),inference(resolution,[status(thm)],[c111, c87])).
% 271.13/271.39 cnf(c304,plain,~id(X258,skolem0022(X257))|~r1(X258),inference(resolution,[status(thm)],[c298, c15])).
% 271.13/271.39 cnf(c312,plain,~r1(skolem0022(X259)),inference(resolution,[status(thm)],[c304, c87])).
% 271.13/271.39 fof(nonzerosnononesexistid,conjecture,(?[Y1]:((![Y2]:((![Y3]:((~r1(Y3))|(~r2(Y3,Y2))))|(~id(Y1,Y2))))&(![Y4]:((~id(Y1,Y4))|(~r1(Y4)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', nonzerosnononesexistid)).
% 271.13/271.39 fof(c0,negated_conjecture,(~(?[Y1]:((![Y2]:((![Y3]:((~r1(Y3))|(~r2(Y3,Y2))))|(~id(Y1,Y2))))&(![Y4]:((~id(Y1,Y4))|(~r1(Y4))))))),inference(assume_negation,[status(cth)],[nonzerosnononesexistid])).
% 271.13/271.39 fof(c1,negated_conjecture,(~(?[Y1]:((![Y2]:((![Y3]:(~r1(Y3)|~r2(Y3,Y2)))|~id(Y1,Y2)))&(![Y4]:(~id(Y1,Y4)|~r1(Y4)))))),inference(fof_simplification,[status(thm)],[c0])).
% 271.13/271.39 fof(c2,negated_conjecture,(![Y1]:((?[Y2]:((?[Y3]:(r1(Y3)&r2(Y3,Y2)))&id(Y1,Y2)))|(?[Y4]:(id(Y1,Y4)&r1(Y4))))),inference(fof_nnf,[status(thm)],[c1])).
% 271.13/271.39 fof(c3,negated_conjecture,(![X2]:((?[X3]:((?[X4]:(r1(X4)&r2(X4,X3)))&id(X2,X3)))|(?[X5]:(id(X2,X5)&r1(X5))))),inference(variable_rename,[status(thm)],[c2])).
% 271.13/271.39 fof(c4,negated_conjecture,(![X2]:(((r1(skolem0002(X2))&r2(skolem0002(X2),skolem0001(X2)))&id(X2,skolem0001(X2)))|(id(X2,skolem0003(X2))&r1(skolem0003(X2))))),inference(skolemize,[status(esa)],[c3])).
% 271.13/271.39 fof(c5,negated_conjecture,(![X2]:((((r1(skolem0002(X2))|id(X2,skolem0003(X2)))&(r1(skolem0002(X2))|r1(skolem0003(X2))))&((r2(skolem0002(X2),skolem0001(X2))|id(X2,skolem0003(X2)))&(r2(skolem0002(X2),skolem0001(X2))|r1(skolem0003(X2)))))&((id(X2,skolem0001(X2))|id(X2,skolem0003(X2)))&(id(X2,skolem0001(X2))|r1(skolem0003(X2)))))),inference(distribute,[status(thm)],[c4])).
% 271.13/271.39 cnf(c7,negated_conjecture,r1(skolem0002(X87))|r1(skolem0003(X87)),inference(split_conjunct,[status(thm)],[c5])).
% 271.13/271.39 cnf(c6,negated_conjecture,r1(skolem0002(X78))|id(X78,skolem0003(X78)),inference(split_conjunct,[status(thm)],[c5])).
% 271.13/271.39 fof(axiom_8,axiom,(![X26]:(![X27]:(((~id(X26,X27))|((~r1(X26))&(~r1(X27))))|(r1(X26)&r1(X27))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_8)).
% 271.13/271.39 fof(c73,plain,(![X26]:(![X27]:((~id(X26,X27)|(~r1(X26)&~r1(X27)))|(r1(X26)&r1(X27))))),inference(fof_simplification,[status(thm)],[axiom_8])).
% 271.13/271.39 fof(c74,plain,(![X52]:(![X53]:((~id(X52,X53)|(~r1(X52)&~r1(X53)))|(r1(X52)&r1(X53))))),inference(variable_rename,[status(thm)],[c73])).
% 271.13/271.39 fof(c75,plain,(![X52]:(![X53]:((((~id(X52,X53)|~r1(X52))|r1(X52))&((~id(X52,X53)|~r1(X52))|r1(X53)))&(((~id(X52,X53)|~r1(X53))|r1(X52))&((~id(X52,X53)|~r1(X53))|r1(X53)))))),inference(distribute,[status(thm)],[c74])).
% 271.13/271.39 cnf(c78,plain,~id(X185,X186)|~r1(X186)|r1(X185),inference(split_conjunct,[status(thm)],[c75])).
% 271.13/271.39 cnf(c253,plain,~r1(skolem0003(X697))|r1(X697)|r1(skolem0002(X697)),inference(resolution,[status(thm)],[c78, c6])).
% 271.13/271.39 cnf(c2461,plain,r1(X698)|r1(skolem0002(X698)),inference(resolution,[status(thm)],[c253, c7])).
% 271.13/271.39 cnf(c2462,plain,r1(skolem0002(skolem0022(X699))),inference(resolution,[status(thm)],[c2461, c312])).
% 271.13/271.39 cnf(c2498,plain,id(skolem0002(skolem0022(X714)),skolem0023),inference(resolution,[status(thm)],[c2462, c116])).
% 271.13/271.39 cnf(c2593,plain,~id(X12006,skolem0002(skolem0022(X12007)))|id(X12006,skolem0023),inference(resolution,[status(thm)],[c2498, c82])).
% 271.13/271.39 fof(axiom_6,axiom,(![X21]:(![X22]:((~id(X21,X22))|id(X22,X21)))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_6)).
% 271.13/271.39 fof(c83,plain,(![X21]:(![X22]:(~id(X21,X22)|id(X22,X21)))),inference(fof_simplification,[status(thm)],[axiom_6])).
% 271.13/271.39 fof(c84,plain,(![X57]:(![X58]:(~id(X57,X58)|id(X58,X57)))),inference(variable_rename,[status(thm)],[c83])).
% 271.13/271.39 cnf(c85,plain,~id(X90,X91)|id(X91,X90),inference(split_conjunct,[status(thm)],[c84])).
% 271.13/271.39 cnf(c11,negated_conjecture,id(X113,skolem0001(X113))|r1(skolem0003(X113)),inference(split_conjunct,[status(thm)],[c5])).
% 271.13/271.39 cnf(c10,negated_conjecture,id(X108,skolem0001(X108))|id(X108,skolem0003(X108)),inference(split_conjunct,[status(thm)],[c5])).
% 271.13/271.39 cnf(c251,plain,~r1(skolem0003(X691))|r1(X691)|id(X691,skolem0001(X691)),inference(resolution,[status(thm)],[c78, c10])).
% 271.13/271.39 cnf(c2305,plain,r1(X692)|id(X692,skolem0001(X692)),inference(resolution,[status(thm)],[c251, c11])).
% 271.13/271.39 cnf(c2365,plain,r1(X694)|id(skolem0001(X694),X694),inference(resolution,[status(thm)],[c2305, c85])).
% 271.13/271.39 cnf(c2374,plain,id(skolem0001(skolem0022(X721)),skolem0022(X721)),inference(resolution,[status(thm)],[c2365, c312])).
% 271.13/271.39 fof(axiom_3a,axiom,(![X3]:(![X10]:((![Y12]:((![Y13]:((~id(Y13,Y12))|(~r2(X3,Y13))))|(~r2(X10,Y12))))|id(X3,X10)))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_3a)).
% 271.13/271.39 fof(c34,plain,(![X3]:(![X10]:((![Y12]:((![Y13]:(~id(Y13,Y12)|~r2(X3,Y13)))|~r2(X10,Y12)))|id(X3,X10)))),inference(fof_simplification,[status(thm)],[axiom_3a])).
% 271.13/271.39 fof(c36,plain,(![X20]:(![X21]:(![X22]:(![X23]:(((~id(X23,X22)|~r2(X20,X23))|~r2(X21,X22))|id(X20,X21)))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,(![X20]:(![X21]:((![X22]:((![X23]:(~id(X23,X22)|~r2(X20,X23)))|~r2(X21,X22)))|id(X20,X21)))),inference(variable_rename,[status(thm)],[c34])).])).
% 271.13/271.39 cnf(c37,plain,~id(X151,X150)|~r2(X149,X151)|~r2(X152,X150)|id(X149,X152),inference(split_conjunct,[status(thm)],[c36])).
% 271.13/271.39 cnf(c303,plain,~id(X969,skolem0022(X967))|~r2(X968,X969)|id(X968,X967),inference(resolution,[status(thm)],[c298, c37])).
% 271.13/271.39 cnf(c3693,plain,~r2(X7483,skolem0001(skolem0022(X7484)))|id(X7483,X7484),inference(resolution,[status(thm)],[c303, c2374])).
% 271.13/271.39 cnf(c9,negated_conjecture,r2(skolem0002(X102),skolem0001(X102))|r1(skolem0003(X102)),inference(split_conjunct,[status(thm)],[c5])).
% 271.13/271.39 cnf(c8,negated_conjecture,r2(skolem0002(X95),skolem0001(X95))|id(X95,skolem0003(X95)),inference(split_conjunct,[status(thm)],[c5])).
% 271.13/271.39 cnf(c125,plain,r2(skolem0002(X408),skolem0001(X408))|id(skolem0003(X408),X408),inference(resolution,[status(thm)],[c8, c85])).
% 271.13/271.39 cnf(c563,plain,r2(skolem0002(skolem0022(X2449)),skolem0001(skolem0022(X2449)))|~r1(skolem0003(skolem0022(X2449))),inference(resolution,[status(thm)],[c125, c304])).
% 271.13/271.39 cnf(c12836,plain,r2(skolem0002(skolem0022(X12674)),skolem0001(skolem0022(X12674))),inference(resolution,[status(thm)],[c563, c9])).
% 271.13/271.39 cnf(c141941,plain,id(skolem0002(skolem0022(X12675)),X12675),inference(resolution,[status(thm)],[c12836, c3693])).
% 271.13/271.39 cnf(c142144,plain,id(X12678,skolem0002(skolem0022(X12678))),inference(resolution,[status(thm)],[c141941, c85])).
% 271.13/271.39 cnf(c142267,plain,id(X12679,skolem0023),inference(resolution,[status(thm)],[c142144, c2593])).
% 271.13/271.39 cnf(c142385,plain,r1(X12680),inference(resolution,[status(thm)],[c142267, c119])).
% 271.13/271.39 cnf(c142424,plain,$false,inference(resolution,[status(thm)],[c142385, c633])).
% 271.13/271.39 % SZS output end CNFRefutation
% 271.13/271.39
% 271.13/271.39 % Initial clauses : 64
% 271.13/271.39 % Processed clauses : 3061
% 271.13/271.39 % Factors computed : 2
% 271.13/271.39 % Resolvents computed: 142363
% 271.13/271.39 % Tautologies deleted: 31
% 271.13/271.39 % Forward subsumed : 6301
% 271.13/271.39 % Backward subsumed : 1311
% 271.13/271.39 % -------- CPU Time ---------
% 271.13/271.39 % User time : 270.735 s
% 271.13/271.39 % System time : 0.223 s
% 271.13/271.39 % Total time : 270.958 s
%------------------------------------------------------------------------------