%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN073+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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 9.63s 9.80s
% Output : Refutation 9.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : NUN073+1 : TPTP v8.1.2. Released v7.3.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n025.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:32:08 EDT 2024
% 0.20/0.35 % CPUTime :
% 9.63/9.80 % Version: 1.5
% 9.63/9.80 % SZS status Theorem
% 9.63/9.80 % SZS output start CNFRefutation
% 9.63/9.80 fof(oneunidtwo,conjecture,(![Y1]:((![Y2]:((![Y4]:((~r1(Y4))|(~r2(Y4,Y2))))|(~id(Y2,Y1))))|(![Y3]:((![Y5]:((~r1(Y5))|(~r2(Y5,Y3))))|(~r2(Y3,Y1)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', oneunidtwo)).
% 9.63/9.80 fof(c0,negated_conjecture,(~(![Y1]:((![Y2]:((![Y4]:((~r1(Y4))|(~r2(Y4,Y2))))|(~id(Y2,Y1))))|(![Y3]:((![Y5]:((~r1(Y5))|(~r2(Y5,Y3))))|(~r2(Y3,Y1))))))),inference(assume_negation,[status(cth)],[oneunidtwo])).
% 9.63/9.80 fof(c1,negated_conjecture,(~(![Y1]:((![Y2]:((![Y4]:(~r1(Y4)|~r2(Y4,Y2)))|~id(Y2,Y1)))|(![Y3]:((![Y5]:(~r1(Y5)|~r2(Y5,Y3)))|~r2(Y3,Y1)))))),inference(fof_simplification,[status(thm)],[c0])).
% 9.63/9.80 fof(c2,negated_conjecture,(?[Y1]:((?[Y2]:((?[Y4]:(r1(Y4)&r2(Y4,Y2)))&id(Y2,Y1)))&(?[Y3]:((?[Y5]:(r1(Y5)&r2(Y5,Y3)))&r2(Y3,Y1))))),inference(fof_nnf,[status(thm)],[c1])).
% 9.63/9.80 fof(c3,negated_conjecture,(?[X2]:((?[X3]:((?[X4]:(r1(X4)&r2(X4,X3)))&id(X3,X2)))&(?[X5]:((?[X6]:(r1(X6)&r2(X6,X5)))&r2(X5,X2))))),inference(variable_rename,[status(thm)],[c2])).
% 9.63/9.80 fof(c4,negated_conjecture,(((r1(skolem0003)&r2(skolem0003,skolem0002))&id(skolem0002,skolem0001))&((r1(skolem0005)&r2(skolem0005,skolem0004))&r2(skolem0004,skolem0001))),inference(skolemize,[status(esa)],[c3])).
% 9.63/9.80 cnf(c8,negated_conjecture,r1(skolem0005),inference(split_conjunct,[status(thm)],[c4])).
% 9.63/9.80 cnf(c9,negated_conjecture,r2(skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c4])).
% 9.63/9.80 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)).
% 9.63/9.80 fof(c11,plain,(![X7]:(![Y10]:((![Y20]:(~id(Y20,Y10)|~r1(Y20)))|~r2(X7,Y10)))),inference(fof_simplification,[status(thm)],[axiom_7a])).
% 9.63/9.80 fof(c13,plain,(![X7]:(![X8]:(![X9]:((~id(X9,X8)|~r1(X9))|~r2(X7,X8))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,(![X7]:(![X8]:((![X9]:(~id(X9,X8)|~r1(X9)))|~r2(X7,X8)))),inference(variable_rename,[status(thm)],[c11])).])).
% 9.63/9.80 cnf(c14,plain,~id(X79,X80)|~r1(X79)|~r2(X81,X80),inference(split_conjunct,[status(thm)],[c13])).
% 9.63/9.80 cnf(c121,plain,~id(X129,skolem0004)|~r1(X129),inference(resolution,[status(thm)],[c14, c9])).
% 9.63/9.80 fof(axiom_6,axiom,(![X21]:(![X22]:((~id(X21,X22))|id(X22,X21)))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_6)).
% 9.63/9.80 fof(c82,plain,(![X21]:(![X22]:(~id(X21,X22)|id(X22,X21)))),inference(fof_simplification,[status(thm)],[axiom_6])).
% 9.63/9.80 fof(c83,plain,(![X58]:(![X59]:(~id(X58,X59)|id(X59,X58)))),inference(variable_rename,[status(thm)],[c82])).
% 9.63/9.80 cnf(c84,plain,~id(X94,X93)|id(X93,X94),inference(split_conjunct,[status(thm)],[c83])).
% 9.63/9.80 cnf(c7,negated_conjecture,id(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c4])).
% 9.63/9.80 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)).
% 9.63/9.80 fof(c79,plain,(![X23]:(![X24]:(![X25]:((~id(X23,X24)|id(X23,X25))|~id(X24,X25))))),inference(fof_simplification,[status(thm)],[axiom_7])).
% 9.63/9.80 fof(c80,plain,(![X55]:(![X56]:(![X57]:((~id(X55,X56)|id(X55,X57))|~id(X56,X57))))),inference(variable_rename,[status(thm)],[c79])).
% 9.63/9.80 cnf(c81,plain,~id(X250,X248)|id(X250,X249)|~id(X248,X249),inference(split_conjunct,[status(thm)],[c80])).
% 9.63/9.80 cnf(c367,plain,~id(X719,skolem0002)|id(X719,skolem0001),inference(resolution,[status(thm)],[c81, c7])).
% 9.63/9.80 cnf(c6,negated_conjecture,r2(skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 9.63/9.80 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)).
% 9.63/9.80 fof(c103,plain,(![X11]:(?[Y21]:(![X12]:((id(X12,Y21)&r2(X11,X12))|(~r2(X11,X12)&~id(X12,Y21)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 9.63/9.80 fof(c104,plain,(![X69]:(?[X70]:(![X71]:((id(X71,X70)&r2(X69,X71))|(~r2(X69,X71)&~id(X71,X70)))))),inference(variable_rename,[status(thm)],[c103])).
% 9.63/9.80 fof(c105,plain,(![X69]:(![X71]:((id(X71,skolem0024(X69))&r2(X69,X71))|(~r2(X69,X71)&~id(X71,skolem0024(X69)))))),inference(skolemize,[status(esa)],[c104])).
% 9.63/9.80 fof(c106,plain,(![X69]:(![X71]:(((id(X71,skolem0024(X69))|~r2(X69,X71))&(id(X71,skolem0024(X69))|~id(X71,skolem0024(X69))))&((r2(X69,X71)|~r2(X69,X71))&(r2(X69,X71)|~id(X71,skolem0024(X69))))))),inference(distribute,[status(thm)],[c105])).
% 9.63/9.81 cnf(c107,plain,id(X273,skolem0024(X272))|~r2(X272,X273),inference(split_conjunct,[status(thm)],[c106])).
% 9.63/9.81 cnf(c376,plain,id(skolem0002,skolem0024(skolem0003)),inference(resolution,[status(thm)],[c107, c6])).
% 9.63/9.81 cnf(c387,plain,id(skolem0024(skolem0003),skolem0002),inference(resolution,[status(thm)],[c376, c84])).
% 9.63/9.81 cnf(c404,plain,~id(X1011,skolem0024(skolem0003))|id(X1011,skolem0002),inference(resolution,[status(thm)],[c387, c81])).
% 9.63/9.81 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)).
% 9.63/9.81 fof(c111,plain,(?[Y24]:(![X19]:((id(X19,Y24)&r1(X19))|(~r1(X19)&~id(X19,Y24))))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 9.63/9.81 fof(c112,plain,(?[X72]:(![X73]:((id(X73,X72)&r1(X73))|(~r1(X73)&~id(X73,X72))))),inference(variable_rename,[status(thm)],[c111])).
% 9.63/9.81 fof(c113,plain,(![X73]:((id(X73,skolem0025)&r1(X73))|(~r1(X73)&~id(X73,skolem0025)))),inference(skolemize,[status(esa)],[c112])).
% 9.63/9.81 fof(c114,plain,(![X73]:(((id(X73,skolem0025)|~r1(X73))&(id(X73,skolem0025)|~id(X73,skolem0025)))&((r1(X73)|~r1(X73))&(r1(X73)|~id(X73,skolem0025))))),inference(distribute,[status(thm)],[c113])).
% 9.63/9.81 cnf(c115,plain,id(X101,skolem0025)|~r1(X101),inference(split_conjunct,[status(thm)],[c114])).
% 9.63/9.81 cnf(c134,plain,id(skolem0005,skolem0025),inference(resolution,[status(thm)],[c115, c8])).
% 9.63/9.81 cnf(c5,negated_conjecture,r1(skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 9.63/9.81 cnf(c137,plain,id(skolem0003,skolem0025),inference(resolution,[status(thm)],[c115, c5])).
% 9.63/9.81 cnf(c142,plain,id(skolem0025,skolem0003),inference(resolution,[status(thm)],[c137, c84])).
% 9.63/9.81 cnf(c340,plain,~id(X455,skolem0025)|id(X455,skolem0003),inference(resolution,[status(thm)],[c81, c142])).
% 9.63/9.81 cnf(c995,plain,id(skolem0005,skolem0003),inference(resolution,[status(thm)],[c340, c134])).
% 9.63/9.81 fof(axiom_5,axiom,(![X20]:id(X20,X20)),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_5)).
% 9.63/9.81 fof(c85,plain,(![X60]:id(X60,X60)),inference(variable_rename,[status(thm)],[axiom_5])).
% 9.63/9.81 cnf(c86,plain,id(X74,X74),inference(split_conjunct,[status(thm)],[c85])).
% 9.63/9.81 fof(axiom_9,axiom,(![X28]:(![X29]:(![X30]:(![X31]:((((~id(X28,X30))|(~id(X29,X31)))|((~r2(X28,X29))&(~r2(X30,X31))))|(r2(X28,X29)&r2(X30,X31))))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_9)).
% 9.63/9.81 fof(c65,plain,(![X28]:(![X29]:(![X30]:(![X31]:(((~id(X28,X30)|~id(X29,X31))|(~r2(X28,X29)&~r2(X30,X31)))|(r2(X28,X29)&r2(X30,X31))))))),inference(fof_simplification,[status(thm)],[axiom_9])).
% 9.63/9.81 fof(c66,plain,(![X49]:(![X50]:(![X51]:(![X52]:(((~id(X49,X51)|~id(X50,X52))|(~r2(X49,X50)&~r2(X51,X52)))|(r2(X49,X50)&r2(X51,X52))))))),inference(variable_rename,[status(thm)],[c65])).
% 9.63/9.81 fof(c67,plain,(![X49]:(![X50]:(![X51]:(![X52]:(((((~id(X49,X51)|~id(X50,X52))|~r2(X49,X50))|r2(X49,X50))&(((~id(X49,X51)|~id(X50,X52))|~r2(X49,X50))|r2(X51,X52)))&((((~id(X49,X51)|~id(X50,X52))|~r2(X51,X52))|r2(X49,X50))&(((~id(X49,X51)|~id(X50,X52))|~r2(X51,X52))|r2(X51,X52)))))))),inference(distribute,[status(thm)],[c66])).
% 9.63/9.81 cnf(c69,plain,~id(X222,X221)|~id(X219,X220)|~r2(X222,X219)|r2(X221,X220),inference(split_conjunct,[status(thm)],[c67])).
% 9.63/9.81 cnf(c276,plain,~id(skolem0005,X598)|~id(skolem0004,X599)|r2(X598,X599),inference(resolution,[status(thm)],[c69, c9])).
% 9.63/9.81 cnf(c1380,plain,~id(skolem0005,X1323)|r2(X1323,skolem0004),inference(resolution,[status(thm)],[c276, c86])).
% 9.63/9.81 cnf(c6012,plain,r2(skolem0003,skolem0004),inference(resolution,[status(thm)],[c1380, c995])).
% 9.63/9.81 cnf(c6028,plain,id(skolem0004,skolem0024(skolem0003)),inference(resolution,[status(thm)],[c6012, c107])).
% 9.63/9.81 cnf(c6140,plain,id(skolem0004,skolem0002),inference(resolution,[status(thm)],[c6028, c404])).
% 9.63/9.81 cnf(c6169,plain,id(skolem0004,skolem0001),inference(resolution,[status(thm)],[c6140, c367])).
% 9.63/9.81 cnf(c6193,plain,id(skolem0001,skolem0004),inference(resolution,[status(thm)],[c6169, c84])).
% 9.63/9.81 cnf(c10,negated_conjecture,r2(skolem0004,skolem0001),inference(split_conjunct,[status(thm)],[c4])).
% 9.63/9.81 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)).
% 9.63/9.81 fof(c33,plain,(![X3]:(![X10]:((![Y12]:((![Y13]:(~id(Y13,Y12)|~r2(X3,Y13)))|~r2(X10,Y12)))|id(X3,X10)))),inference(fof_simplification,[status(thm)],[axiom_3a])).
% 9.63/9.81 fof(c35,plain,(![X21]:(![X22]:(![X23]:(![X24]:(((~id(X24,X23)|~r2(X21,X24))|~r2(X22,X23))|id(X21,X22)))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,(![X21]:(![X22]:((![X23]:((![X24]:(~id(X24,X23)|~r2(X21,X24)))|~r2(X22,X23)))|id(X21,X22)))),inference(variable_rename,[status(thm)],[c33])).])).
% 9.63/9.81 cnf(c36,plain,~id(X120,X118)|~r2(X121,X120)|~r2(X119,X118)|id(X121,X119),inference(split_conjunct,[status(thm)],[c35])).
% 9.63/9.81 cnf(c162,plain,~id(X386,skolem0004)|~r2(X385,X386)|id(X385,skolem0005),inference(resolution,[status(thm)],[c36, c9])).
% 9.63/9.81 cnf(c738,plain,~id(skolem0001,skolem0004)|id(skolem0004,skolem0005),inference(resolution,[status(thm)],[c162, c10])).
% 9.63/9.81 cnf(c12291,plain,id(skolem0004,skolem0005),inference(resolution,[status(thm)],[c738, c6193])).
% 9.63/9.81 cnf(c12298,plain,id(skolem0005,skolem0004),inference(resolution,[status(thm)],[c12291, c84])).
% 9.63/9.81 cnf(c12314,plain,~r1(skolem0005),inference(resolution,[status(thm)],[c12298, c121])).
% 9.63/9.81 cnf(c12326,plain,$false,inference(resolution,[status(thm)],[c12314, c8])).
% 9.63/9.81 % SZS output end CNFRefutation
% 9.63/9.81
% 9.63/9.81 % Initial clauses : 64
% 9.63/9.81 % Processed clauses : 883
% 9.63/9.81 % Factors computed : 2
% 9.63/9.81 % Resolvents computed: 12207
% 9.63/9.81 % Tautologies deleted: 20
% 9.63/9.81 % Forward subsumed : 1308
% 9.63/9.81 % Backward subsumed : 16
% 9.63/9.81 % -------- CPU Time ---------
% 9.63/9.81 % User time : 9.414 s
% 9.63/9.81 % System time : 0.034 s
% 9.63/9.81 % Total time : 9.448 s
%------------------------------------------------------------------------------