%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU173+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:46 EDT 2024
% Result : Theorem 8.16s 8.53s
% Output : Refutation 8.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU173+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 11:27:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 8.16/8.53 % Version: 1.5
% 8.16/8.53 % SZS status Theorem
% 8.16/8.53 % SZS output start CNFRefutation
% 8.16/8.53 fof(fc1_subset_1,axiom,(![A]:(~empty(powerset(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc1_subset_1)).
% 8.16/8.53 fof(c43,plain,(![A]:~empty(powerset(A))),inference(fof_simplification,[status(thm)],[fc1_subset_1])).
% 8.16/8.53 fof(c44,plain,(![X17]:~empty(powerset(X17))),inference(variable_rename,[status(thm)],[c43])).
% 8.16/8.53 cnf(c45,plain,~empty(powerset(X50)),inference(split_conjunct,[status(thm)],[c44])).
% 8.16/8.53 fof(l71_subset_1,conjecture,(![A]:(![B]:((![C]:(in(C,A)=>in(C,B)))=>element(A,powerset(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l71_subset_1)).
% 8.16/8.53 fof(c35,negated_conjecture,(~(![A]:(![B]:((![C]:(in(C,A)=>in(C,B)))=>element(A,powerset(B)))))),inference(assume_negation,[status(cth)],[l71_subset_1])).
% 8.16/8.53 fof(c36,negated_conjecture,(?[A]:(?[B]:((![C]:(~in(C,A)|in(C,B)))&~element(A,powerset(B))))),inference(fof_nnf,[status(thm)],[c35])).
% 8.16/8.53 fof(c37,negated_conjecture,(?[X14]:(?[X15]:((![X16]:(~in(X16,X14)|in(X16,X15)))&~element(X14,powerset(X15))))),inference(variable_rename,[status(thm)],[c36])).
% 8.16/8.53 fof(c39,negated_conjecture,(![X16]:((~in(X16,skolem0005)|in(X16,skolem0006))&~element(skolem0005,powerset(skolem0006)))),inference(shift_quantors,[status(thm)],[fof(c38,negated_conjecture,((![X16]:(~in(X16,skolem0005)|in(X16,skolem0006)))&~element(skolem0005,powerset(skolem0006))),inference(skolemize,[status(esa)],[c37])).])).
% 8.16/8.53 cnf(c41,negated_conjecture,~element(skolem0005,powerset(skolem0006)),inference(split_conjunct,[status(thm)],[c39])).
% 8.16/8.53 fof(d2_subset_1,axiom,(![A]:(![B]:(((~empty(A))=>(element(B,A)<=>in(B,A)))&(empty(A)=>(element(B,A)<=>empty(B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_subset_1)).
% 8.16/8.53 fof(c61,plain,(![A]:(![B]:((~empty(A)=>(element(B,A)<=>in(B,A)))&(empty(A)=>(element(B,A)<=>empty(B)))))),inference(fof_simplification,[status(thm)],[d2_subset_1])).
% 8.16/8.53 fof(c62,plain,(![A]:(![B]:((empty(A)|((~element(B,A)|in(B,A))&(~in(B,A)|element(B,A))))&(~empty(A)|((~element(B,A)|empty(B))&(~empty(B)|element(B,A))))))),inference(fof_nnf,[status(thm)],[c61])).
% 8.16/8.53 fof(c63,plain,((![A]:(empty(A)|((![B]:(~element(B,A)|in(B,A)))&(![B]:(~in(B,A)|element(B,A))))))&(![A]:(~empty(A)|((![B]:(~element(B,A)|empty(B)))&(![B]:(~empty(B)|element(B,A))))))),inference(shift_quantors,[status(thm)],[c62])).
% 8.16/8.53 fof(c65,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((empty(X26)|((~element(X27,X26)|in(X27,X26))&(~in(X28,X26)|element(X28,X26))))&(~empty(X29)|((~element(X30,X29)|empty(X30))&(~empty(X31)|element(X31,X29))))))))))),inference(shift_quantors,[status(thm)],[fof(c64,plain,((![X26]:(empty(X26)|((![X27]:(~element(X27,X26)|in(X27,X26)))&(![X28]:(~in(X28,X26)|element(X28,X26))))))&(![X29]:(~empty(X29)|((![X30]:(~element(X30,X29)|empty(X30)))&(![X31]:(~empty(X31)|element(X31,X29))))))),inference(variable_rename,[status(thm)],[c63])).])).
% 8.16/8.53 fof(c66,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(((empty(X26)|(~element(X27,X26)|in(X27,X26)))&(empty(X26)|(~in(X28,X26)|element(X28,X26))))&((~empty(X29)|(~element(X30,X29)|empty(X30)))&(~empty(X29)|(~empty(X31)|element(X31,X29))))))))))),inference(distribute,[status(thm)],[c65])).
% 8.16/8.53 cnf(c68,plain,empty(X130)|~in(X131,X130)|element(X131,X130),inference(split_conjunct,[status(thm)],[c66])).
% 8.16/8.53 fof(d3_tarski,axiom,(![A]:(![B]:(subset(A,B)<=>(![C]:(in(C,A)=>in(C,B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_tarski)).
% 8.16/8.53 fof(c52,plain,(![A]:(![B]:((~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))&((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[d3_tarski])).
% 8.16/8.53 fof(c53,plain,((![A]:(![B]:(~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))))&(![A]:(![B]:((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c52])).
% 8.16/8.53 fof(c54,plain,((![X20]:(![X21]:(~subset(X20,X21)|(![X22]:(~in(X22,X20)|in(X22,X21))))))&(![X23]:(![X24]:((?[X25]:(in(X25,X23)&~in(X25,X24)))|subset(X23,X24))))),inference(variable_rename,[status(thm)],[c53])).
% 8.16/8.53 fof(c56,plain,(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((~subset(X20,X21)|(~in(X22,X20)|in(X22,X21)))&((in(skolem0008(X23,X24),X23)&~in(skolem0008(X23,X24),X24))|subset(X23,X24)))))))),inference(shift_quantors,[status(thm)],[fof(c55,plain,((![X20]:(![X21]:(~subset(X20,X21)|(![X22]:(~in(X22,X20)|in(X22,X21))))))&(![X23]:(![X24]:((in(skolem0008(X23,X24),X23)&~in(skolem0008(X23,X24),X24))|subset(X23,X24))))),inference(skolemize,[status(esa)],[c54])).])).
% 8.16/8.53 fof(c57,plain,(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((~subset(X20,X21)|(~in(X22,X20)|in(X22,X21)))&((in(skolem0008(X23,X24),X23)|subset(X23,X24))&(~in(skolem0008(X23,X24),X24)|subset(X23,X24))))))))),inference(distribute,[status(thm)],[c56])).
% 8.16/8.53 cnf(c60,plain,~in(skolem0008(X122,X123),X123)|subset(X122,X123),inference(split_conjunct,[status(thm)],[c57])).
% 8.16/8.53 cnf(c40,negated_conjecture,~in(X98,skolem0005)|in(X98,skolem0006),inference(split_conjunct,[status(thm)],[c39])).
% 8.16/8.53 cnf(c59,plain,in(skolem0008(X113,X114),X113)|subset(X113,X114),inference(split_conjunct,[status(thm)],[c57])).
% 8.16/8.53 cnf(c165,plain,subset(skolem0005,X292)|in(skolem0008(skolem0005,X292),skolem0006),inference(resolution,[status(thm)],[c59, c40])).
% 8.16/8.53 cnf(c860,plain,subset(skolem0005,skolem0006),inference(resolution,[status(thm)],[c165, c60])).
% 8.16/8.53 cnf(reflexivity,axiom,X41=X41,theory(equality)).
% 8.16/8.53 fof(d1_zfmisc_1,axiom,(![A]:(![B]:(B=powerset(A)<=>(![C]:(in(C,B)<=>subset(C,A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_zfmisc_1)).
% 8.16/8.53 fof(c71,plain,(![A]:(![B]:((B!=powerset(A)|(![C]:((~in(C,B)|subset(C,A))&(~subset(C,A)|in(C,B)))))&((?[C]:((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))|B=powerset(A))))),inference(fof_nnf,[status(thm)],[d1_zfmisc_1])).
% 8.16/8.53 fof(c72,plain,((![A]:(![B]:(B!=powerset(A)|((![C]:(~in(C,B)|subset(C,A)))&(![C]:(~subset(C,A)|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))|B=powerset(A))))),inference(shift_quantors,[status(thm)],[c71])).
% 8.16/8.53 fof(c73,plain,((![X32]:(![X33]:(X33!=powerset(X32)|((![X34]:(~in(X34,X33)|subset(X34,X32)))&(![X35]:(~subset(X35,X32)|in(X35,X33)))))))&(![X36]:(![X37]:((?[X38]:((~in(X38,X37)|~subset(X38,X36))&(in(X38,X37)|subset(X38,X36))))|X37=powerset(X36))))),inference(variable_rename,[status(thm)],[c72])).
% 8.16/8.53 fof(c75,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:((X33!=powerset(X32)|((~in(X34,X33)|subset(X34,X32))&(~subset(X35,X32)|in(X35,X33))))&(((~in(skolem0009(X36,X37),X37)|~subset(skolem0009(X36,X37),X36))&(in(skolem0009(X36,X37),X37)|subset(skolem0009(X36,X37),X36)))|X37=powerset(X36))))))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,((![X32]:(![X33]:(X33!=powerset(X32)|((![X34]:(~in(X34,X33)|subset(X34,X32)))&(![X35]:(~subset(X35,X32)|in(X35,X33)))))))&(![X36]:(![X37]:(((~in(skolem0009(X36,X37),X37)|~subset(skolem0009(X36,X37),X36))&(in(skolem0009(X36,X37),X37)|subset(skolem0009(X36,X37),X36)))|X37=powerset(X36))))),inference(skolemize,[status(esa)],[c73])).])).
% 8.16/8.53 fof(c76,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(((X33!=powerset(X32)|(~in(X34,X33)|subset(X34,X32)))&(X33!=powerset(X32)|(~subset(X35,X32)|in(X35,X33))))&(((~in(skolem0009(X36,X37),X37)|~subset(skolem0009(X36,X37),X36))|X37=powerset(X36))&((in(skolem0009(X36,X37),X37)|subset(skolem0009(X36,X37),X36))|X37=powerset(X36)))))))))),inference(distribute,[status(thm)],[c75])).
% 8.16/8.53 cnf(c78,plain,X143!=powerset(X141)|~subset(X142,X141)|in(X142,X143),inference(split_conjunct,[status(thm)],[c76])).
% 8.16/8.53 cnf(c283,plain,~subset(X298,X299)|in(X298,powerset(X299)),inference(resolution,[status(thm)],[c78, reflexivity])).
% 8.16/8.53 cnf(c888,plain,in(skolem0005,powerset(skolem0006)),inference(resolution,[status(thm)],[c283, c860])).
% 8.16/8.53 cnf(c929,plain,empty(powerset(skolem0006))|element(skolem0005,powerset(skolem0006)),inference(resolution,[status(thm)],[c888, c68])).
% 8.16/8.53 cnf(c17577,plain,empty(powerset(skolem0006)),inference(resolution,[status(thm)],[c929, c41])).
% 8.16/8.53 cnf(c17583,plain,$false,inference(resolution,[status(thm)],[c17577, c45])).
% 8.16/8.53 % SZS output end CNFRefutation
% 8.16/8.53
% 8.16/8.53 % Initial clauses : 38
% 8.16/8.53 % Processed clauses : 792
% 8.16/8.53 % Factors computed : 28
% 8.16/8.53 % Resolvents computed: 17514
% 8.16/8.53 % Tautologies deleted: 12
% 8.16/8.53 % Forward subsumed : 1975
% 8.16/8.53 % Backward subsumed : 19
% 8.16/8.53 % -------- CPU Time ---------
% 8.16/8.53 % User time : 7.941 s
% 8.16/8.53 % System time : 0.041 s
% 8.16/8.53 % Total time : 7.982 s
%------------------------------------------------------------------------------