%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN065+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:08 EDT 2024
% Result : Theorem 266.15s 266.47s
% Output : Refutation 266.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NUN065+1 : TPTP v8.1.2. Released v7.3.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n012.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 : Wed May 8 22:35:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 266.15/266.47 % Version: 1.5
% 266.15/266.47 % SZS status Theorem
% 266.15/266.47 % SZS output start CNFRefutation
% 266.15/266.47 fof(axiom_5,axiom,(![X20]:id(X20,X20)),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_5)).
% 266.15/266.47 fof(c86,plain,(![X59]:id(X59,X59)),inference(variable_rename,[status(thm)],[axiom_5])).
% 266.15/266.47 cnf(c87,plain,id(X73,X73),inference(split_conjunct,[status(thm)],[c86])).
% 266.15/266.47 fof(axiom_7a,axiom,(![X7]:(![Y10]:((![Y20]:((~id(Y20,Y10))|(~r1(Y20))))|(~r2(X7,Y10))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_7a)).
% 266.15/266.47 fof(c12,plain,(![X7]:(![Y10]:((![Y20]:(~id(Y20,Y10)|~r1(Y20)))|~r2(X7,Y10)))),inference(fof_simplification,[status(thm)],[axiom_7a])).
% 266.15/266.47 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])).])).
% 266.15/266.47 cnf(c15,plain,~id(X118,X116)|~r1(X118)|~r2(X117,X116),inference(split_conjunct,[status(thm)],[c14])).
% 266.15/266.47 fof(axiom_2,axiom,(![X11]:(?[Y21]:(![X12]:((id(X12,Y21)&r2(X11,X12))|((~r2(X11,X12))&(~id(X12,Y21))))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_2)).
% 266.15/266.47 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])).
% 266.15/266.47 fof(c105,plain,(![X68]:(?[X69]:(![X70]:((id(X70,X69)&r2(X68,X70))|(~r2(X68,X70)&~id(X70,X69)))))),inference(variable_rename,[status(thm)],[c104])).
% 266.15/266.47 fof(c106,plain,(![X68]:(![X70]:((id(X70,skolem0022(X68))&r2(X68,X70))|(~r2(X68,X70)&~id(X70,skolem0022(X68)))))),inference(skolemize,[status(esa)],[c105])).
% 266.15/266.47 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])).
% 266.15/266.47 cnf(c111,plain,r2(X242,X243)|~id(X243,skolem0022(X242)),inference(split_conjunct,[status(thm)],[c107])).
% 266.15/266.47 cnf(c298,plain,r2(X244,skolem0022(X244)),inference(resolution,[status(thm)],[c111, c87])).
% 266.15/266.47 cnf(c304,plain,~id(X257,skolem0022(X258))|~r1(X257),inference(resolution,[status(thm)],[c298, c15])).
% 266.15/266.47 cnf(c312,plain,~r1(skolem0022(X259)),inference(resolution,[status(thm)],[c304, c87])).
% 266.15/266.47 fof(nononesexistid,conjecture,(?[Y1]:((![Y2]:((![Y3]:((~r1(Y3))|(~r2(Y3,Y2))))|(~id(Y1,Y2))))&(![Y4]:((~id(Y1,Y4))|(~r1(Y4)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', nononesexistid)).
% 266.15/266.47 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)],[nononesexistid])).
% 266.15/266.47 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])).
% 266.15/266.47 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])).
% 266.15/266.47 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])).
% 266.15/266.47 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])).
% 266.15/266.47 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])).
% 266.15/266.47 cnf(c7,negated_conjecture,r1(skolem0002(X87))|r1(skolem0003(X87)),inference(split_conjunct,[status(thm)],[c5])).
% 266.15/266.47 cnf(c6,negated_conjecture,r1(skolem0002(X78))|id(X78,skolem0003(X78)),inference(split_conjunct,[status(thm)],[c5])).
% 266.15/266.47 fof(axiom_8,axiom,(![X26]:(![X27]:(((~id(X26,X27))|((~r1(X26))&(~r1(X27))))|(r1(X26)&r1(X27))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_8)).
% 266.15/266.47 fof(c73,plain,(![X26]:(![X27]:((~id(X26,X27)|(~r1(X26)&~r1(X27)))|(r1(X26)&r1(X27))))),inference(fof_simplification,[status(thm)],[axiom_8])).
% 266.15/266.47 fof(c74,plain,(![X52]:(![X53]:((~id(X52,X53)|(~r1(X52)&~r1(X53)))|(r1(X52)&r1(X53))))),inference(variable_rename,[status(thm)],[c73])).
% 266.15/266.47 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])).
% 266.15/266.47 cnf(c78,plain,~id(X186,X185)|~r1(X185)|r1(X186),inference(split_conjunct,[status(thm)],[c75])).
% 266.15/266.47 cnf(c253,plain,~r1(skolem0003(X694))|r1(X694)|r1(skolem0002(X694)),inference(resolution,[status(thm)],[c78, c6])).
% 266.15/266.47 cnf(c2490,plain,r1(X697)|r1(skolem0002(X697)),inference(resolution,[status(thm)],[c253, c7])).
% 266.15/266.47 cnf(c2553,plain,r1(skolem0002(skolem0022(X698))),inference(resolution,[status(thm)],[c2490, c312])).
% 266.15/266.47 fof(axiom_6,axiom,(![X21]:(![X22]:((~id(X21,X22))|id(X22,X21)))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_6)).
% 266.15/266.47 fof(c83,plain,(![X21]:(![X22]:(~id(X21,X22)|id(X22,X21)))),inference(fof_simplification,[status(thm)],[axiom_6])).
% 266.15/266.47 fof(c84,plain,(![X57]:(![X58]:(~id(X57,X58)|id(X58,X57)))),inference(variable_rename,[status(thm)],[c83])).
% 266.15/266.47 cnf(c85,plain,~id(X90,X91)|id(X91,X90),inference(split_conjunct,[status(thm)],[c84])).
% 266.15/266.47 cnf(c11,negated_conjecture,id(X113,skolem0001(X113))|r1(skolem0003(X113)),inference(split_conjunct,[status(thm)],[c5])).
% 266.15/266.47 cnf(c10,negated_conjecture,id(X108,skolem0001(X108))|id(X108,skolem0003(X108)),inference(split_conjunct,[status(thm)],[c5])).
% 266.15/266.47 cnf(c247,plain,~r1(skolem0003(X681))|r1(X681)|id(X681,skolem0001(X681)),inference(resolution,[status(thm)],[c78, c10])).
% 266.15/266.47 cnf(c2324,plain,r1(X682)|id(X682,skolem0001(X682)),inference(resolution,[status(thm)],[c247, c11])).
% 266.15/266.47 cnf(c2361,plain,r1(X684)|id(skolem0001(X684),X684),inference(resolution,[status(thm)],[c2324, c85])).
% 266.15/266.47 cnf(c2387,plain,id(skolem0001(skolem0022(X693)),skolem0022(X693)),inference(resolution,[status(thm)],[c2361, c312])).
% 266.15/266.47 fof(axiom_3a,axiom,(![X3]:(![X10]:((![Y12]:((![Y13]:((~id(Y13,Y12))|(~r2(X3,Y13))))|(~r2(X10,Y12))))|id(X3,X10)))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_3a)).
% 266.15/266.47 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])).
% 266.15/266.47 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])).])).
% 266.15/266.47 cnf(c37,plain,~id(X151,X150)|~r2(X152,X151)|~r2(X149,X150)|id(X152,X149),inference(split_conjunct,[status(thm)],[c36])).
% 266.15/266.47 cnf(c303,plain,~id(X987,skolem0022(X988))|~r2(X986,X987)|id(X986,X988),inference(resolution,[status(thm)],[c298, c37])).
% 266.15/266.47 cnf(c3714,plain,~r2(X7311,skolem0001(skolem0022(X7310)))|id(X7311,X7310),inference(resolution,[status(thm)],[c303, c2387])).
% 266.15/266.47 cnf(c9,negated_conjecture,r2(skolem0002(X102),skolem0001(X102))|r1(skolem0003(X102)),inference(split_conjunct,[status(thm)],[c5])).
% 266.15/266.47 cnf(c8,negated_conjecture,r2(skolem0002(X95),skolem0001(X95))|id(X95,skolem0003(X95)),inference(split_conjunct,[status(thm)],[c5])).
% 266.15/266.47 cnf(c125,plain,r2(skolem0002(X408),skolem0001(X408))|id(skolem0003(X408),X408),inference(resolution,[status(thm)],[c8, c85])).
% 266.15/266.47 cnf(c555,plain,r2(skolem0002(skolem0022(X2418)),skolem0001(skolem0022(X2418)))|~r1(skolem0003(skolem0022(X2418))),inference(resolution,[status(thm)],[c125, c304])).
% 266.15/266.47 cnf(c12481,plain,r2(skolem0002(skolem0022(X12506)),skolem0001(skolem0022(X12506))),inference(resolution,[status(thm)],[c555, c9])).
% 266.15/266.47 cnf(c139818,plain,id(skolem0002(skolem0022(X12508)),X12508),inference(resolution,[status(thm)],[c12481, c3714])).
% 266.15/266.47 cnf(c140059,plain,~r1(skolem0002(skolem0022(skolem0022(X12511)))),inference(resolution,[status(thm)],[c139818, c304])).
% 266.15/266.47 cnf(c140235,plain,$false,inference(resolution,[status(thm)],[c140059, c2553])).
% 266.15/266.47 % SZS output end CNFRefutation
% 266.15/266.47
% 266.15/266.47 % Initial clauses : 64
% 266.15/266.47 % Processed clauses : 3017
% 266.15/266.47 % Factors computed : 2
% 266.15/266.47 % Resolvents computed: 140156
% 266.15/266.47 % Tautologies deleted: 31
% 266.15/266.47 % Forward subsumed : 6198
% 266.15/266.47 % Backward subsumed : 171
% 266.15/266.47 % -------- CPU Time ---------
% 266.15/266.47 % User time : 265.775 s
% 266.15/266.47 % System time : 0.260 s
% 266.15/266.47 % Total time : 266.035 s
%------------------------------------------------------------------------------