%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN080+2 : 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 3.88s 4.07s
% Output : Refutation 3.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUN080+2 : TPTP v8.1.2. Released v7.3.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n018.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.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 22:30:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 3.88/4.07 % Version: 1.5
% 3.88/4.07 % SZS status Theorem
% 3.88/4.07 % SZS output start CNFRefutation
% 3.88/4.07 fof(axiom_4a,axiom,(![X4]:(?[Y9]:((?[Y16]:(r1(Y16)&r3(X4,Y16,Y9)))&Y9=X4))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_4a)).
% 3.88/4.07 fof(c26,plain,(![X19]:(?[X20]:((?[X21]:(r1(X21)&r3(X19,X21,X20)))&X20=X19))),inference(variable_rename,[status(thm)],[axiom_4a])).
% 3.88/4.07 fof(c27,plain,(![X19]:((r1(skolem0008(X19))&r3(X19,skolem0008(X19),skolem0007(X19)))&skolem0007(X19)=X19)),inference(skolemize,[status(esa)],[c26])).
% 3.88/4.07 cnf(c28,plain,r1(skolem0008(X54)),inference(split_conjunct,[status(thm)],[c27])).
% 3.88/4.07 cnf(c30,plain,skolem0007(X55)=X55,inference(split_conjunct,[status(thm)],[c27])).
% 3.88/4.07 cnf(symmetry,axiom,X57!=X56|X56=X57,theory(equality)).
% 3.88/4.07 cnf(c82,plain,X60=skolem0007(X60),inference(resolution,[status(thm)],[symmetry, c30])).
% 3.88/4.07 cnf(c0,axiom,X77!=X76|~r1(X77)|r1(X76),theory(equality)).
% 3.88/4.07 cnf(c91,plain,~r1(X119)|r1(skolem0007(X119)),inference(resolution,[status(thm)],[c0, c82])).
% 3.88/4.07 cnf(c133,plain,r1(skolem0007(skolem0008(X121))),inference(resolution,[status(thm)],[c91, c28])).
% 3.88/4.07 fof(axiom_2,axiom,(![X11]:(?[Y21]:(![X12]:(((~r2(X11,X12))&X12!=Y21)|(r2(X11,X12)&X12=Y21))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_2)).
% 3.88/4.07 fof(c65,plain,(![X11]:(?[Y21]:(![X12]:((~r2(X11,X12)&X12!=Y21)|(r2(X11,X12)&X12=Y21))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 3.88/4.07 fof(c66,plain,(![X46]:(?[X47]:(![X48]:((~r2(X46,X48)&X48!=X47)|(r2(X46,X48)&X48=X47))))),inference(variable_rename,[status(thm)],[c65])).
% 3.88/4.07 fof(c67,plain,(![X46]:(![X48]:((~r2(X46,X48)&X48!=skolem0019(X46))|(r2(X46,X48)&X48=skolem0019(X46))))),inference(skolemize,[status(esa)],[c66])).
% 3.88/4.07 fof(c68,plain,(![X46]:(![X48]:(((~r2(X46,X48)|r2(X46,X48))&(~r2(X46,X48)|X48=skolem0019(X46)))&((X48!=skolem0019(X46)|r2(X46,X48))&(X48!=skolem0019(X46)|X48=skolem0019(X46)))))),inference(distribute,[status(thm)],[c67])).
% 3.88/4.07 cnf(c71,plain,X197!=skolem0019(X198)|r2(X198,X197),inference(split_conjunct,[status(thm)],[c68])).
% 3.88/4.07 cnf(c240,plain,r2(X207,skolem0007(skolem0019(X207))),inference(resolution,[status(thm)],[c71, c30])).
% 3.88/4.07 cnf(reflexivity,axiom,X51=X51,theory(equality)).
% 3.88/4.07 cnf(c239,plain,r2(X199,skolem0019(X199)),inference(resolution,[status(thm)],[c71, reflexivity])).
% 3.88/4.07 fof(axiom_1a,axiom,(![X1]:(![X8]:(?[Y4]:((?[Y5]:((?[Y15]:(r2(X8,Y15)&r3(X1,Y15,Y5)))&Y5=Y4))&(?[Y7]:(r2(Y7,Y4)&r3(X1,X8,Y7))))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_1a)).
% 3.88/4.07 fof(c42,plain,(![X32]:(![X33]:(?[X34]:((?[X35]:((?[X36]:(r2(X33,X36)&r3(X32,X36,X35)))&X35=X34))&(?[X37]:(r2(X37,X34)&r3(X32,X33,X37))))))),inference(variable_rename,[status(thm)],[axiom_1a])).
% 3.88/4.07 fof(c43,plain,(![X32]:(![X33]:(((r2(X33,skolem0015(X32,X33))&r3(X32,skolem0015(X32,X33),skolem0014(X32,X33)))&skolem0014(X32,X33)=skolem0013(X32,X33))&(r2(skolem0016(X32,X33),skolem0013(X32,X33))&r3(X32,X33,skolem0016(X32,X33)))))),inference(skolemize,[status(esa)],[c42])).
% 3.88/4.07 cnf(c48,plain,r3(X73,X72,skolem0016(X73,X72)),inference(split_conjunct,[status(thm)],[c43])).
% 3.88/4.07 fof(xplustwoeqy,conjecture,(?[Y1]:(?[Y2]:(?[Y3]:(Y3=Y2&(?[Y4]:(r3(Y1,Y4,Y3)&(?[Y5]:(r2(Y5,Y4)&(?[Y6]:(r1(Y6)&r2(Y6,Y5))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', xplustwoeqy)).
% 3.88/4.07 fof(c4,negated_conjecture,(~(?[Y1]:(?[Y2]:(?[Y3]:(Y3=Y2&(?[Y4]:(r3(Y1,Y4,Y3)&(?[Y5]:(r2(Y5,Y4)&(?[Y6]:(r1(Y6)&r2(Y6,Y5)))))))))))),inference(assume_negation,[status(cth)],[xplustwoeqy])).
% 3.88/4.07 fof(c5,negated_conjecture,(![Y1]:(![Y2]:(![Y3]:(Y3!=Y2|(![Y4]:(~r3(Y1,Y4,Y3)|(![Y5]:(~r2(Y5,Y4)|(![Y6]:(~r1(Y6)|~r2(Y6,Y5))))))))))),inference(fof_nnf,[status(thm)],[c4])).
% 3.88/4.07 fof(c7,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(X4!=X3|(~r3(X2,X5,X4)|(~r2(X6,X5)|(~r1(X7)|~r2(X7,X6))))))))))),inference(shift_quantors,[status(thm)],[fof(c6,negated_conjecture,(![X2]:(![X3]:(![X4]:(X4!=X3|(![X5]:(~r3(X2,X5,X4)|(![X6]:(~r2(X6,X5)|(![X7]:(~r1(X7)|~r2(X7,X6))))))))))),inference(variable_rename,[status(thm)],[c5])).])).
% 3.88/4.07 cnf(c8,negated_conjecture,X113!=X115|~r3(X117,X116,X113)|~r2(X114,X116)|~r1(X112)|~r2(X112,X114),inference(split_conjunct,[status(thm)],[c7])).
% 3.88/4.07 cnf(c126,plain,skolem0016(X365,X367)!=X366|~r2(X364,X367)|~r1(X368)|~r2(X368,X364),inference(resolution,[status(thm)],[c8, c48])).
% 3.88/4.07 cnf(c511,plain,~r2(X2000,X1999)|~r1(X1998)|~r2(X1998,X2000),inference(resolution,[status(thm)],[c126, reflexivity])).
% 3.88/4.07 cnf(c10611,plain,~r2(skolem0019(X2003),X2004)|~r1(X2003),inference(resolution,[status(thm)],[c511, c239])).
% 3.88/4.07 cnf(c10644,plain,~r1(X2005),inference(resolution,[status(thm)],[c10611, c240])).
% 3.88/4.07 cnf(c10655,plain,$false,inference(resolution,[status(thm)],[c10644, c133])).
% 3.88/4.07 % SZS output end CNFRefutation
% 3.88/4.07
% 3.88/4.07 % Initial clauses : 47
% 3.88/4.07 % Processed clauses : 491
% 3.88/4.07 % Factors computed : 20
% 3.88/4.07 % Resolvents computed: 10607
% 3.88/4.07 % Tautologies deleted: 11
% 3.88/4.07 % Forward subsumed : 756
% 3.88/4.07 % Backward subsumed : 53
% 3.88/4.07 % -------- CPU Time ---------
% 3.88/4.07 % User time : 3.682 s
% 3.88/4.07 % System time : 0.032 s
% 3.88/4.07 % Total time : 3.714 s
%------------------------------------------------------------------------------