%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM390+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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 50.34s 50.54s
% Output : Refutation 50.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : NUM390+1 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n007.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 16:20:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 50.34/50.54 % Version: 1.5
% 50.34/50.54 % SZS status Theorem
% 50.34/50.54 % SZS output start CNFRefutation
% 50.34/50.54 fof(t22_ordinal1,conjecture,(![A]:(epsilon_transitive(A)=>(![B]:(ordinal(B)=>(![C]:(ordinal(C)=>((subset(A,B)&in(B,C))=>in(A,C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t22_ordinal1)).
% 50.34/50.54 fof(c41,negated_conjecture,(~(![A]:(epsilon_transitive(A)=>(![B]:(ordinal(B)=>(![C]:(ordinal(C)=>((subset(A,B)&in(B,C))=>in(A,C))))))))),inference(assume_negation,[status(cth)],[t22_ordinal1])).
% 50.34/50.54 fof(c42,negated_conjecture,(?[A]:(epsilon_transitive(A)&(?[B]:(ordinal(B)&(?[C]:(ordinal(C)&((subset(A,B)&in(B,C))&~in(A,C)))))))),inference(fof_nnf,[status(thm)],[c41])).
% 50.34/50.54 fof(c43,negated_conjecture,(?[X21]:(epsilon_transitive(X21)&(?[X22]:(ordinal(X22)&(?[X23]:(ordinal(X23)&((subset(X21,X22)&in(X22,X23))&~in(X21,X23)))))))),inference(variable_rename,[status(thm)],[c42])).
% 50.34/50.54 fof(c44,negated_conjecture,(epsilon_transitive(skolem0001)&(ordinal(skolem0002)&(ordinal(skolem0003)&((subset(skolem0001,skolem0002)&in(skolem0002,skolem0003))&~in(skolem0001,skolem0003))))),inference(skolemize,[status(esa)],[c43])).
% 50.34/50.54 cnf(c49,negated_conjecture,in(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c44])).
% 50.34/50.54 fof(t7_boole,axiom,(![A]:(![B]:(~(in(A,B)&empty(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_boole)).
% 50.34/50.54 fof(c20,plain,(![A]:(![B]:(~in(A,B)|~empty(B)))),inference(fof_nnf,[status(thm)],[t7_boole])).
% 50.34/50.54 fof(c21,plain,(![X6]:(![X7]:(~in(X6,X7)|~empty(X7)))),inference(variable_rename,[status(thm)],[c20])).
% 50.34/50.54 cnf(c22,plain,~in(X113,X112)|~empty(X112),inference(split_conjunct,[status(thm)],[c21])).
% 50.34/50.54 cnf(c198,plain,~empty(skolem0003),inference(resolution,[status(thm)],[c22, c49])).
% 50.34/50.54 cnf(c50,negated_conjecture,~in(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c44])).
% 50.34/50.54 fof(t2_subset,axiom,(![A]:(![B]:(element(A,B)=>(empty(B)|in(A,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t2_subset)).
% 50.34/50.54 fof(c38,plain,(![A]:(![B]:(~element(A,B)|(empty(B)|in(A,B))))),inference(fof_nnf,[status(thm)],[t2_subset])).
% 50.34/50.54 fof(c39,plain,(![X19]:(![X20]:(~element(X19,X20)|(empty(X20)|in(X19,X20))))),inference(variable_rename,[status(thm)],[c38])).
% 50.34/50.54 cnf(c40,plain,~element(X163,X162)|empty(X162)|in(X163,X162),inference(split_conjunct,[status(thm)],[c39])).
% 50.34/50.54 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)).
% 50.34/50.54 fof(c29,plain,(![A]:(![B]:(![C]:((~in(A,B)|~element(B,powerset(C)))|element(A,C))))),inference(fof_nnf,[status(thm)],[t4_subset])).
% 50.34/50.54 fof(c30,plain,(![X12]:(![X13]:(![X14]:((~in(X12,X13)|~element(X13,powerset(X14)))|element(X12,X14))))),inference(variable_rename,[status(thm)],[c29])).
% 50.34/50.54 cnf(c31,plain,~in(X141,X143)|~element(X143,powerset(X142))|element(X141,X142),inference(split_conjunct,[status(thm)],[c30])).
% 50.34/50.54 fof(t3_subset,axiom,(![A]:(![B]:(element(A,powerset(B))<=>subset(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_subset)).
% 50.34/50.54 fof(c32,plain,(![A]:(![B]:((~element(A,powerset(B))|subset(A,B))&(~subset(A,B)|element(A,powerset(B)))))),inference(fof_nnf,[status(thm)],[t3_subset])).
% 50.34/50.54 fof(c33,plain,((![A]:(![B]:(~element(A,powerset(B))|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|element(A,powerset(B)))))),inference(shift_quantors,[status(thm)],[c32])).
% 50.34/50.54 fof(c35,plain,(![X15]:(![X16]:(![X17]:(![X18]:((~element(X15,powerset(X16))|subset(X15,X16))&(~subset(X17,X18)|element(X17,powerset(X18)))))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,((![X15]:(![X16]:(~element(X15,powerset(X16))|subset(X15,X16))))&(![X17]:(![X18]:(~subset(X17,X18)|element(X17,powerset(X18)))))),inference(variable_rename,[status(thm)],[c33])).])).
% 50.34/50.54 cnf(c37,plain,~subset(X156,X157)|element(X156,powerset(X157)),inference(split_conjunct,[status(thm)],[c35])).
% 50.34/50.54 cnf(c47,negated_conjecture,ordinal(skolem0003),inference(split_conjunct,[status(thm)],[c44])).
% 50.34/50.54 fof(cc1_ordinal1,axiom,(![A]:(ordinal(A)=>(epsilon_transitive(A)&epsilon_connected(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc1_ordinal1)).
% 50.34/50.54 fof(c154,plain,(![A]:(~ordinal(A)|(epsilon_transitive(A)&epsilon_connected(A)))),inference(fof_nnf,[status(thm)],[cc1_ordinal1])).
% 50.34/50.54 fof(c155,plain,(![X57]:(~ordinal(X57)|(epsilon_transitive(X57)&epsilon_connected(X57)))),inference(variable_rename,[status(thm)],[c154])).
% 50.34/50.54 fof(c156,plain,(![X57]:((~ordinal(X57)|epsilon_transitive(X57))&(~ordinal(X57)|epsilon_connected(X57)))),inference(distribute,[status(thm)],[c155])).
% 50.34/50.54 cnf(c157,plain,~ordinal(X92)|epsilon_transitive(X92),inference(split_conjunct,[status(thm)],[c156])).
% 50.34/50.54 cnf(c185,plain,epsilon_transitive(skolem0003),inference(resolution,[status(thm)],[c157, c47])).
% 50.34/50.54 fof(d2_ordinal1,axiom,(![A]:(epsilon_transitive(A)<=>(![B]:(in(B,A)=>subset(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_ordinal1)).
% 50.34/50.54 fof(c133,plain,(![A]:((~epsilon_transitive(A)|(![B]:(~in(B,A)|subset(B,A))))&((?[B]:(in(B,A)&~subset(B,A)))|epsilon_transitive(A)))),inference(fof_nnf,[status(thm)],[d2_ordinal1])).
% 50.34/50.54 fof(c134,plain,((![A]:(~epsilon_transitive(A)|(![B]:(~in(B,A)|subset(B,A)))))&(![A]:((?[B]:(in(B,A)&~subset(B,A)))|epsilon_transitive(A)))),inference(shift_quantors,[status(thm)],[c133])).
% 50.34/50.54 fof(c135,plain,((![X50]:(~epsilon_transitive(X50)|(![X51]:(~in(X51,X50)|subset(X51,X50)))))&(![X52]:((?[X53]:(in(X53,X52)&~subset(X53,X52)))|epsilon_transitive(X52)))),inference(variable_rename,[status(thm)],[c134])).
% 50.34/50.54 fof(c137,plain,(![X50]:(![X51]:(![X52]:((~epsilon_transitive(X50)|(~in(X51,X50)|subset(X51,X50)))&((in(skolem0016(X52),X52)&~subset(skolem0016(X52),X52))|epsilon_transitive(X52)))))),inference(shift_quantors,[status(thm)],[fof(c136,plain,((![X50]:(~epsilon_transitive(X50)|(![X51]:(~in(X51,X50)|subset(X51,X50)))))&(![X52]:((in(skolem0016(X52),X52)&~subset(skolem0016(X52),X52))|epsilon_transitive(X52)))),inference(skolemize,[status(esa)],[c135])).])).
% 50.34/50.54 fof(c138,plain,(![X50]:(![X51]:(![X52]:((~epsilon_transitive(X50)|(~in(X51,X50)|subset(X51,X50)))&((in(skolem0016(X52),X52)|epsilon_transitive(X52))&(~subset(skolem0016(X52),X52)|epsilon_transitive(X52))))))),inference(distribute,[status(thm)],[c137])).
% 50.34/50.54 cnf(c139,plain,~epsilon_transitive(X171)|~in(X172,X171)|subset(X172,X171),inference(split_conjunct,[status(thm)],[c138])).
% 50.34/50.54 cnf(c314,plain,~epsilon_transitive(skolem0003)|subset(skolem0002,skolem0003),inference(resolution,[status(thm)],[c139, c49])).
% 50.34/50.54 cnf(c708,plain,subset(skolem0002,skolem0003),inference(resolution,[status(thm)],[c314, c185])).
% 50.34/50.54 cnf(c711,plain,element(skolem0002,powerset(skolem0003)),inference(resolution,[status(thm)],[c708, c37])).
% 50.34/50.54 cnf(c804,plain,~in(X333,skolem0002)|element(X333,skolem0003),inference(resolution,[status(thm)],[c711, c31])).
% 50.34/50.54 cnf(reflexivity,axiom,X63=X63,theory(equality)).
% 50.34/50.54 cnf(c1,axiom,X73!=X74|X75!=X72|~in(X73,X75)|in(X74,X72),theory(equality)).
% 50.34/50.54 cnf(c176,plain,skolem0002!=X180|skolem0003!=X181|in(X180,X181),inference(resolution,[status(thm)],[c49, c1])).
% 50.34/50.54 cnf(c340,plain,skolem0002!=X235|in(X235,skolem0003),inference(resolution,[status(thm)],[c176, reflexivity])).
% 50.34/50.54 cnf(symmetry,axiom,X65!=X66|X66=X65,theory(equality)).
% 50.34/50.54 cnf(c48,negated_conjecture,subset(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c44])).
% 50.34/50.54 fof(d8_xboole_0,axiom,(![A]:(![B]:(proper_subset(A,B)<=>(subset(A,B)&A!=B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d8_xboole_0)).
% 50.34/50.54 fof(c125,plain,(![A]:(![B]:((~proper_subset(A,B)|(subset(A,B)&A!=B))&((~subset(A,B)|A=B)|proper_subset(A,B))))),inference(fof_nnf,[status(thm)],[d8_xboole_0])).
% 50.34/50.54 fof(c126,plain,((![A]:(![B]:(~proper_subset(A,B)|(subset(A,B)&A!=B))))&(![A]:(![B]:((~subset(A,B)|A=B)|proper_subset(A,B))))),inference(shift_quantors,[status(thm)],[c125])).
% 50.34/50.54 fof(c128,plain,(![X46]:(![X47]:(![X48]:(![X49]:((~proper_subset(X46,X47)|(subset(X46,X47)&X46!=X47))&((~subset(X48,X49)|X48=X49)|proper_subset(X48,X49))))))),inference(shift_quantors,[status(thm)],[fof(c127,plain,((![X46]:(![X47]:(~proper_subset(X46,X47)|(subset(X46,X47)&X46!=X47))))&(![X48]:(![X49]:((~subset(X48,X49)|X48=X49)|proper_subset(X48,X49))))),inference(variable_rename,[status(thm)],[c126])).])).
% 50.34/50.54 fof(c129,plain,(![X46]:(![X47]:(![X48]:(![X49]:(((~proper_subset(X46,X47)|subset(X46,X47))&(~proper_subset(X46,X47)|X46!=X47))&((~subset(X48,X49)|X48=X49)|proper_subset(X48,X49))))))),inference(distribute,[status(thm)],[c128])).
% 50.34/50.54 cnf(c132,plain,~subset(X170,X169)|X170=X169|proper_subset(X170,X169),inference(split_conjunct,[status(thm)],[c129])).
% 50.34/50.54 cnf(c313,plain,skolem0001=skolem0002|proper_subset(skolem0001,skolem0002),inference(resolution,[status(thm)],[c132, c48])).
% 50.34/50.54 cnf(c699,plain,proper_subset(skolem0001,skolem0002)|skolem0002=skolem0001,inference(resolution,[status(thm)],[c313, symmetry])).
% 50.34/50.54 cnf(c3662,plain,proper_subset(skolem0001,skolem0002)|in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c699, c340])).
% 50.34/50.54 cnf(c9222,plain,proper_subset(skolem0001,skolem0002),inference(resolution,[status(thm)],[c3662, c50])).
% 50.34/50.54 cnf(c131,plain,~proper_subset(X136,X135)|X136!=X135,inference(split_conjunct,[status(thm)],[c129])).
% 50.34/50.54 cnf(c45,negated_conjecture,epsilon_transitive(skolem0001),inference(split_conjunct,[status(thm)],[c44])).
% 50.34/50.54 cnf(c46,negated_conjecture,ordinal(skolem0002),inference(split_conjunct,[status(thm)],[c44])).
% 50.34/50.54 fof(t21_ordinal1,axiom,(![A]:(epsilon_transitive(A)=>(![B]:(ordinal(B)=>(proper_subset(A,B)=>in(A,B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t21_ordinal1)).
% 50.34/50.54 fof(c51,plain,(![A]:(~epsilon_transitive(A)|(![B]:(~ordinal(B)|(~proper_subset(A,B)|in(A,B)))))),inference(fof_nnf,[status(thm)],[t21_ordinal1])).
% 50.34/50.54 fof(c53,plain,(![X24]:(![X25]:(~epsilon_transitive(X24)|(~ordinal(X25)|(~proper_subset(X24,X25)|in(X24,X25)))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,(![X24]:(~epsilon_transitive(X24)|(![X25]:(~ordinal(X25)|(~proper_subset(X24,X25)|in(X24,X25)))))),inference(variable_rename,[status(thm)],[c51])).])).
% 50.34/50.54 cnf(c54,plain,~epsilon_transitive(X165)|~ordinal(X164)|~proper_subset(X165,X164)|in(X165,X164),inference(split_conjunct,[status(thm)],[c53])).
% 50.34/50.54 cnf(c705,plain,skolem0001=skolem0002|~epsilon_transitive(skolem0001)|~ordinal(skolem0002)|in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c313, c54])).
% 50.34/50.54 cnf(c3672,plain,skolem0001=skolem0002|~epsilon_transitive(skolem0001)|in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c705, c46])).
% 50.34/50.54 cnf(c46546,plain,skolem0001=skolem0002|in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c3672, c45])).
% 50.34/50.54 cnf(c46611,plain,in(skolem0001,skolem0002)|~proper_subset(skolem0001,skolem0002),inference(resolution,[status(thm)],[c46546, c131])).
% 50.34/50.54 cnf(c46679,plain,in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c46611, c9222])).
% 50.34/50.54 cnf(c46681,plain,element(skolem0001,skolem0003),inference(resolution,[status(thm)],[c46679, c804])).
% 50.34/50.54 cnf(c46695,plain,empty(skolem0003)|in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c46681, c40])).
% 50.34/50.54 cnf(c46799,plain,empty(skolem0003),inference(resolution,[status(thm)],[c46695, c50])).
% 50.34/50.54 cnf(c46858,plain,$false,inference(resolution,[status(thm)],[c46799, c198])).
% 50.34/50.54 % SZS output end CNFRefutation
% 50.34/50.54
% 50.34/50.54 % Initial clauses : 85
% 50.34/50.54 % Processed clauses : 2549
% 50.34/50.54 % Factors computed : 8
% 50.34/50.54 % Resolvents computed: 46701
% 50.34/50.54 % Tautologies deleted: 76
% 50.34/50.54 % Forward subsumed : 5812
% 50.34/50.54 % Backward subsumed : 356
% 50.34/50.54 % -------- CPU Time ---------
% 50.34/50.54 % User time : 50.065 s
% 50.34/50.54 % System time : 0.114 s
% 50.34/50.54 % Total time : 50.179 s
%------------------------------------------------------------------------------