%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN080+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:10 EDT 2024
% Result : Theorem 2.75s 2.96s
% Output : Refutation 2.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUN080+1 : TPTP v8.1.2. Released v7.3.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % 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:31:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 2.75/2.96 % Version: 1.5
% 2.75/2.96 % SZS status Theorem
% 2.75/2.96 % SZS output start CNFRefutation
% 2.75/2.96 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)).
% 2.75/2.96 fof(c22,plain,(![X19]:(?[X20]:(id(X20,X19)&(?[X21]:(r1(X21)&r3(X19,X21,X20)))))),inference(variable_rename,[status(thm)],[axiom_4a])).
% 2.75/2.96 fof(c23,plain,(![X19]:(id(skolem0007(X19),X19)&(r1(skolem0008(X19))&r3(X19,skolem0008(X19),skolem0007(X19))))),inference(skolemize,[status(esa)],[c22])).
% 2.75/2.96 cnf(c24,plain,id(skolem0007(X79),X79),inference(split_conjunct,[status(thm)],[c23])).
% 2.75/2.96 fof(axiom_6,axiom,(![X21]:(![X22]:((~id(X21,X22))|id(X22,X21)))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_6)).
% 2.75/2.96 fof(c75,plain,(![X21]:(![X22]:(~id(X21,X22)|id(X22,X21)))),inference(fof_simplification,[status(thm)],[axiom_6])).
% 2.75/2.96 fof(c76,plain,(![X59]:(![X60]:(~id(X59,X60)|id(X60,X59)))),inference(variable_rename,[status(thm)],[c75])).
% 2.75/2.96 cnf(c77,plain,~id(X99,X100)|id(X100,X99),inference(split_conjunct,[status(thm)],[c76])).
% 2.75/2.96 cnf(c116,plain,id(X102,skolem0007(X102)),inference(resolution,[status(thm)],[c77, c24])).
% 2.75/2.96 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)).
% 2.75/2.96 fof(c65,plain,(![X26]:(![X27]:((~id(X26,X27)|(~r1(X26)&~r1(X27)))|(r1(X26)&r1(X27))))),inference(fof_simplification,[status(thm)],[axiom_8])).
% 2.75/2.96 fof(c66,plain,(![X54]:(![X55]:((~id(X54,X55)|(~r1(X54)&~r1(X55)))|(r1(X54)&r1(X55))))),inference(variable_rename,[status(thm)],[c65])).
% 2.75/2.96 fof(c67,plain,(![X54]:(![X55]:((((~id(X54,X55)|~r1(X54))|r1(X54))&((~id(X54,X55)|~r1(X54))|r1(X55)))&(((~id(X54,X55)|~r1(X55))|r1(X54))&((~id(X54,X55)|~r1(X55))|r1(X55)))))),inference(distribute,[status(thm)],[c66])).
% 2.75/2.96 cnf(c69,plain,~id(X141,X140)|~r1(X141)|r1(X140),inference(split_conjunct,[status(thm)],[c67])).
% 2.75/2.96 cnf(c160,plain,~r1(X143)|r1(skolem0007(X143)),inference(resolution,[status(thm)],[c69, c116])).
% 2.75/2.96 cnf(c25,plain,r1(skolem0008(X78)),inference(split_conjunct,[status(thm)],[c23])).
% 2.75/2.96 cnf(c172,plain,r1(skolem0007(skolem0008(X146))),inference(resolution,[status(thm)],[c160, c25])).
% 2.75/2.96 cnf(c179,plain,r1(skolem0007(skolem0007(skolem0008(X171)))),inference(resolution,[status(thm)],[c172, c160])).
% 2.75/2.96 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)).
% 2.75/2.96 fof(c96,plain,(![X11]:(?[Y21]:(![X12]:((id(X12,Y21)&r2(X11,X12))|(~r2(X11,X12)&~id(X12,Y21)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 2.75/2.96 fof(c97,plain,(![X70]:(?[X71]:(![X72]:((id(X72,X71)&r2(X70,X72))|(~r2(X70,X72)&~id(X72,X71)))))),inference(variable_rename,[status(thm)],[c96])).
% 2.75/2.96 fof(c98,plain,(![X70]:(![X72]:((id(X72,skolem0019(X70))&r2(X70,X72))|(~r2(X70,X72)&~id(X72,skolem0019(X70)))))),inference(skolemize,[status(esa)],[c97])).
% 2.75/2.96 fof(c99,plain,(![X70]:(![X72]:(((id(X72,skolem0019(X70))|~r2(X70,X72))&(id(X72,skolem0019(X70))|~id(X72,skolem0019(X70))))&((r2(X70,X72)|~r2(X70,X72))&(r2(X70,X72)|~id(X72,skolem0019(X70))))))),inference(distribute,[status(thm)],[c98])).
% 2.75/2.96 cnf(c103,plain,r2(X263,X262)|~id(X262,skolem0019(X263)),inference(split_conjunct,[status(thm)],[c99])).
% 2.75/2.96 cnf(c274,plain,r2(X273,skolem0007(skolem0019(X273))),inference(resolution,[status(thm)],[c103, c24])).
% 2.75/2.96 fof(axiom_5,axiom,(![X20]:id(X20,X20)),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_5)).
% 2.75/2.96 fof(c78,plain,(![X61]:id(X61,X61)),inference(variable_rename,[status(thm)],[axiom_5])).
% 2.75/2.96 cnf(c79,plain,id(X75,X75),inference(split_conjunct,[status(thm)],[c78])).
% 2.75/2.96 cnf(c273,plain,r2(X268,skolem0019(X268)),inference(resolution,[status(thm)],[c103, c79])).
% 2.75/2.96 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)).
% 2.75/2.96 fof(c72,plain,(![X23]:(![X24]:(![X25]:((~id(X23,X24)|id(X23,X25))|~id(X24,X25))))),inference(fof_simplification,[status(thm)],[axiom_7])).
% 2.75/2.96 fof(c73,plain,(![X56]:(![X57]:(![X58]:((~id(X56,X57)|id(X56,X58))|~id(X57,X58))))),inference(variable_rename,[status(thm)],[c72])).
% 2.75/2.96 cnf(c74,plain,~id(X315,X316)|id(X315,X314)|~id(X316,X314),inference(split_conjunct,[status(thm)],[c73])).
% 2.75/2.96 cnf(c325,plain,~id(X379,X380)|id(X379,skolem0007(X380)),inference(resolution,[status(thm)],[c74, c116])).
% 2.75/2.96 cnf(c416,plain,id(X382,skolem0007(skolem0007(X382))),inference(resolution,[status(thm)],[c325, c116])).
% 2.75/2.96 fof(xplustwoidy,conjecture,(?[Y1]:(?[Y2]:(?[Y3]:(id(Y3,Y2)&(?[Y4]:(r3(Y1,Y4,Y3)&(?[Y5]:(r2(Y5,Y4)&(?[Y6]:(r1(Y6)&r2(Y6,Y5))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', xplustwoidy)).
% 2.75/2.96 fof(c0,negated_conjecture,(~(?[Y1]:(?[Y2]:(?[Y3]:(id(Y3,Y2)&(?[Y4]:(r3(Y1,Y4,Y3)&(?[Y5]:(r2(Y5,Y4)&(?[Y6]:(r1(Y6)&r2(Y6,Y5)))))))))))),inference(assume_negation,[status(cth)],[xplustwoidy])).
% 2.75/2.96 fof(c1,negated_conjecture,(![Y1]:(![Y2]:(![Y3]:(~id(Y3,Y2)|(![Y4]:(~r3(Y1,Y4,Y3)|(![Y5]:(~r2(Y5,Y4)|(![Y6]:(~r1(Y6)|~r2(Y6,Y5))))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 2.75/2.96 fof(c3,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(~id(X4,X3)|(~r3(X2,X5,X4)|(~r2(X6,X5)|(~r1(X7)|~r2(X7,X6))))))))))),inference(shift_quantors,[status(thm)],[fof(c2,negated_conjecture,(![X2]:(![X3]:(![X4]:(~id(X4,X3)|(![X5]:(~r3(X2,X5,X4)|(![X6]:(~r2(X6,X5)|(![X7]:(~r1(X7)|~r2(X7,X6))))))))))),inference(variable_rename,[status(thm)],[c1])).])).
% 2.75/2.96 cnf(c4,negated_conjecture,~id(X81,X85)|~r3(X80,X82,X81)|~r2(X83,X82)|~r1(X84)|~r2(X84,X83),inference(split_conjunct,[status(thm)],[c3])).
% 2.75/2.96 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/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_1a)).
% 2.75/2.96 fof(c38,plain,(![X32]:(![X33]:(?[X34]:((?[X35]:(id(X35,X34)&(?[X36]:(r2(X33,X36)&r3(X32,X36,X35)))))&(?[X37]:(r2(X37,X34)&r3(X32,X33,X37))))))),inference(variable_rename,[status(thm)],[axiom_1a])).
% 2.75/2.96 fof(c39,plain,(![X32]:(![X33]:((id(skolem0014(X32,X33),skolem0013(X32,X33))&(r2(X33,skolem0015(X32,X33))&r3(X32,skolem0015(X32,X33),skolem0014(X32,X33))))&(r2(skolem0016(X32,X33),skolem0013(X32,X33))&r3(X32,X33,skolem0016(X32,X33)))))),inference(skolemize,[status(esa)],[c38])).
% 2.75/2.96 cnf(c44,plain,r3(X98,X97,skolem0016(X98,X97)),inference(split_conjunct,[status(thm)],[c39])).
% 2.75/2.96 cnf(c114,plain,~id(skolem0016(X384,X386),X388)|~r2(X385,X386)|~r1(X387)|~r2(X387,X385),inference(resolution,[status(thm)],[c44, c4])).
% 2.75/2.96 cnf(c438,plain,~r2(X1707,X1706)|~r1(X1708)|~r2(X1708,X1707),inference(resolution,[status(thm)],[c114, c416])).
% 2.75/2.96 cnf(c5128,plain,~r2(skolem0019(X1710),X1711)|~r1(X1710),inference(resolution,[status(thm)],[c438, c273])).
% 2.75/2.96 cnf(c5161,plain,~r1(X1712),inference(resolution,[status(thm)],[c5128, c274])).
% 2.75/2.96 cnf(c5169,plain,$false,inference(resolution,[status(thm)],[c5161, c179])).
% 2.75/2.96 % SZS output end CNFRefutation
% 2.75/2.96
% 2.75/2.96 % Initial clauses : 59
% 2.75/2.96 % Processed clauses : 451
% 2.75/2.96 % Factors computed : 7
% 2.75/2.96 % Resolvents computed: 5107
% 2.75/2.96 % Tautologies deleted: 20
% 2.75/2.96 % Forward subsumed : 612
% 2.75/2.96 % Backward subsumed : 66
% 2.75/2.96 % -------- CPU Time ---------
% 2.75/2.96 % User time : 2.587 s
% 2.75/2.96 % System time : 0.020 s
% 2.75/2.96 % Total time : 2.607 s
%------------------------------------------------------------------------------