%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN087+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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 19.70s 19.90s
% Output : Refutation 19.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : NUN087+1 : TPTP v8.1.2. Released v7.3.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 22:35:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 19.70/19.90 % Version: 1.5
% 19.70/19.90 % SZS status Theorem
% 19.70/19.90 % SZS output start CNFRefutation
% 19.70/19.90 fof(axiom_5,axiom,(![X20]:id(X20,X20)),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_5)).
% 19.70/19.90 fof(c79,plain,(![X58]:id(X58,X58)),inference(variable_rename,[status(thm)],[axiom_5])).
% 19.70/19.90 cnf(c80,plain,id(X72,X72),inference(split_conjunct,[status(thm)],[c79])).
% 19.70/19.90 fof(axiom_1,axiom,(?[Y24]:(![X19]:((id(X19,Y24)&r1(X19))|((~r1(X19))&(~id(X19,Y24)))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_1)).
% 19.70/19.90 fof(c105,plain,(?[Y24]:(![X19]:((id(X19,Y24)&r1(X19))|(~r1(X19)&~id(X19,Y24))))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 19.70/19.90 fof(c106,plain,(?[X70]:(![X71]:((id(X71,X70)&r1(X71))|(~r1(X71)&~id(X71,X70))))),inference(variable_rename,[status(thm)],[c105])).
% 19.70/19.90 fof(c107,plain,(![X71]:((id(X71,skolem0020)&r1(X71))|(~r1(X71)&~id(X71,skolem0020)))),inference(skolemize,[status(esa)],[c106])).
% 19.70/19.90 fof(c108,plain,(![X71]:(((id(X71,skolem0020)|~r1(X71))&(id(X71,skolem0020)|~id(X71,skolem0020)))&((r1(X71)|~r1(X71))&(r1(X71)|~id(X71,skolem0020))))),inference(distribute,[status(thm)],[c107])).
% 19.70/19.90 cnf(c112,plain,r1(X113)|~id(X113,skolem0020),inference(split_conjunct,[status(thm)],[c108])).
% 19.70/19.90 cnf(c137,plain,r1(skolem0020),inference(resolution,[status(thm)],[c112, c80])).
% 19.70/19.90 fof(zerotimeszeroeqzero,conjecture,(?[Y1]:((?[Y2]:(r1(Y2)&r4(Y2,Y2,Y1)))&(?[Y3]:(id(Y1,Y3)&r1(Y3))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', zerotimeszeroeqzero)).
% 19.70/19.90 fof(c0,negated_conjecture,(~(?[Y1]:((?[Y2]:(r1(Y2)&r4(Y2,Y2,Y1)))&(?[Y3]:(id(Y1,Y3)&r1(Y3)))))),inference(assume_negation,[status(cth)],[zerotimeszeroeqzero])).
% 19.70/19.90 fof(c1,negated_conjecture,(![Y1]:((![Y2]:(~r1(Y2)|~r4(Y2,Y2,Y1)))|(![Y3]:(~id(Y1,Y3)|~r1(Y3))))),inference(fof_nnf,[status(thm)],[c0])).
% 19.70/19.90 fof(c3,negated_conjecture,(![X2]:(![X3]:(![X4]:((~r1(X3)|~r4(X3,X3,X2))|(~id(X2,X4)|~r1(X4)))))),inference(shift_quantors,[status(thm)],[fof(c2,negated_conjecture,(![X2]:((![X3]:(~r1(X3)|~r4(X3,X3,X2)))|(![X4]:(~id(X2,X4)|~r1(X4))))),inference(variable_rename,[status(thm)],[c1])).])).
% 19.70/19.90 cnf(c4,negated_conjecture,~r1(X77)|~r4(X77,X77,X78)|~id(X78,X79)|~r1(X79),inference(split_conjunct,[status(thm)],[c3])).
% 19.70/19.90 fof(axiom_4,axiom,(![X16]:(![X17]:(?[Y23]:(![X18]:((id(X18,Y23)&r4(X16,X17,X18))|((~r4(X16,X17,X18))&(~id(X18,Y23)))))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_4)).
% 19.70/19.90 fof(c81,plain,(![X16]:(![X17]:(?[Y23]:(![X18]:((id(X18,Y23)&r4(X16,X17,X18))|(~r4(X16,X17,X18)&~id(X18,Y23))))))),inference(fof_simplification,[status(thm)],[axiom_4])).
% 19.70/19.90 fof(c82,plain,(![X59]:(![X60]:(?[X61]:(![X62]:((id(X62,X61)&r4(X59,X60,X62))|(~r4(X59,X60,X62)&~id(X62,X61))))))),inference(variable_rename,[status(thm)],[c81])).
% 19.70/19.90 fof(c83,plain,(![X59]:(![X60]:(![X62]:((id(X62,skolem0017(X59,X60))&r4(X59,X60,X62))|(~r4(X59,X60,X62)&~id(X62,skolem0017(X59,X60))))))),inference(skolemize,[status(esa)],[c82])).
% 19.70/19.90 fof(c84,plain,(![X59]:(![X60]:(![X62]:(((id(X62,skolem0017(X59,X60))|~r4(X59,X60,X62))&(id(X62,skolem0017(X59,X60))|~id(X62,skolem0017(X59,X60))))&((r4(X59,X60,X62)|~r4(X59,X60,X62))&(r4(X59,X60,X62)|~id(X62,skolem0017(X59,X60)))))))),inference(distribute,[status(thm)],[c83])).
% 19.70/19.90 cnf(c88,plain,r4(X339,X340,X341)|~id(X341,skolem0017(X339,X340)),inference(split_conjunct,[status(thm)],[c84])).
% 19.70/19.90 cnf(c360,plain,r4(X343,X342,skolem0017(X343,X342)),inference(resolution,[status(thm)],[c88, c80])).
% 19.70/19.90 cnf(c362,plain,~r1(X1249)|~id(skolem0017(X1249,X1249),X1250)|~r1(X1250),inference(resolution,[status(thm)],[c360, c4])).
% 19.70/19.90 fof(axiom_6,axiom,(![X21]:(![X22]:((~id(X21,X22))|id(X22,X21)))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_6)).
% 19.70/19.90 fof(c76,plain,(![X21]:(![X22]:(~id(X21,X22)|id(X22,X21)))),inference(fof_simplification,[status(thm)],[axiom_6])).
% 19.70/19.90 fof(c77,plain,(![X56]:(![X57]:(~id(X56,X57)|id(X57,X56)))),inference(variable_rename,[status(thm)],[c76])).
% 19.70/19.90 cnf(c78,plain,~id(X93,X94)|id(X94,X93),inference(split_conjunct,[status(thm)],[c77])).
% 19.70/19.90 cnf(c85,plain,id(X323,skolem0017(X321,X322))|~r4(X321,X322,X323),inference(split_conjunct,[status(thm)],[c84])).
% 19.70/19.90 fof(axiom_4a,axiom,(![X4]:(?[Y9]:(id(Y9,X4)&(?[Y16]:(r1(Y16)&r3(X4,Y16,Y9)))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_4a)).
% 19.70/19.90 fof(c22,plain,(![X16]:(?[X17]:(id(X17,X16)&(?[X18]:(r1(X18)&r3(X16,X18,X17)))))),inference(variable_rename,[status(thm)],[axiom_4a])).
% 19.70/19.90 fof(c23,plain,(![X16]:(id(skolem0007(X16),X16)&(r1(skolem0008(X16))&r3(X16,skolem0008(X16),skolem0007(X16))))),inference(skolemize,[status(esa)],[c22])).
% 19.70/19.90 cnf(c24,plain,id(skolem0007(X76),X76),inference(split_conjunct,[status(thm)],[c23])).
% 19.70/19.90 fof(axiom_7,axiom,(![X23]:(![X24]:(![X25]:(((~id(X23,X24))|id(X23,X25))|(~id(X24,X25)))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_7)).
% 19.70/19.90 fof(c73,plain,(![X23]:(![X24]:(![X25]:((~id(X23,X24)|id(X23,X25))|~id(X24,X25))))),inference(fof_simplification,[status(thm)],[axiom_7])).
% 19.70/19.90 fof(c74,plain,(![X53]:(![X54]:(![X55]:((~id(X53,X54)|id(X53,X55))|~id(X54,X55))))),inference(variable_rename,[status(thm)],[c73])).
% 19.70/19.90 cnf(c75,plain,~id(X310,X308)|id(X310,X309)|~id(X308,X309),inference(split_conjunct,[status(thm)],[c74])).
% 19.70/19.90 cnf(c316,plain,~id(X374,skolem0007(X373))|id(X374,X373),inference(resolution,[status(thm)],[c75, c24])).
% 19.70/19.90 cnf(c26,plain,r3(X121,skolem0008(X121),skolem0007(X121)),inference(split_conjunct,[status(thm)],[c23])).
% 19.70/19.90 fof(axiom_3,axiom,(![X13]:(![X14]:(?[Y22]:(![X15]:((id(X15,Y22)&r3(X13,X14,X15))|((~r3(X13,X14,X15))&(~id(X15,Y22)))))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_3)).
% 19.70/19.90 fof(c89,plain,(![X13]:(![X14]:(?[Y22]:(![X15]:((id(X15,Y22)&r3(X13,X14,X15))|(~r3(X13,X14,X15)&~id(X15,Y22))))))),inference(fof_simplification,[status(thm)],[axiom_3])).
% 19.70/19.90 fof(c90,plain,(![X63]:(![X64]:(?[X65]:(![X66]:((id(X66,X65)&r3(X63,X64,X66))|(~r3(X63,X64,X66)&~id(X66,X65))))))),inference(variable_rename,[status(thm)],[c89])).
% 19.70/19.90 fof(c91,plain,(![X63]:(![X64]:(![X66]:((id(X66,skolem0018(X63,X64))&r3(X63,X64,X66))|(~r3(X63,X64,X66)&~id(X66,skolem0018(X63,X64))))))),inference(skolemize,[status(esa)],[c90])).
% 19.70/19.90 fof(c92,plain,(![X63]:(![X64]:(![X66]:(((id(X66,skolem0018(X63,X64))|~r3(X63,X64,X66))&(id(X66,skolem0018(X63,X64))|~id(X66,skolem0018(X63,X64))))&((r3(X63,X64,X66)|~r3(X63,X64,X66))&(r3(X63,X64,X66)|~id(X66,skolem0018(X63,X64)))))))),inference(distribute,[status(thm)],[c91])).
% 19.70/19.90 cnf(c93,plain,id(X348,skolem0018(X350,X349))|~r3(X350,X349,X348),inference(split_conjunct,[status(thm)],[c92])).
% 19.70/19.90 cnf(c372,plain,id(skolem0007(X1319),skolem0018(X1319,skolem0008(X1319))),inference(resolution,[status(thm)],[c93, c26])).
% 19.70/19.90 cnf(c3723,plain,id(skolem0018(X2769,skolem0008(X2769)),skolem0007(X2769)),inference(resolution,[status(thm)],[c372, c78])).
% 19.70/19.90 cnf(c13844,plain,id(skolem0018(X2770,skolem0008(X2770)),X2770),inference(resolution,[status(thm)],[c3723, c316])).
% 19.70/19.90 fof(axiom_5a,axiom,(![X5]:(?[Y8]:((?[Y17]:(r1(Y17)&r4(X5,Y17,Y8)))&(?[Y18]:(id(Y8,Y18)&r1(Y18)))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_5a)).
% 19.70/19.90 fof(c16,plain,(![X12]:(?[X13]:((?[X14]:(r1(X14)&r4(X12,X14,X13)))&(?[X15]:(id(X13,X15)&r1(X15)))))),inference(variable_rename,[status(thm)],[axiom_5a])).
% 19.70/19.90 fof(c17,plain,(![X12]:((r1(skolem0005(X12))&r4(X12,skolem0005(X12),skolem0004(X12)))&(id(skolem0004(X12),skolem0006(X12))&r1(skolem0006(X12))))),inference(skolemize,[status(esa)],[c16])).
% 19.70/19.90 cnf(c18,plain,r1(skolem0005(X73)),inference(split_conjunct,[status(thm)],[c17])).
% 19.70/19.90 cnf(c109,plain,id(X101,skolem0020)|~r1(X101),inference(split_conjunct,[status(thm)],[c108])).
% 19.70/19.90 cnf(c123,plain,id(skolem0005(X103),skolem0020),inference(resolution,[status(thm)],[c109, c18])).
% 19.70/19.90 cnf(c21,plain,r1(skolem0006(X74)),inference(split_conjunct,[status(thm)],[c17])).
% 19.70/19.90 cnf(c20,plain,id(skolem0004(X85),skolem0006(X85)),inference(split_conjunct,[status(thm)],[c17])).
% 19.70/19.90 cnf(c116,plain,id(skolem0006(X118),skolem0004(X118)),inference(resolution,[status(thm)],[c78, c20])).
% 19.70/19.90 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)).
% 19.70/19.90 fof(c66,plain,(![X26]:(![X27]:((~id(X26,X27)|(~r1(X26)&~r1(X27)))|(r1(X26)&r1(X27))))),inference(fof_simplification,[status(thm)],[axiom_8])).
% 19.70/19.90 fof(c67,plain,(![X51]:(![X52]:((~id(X51,X52)|(~r1(X51)&~r1(X52)))|(r1(X51)&r1(X52))))),inference(variable_rename,[status(thm)],[c66])).
% 19.70/19.90 fof(c68,plain,(![X51]:(![X52]:((((~id(X51,X52)|~r1(X51))|r1(X51))&((~id(X51,X52)|~r1(X51))|r1(X52)))&(((~id(X51,X52)|~r1(X52))|r1(X51))&((~id(X51,X52)|~r1(X52))|r1(X52)))))),inference(distribute,[status(thm)],[c67])).
% 19.70/19.90 cnf(c70,plain,~id(X134,X135)|~r1(X134)|r1(X135),inference(split_conjunct,[status(thm)],[c68])).
% 19.70/19.90 cnf(c164,plain,~r1(skolem0006(X328))|r1(skolem0004(X328)),inference(resolution,[status(thm)],[c70, c116])).
% 19.70/19.90 cnf(c345,plain,r1(skolem0004(X329)),inference(resolution,[status(thm)],[c164, c21])).
% 19.70/19.90 cnf(c346,plain,id(skolem0004(X330),skolem0020),inference(resolution,[status(thm)],[c345, c109])).
% 19.70/19.90 cnf(c19,plain,r4(X119,skolem0005(X119),skolem0004(X119)),inference(split_conjunct,[status(thm)],[c17])).
% 19.70/19.90 fof(axiom_11,axiom,(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(((((~id(X38,X41))|(~id(X39,X42)))|(~id(X40,X43)))|((~r4(X38,X39,X40))&(~r4(X41,X42,X43))))|(r4(X38,X39,X40)&r4(X41,X42,X43))))))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_11)).
% 19.70/19.90 fof(c45,plain,(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:((((~id(X38,X41)|~id(X39,X42))|~id(X40,X43))|(~r4(X38,X39,X40)&~r4(X41,X42,X43)))|(r4(X38,X39,X40)&r4(X41,X42,X43))))))))),inference(fof_simplification,[status(thm)],[axiom_11])).
% 19.70/19.90 fof(c46,plain,(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:((((~id(X35,X38)|~id(X36,X39))|~id(X37,X40))|(~r4(X35,X36,X37)&~r4(X38,X39,X40)))|(r4(X35,X36,X37)&r4(X38,X39,X40))))))))),inference(variable_rename,[status(thm)],[c45])).
% 19.70/19.90 fof(c47,plain,(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:((((((~id(X35,X38)|~id(X36,X39))|~id(X37,X40))|~r4(X35,X36,X37))|r4(X35,X36,X37))&((((~id(X35,X38)|~id(X36,X39))|~id(X37,X40))|~r4(X35,X36,X37))|r4(X38,X39,X40)))&(((((~id(X35,X38)|~id(X36,X39))|~id(X37,X40))|~r4(X38,X39,X40))|r4(X35,X36,X37))&((((~id(X35,X38)|~id(X36,X39))|~id(X37,X40))|~r4(X38,X39,X40))|r4(X38,X39,X40)))))))))),inference(distribute,[status(thm)],[c46])).
% 19.70/19.90 cnf(c49,plain,~id(X167,X169)|~id(X170,X168)|~id(X171,X172)|~r4(X167,X170,X171)|r4(X169,X168,X172),inference(split_conjunct,[status(thm)],[c47])).
% 19.70/19.90 cnf(c199,plain,~id(X559,X558)|~id(skolem0005(X559),X561)|~id(skolem0004(X559),X560)|r4(X558,X561,X560),inference(resolution,[status(thm)],[c49, c19])).
% 19.70/19.90 cnf(c1075,plain,~id(X4499,X4500)|~id(skolem0005(X4499),X4498)|r4(X4500,X4498,skolem0020),inference(resolution,[status(thm)],[c199, c346])).
% 19.70/19.90 cnf(c31210,plain,~id(X4512,X4513)|r4(X4513,skolem0020,skolem0020),inference(resolution,[status(thm)],[c1075, c123])).
% 19.70/19.90 cnf(c31371,plain,r4(X4514,skolem0020,skolem0020),inference(resolution,[status(thm)],[c31210, c13844])).
% 19.70/19.90 cnf(c31838,plain,id(skolem0020,skolem0017(X4673,skolem0020)),inference(resolution,[status(thm)],[c31371, c85])).
% 19.70/19.90 cnf(c32763,plain,id(skolem0017(X4678,skolem0020),skolem0020),inference(resolution,[status(thm)],[c31838, c78])).
% 19.70/19.90 cnf(c32808,plain,~r1(skolem0020),inference(resolution,[status(thm)],[c32763, c362])).
% 19.70/19.90 cnf(c32852,plain,$false,inference(resolution,[status(thm)],[c32808, c137])).
% 19.70/19.90 % SZS output end CNFRefutation
% 19.70/19.90
% 19.70/19.90 % Initial clauses : 59
% 19.70/19.90 % Processed clauses : 1150
% 19.70/19.90 % Factors computed : 15
% 19.70/19.90 % Resolvents computed: 32734
% 19.70/19.90 % Tautologies deleted: 25
% 19.70/19.90 % Forward subsumed : 2193
% 19.70/19.90 % Backward subsumed : 44
% 19.70/19.90 % -------- CPU Time ---------
% 19.70/19.90 % User time : 19.438 s
% 19.70/19.90 % System time : 0.071 s
% 19.70/19.90 % Total time : 19.509 s
%------------------------------------------------------------------------------