%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN069+2 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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 0.51s 0.71s
% Output : Refutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUN069+2 : TPTP v8.1.2. Released v7.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n023.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:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.51/0.71 % Version: 1.5
% 0.51/0.71 % SZS status Theorem
% 0.51/0.71 % SZS output start CNFRefutation
% 0.51/0.71 fof(axiom_5a,axiom,(![X5]:(?[Y8]:((?[Y17]:(r1(Y17)&r4(X5,Y17,Y8)))&(?[Y18]:(r1(Y18)&Y8=Y18))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_5a)).
% 0.51/0.71 fof(c20,plain,(![X11]:(?[X12]:((?[X13]:(r1(X13)&r4(X11,X13,X12)))&(?[X14]:(r1(X14)&X12=X14))))),inference(variable_rename,[status(thm)],[axiom_5a])).
% 0.51/0.71 fof(c21,plain,(![X11]:((r1(skolem0005(X11))&r4(X11,skolem0005(X11),skolem0004(X11)))&(r1(skolem0006(X11))&skolem0004(X11)=skolem0006(X11)))),inference(skolemize,[status(esa)],[c20])).
% 0.51/0.71 cnf(c24,plain,r1(skolem0006(X49)),inference(split_conjunct,[status(thm)],[c21])).
% 0.51/0.71 cnf(c0,axiom,X73!=X72|~r1(X73)|r1(X72),theory(equality)).
% 0.51/0.71 cnf(symmetry,axiom,X52!=X53|X53=X52,theory(equality)).
% 0.51/0.71 cnf(c25,plain,skolem0004(X65)=skolem0006(X65),inference(split_conjunct,[status(thm)],[c21])).
% 0.51/0.71 cnf(c89,plain,skolem0006(X110)=skolem0004(X110),inference(resolution,[status(thm)],[c25, symmetry])).
% 0.51/0.71 cnf(c130,plain,~r1(skolem0006(X268))|r1(skolem0004(X268)),inference(resolution,[status(thm)],[c89, c0])).
% 0.51/0.71 cnf(c352,plain,r1(skolem0004(X271)),inference(resolution,[status(thm)],[c130, c24])).
% 0.51/0.71 cnf(reflexivity,axiom,X47=X47,theory(equality)).
% 0.51/0.71 fof(axiom_2a,axiom,(![X2]:(![X9]:(?[Y2]:((?[Y3]:((?[Y14]:(r2(X9,Y14)&r4(X2,Y14,Y3)))&Y3=Y2))&(?[Y6]:(r3(Y6,X2,Y2)&r4(X2,X9,Y6))))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_2a)).
% 0.51/0.71 fof(c35,plain,(![X22]:(![X23]:(?[X24]:((?[X25]:((?[X26]:(r2(X23,X26)&r4(X22,X26,X25)))&X25=X24))&(?[X27]:(r3(X27,X22,X24)&r4(X22,X23,X27))))))),inference(variable_rename,[status(thm)],[axiom_2a])).
% 0.51/0.71 fof(c36,plain,(![X22]:(![X23]:(((r2(X23,skolem0011(X22,X23))&r4(X22,skolem0011(X22,X23),skolem0010(X22,X23)))&skolem0010(X22,X23)=skolem0009(X22,X23))&(r3(skolem0012(X22,X23),X22,skolem0009(X22,X23))&r4(X22,X23,skolem0012(X22,X23)))))),inference(skolemize,[status(esa)],[c35])).
% 0.51/0.71 cnf(c37,plain,r2(X59,skolem0011(X58,X59)),inference(split_conjunct,[status(thm)],[c36])).
% 0.51/0.71 fof(oneeqone,conjecture,(?[Y1]:(Y1=Y1&(?[Y2]:(r1(Y2)&r2(Y2,Y1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', oneeqone)).
% 0.51/0.71 fof(c4,negated_conjecture,(~(?[Y1]:(Y1=Y1&(?[Y2]:(r1(Y2)&r2(Y2,Y1)))))),inference(assume_negation,[status(cth)],[oneeqone])).
% 0.51/0.71 fof(c5,negated_conjecture,(![Y1]:(Y1!=Y1|(![Y2]:(~r1(Y2)|~r2(Y2,Y1))))),inference(fof_nnf,[status(thm)],[c4])).
% 0.51/0.71 fof(c7,negated_conjecture,(![X2]:(![X3]:(X2!=X2|(~r1(X3)|~r2(X3,X2))))),inference(shift_quantors,[status(thm)],[fof(c6,negated_conjecture,(![X2]:(X2!=X2|(![X3]:(~r1(X3)|~r2(X3,X2))))),inference(variable_rename,[status(thm)],[c5])).])).
% 0.51/0.71 cnf(c8,negated_conjecture,X108!=X108|~r1(X109)|~r2(X109,X108),inference(split_conjunct,[status(thm)],[c7])).
% 0.51/0.71 cnf(c126,plain,skolem0011(X357,X356)!=skolem0011(X357,X356)|~r1(X356),inference(resolution,[status(thm)],[c8, c37])).
% 0.51/0.71 cnf(c507,plain,~r1(X358),inference(resolution,[status(thm)],[c126, reflexivity])).
% 0.51/0.71 cnf(c508,plain,$false,inference(resolution,[status(thm)],[c507, c352])).
% 0.51/0.71 % SZS output end CNFRefutation
% 0.51/0.71
% 0.51/0.71 % Initial clauses : 47
% 0.51/0.71 % Processed clauses : 118
% 0.51/0.71 % Factors computed : 2
% 0.51/0.71 % Resolvents computed: 441
% 0.51/0.71 % Tautologies deleted: 11
% 0.51/0.71 % Forward subsumed : 94
% 0.51/0.71 % Backward subsumed : 14
% 0.51/0.71 % -------- CPU Time ---------
% 0.51/0.71 % User time : 0.350 s
% 0.51/0.71 % System time : 0.015 s
% 0.51/0.71 % Total time : 0.365 s
%------------------------------------------------------------------------------