%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN087+2 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:12 EDT 2024
% Result : Theorem 20.81s 21.01s
% Output : Refutation 20.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : NUN087+2 : TPTP v8.1.2. Released v7.3.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n029.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 22:31:08 EDT 2024
% 0.15/0.37 % CPUTime :
% 20.81/21.01 % Version: 1.5
% 20.81/21.01 % SZS status Theorem
% 20.81/21.01 % SZS output start CNFRefutation
% 20.81/21.01 cnf(reflexivity,axiom,X48=X48,theory(equality)).
% 20.81/21.01 fof(axiom_1,axiom,(?[Y24]:(![X19]:(((~r1(X19))&X19!=Y24)|(r1(X19)&X19=Y24)))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_1)).
% 20.81/21.01 fof(c73,plain,(?[Y24]:(![X19]:((~r1(X19)&X19!=Y24)|(r1(X19)&X19=Y24)))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 20.81/21.01 fof(c74,plain,(?[X46]:(![X47]:((~r1(X47)&X47!=X46)|(r1(X47)&X47=X46)))),inference(variable_rename,[status(thm)],[c73])).
% 20.81/21.01 fof(c75,plain,(![X47]:((~r1(X47)&X47!=skolem0020)|(r1(X47)&X47=skolem0020))),inference(skolemize,[status(esa)],[c74])).
% 20.81/21.01 fof(c76,plain,(![X47]:(((~r1(X47)|r1(X47))&(~r1(X47)|X47=skolem0020))&((X47!=skolem0020|r1(X47))&(X47!=skolem0020|X47=skolem0020)))),inference(distribute,[status(thm)],[c75])).
% 20.81/21.01 cnf(c79,plain,X96!=skolem0020|r1(X96),inference(split_conjunct,[status(thm)],[c76])).
% 20.81/21.01 cnf(c118,plain,r1(skolem0020),inference(resolution,[status(thm)],[c79, reflexivity])).
% 20.81/21.01 fof(zerotimeszeroeqzero,conjecture,(?[Y1]:((?[Y2]:(r1(Y2)&r4(Y2,Y2,Y1)))&(?[Y3]:(r1(Y3)&Y1=Y3)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', zerotimeszeroeqzero)).
% 20.81/21.01 fof(c4,negated_conjecture,(~(?[Y1]:((?[Y2]:(r1(Y2)&r4(Y2,Y2,Y1)))&(?[Y3]:(r1(Y3)&Y1=Y3))))),inference(assume_negation,[status(cth)],[zerotimeszeroeqzero])).
% 20.81/21.01 fof(c5,negated_conjecture,(![Y1]:((![Y2]:(~r1(Y2)|~r4(Y2,Y2,Y1)))|(![Y3]:(~r1(Y3)|Y1!=Y3)))),inference(fof_nnf,[status(thm)],[c4])).
% 20.81/21.01 fof(c7,negated_conjecture,(![X2]:(![X3]:(![X4]:((~r1(X3)|~r4(X3,X3,X2))|(~r1(X4)|X2!=X4))))),inference(shift_quantors,[status(thm)],[fof(c6,negated_conjecture,(![X2]:((![X3]:(~r1(X3)|~r4(X3,X3,X2)))|(![X4]:(~r1(X4)|X2!=X4)))),inference(variable_rename,[status(thm)],[c5])).])).
% 20.81/21.01 cnf(c8,negated_conjecture,~r1(X111)|~r4(X111,X111,X110)|~r1(X109)|X110!=X109,inference(split_conjunct,[status(thm)],[c7])).
% 20.81/21.01 fof(axiom_4,axiom,(![X16]:(![X17]:(?[Y23]:(![X18]:(((~r4(X16,X17,X18))&X18!=Y23)|(r4(X16,X17,X18)&X18=Y23)))))),file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_4)).
% 20.81/21.01 fof(c49,plain,(![X16]:(![X17]:(?[Y23]:(![X18]:((~r4(X16,X17,X18)&X18!=Y23)|(r4(X16,X17,X18)&X18=Y23)))))),inference(fof_simplification,[status(thm)],[axiom_4])).
% 20.81/21.01 fof(c50,plain,(![X35]:(![X36]:(?[X37]:(![X38]:((~r4(X35,X36,X38)&X38!=X37)|(r4(X35,X36,X38)&X38=X37)))))),inference(variable_rename,[status(thm)],[c49])).
% 20.81/21.01 fof(c51,plain,(![X35]:(![X36]:(![X38]:((~r4(X35,X36,X38)&X38!=skolem0017(X35,X36))|(r4(X35,X36,X38)&X38=skolem0017(X35,X36)))))),inference(skolemize,[status(esa)],[c50])).
% 20.81/21.01 fof(c52,plain,(![X35]:(![X36]:(![X38]:(((~r4(X35,X36,X38)|r4(X35,X36,X38))&(~r4(X35,X36,X38)|X38=skolem0017(X35,X36)))&((X38!=skolem0017(X35,X36)|r4(X35,X36,X38))&(X38!=skolem0017(X35,X36)|X38=skolem0017(X35,X36))))))),inference(distribute,[status(thm)],[c51])).
% 20.81/21.01 cnf(c55,plain,X206!=skolem0017(X207,X208)|r4(X207,X208,X206),inference(split_conjunct,[status(thm)],[c52])).
% 20.81/21.01 cnf(c256,plain,r4(X215,X214,skolem0017(X215,X214)),inference(resolution,[status(thm)],[c55, reflexivity])).
% 20.81/21.01 cnf(c258,plain,~r1(X1024)|~r1(X1023)|skolem0017(X1024,X1024)!=X1023,inference(resolution,[status(thm)],[c256, c8])).
% 20.81/21.01 cnf(symmetry,axiom,X54!=X53|X53=X54,theory(equality)).
% 20.81/21.01 cnf(c54,plain,~r4(X197,X198,X196)|X196=skolem0017(X197,X198),inference(split_conjunct,[status(thm)],[c52])).
% 20.81/21.01 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)).
% 20.81/21.01 fof(c26,plain,(![X16]:(?[X17]:((?[X18]:(r1(X18)&r3(X16,X18,X17)))&X17=X16))),inference(variable_rename,[status(thm)],[axiom_4a])).
% 20.81/21.01 fof(c27,plain,(![X16]:((r1(skolem0008(X16))&r3(X16,skolem0008(X16),skolem0007(X16)))&skolem0007(X16)=X16)),inference(skolemize,[status(esa)],[c26])).
% 20.81/21.01 cnf(c30,plain,skolem0007(X52)=X52,inference(split_conjunct,[status(thm)],[c27])).
% 20.81/21.01 cnf(c81,plain,X57=skolem0007(X57),inference(resolution,[status(thm)],[symmetry, c30])).
% 20.81/21.01 cnf(transitivity,axiom,X63!=X61|X61!=X62|X63=X62,theory(equality)).
% 20.81/21.01 cnf(c85,plain,X221!=X220|X221=skolem0007(X220),inference(resolution,[status(thm)],[transitivity, c81])).
% 20.81/21.01 cnf(c274,plain,X224=skolem0007(skolem0007(X224)),inference(resolution,[status(thm)],[c85, c81])).
% 20.81/21.01 cnf(c289,plain,skolem0007(skolem0007(X225))=X225,inference(resolution,[status(thm)],[c274, symmetry])).
% 20.81/21.01 cnf(c86,plain,X254!=skolem0007(X253)|X254=X253,inference(resolution,[status(thm)],[transitivity, c30])).
% 20.81/21.01 cnf(c333,plain,skolem0007(skolem0007(skolem0007(X593)))=X593,inference(resolution,[status(thm)],[c86, c289])).
% 20.81/21.01 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)).
% 20.81/21.01 fof(c20,plain,(![X12]:(?[X13]:((?[X14]:(r1(X14)&r4(X12,X14,X13)))&(?[X15]:(r1(X15)&X13=X15))))),inference(variable_rename,[status(thm)],[axiom_5a])).
% 20.81/21.01 fof(c21,plain,(![X12]:((r1(skolem0005(X12))&r4(X12,skolem0005(X12),skolem0004(X12)))&(r1(skolem0006(X12))&skolem0004(X12)=skolem0006(X12)))),inference(skolemize,[status(esa)],[c20])).
% 20.81/21.01 cnf(c22,plain,r1(skolem0005(X49)),inference(split_conjunct,[status(thm)],[c21])).
% 20.81/21.01 cnf(c78,plain,~r1(X76)|X76=skolem0020,inference(split_conjunct,[status(thm)],[c76])).
% 20.81/21.01 cnf(c94,plain,skolem0005(X77)=skolem0020,inference(resolution,[status(thm)],[c78, c22])).
% 20.81/21.01 cnf(c24,plain,r1(skolem0006(X50)),inference(split_conjunct,[status(thm)],[c21])).
% 20.81/21.01 cnf(c0,axiom,X74!=X73|~r1(X74)|r1(X73),theory(equality)).
% 20.81/21.01 cnf(c25,plain,skolem0004(X66)=skolem0006(X66),inference(split_conjunct,[status(thm)],[c21])).
% 20.81/21.01 cnf(c88,plain,skolem0006(X112)=skolem0004(X112),inference(resolution,[status(thm)],[c25, symmetry])).
% 20.81/21.01 cnf(c128,plain,~r1(skolem0006(X270))|r1(skolem0004(X270)),inference(resolution,[status(thm)],[c88, c0])).
% 20.81/21.01 cnf(c347,plain,r1(skolem0004(X273)),inference(resolution,[status(thm)],[c128, c24])).
% 20.81/21.01 cnf(c354,plain,skolem0004(X279)=skolem0020,inference(resolution,[status(thm)],[c347, c78])).
% 20.81/21.01 cnf(c3,axiom,X103!=X99|X104!=X100|X101!=X102|~r4(X103,X104,X101)|r4(X99,X100,X102),theory(equality)).
% 20.81/21.01 cnf(c23,plain,r4(X127,skolem0005(X127),skolem0004(X127)),inference(split_conjunct,[status(thm)],[c21])).
% 20.81/21.01 cnf(c159,plain,X475!=X474|skolem0005(X475)!=X476|skolem0004(X475)!=X473|r4(X474,X476,X473),inference(resolution,[status(thm)],[c23, c3])).
% 20.81/21.01 cnf(c837,plain,X3521!=X3522|skolem0005(X3521)!=X3523|r4(X3522,X3523,skolem0020),inference(resolution,[status(thm)],[c159, c354])).
% 20.81/21.01 cnf(c24088,plain,X4095!=X4096|r4(X4096,skolem0020,skolem0020),inference(resolution,[status(thm)],[c837, c94])).
% 20.81/21.01 cnf(c30628,plain,r4(X4097,skolem0020,skolem0020),inference(resolution,[status(thm)],[c24088, c333])).
% 20.81/21.01 cnf(c31015,plain,skolem0020=skolem0017(X4232,skolem0020),inference(resolution,[status(thm)],[c30628, c54])).
% 20.81/21.01 cnf(c31814,plain,skolem0017(X4234,skolem0020)=skolem0020,inference(resolution,[status(thm)],[c31015, symmetry])).
% 20.81/21.01 cnf(c31899,plain,~r1(skolem0020),inference(resolution,[status(thm)],[c31814, c258])).
% 20.81/21.01 cnf(c31977,plain,$false,inference(resolution,[status(thm)],[c31899, c118])).
% 20.81/21.01 % SZS output end CNFRefutation
% 20.81/21.01
% 20.81/21.01 % Initial clauses : 47
% 20.81/21.01 % Processed clauses : 965
% 20.81/21.01 % Factors computed : 20
% 20.81/21.01 % Resolvents computed: 31877
% 20.81/21.01 % Tautologies deleted: 14
% 20.81/21.01 % Forward subsumed : 1998
% 20.81/21.01 % Backward subsumed : 17
% 20.81/21.01 % -------- CPU Time ---------
% 20.81/21.01 % User time : 20.564 s
% 20.81/21.01 % System time : 0.078 s
% 20.81/21.01 % Total time : 20.642 s
%------------------------------------------------------------------------------