%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN081+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:11 EDT 2024
% Result : Theorem 12.57s 12.80s
% Output : Refutation 12.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUN081+1 : TPTP v8.1.2. Released v7.3.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n010.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:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 12.57/12.80 % Version: 1.5
% 12.57/12.80 % SZS status Theorem
% 12.57/12.80 % SZS output start CNFRefutation
% 12.57/12.80 fof(axiom_6a,axiom,(![X6]:((?[Y19]:(id(X6,Y19)&r1(Y19)))|(?[Y1]:(?[Y11]:(id(X6,Y11)&r2(Y1,Y11)))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_6a)).
% 12.57/12.80 fof(c9,plain,(![X12]:((?[X13]:(id(X12,X13)&r1(X13)))|(?[X14]:(?[X15]:(id(X12,X15)&r2(X14,X15)))))),inference(variable_rename,[status(thm)],[axiom_6a])).
% 12.57/12.80 fof(c10,plain,(![X12]:((id(X12,skolem0001(X12))&r1(skolem0001(X12)))|(id(X12,skolem0003(X12))&r2(skolem0002(X12),skolem0003(X12))))),inference(skolemize,[status(esa)],[c9])).
% 12.57/12.80 fof(c11,plain,(![X12]:(((id(X12,skolem0001(X12))|id(X12,skolem0003(X12)))&(id(X12,skolem0001(X12))|r2(skolem0002(X12),skolem0003(X12))))&((r1(skolem0001(X12))|id(X12,skolem0003(X12)))&(r1(skolem0001(X12))|r2(skolem0002(X12),skolem0003(X12)))))),inference(distribute,[status(thm)],[c10])).
% 12.57/12.80 cnf(c14,plain,r1(skolem0001(X119))|id(X119,skolem0003(X119)),inference(split_conjunct,[status(thm)],[c11])).
% 12.57/12.80 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)).
% 12.57/12.80 fof(c5,plain,(![X7]:(![Y10]:((![Y20]:(~id(Y20,Y10)|~r1(Y20)))|~r2(X7,Y10)))),inference(fof_simplification,[status(thm)],[axiom_7a])).
% 12.57/12.80 fof(c7,plain,(![X9]:(![X10]:(![X11]:((~id(X11,X10)|~r1(X11))|~r2(X9,X10))))),inference(shift_quantors,[status(thm)],[fof(c6,plain,(![X9]:(![X10]:((![X11]:(~id(X11,X10)|~r1(X11)))|~r2(X9,X10)))),inference(variable_rename,[status(thm)],[c5])).])).
% 12.57/12.80 cnf(c8,plain,~id(X98,X96)|~r1(X98)|~r2(X97,X96),inference(split_conjunct,[status(thm)],[c7])).
% 12.57/12.80 cnf(c15,plain,r1(skolem0001(X124))|r2(skolem0002(X124),skolem0003(X124)),inference(split_conjunct,[status(thm)],[c11])).
% 12.57/12.80 cnf(c142,plain,r1(skolem0001(X434))|~id(X433,skolem0003(X434))|~r1(X433),inference(resolution,[status(thm)],[c15, c8])).
% 12.57/12.80 cnf(c664,plain,r1(skolem0001(X435))|~r1(X435),inference(resolution,[status(thm)],[c142, c14])).
% 12.57/12.80 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)).
% 12.57/12.80 fof(c105,plain,(?[Y24]:(![X19]:((id(X19,Y24)&r1(X19))|(~r1(X19)&~id(X19,Y24))))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 12.57/12.80 fof(c106,plain,(?[X74]:(![X75]:((id(X75,X74)&r1(X75))|(~r1(X75)&~id(X75,X74))))),inference(variable_rename,[status(thm)],[c105])).
% 12.57/12.80 fof(c107,plain,(![X75]:((id(X75,skolem0020)&r1(X75))|(~r1(X75)&~id(X75,skolem0020)))),inference(skolemize,[status(esa)],[c106])).
% 12.57/12.80 fof(c108,plain,(![X75]:(((id(X75,skolem0020)|~r1(X75))&(id(X75,skolem0020)|~id(X75,skolem0020)))&((r1(X75)|~r1(X75))&(r1(X75)|~id(X75,skolem0020))))),inference(distribute,[status(thm)],[c107])).
% 12.57/12.80 cnf(c112,plain,r1(X121)|~id(X121,skolem0020),inference(split_conjunct,[status(thm)],[c108])).
% 12.57/12.80 fof(axiom_6,axiom,(![X21]:(![X22]:((~id(X21,X22))|id(X22,X21)))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_6)).
% 12.57/12.80 fof(c76,plain,(![X21]:(![X22]:(~id(X21,X22)|id(X22,X21)))),inference(fof_simplification,[status(thm)],[axiom_6])).
% 12.57/12.80 fof(c77,plain,(![X60]:(![X61]:(~id(X60,X61)|id(X61,X60)))),inference(variable_rename,[status(thm)],[c76])).
% 12.57/12.80 cnf(c78,plain,~id(X102,X101)|id(X101,X102),inference(split_conjunct,[status(thm)],[c77])).
% 12.57/12.80 fof(axiom_5,axiom,(![X20]:id(X20,X20)),file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_5)).
% 12.57/12.80 fof(c79,plain,(![X62]:id(X62,X62)),inference(variable_rename,[status(thm)],[axiom_5])).
% 12.57/12.80 cnf(c80,plain,id(X76,X76),inference(split_conjunct,[status(thm)],[c79])).
% 12.57/12.80 cnf(c136,plain,r1(skolem0020),inference(resolution,[status(thm)],[c112, c80])).
% 12.57/12.80 cnf(c12,plain,id(X106,skolem0001(X106))|id(X106,skolem0003(X106)),inference(split_conjunct,[status(thm)],[c11])).
% 12.57/12.80 cnf(c13,plain,id(X113,skolem0001(X113))|r2(skolem0002(X113),skolem0003(X113)),inference(split_conjunct,[status(thm)],[c11])).
% 12.57/12.80 cnf(c129,plain,id(X416,skolem0001(X416))|~id(X415,skolem0003(X416))|~r1(X415),inference(resolution,[status(thm)],[c13, c8])).
% 12.57/12.80 cnf(c540,plain,id(X425,skolem0001(X425))|~r1(X425),inference(resolution,[status(thm)],[c129, c12])).
% 12.57/12.80 cnf(c589,plain,id(skolem0020,skolem0001(skolem0020)),inference(resolution,[status(thm)],[c540, c136])).
% 12.57/12.80 cnf(c602,plain,id(skolem0001(skolem0020),skolem0020),inference(resolution,[status(thm)],[c589, c78])).
% 12.57/12.80 cnf(c603,plain,r1(skolem0001(skolem0020)),inference(resolution,[status(thm)],[c602, c112])).
% 12.57/12.80 cnf(c679,plain,r1(skolem0001(skolem0001(skolem0020))),inference(resolution,[status(thm)],[c664, c603])).
% 12.57/12.80 cnf(c730,plain,r1(skolem0001(skolem0001(skolem0001(skolem0020)))),inference(resolution,[status(thm)],[c679, c664])).
% 12.57/12.80 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)).
% 12.57/12.80 fof(c97,plain,(![X11]:(?[Y21]:(![X12]:((id(X12,Y21)&r2(X11,X12))|(~r2(X11,X12)&~id(X12,Y21)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 12.57/12.80 fof(c98,plain,(![X71]:(?[X72]:(![X73]:((id(X73,X72)&r2(X71,X73))|(~r2(X71,X73)&~id(X73,X72)))))),inference(variable_rename,[status(thm)],[c97])).
% 12.57/12.80 fof(c99,plain,(![X71]:(![X73]:((id(X73,skolem0019(X71))&r2(X71,X73))|(~r2(X71,X73)&~id(X73,skolem0019(X71)))))),inference(skolemize,[status(esa)],[c98])).
% 12.57/12.80 fof(c100,plain,(![X71]:(![X73]:(((id(X73,skolem0019(X71))|~r2(X71,X73))&(id(X73,skolem0019(X71))|~id(X73,skolem0019(X71))))&((r2(X71,X73)|~r2(X71,X73))&(r2(X71,X73)|~id(X73,skolem0019(X71))))))),inference(distribute,[status(thm)],[c99])).
% 12.57/12.80 cnf(c104,plain,r2(X265,X264)|~id(X264,skolem0019(X265)),inference(split_conjunct,[status(thm)],[c100])).
% 12.57/12.80 cnf(c272,plain,r2(X270,skolem0019(X270)),inference(resolution,[status(thm)],[c104, c80])).
% 12.57/12.80 cnf(c277,plain,~id(X281,skolem0019(X282))|~r1(X281),inference(resolution,[status(thm)],[c272, c8])).
% 12.57/12.80 cnf(c289,plain,~r1(skolem0019(X283)),inference(resolution,[status(thm)],[c277, c80])).
% 12.57/12.80 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)).
% 12.57/12.80 fof(c66,plain,(![X26]:(![X27]:((~id(X26,X27)|(~r1(X26)&~r1(X27)))|(r1(X26)&r1(X27))))),inference(fof_simplification,[status(thm)],[axiom_8])).
% 12.57/12.80 fof(c67,plain,(![X55]:(![X56]:((~id(X55,X56)|(~r1(X55)&~r1(X56)))|(r1(X55)&r1(X56))))),inference(variable_rename,[status(thm)],[c66])).
% 12.57/12.80 fof(c68,plain,(![X55]:(![X56]:((((~id(X55,X56)|~r1(X55))|r1(X55))&((~id(X55,X56)|~r1(X55))|r1(X56)))&(((~id(X55,X56)|~r1(X56))|r1(X55))&((~id(X55,X56)|~r1(X56))|r1(X56)))))),inference(distribute,[status(thm)],[c67])).
% 12.57/12.80 cnf(c71,plain,~id(X208,X207)|~r1(X207)|r1(X208),inference(split_conjunct,[status(thm)],[c68])).
% 12.57/12.80 cnf(c242,plain,~r1(skolem0001(X696))|r1(X696)|id(X696,skolem0003(X696)),inference(resolution,[status(thm)],[c71, c12])).
% 12.57/12.80 cnf(c1411,plain,r1(X708)|id(X708,skolem0003(X708)),inference(resolution,[status(thm)],[c242, c14])).
% 12.57/12.80 cnf(c1458,plain,r1(X711)|id(skolem0003(X711),X711),inference(resolution,[status(thm)],[c1411, c78])).
% 12.57/12.80 cnf(c1492,plain,id(skolem0003(skolem0019(X827)),skolem0019(X827)),inference(resolution,[status(thm)],[c1458, c289])).
% 12.57/12.80 cnf(c1771,plain,r2(X829,skolem0003(skolem0019(X829))),inference(resolution,[status(thm)],[c1492, c104])).
% 12.57/12.80 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)).
% 12.57/12.80 fof(c22,plain,(![X20]:(?[X21]:(id(X21,X20)&(?[X22]:(r1(X22)&r3(X20,X22,X21)))))),inference(variable_rename,[status(thm)],[axiom_4a])).
% 12.57/12.80 fof(c23,plain,(![X20]:(id(skolem0007(X20),X20)&(r1(skolem0008(X20))&r3(X20,skolem0008(X20),skolem0007(X20))))),inference(skolemize,[status(esa)],[c22])).
% 12.57/12.80 cnf(c24,plain,id(skolem0007(X80),X80),inference(split_conjunct,[status(thm)],[c23])).
% 12.57/12.80 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)).
% 12.57/12.80 fof(c38,plain,(![X33]:(![X34]:(?[X35]:((?[X36]:(id(X36,X35)&(?[X37]:(r2(X34,X37)&r3(X33,X37,X36)))))&(?[X38]:(r2(X38,X35)&r3(X33,X34,X38))))))),inference(variable_rename,[status(thm)],[axiom_1a])).
% 12.57/12.80 fof(c39,plain,(![X33]:(![X34]:((id(skolem0014(X33,X34),skolem0013(X33,X34))&(r2(X34,skolem0015(X33,X34))&r3(X33,skolem0015(X33,X34),skolem0014(X33,X34))))&(r2(skolem0016(X33,X34),skolem0013(X33,X34))&r3(X33,X34,skolem0016(X33,X34)))))),inference(skolemize,[status(esa)],[c38])).
% 12.57/12.81 cnf(c41,plain,r2(X92,skolem0015(X91,X92)),inference(split_conjunct,[status(thm)],[c39])).
% 12.57/12.81 cnf(c101,plain,id(X244,skolem0019(X245))|~r2(X245,X244),inference(split_conjunct,[status(thm)],[c100])).
% 12.57/12.81 cnf(c259,plain,id(skolem0015(X249,X248),skolem0019(X248)),inference(resolution,[status(thm)],[c101, c41])).
% 12.57/12.81 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)).
% 12.57/12.81 fof(c73,plain,(![X23]:(![X24]:(![X25]:((~id(X23,X24)|id(X23,X25))|~id(X24,X25))))),inference(fof_simplification,[status(thm)],[axiom_7])).
% 12.57/12.81 fof(c74,plain,(![X57]:(![X58]:(![X59]:((~id(X57,X58)|id(X57,X59))|~id(X58,X59))))),inference(variable_rename,[status(thm)],[c73])).
% 12.57/12.81 cnf(c75,plain,~id(X318,X317)|id(X318,X316)|~id(X317,X316),inference(split_conjunct,[status(thm)],[c74])).
% 12.57/12.81 cnf(c324,plain,~id(X1123,skolem0015(X1122,X1121))|id(X1123,skolem0019(X1121)),inference(resolution,[status(thm)],[c75, c259])).
% 12.57/12.81 cnf(c2855,plain,id(skolem0007(skolem0015(X2640,X2639)),skolem0019(X2639)),inference(resolution,[status(thm)],[c324, c24])).
% 12.57/12.81 cnf(c12612,plain,r2(X2643,skolem0007(skolem0015(X2644,X2643))),inference(resolution,[status(thm)],[c2855, c104])).
% 12.57/12.81 fof(xplusyidthree,conjecture,(?[Y1]:(?[Y2]:(?[Y3]:(r3(Y1,Y2,Y3)&(?[Y4]:(id(Y3,Y4)&(?[Y5]:(r2(Y5,Y4)&(?[Y6]:(r2(Y6,Y5)&(?[Y7]:(r1(Y7)&r2(Y7,Y6))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', xplusyidthree)).
% 12.57/12.81 fof(c0,negated_conjecture,(~(?[Y1]:(?[Y2]:(?[Y3]:(r3(Y1,Y2,Y3)&(?[Y4]:(id(Y3,Y4)&(?[Y5]:(r2(Y5,Y4)&(?[Y6]:(r2(Y6,Y5)&(?[Y7]:(r1(Y7)&r2(Y7,Y6)))))))))))))),inference(assume_negation,[status(cth)],[xplusyidthree])).
% 12.57/12.81 fof(c1,negated_conjecture,(![Y1]:(![Y2]:(![Y3]:(~r3(Y1,Y2,Y3)|(![Y4]:(~id(Y3,Y4)|(![Y5]:(~r2(Y5,Y4)|(![Y6]:(~r2(Y6,Y5)|(![Y7]:(~r1(Y7)|~r2(Y7,Y6))))))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 12.57/12.81 fof(c3,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(~r3(X2,X3,X4)|(~id(X4,X5)|(~r2(X6,X5)|(~r2(X7,X6)|(~r1(X8)|~r2(X8,X7))))))))))))),inference(shift_quantors,[status(thm)],[fof(c2,negated_conjecture,(![X2]:(![X3]:(![X4]:(~r3(X2,X3,X4)|(![X5]:(~id(X4,X5)|(![X6]:(~r2(X6,X5)|(![X7]:(~r2(X7,X6)|(![X8]:(~r1(X8)|~r2(X8,X7))))))))))))),inference(variable_rename,[status(thm)],[c1])).])).
% 12.57/12.81 cnf(c4,negated_conjecture,~r3(X86,X82,X87)|~id(X87,X85)|~r2(X84,X85)|~r2(X81,X84)|~r1(X83)|~r2(X83,X81),inference(split_conjunct,[status(thm)],[c3])).
% 12.57/12.81 cnf(c26,plain,r3(X129,skolem0008(X129),skolem0007(X129)),inference(split_conjunct,[status(thm)],[c23])).
% 12.57/12.81 cnf(c145,plain,~id(skolem0007(X441),X439)|~r2(X443,X439)|~r2(X440,X443)|~r1(X442)|~r2(X442,X440),inference(resolution,[status(thm)],[c26, c4])).
% 12.57/12.81 cnf(c700,plain,~r2(X2848,skolem0007(X2849))|~r2(X2851,X2848)|~r1(X2850)|~r2(X2850,X2851),inference(resolution,[status(thm)],[c145, c80])).
% 12.57/12.81 cnf(c13917,plain,~r2(X3782,X3780)|~r1(X3781)|~r2(X3781,X3782),inference(resolution,[status(thm)],[c700, c12612])).
% 12.57/12.81 cnf(c18014,plain,~r2(skolem0019(X3785),X3784)|~r1(X3785),inference(resolution,[status(thm)],[c13917, c272])).
% 12.57/12.81 cnf(c18114,plain,~r1(X3786),inference(resolution,[status(thm)],[c18014, c1771])).
% 12.57/12.81 cnf(c18132,plain,$false,inference(resolution,[status(thm)],[c18114, c730])).
% 12.57/12.81 % SZS output end CNFRefutation
% 12.57/12.81
% 12.57/12.81 % Initial clauses : 59
% 12.57/12.81 % Processed clauses : 914
% 12.57/12.81 % Factors computed : 29
% 12.57/12.81 % Resolvents computed: 18100
% 12.57/12.81 % Tautologies deleted: 24
% 12.57/12.81 % Forward subsumed : 1556
% 12.57/12.81 % Backward subsumed : 112
% 12.57/12.81 % -------- CPU Time ---------
% 12.57/12.81 % User time : 12.415 s
% 12.57/12.81 % System time : 0.045 s
% 12.57/12.81 % Total time : 12.460 s
%------------------------------------------------------------------------------