%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM394+1 : TPTP v8.1.2. Released v3.2.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:35:42 EDT 2024
% Result : Theorem 30.39s 30.58s
% Output : Refutation 30.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : NUM394+1 : TPTP v8.1.2. Released v3.2.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n018.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 17:04:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 30.39/30.58 % Version: 1.5
% 30.39/30.58 % SZS status Theorem
% 30.39/30.58 % SZS output start CNFRefutation
% 30.39/30.58 fof(existence_m1_subset_1,axiom,(![A]:(?[B]:element(B,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', existence_m1_subset_1)).
% 30.39/30.58 fof(c122,plain,(![X41]:(?[X42]:element(X42,X41))),inference(variable_rename,[status(thm)],[existence_m1_subset_1])).
% 30.39/30.58 fof(c123,plain,(![X41]:element(skolem0014(X41),X41)),inference(skolemize,[status(esa)],[c122])).
% 30.39/30.58 cnf(c124,plain,element(skolem0014(X76),X76),inference(split_conjunct,[status(thm)],[c123])).
% 30.39/30.58 fof(t2_subset,axiom,(![A]:(![B]:(element(A,B)=>(empty(B)|in(A,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t2_subset)).
% 30.39/30.58 fof(c35,plain,(![A]:(![B]:(~element(A,B)|(empty(B)|in(A,B))))),inference(fof_nnf,[status(thm)],[t2_subset])).
% 30.39/30.58 fof(c36,plain,(![X17]:(![X18]:(~element(X17,X18)|(empty(X18)|in(X17,X18))))),inference(variable_rename,[status(thm)],[c35])).
% 30.39/30.58 cnf(c37,plain,~element(X144,X143)|empty(X143)|in(X144,X143),inference(split_conjunct,[status(thm)],[c36])).
% 30.39/30.58 cnf(c280,plain,empty(X201)|in(skolem0014(X201),X201),inference(resolution,[status(thm)],[c37, c124])).
% 30.39/30.58 fof(t7_boole,axiom,(![A]:(![B]:(~(in(A,B)&empty(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_boole)).
% 30.39/30.58 fof(c17,plain,(![A]:(![B]:(~in(A,B)|~empty(B)))),inference(fof_nnf,[status(thm)],[t7_boole])).
% 30.39/30.58 fof(c18,plain,(![X4]:(![X5]:(~in(X4,X5)|~empty(X5)))),inference(variable_rename,[status(thm)],[c17])).
% 30.39/30.58 cnf(c19,plain,~in(X101,X100)|~empty(X100),inference(split_conjunct,[status(thm)],[c18])).
% 30.39/30.58 fof(t26_ordinal1,conjecture,(![A]:(ordinal(A)=>(![B]:(ordinal(B)=>(ordinal_subset(A,B)|in(B,A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t26_ordinal1)).
% 30.39/30.58 fof(c38,negated_conjecture,(~(![A]:(ordinal(A)=>(![B]:(ordinal(B)=>(ordinal_subset(A,B)|in(B,A))))))),inference(assume_negation,[status(cth)],[t26_ordinal1])).
% 30.39/30.58 fof(c39,negated_conjecture,(?[A]:(ordinal(A)&(?[B]:(ordinal(B)&(~ordinal_subset(A,B)&~in(B,A)))))),inference(fof_nnf,[status(thm)],[c38])).
% 30.39/30.58 fof(c40,negated_conjecture,(?[X19]:(ordinal(X19)&(?[X20]:(ordinal(X20)&(~ordinal_subset(X19,X20)&~in(X20,X19)))))),inference(variable_rename,[status(thm)],[c39])).
% 30.39/30.58 fof(c41,negated_conjecture,(ordinal(skolem0001)&(ordinal(skolem0002)&(~ordinal_subset(skolem0001,skolem0002)&~in(skolem0002,skolem0001)))),inference(skolemize,[status(esa)],[c40])).
% 30.39/30.58 cnf(c44,negated_conjecture,~ordinal_subset(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 30.39/30.58 cnf(reflexivity,axiom,X56=X56,theory(equality)).
% 30.39/30.58 cnf(c9,axiom,X94!=X92|X93!=X95|~ordinal_subset(X94,X93)|ordinal_subset(X92,X95),theory(equality)).
% 30.39/30.58 cnf(c43,negated_conjecture,ordinal(skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 30.39/30.58 fof(reflexivity_r1_ordinal1,axiom,(![A]:(![B]:((ordinal(A)&ordinal(B))=>ordinal_subset(A,A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r1_ordinal1)).
% 30.39/30.58 fof(c57,plain,(![A]:(![B]:((~ordinal(A)|~ordinal(B))|ordinal_subset(A,A)))),inference(fof_nnf,[status(thm)],[reflexivity_r1_ordinal1])).
% 30.39/30.58 fof(c58,plain,(![A]:((~ordinal(A)|(![B]:~ordinal(B)))|ordinal_subset(A,A))),inference(shift_quantors,[status(thm)],[c57])).
% 30.39/30.58 fof(c60,plain,(![X26]:(![X27]:((~ordinal(X26)|~ordinal(X27))|ordinal_subset(X26,X26)))),inference(shift_quantors,[status(thm)],[fof(c59,plain,(![X26]:((~ordinal(X26)|(![X27]:~ordinal(X27)))|ordinal_subset(X26,X26))),inference(variable_rename,[status(thm)],[c58])).])).
% 30.39/30.58 cnf(c61,plain,~ordinal(X148)|~ordinal(X147)|ordinal_subset(X148,X148),inference(split_conjunct,[status(thm)],[c60])).
% 30.39/30.58 cnf(c286,plain,~ordinal(X149)|ordinal_subset(X149,X149),inference(factor,[status(thm)],[c61])).
% 30.39/30.58 cnf(c292,plain,ordinal_subset(skolem0002,skolem0002),inference(resolution,[status(thm)],[c286, c43])).
% 30.39/30.58 cnf(c295,plain,skolem0002!=X212|skolem0002!=X213|ordinal_subset(X212,X213),inference(resolution,[status(thm)],[c292, c9])).
% 30.39/30.58 cnf(c693,plain,skolem0002!=X296|ordinal_subset(X296,skolem0002),inference(resolution,[status(thm)],[c295, reflexivity])).
% 30.39/30.58 cnf(c45,negated_conjecture,~in(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 30.39/30.58 cnf(c42,negated_conjecture,ordinal(skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 30.39/30.58 fof(t24_ordinal1,axiom,(![A]:(ordinal(A)=>(![B]:(ordinal(B)=>(~(((~in(A,B))&A!=B)&(~in(B,A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t24_ordinal1)).
% 30.39/30.58 fof(c46,plain,(![A]:(ordinal(A)=>(![B]:(ordinal(B)=>(~((~in(A,B)&A!=B)&~in(B,A))))))),inference(fof_simplification,[status(thm)],[t24_ordinal1])).
% 30.39/30.58 fof(c47,plain,(![A]:(~ordinal(A)|(![B]:(~ordinal(B)|((in(A,B)|A=B)|in(B,A)))))),inference(fof_nnf,[status(thm)],[c46])).
% 30.39/30.58 fof(c49,plain,(![X21]:(![X22]:(~ordinal(X21)|(~ordinal(X22)|((in(X21,X22)|X21=X22)|in(X22,X21)))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,(![X21]:(~ordinal(X21)|(![X22]:(~ordinal(X22)|((in(X21,X22)|X21=X22)|in(X22,X21)))))),inference(variable_rename,[status(thm)],[c47])).])).
% 30.39/30.58 cnf(c50,plain,~ordinal(X145)|~ordinal(X146)|in(X145,X146)|X145=X146|in(X146,X145),inference(split_conjunct,[status(thm)],[c49])).
% 30.39/30.58 cnf(c284,plain,~ordinal(X206)|in(X206,skolem0001)|X206=skolem0001|in(skolem0001,X206),inference(resolution,[status(thm)],[c50, c42])).
% 30.39/30.58 cnf(c639,plain,in(skolem0002,skolem0001)|skolem0002=skolem0001|in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c284, c43])).
% 30.39/30.58 cnf(c3385,plain,skolem0002=skolem0001|in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c639, c45])).
% 30.39/30.58 cnf(c8348,plain,in(skolem0001,skolem0002)|ordinal_subset(skolem0001,skolem0002),inference(resolution,[status(thm)],[c3385, c693])).
% 30.39/30.58 cnf(c10663,plain,in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c8348, c44])).
% 30.39/30.58 cnf(c10682,plain,~empty(skolem0002),inference(resolution,[status(thm)],[c10663, c19])).
% 30.39/30.58 cnf(c10683,plain,in(skolem0014(skolem0002),skolem0002),inference(resolution,[status(thm)],[c10682, c280])).
% 30.39/30.58 fof(t5_subset,axiom,(![A]:(![B]:(![C]:(~((in(A,B)&element(B,powerset(C)))&empty(C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t5_subset)).
% 30.39/30.58 fof(c23,plain,(![A]:(![B]:(![C]:((~in(A,B)|~element(B,powerset(C)))|~empty(C))))),inference(fof_nnf,[status(thm)],[t5_subset])).
% 30.39/30.58 fof(c24,plain,(![X7]:(![X8]:(![X9]:((~in(X7,X8)|~element(X8,powerset(X9)))|~empty(X9))))),inference(variable_rename,[status(thm)],[c23])).
% 30.39/30.58 cnf(c25,plain,~in(X131,X129)|~element(X129,powerset(X130))|~empty(X130),inference(split_conjunct,[status(thm)],[c24])).
% 30.39/30.58 fof(t3_subset,axiom,(![A]:(![B]:(element(A,powerset(B))<=>subset(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_subset)).
% 30.39/30.58 fof(c29,plain,(![A]:(![B]:((~element(A,powerset(B))|subset(A,B))&(~subset(A,B)|element(A,powerset(B)))))),inference(fof_nnf,[status(thm)],[t3_subset])).
% 30.39/30.58 fof(c30,plain,((![A]:(![B]:(~element(A,powerset(B))|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|element(A,powerset(B)))))),inference(shift_quantors,[status(thm)],[c29])).
% 30.39/30.58 fof(c32,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~element(X13,powerset(X14))|subset(X13,X14))&(~subset(X15,X16)|element(X15,powerset(X16)))))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,((![X13]:(![X14]:(~element(X13,powerset(X14))|subset(X13,X14))))&(![X15]:(![X16]:(~subset(X15,X16)|element(X15,powerset(X16)))))),inference(variable_rename,[status(thm)],[c30])).])).
% 30.39/30.58 cnf(c34,plain,~subset(X138,X137)|element(X138,powerset(X137)),inference(split_conjunct,[status(thm)],[c32])).
% 30.39/30.58 fof(redefinition_r1_ordinal1,axiom,(![A]:(![B]:((ordinal(A)&ordinal(B))=>(ordinal_subset(A,B)<=>subset(A,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', redefinition_r1_ordinal1)).
% 30.39/30.58 fof(c62,plain,(![A]:(![B]:((~ordinal(A)|~ordinal(B))|((~ordinal_subset(A,B)|subset(A,B))&(~subset(A,B)|ordinal_subset(A,B)))))),inference(fof_nnf,[status(thm)],[redefinition_r1_ordinal1])).
% 30.39/30.58 fof(c63,plain,(![X28]:(![X29]:((~ordinal(X28)|~ordinal(X29))|((~ordinal_subset(X28,X29)|subset(X28,X29))&(~subset(X28,X29)|ordinal_subset(X28,X29)))))),inference(variable_rename,[status(thm)],[c62])).
% 30.39/30.58 fof(c64,plain,(![X28]:(![X29]:(((~ordinal(X28)|~ordinal(X29))|(~ordinal_subset(X28,X29)|subset(X28,X29)))&((~ordinal(X28)|~ordinal(X29))|(~subset(X28,X29)|ordinal_subset(X28,X29)))))),inference(distribute,[status(thm)],[c63])).
% 30.39/30.58 cnf(c65,plain,~ordinal(X151)|~ordinal(X152)|~ordinal_subset(X151,X152)|subset(X151,X152),inference(split_conjunct,[status(thm)],[c64])).
% 30.39/30.58 fof(connectedness_r1_ordinal1,axiom,(![A]:(![B]:((ordinal(A)&ordinal(B))=>(ordinal_subset(A,B)|ordinal_subset(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', connectedness_r1_ordinal1)).
% 30.39/30.58 fof(c134,plain,(![A]:(![B]:((~ordinal(A)|~ordinal(B))|(ordinal_subset(A,B)|ordinal_subset(B,A))))),inference(fof_nnf,[status(thm)],[connectedness_r1_ordinal1])).
% 30.39/30.58 fof(c135,plain,(![X47]:(![X48]:((~ordinal(X47)|~ordinal(X48))|(ordinal_subset(X47,X48)|ordinal_subset(X48,X47))))),inference(variable_rename,[status(thm)],[c134])).
% 30.39/30.58 cnf(c136,plain,~ordinal(X163)|~ordinal(X164)|ordinal_subset(X163,X164)|ordinal_subset(X164,X163),inference(split_conjunct,[status(thm)],[c135])).
% 30.39/30.58 cnf(c321,plain,~ordinal(X237)|ordinal_subset(X237,skolem0001)|ordinal_subset(skolem0001,X237),inference(resolution,[status(thm)],[c136, c42])).
% 30.39/30.58 cnf(c784,plain,ordinal_subset(skolem0002,skolem0001)|ordinal_subset(skolem0001,skolem0002),inference(resolution,[status(thm)],[c321, c43])).
% 30.39/30.58 cnf(c4892,plain,ordinal_subset(skolem0002,skolem0001),inference(resolution,[status(thm)],[c784, c44])).
% 30.39/30.58 cnf(c4893,plain,~ordinal(skolem0002)|~ordinal(skolem0001)|subset(skolem0002,skolem0001),inference(resolution,[status(thm)],[c4892, c65])).
% 30.39/30.58 cnf(c35002,plain,~ordinal(skolem0002)|subset(skolem0002,skolem0001),inference(resolution,[status(thm)],[c4893, c42])).
% 30.39/30.58 cnf(c35003,plain,subset(skolem0002,skolem0001),inference(resolution,[status(thm)],[c35002, c43])).
% 30.39/30.58 cnf(c35006,plain,element(skolem0002,powerset(skolem0001)),inference(resolution,[status(thm)],[c35003, c34])).
% 30.39/30.58 cnf(c35007,plain,~in(X2025,skolem0002)|~empty(skolem0001),inference(resolution,[status(thm)],[c35006, c25])).
% 30.39/30.58 cnf(c35088,plain,~empty(skolem0001),inference(resolution,[status(thm)],[c35007, c10683])).
% 30.39/30.58 fof(antisymmetry_r2_hidden,axiom,(![A]:(![B]:(in(A,B)=>(~in(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', antisymmetry_r2_hidden)).
% 30.39/30.58 fof(c157,plain,(![A]:(![B]:(in(A,B)=>~in(B,A)))),inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden])).
% 30.39/30.58 fof(c158,plain,(![A]:(![B]:(~in(A,B)|~in(B,A)))),inference(fof_nnf,[status(thm)],[c157])).
% 30.39/30.58 fof(c159,plain,(![X54]:(![X55]:(~in(X54,X55)|~in(X55,X54)))),inference(variable_rename,[status(thm)],[c158])).
% 30.39/30.58 cnf(c160,plain,~in(X116,X117)|~in(X117,X116),inference(split_conjunct,[status(thm)],[c159])).
% 30.39/30.58 cnf(c259,plain,~in(X118,X118),inference(factor,[status(thm)],[c160])).
% 30.39/30.58 fof(t4_subset,axiom,(![A]:(![B]:(![C]:((in(A,B)&element(B,powerset(C)))=>element(A,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t4_subset)).
% 30.39/30.58 fof(c26,plain,(![A]:(![B]:(![C]:((~in(A,B)|~element(B,powerset(C)))|element(A,C))))),inference(fof_nnf,[status(thm)],[t4_subset])).
% 30.39/30.58 fof(c27,plain,(![X10]:(![X11]:(![X12]:((~in(X10,X11)|~element(X11,powerset(X12)))|element(X10,X12))))),inference(variable_rename,[status(thm)],[c26])).
% 30.39/30.58 cnf(c28,plain,~in(X133,X132)|~element(X132,powerset(X134))|element(X133,X134),inference(split_conjunct,[status(thm)],[c27])).
% 30.39/30.58 cnf(c35010,plain,~in(X2030,skolem0002)|element(X2030,skolem0001),inference(resolution,[status(thm)],[c35006, c28])).
% 30.39/30.58 cnf(c35215,plain,element(skolem0001,skolem0001),inference(resolution,[status(thm)],[c35010, c10663])).
% 30.39/30.58 cnf(c35217,plain,empty(skolem0001)|in(skolem0001,skolem0001),inference(resolution,[status(thm)],[c35215, c37])).
% 30.39/30.58 cnf(c35358,plain,empty(skolem0001),inference(resolution,[status(thm)],[c35217, c259])).
% 30.39/30.58 cnf(c35371,plain,$false,inference(resolution,[status(thm)],[c35358, c35088])).
% 30.39/30.58 % SZS output end CNFRefutation
% 30.39/30.58
% 30.39/30.58 % Initial clauses : 80
% 30.39/30.58 % Processed clauses : 2088
% 30.39/30.58 % Factors computed : 12
% 30.39/30.58 % Resolvents computed: 35269
% 30.39/30.58 % Tautologies deleted: 63
% 30.39/30.58 % Forward subsumed : 5086
% 30.39/30.58 % Backward subsumed : 182
% 30.39/30.58 % -------- CPU Time ---------
% 30.39/30.58 % User time : 30.137 s
% 30.39/30.58 % System time : 0.083 s
% 30.39/30.58 % Total time : 30.220 s
%------------------------------------------------------------------------------