%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU118+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:40:34 EDT 2024
% Result : Theorem 229.61s 229.93s
% Output : Refutation 229.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SEU118+1 : TPTP v8.1.2. Released v3.2.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.32 % Computer : n025.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Wed May 8 10:52:53 EDT 2024
% 0.14/0.32 % CPUTime :
% 229.61/229.93 % Version: 1.5
% 229.61/229.93 % SZS status Theorem
% 229.61/229.93 % SZS output start CNFRefutation
% 229.61/229.93 fof(t34_finsub_1,conjecture,(![A]:(![B]:(element(B,powerset(A))=>(finite(A)=>element(B,finite_subsets(A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t34_finsub_1)).
% 229.61/229.93 fof(c39,negated_conjecture,(~(![A]:(![B]:(element(B,powerset(A))=>(finite(A)=>element(B,finite_subsets(A))))))),inference(assume_negation,[status(cth)],[t34_finsub_1])).
% 229.61/229.93 fof(c40,negated_conjecture,(?[A]:(?[B]:(element(B,powerset(A))&(finite(A)&~element(B,finite_subsets(A)))))),inference(fof_nnf,[status(thm)],[c39])).
% 229.61/229.93 fof(c41,negated_conjecture,(?[X17]:(?[X18]:(element(X18,powerset(X17))&(finite(X17)&~element(X18,finite_subsets(X17)))))),inference(variable_rename,[status(thm)],[c40])).
% 229.61/229.93 fof(c42,negated_conjecture,(element(skolem0002,powerset(skolem0001))&(finite(skolem0001)&~element(skolem0002,finite_subsets(skolem0001)))),inference(skolemize,[status(esa)],[c41])).
% 229.61/229.93 cnf(c45,negated_conjecture,~element(skolem0002,finite_subsets(skolem0001)),inference(split_conjunct,[status(thm)],[c42])).
% 229.61/229.93 fof(t1_subset,axiom,(![A]:(![B]:(in(A,B)=>element(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t1_subset)).
% 229.61/229.93 fof(c49,plain,(![A]:(![B]:(~in(A,B)|element(A,B)))),inference(fof_nnf,[status(thm)],[t1_subset])).
% 229.61/229.93 fof(c50,plain,(![X21]:(![X22]:(~in(X21,X22)|element(X21,X22)))),inference(variable_rename,[status(thm)],[c49])).
% 229.61/229.93 cnf(c51,plain,~in(X148,X147)|element(X148,X147),inference(split_conjunct,[status(thm)],[c50])).
% 229.61/229.93 cnf(c44,negated_conjecture,finite(skolem0001),inference(split_conjunct,[status(thm)],[c42])).
% 229.61/229.93 cnf(c43,negated_conjecture,element(skolem0002,powerset(skolem0001)),inference(split_conjunct,[status(thm)],[c42])).
% 229.61/229.93 fof(t3_subset,axiom,(![A]:(![B]:(element(A,powerset(B))<=>subset(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_subset)).
% 229.61/229.93 fof(c33,plain,(![A]:(![B]:((~element(A,powerset(B))|subset(A,B))&(~subset(A,B)|element(A,powerset(B)))))),inference(fof_nnf,[status(thm)],[t3_subset])).
% 229.61/229.93 fof(c34,plain,((![A]:(![B]:(~element(A,powerset(B))|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|element(A,powerset(B)))))),inference(shift_quantors,[status(thm)],[c33])).
% 229.61/229.93 fof(c36,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(c35,plain,((![X13]:(![X14]:(~element(X13,powerset(X14))|subset(X13,X14))))&(![X15]:(![X16]:(~subset(X15,X16)|element(X15,powerset(X16)))))),inference(variable_rename,[status(thm)],[c34])).])).
% 229.61/229.93 cnf(c37,plain,~element(X200,powerset(X201))|subset(X200,X201),inference(split_conjunct,[status(thm)],[c36])).
% 229.61/229.93 cnf(c354,plain,subset(skolem0002,skolem0001),inference(resolution,[status(thm)],[c37, c43])).
% 229.61/229.93 fof(t13_finset_1,axiom,(![A]:(![B]:((subset(A,B)&finite(B))=>finite(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13_finset_1)).
% 229.61/229.93 fof(c52,plain,(![A]:(![B]:((~subset(A,B)|~finite(B))|finite(A)))),inference(fof_nnf,[status(thm)],[t13_finset_1])).
% 229.61/229.93 fof(c53,plain,(![A]:((![B]:(~subset(A,B)|~finite(B)))|finite(A))),inference(shift_quantors,[status(thm)],[c52])).
% 229.61/229.93 fof(c55,plain,(![X23]:(![X24]:((~subset(X23,X24)|~finite(X24))|finite(X23)))),inference(shift_quantors,[status(thm)],[fof(c54,plain,(![X23]:((![X24]:(~subset(X23,X24)|~finite(X24)))|finite(X23))),inference(variable_rename,[status(thm)],[c53])).])).
% 229.61/229.93 cnf(c56,plain,~subset(X214,X213)|~finite(X213)|finite(X214),inference(split_conjunct,[status(thm)],[c55])).
% 229.61/229.93 cnf(c380,plain,~finite(skolem0001)|finite(skolem0002),inference(resolution,[status(thm)],[c56, c354])).
% 229.61/229.93 cnf(c505,plain,finite(skolem0002),inference(resolution,[status(thm)],[c380, c44])).
% 229.61/229.93 fof(fc2_finsub_1,axiom,(![A]:((((~empty(finite_subsets(A)))&cup_closed(finite_subsets(A)))&diff_closed(finite_subsets(A)))&preboolean(finite_subsets(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc2_finsub_1)).
% 229.61/229.93 fof(c119,plain,(![A]:(((~empty(finite_subsets(A))&cup_closed(finite_subsets(A)))&diff_closed(finite_subsets(A)))&preboolean(finite_subsets(A)))),inference(fof_simplification,[status(thm)],[fc2_finsub_1])).
% 229.61/229.93 fof(c120,plain,((((![A]:~empty(finite_subsets(A)))&(![A]:cup_closed(finite_subsets(A))))&(![A]:diff_closed(finite_subsets(A))))&(![A]:preboolean(finite_subsets(A)))),inference(shift_quantors,[status(thm)],[c119])).
% 229.61/229.93 fof(c122,plain,(![X40]:(![X41]:(![X42]:(![X43]:(((~empty(finite_subsets(X40))&cup_closed(finite_subsets(X41)))&diff_closed(finite_subsets(X42)))&preboolean(finite_subsets(X43))))))),inference(shift_quantors,[status(thm)],[fof(c121,plain,((((![X40]:~empty(finite_subsets(X40)))&(![X41]:cup_closed(finite_subsets(X41))))&(![X42]:diff_closed(finite_subsets(X42))))&(![X43]:preboolean(finite_subsets(X43)))),inference(variable_rename,[status(thm)],[c120])).])).
% 229.61/229.93 cnf(c126,plain,preboolean(finite_subsets(X95)),inference(split_conjunct,[status(thm)],[c122])).
% 229.61/229.93 cnf(reflexivity,axiom,X66=X66,theory(equality)).
% 229.61/229.93 fof(d5_finsub_1,axiom,(![A]:(![B]:(preboolean(B)=>(B=finite_subsets(A)<=>(![C]:(in(C,B)<=>(subset(C,A)&finite(C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d5_finsub_1)).
% 229.61/229.93 fof(c144,plain,(![A]:(![B]:(~preboolean(B)|((B!=finite_subsets(A)|(![C]:((~in(C,B)|(subset(C,A)&finite(C)))&((~subset(C,A)|~finite(C))|in(C,B)))))&((?[C]:((~in(C,B)|(~subset(C,A)|~finite(C)))&(in(C,B)|(subset(C,A)&finite(C)))))|B=finite_subsets(A)))))),inference(fof_nnf,[status(thm)],[d5_finsub_1])).
% 229.61/229.93 fof(c145,plain,(![A]:(![B]:(~preboolean(B)|((B!=finite_subsets(A)|((![C]:(~in(C,B)|(subset(C,A)&finite(C))))&(![C]:((~subset(C,A)|~finite(C))|in(C,B)))))&((?[C]:((~in(C,B)|(~subset(C,A)|~finite(C)))&(in(C,B)|(subset(C,A)&finite(C)))))|B=finite_subsets(A)))))),inference(shift_quantors,[status(thm)],[c144])).
% 229.61/229.93 fof(c146,plain,(![X52]:(![X53]:(~preboolean(X53)|((X53!=finite_subsets(X52)|((![X54]:(~in(X54,X53)|(subset(X54,X52)&finite(X54))))&(![X55]:((~subset(X55,X52)|~finite(X55))|in(X55,X53)))))&((?[X56]:((~in(X56,X53)|(~subset(X56,X52)|~finite(X56)))&(in(X56,X53)|(subset(X56,X52)&finite(X56)))))|X53=finite_subsets(X52)))))),inference(variable_rename,[status(thm)],[c145])).
% 229.61/229.93 fof(c148,plain,(![X52]:(![X53]:(![X54]:(![X55]:(~preboolean(X53)|((X53!=finite_subsets(X52)|((~in(X54,X53)|(subset(X54,X52)&finite(X54)))&((~subset(X55,X52)|~finite(X55))|in(X55,X53))))&(((~in(skolem0013(X52,X53),X53)|(~subset(skolem0013(X52,X53),X52)|~finite(skolem0013(X52,X53))))&(in(skolem0013(X52,X53),X53)|(subset(skolem0013(X52,X53),X52)&finite(skolem0013(X52,X53)))))|X53=finite_subsets(X52)))))))),inference(shift_quantors,[status(thm)],[fof(c147,plain,(![X52]:(![X53]:(~preboolean(X53)|((X53!=finite_subsets(X52)|((![X54]:(~in(X54,X53)|(subset(X54,X52)&finite(X54))))&(![X55]:((~subset(X55,X52)|~finite(X55))|in(X55,X53)))))&(((~in(skolem0013(X52,X53),X53)|(~subset(skolem0013(X52,X53),X52)|~finite(skolem0013(X52,X53))))&(in(skolem0013(X52,X53),X53)|(subset(skolem0013(X52,X53),X52)&finite(skolem0013(X52,X53)))))|X53=finite_subsets(X52)))))),inference(skolemize,[status(esa)],[c146])).])).
% 229.61/229.93 fof(c149,plain,(![X52]:(![X53]:(![X54]:(![X55]:((((~preboolean(X53)|(X53!=finite_subsets(X52)|(~in(X54,X53)|subset(X54,X52))))&(~preboolean(X53)|(X53!=finite_subsets(X52)|(~in(X54,X53)|finite(X54)))))&(~preboolean(X53)|(X53!=finite_subsets(X52)|((~subset(X55,X52)|~finite(X55))|in(X55,X53)))))&((~preboolean(X53)|((~in(skolem0013(X52,X53),X53)|(~subset(skolem0013(X52,X53),X52)|~finite(skolem0013(X52,X53))))|X53=finite_subsets(X52)))&((~preboolean(X53)|((in(skolem0013(X52,X53),X53)|subset(skolem0013(X52,X53),X52))|X53=finite_subsets(X52)))&(~preboolean(X53)|((in(skolem0013(X52,X53),X53)|finite(skolem0013(X52,X53)))|X53=finite_subsets(X52)))))))))),inference(distribute,[status(thm)],[c148])).
% 229.61/229.93 cnf(c152,plain,~preboolean(X252)|X252!=finite_subsets(X251)|~subset(X250,X251)|~finite(X250)|in(X250,X252),inference(split_conjunct,[status(thm)],[c149])).
% 229.61/229.93 cnf(c514,plain,~preboolean(finite_subsets(X909))|~subset(X908,X909)|~finite(X908)|in(X908,finite_subsets(X909)),inference(resolution,[status(thm)],[c152, reflexivity])).
% 229.61/229.93 cnf(c3009,plain,~preboolean(finite_subsets(skolem0001))|~finite(skolem0002)|in(skolem0002,finite_subsets(skolem0001)),inference(resolution,[status(thm)],[c514, c354])).
% 229.61/229.93 cnf(c161051,plain,~finite(skolem0002)|in(skolem0002,finite_subsets(skolem0001)),inference(resolution,[status(thm)],[c3009, c126])).
% 229.61/229.93 cnf(c165835,plain,in(skolem0002,finite_subsets(skolem0001)),inference(resolution,[status(thm)],[c161051, c505])).
% 229.61/229.93 cnf(c165949,plain,element(skolem0002,finite_subsets(skolem0001)),inference(resolution,[status(thm)],[c165835, c51])).
% 229.61/229.93 cnf(c165955,plain,$false,inference(resolution,[status(thm)],[c165949, c45])).
% 229.61/229.93 % SZS output end CNFRefutation
% 229.61/229.93
% 229.61/229.93 % Initial clauses : 89
% 229.61/229.93 % Processed clauses : 3724
% 229.61/229.93 % Factors computed : 30
% 229.61/229.93 % Resolvents computed: 165748
% 229.61/229.93 % Tautologies deleted: 41
% 229.61/229.93 % Forward subsumed : 5940
% 229.61/229.93 % Backward subsumed : 322
% 229.61/229.93 % -------- CPU Time ---------
% 229.61/229.93 % User time : 229.183 s
% 229.61/229.93 % System time : 0.255 s
% 229.61/229.93 % Total time : 229.438 s
%------------------------------------------------------------------------------