%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET596+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:39:47 EDT 2024
% Result : Theorem 7.70s 7.88s
% Output : Refutation 7.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SET596+3 : TPTP v8.1.2. Released v2.2.0.
% 0.14/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.37 % Computer : n022.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Wed May 8 19:10:08 EDT 2024
% 0.22/0.37 % CPUTime :
% 7.70/7.88 % Version: 1.5
% 7.70/7.88 % SZS status Theorem
% 7.70/7.88 % SZS output start CNFRefutation
% 7.70/7.88 fof(prove_th55,conjecture,(![B]:(![C]:(![D]:((subset(B,C)&intersection(C,D)=empty_set)=>intersection(B,D)=empty_set)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_th55)).
% 7.70/7.88 fof(c4,negated_conjecture,(~(![B]:(![C]:(![D]:((subset(B,C)&intersection(C,D)=empty_set)=>intersection(B,D)=empty_set))))),inference(assume_negation,[status(cth)],[prove_th55])).
% 7.70/7.88 fof(c5,negated_conjecture,(?[B]:(?[C]:(?[D]:((subset(B,C)&intersection(C,D)=empty_set)&intersection(B,D)!=empty_set)))),inference(fof_nnf,[status(thm)],[c4])).
% 7.70/7.88 fof(c6,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((subset(X2,X3)&intersection(X3,X4)=empty_set)&intersection(X2,X4)!=empty_set)))),inference(variable_rename,[status(thm)],[c5])).
% 7.70/7.88 fof(c7,negated_conjecture,((subset(skolem0001,skolem0002)&intersection(skolem0002,skolem0003)=empty_set)&intersection(skolem0001,skolem0003)!=empty_set),inference(skolemize,[status(esa)],[c6])).
% 7.70/7.88 cnf(c10,negated_conjecture,intersection(skolem0001,skolem0003)!=empty_set,inference(split_conjunct,[status(thm)],[c7])).
% 7.70/7.88 cnf(transitivity,axiom,X56!=X55|X55!=X54|X56=X54,theory(equality)).
% 7.70/7.88 cnf(c9,negated_conjecture,intersection(skolem0002,skolem0003)=empty_set,inference(split_conjunct,[status(thm)],[c7])).
% 7.70/7.88 cnf(c84,plain,X170!=intersection(skolem0002,skolem0003)|X170=empty_set,inference(resolution,[status(thm)],[c9, transitivity])).
% 7.70/7.88 cnf(c8,negated_conjecture,subset(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c7])).
% 7.70/7.88 fof(intersection_of_subset,axiom,(![B]:(![C]:(![D]:(subset(B,C)=>subset(intersection(B,D),intersection(C,D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', intersection_of_subset)).
% 7.70/7.88 fof(c61,plain,(![B]:(![C]:(![D]:(~subset(B,C)|subset(intersection(B,D),intersection(C,D)))))),inference(fof_nnf,[status(thm)],[intersection_of_subset])).
% 7.70/7.88 fof(c62,plain,(![B]:(![C]:(~subset(B,C)|(![D]:subset(intersection(B,D),intersection(C,D)))))),inference(shift_quantors,[status(thm)],[c61])).
% 7.70/7.88 fof(c64,plain,(![X36]:(![X37]:(![X38]:(~subset(X36,X37)|subset(intersection(X36,X38),intersection(X37,X38)))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,(![X36]:(![X37]:(~subset(X36,X37)|(![X38]:subset(intersection(X36,X38),intersection(X37,X38)))))),inference(variable_rename,[status(thm)],[c62])).])).
% 7.70/7.88 cnf(c65,plain,~subset(X142,X143)|subset(intersection(X142,X144),intersection(X143,X144)),inference(split_conjunct,[status(thm)],[c64])).
% 7.70/7.88 cnf(c219,plain,subset(intersection(skolem0001,X192),intersection(skolem0002,X192)),inference(resolution,[status(thm)],[c65, c8])).
% 7.70/7.88 fof(equal_defn,axiom,(![B]:(![C]:(B=C<=>(subset(B,C)&subset(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', equal_defn)).
% 7.70/7.88 fof(c33,plain,(![B]:(![C]:((B!=C|(subset(B,C)&subset(C,B)))&((~subset(B,C)|~subset(C,B))|B=C)))),inference(fof_nnf,[status(thm)],[equal_defn])).
% 7.70/7.88 fof(c34,plain,((![B]:(![C]:(B!=C|(subset(B,C)&subset(C,B)))))&(![B]:(![C]:((~subset(B,C)|~subset(C,B))|B=C)))),inference(shift_quantors,[status(thm)],[c33])).
% 7.70/7.88 fof(c36,plain,(![X19]:(![X20]:(![X21]:(![X22]:((X19!=X20|(subset(X19,X20)&subset(X20,X19)))&((~subset(X21,X22)|~subset(X22,X21))|X21=X22)))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,((![X19]:(![X20]:(X19!=X20|(subset(X19,X20)&subset(X20,X19)))))&(![X21]:(![X22]:((~subset(X21,X22)|~subset(X22,X21))|X21=X22)))),inference(variable_rename,[status(thm)],[c34])).])).
% 7.70/7.88 fof(c37,plain,(![X19]:(![X20]:(![X21]:(![X22]:(((X19!=X20|subset(X19,X20))&(X19!=X20|subset(X20,X19)))&((~subset(X21,X22)|~subset(X22,X21))|X21=X22)))))),inference(distribute,[status(thm)],[c36])).
% 7.70/7.88 cnf(c40,plain,~subset(X120,X121)|~subset(X121,X120)|X120=X121,inference(split_conjunct,[status(thm)],[c37])).
% 7.70/7.88 fof(empty_defn,axiom,(![B]:(empty(B)<=>(![C]:(~member(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', empty_defn)).
% 7.70/7.88 fof(c21,plain,(![B]:(empty(B)<=>(![C]:~member(C,B)))),inference(fof_simplification,[status(thm)],[empty_defn])).
% 7.70/7.88 fof(c22,plain,(![B]:((~empty(B)|(![C]:~member(C,B)))&((?[C]:member(C,B))|empty(B)))),inference(fof_nnf,[status(thm)],[c21])).
% 7.70/7.88 fof(c23,plain,((![B]:(~empty(B)|(![C]:~member(C,B))))&(![B]:((?[C]:member(C,B))|empty(B)))),inference(shift_quantors,[status(thm)],[c22])).
% 7.70/7.88 fof(c24,plain,((![X12]:(~empty(X12)|(![X13]:~member(X13,X12))))&(![X14]:((?[X15]:member(X15,X14))|empty(X14)))),inference(variable_rename,[status(thm)],[c23])).
% 7.70/7.88 fof(c26,plain,(![X12]:(![X13]:(![X14]:((~empty(X12)|~member(X13,X12))&(member(skolem0005(X14),X14)|empty(X14)))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X12]:(~empty(X12)|(![X13]:~member(X13,X12))))&(![X14]:(member(skolem0005(X14),X14)|empty(X14)))),inference(skolemize,[status(esa)],[c24])).])).
% 7.70/7.88 cnf(c27,plain,~empty(X44)|~member(X43,X44),inference(split_conjunct,[status(thm)],[c26])).
% 7.70/7.88 fof(subset_defn,axiom,(![B]:(![C]:(subset(B,C)<=>(![D]:(member(D,B)=>member(D,C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', subset_defn)).
% 7.70/7.88 fof(c41,plain,(![B]:(![C]:((~subset(B,C)|(![D]:(~member(D,B)|member(D,C))))&((?[D]:(member(D,B)&~member(D,C)))|subset(B,C))))),inference(fof_nnf,[status(thm)],[subset_defn])).
% 7.70/7.88 fof(c42,plain,((![B]:(![C]:(~subset(B,C)|(![D]:(~member(D,B)|member(D,C))))))&(![B]:(![C]:((?[D]:(member(D,B)&~member(D,C)))|subset(B,C))))),inference(shift_quantors,[status(thm)],[c41])).
% 7.70/7.88 fof(c43,plain,((![X23]:(![X24]:(~subset(X23,X24)|(![X25]:(~member(X25,X23)|member(X25,X24))))))&(![X26]:(![X27]:((?[X28]:(member(X28,X26)&~member(X28,X27)))|subset(X26,X27))))),inference(variable_rename,[status(thm)],[c42])).
% 7.70/7.88 fof(c45,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((~subset(X23,X24)|(~member(X25,X23)|member(X25,X24)))&((member(skolem0006(X26,X27),X26)&~member(skolem0006(X26,X27),X27))|subset(X26,X27)))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,((![X23]:(![X24]:(~subset(X23,X24)|(![X25]:(~member(X25,X23)|member(X25,X24))))))&(![X26]:(![X27]:((member(skolem0006(X26,X27),X26)&~member(skolem0006(X26,X27),X27))|subset(X26,X27))))),inference(skolemize,[status(esa)],[c43])).])).
% 7.70/7.88 fof(c46,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((~subset(X23,X24)|(~member(X25,X23)|member(X25,X24)))&((member(skolem0006(X26,X27),X26)|subset(X26,X27))&(~member(skolem0006(X26,X27),X27)|subset(X26,X27))))))))),inference(distribute,[status(thm)],[c45])).
% 7.70/7.88 cnf(c48,plain,member(skolem0006(X90,X89),X90)|subset(X90,X89),inference(split_conjunct,[status(thm)],[c46])).
% 7.70/7.88 cnf(c109,plain,subset(X95,X96)|~empty(X95),inference(resolution,[status(thm)],[c48, c27])).
% 7.70/7.88 fof(empty_set_defn,axiom,(![B]:(~member(B,empty_set))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', empty_set_defn)).
% 7.70/7.88 fof(c58,plain,(![B]:~member(B,empty_set)),inference(fof_simplification,[status(thm)],[empty_set_defn])).
% 7.70/7.88 fof(c59,plain,(![X35]:~member(X35,empty_set)),inference(variable_rename,[status(thm)],[c58])).
% 7.70/7.88 cnf(c60,plain,~member(X42,empty_set),inference(split_conjunct,[status(thm)],[c59])).
% 7.70/7.88 cnf(c28,plain,member(skolem0005(X60),X60)|empty(X60),inference(split_conjunct,[status(thm)],[c26])).
% 7.70/7.88 cnf(c74,plain,empty(empty_set),inference(resolution,[status(thm)],[c28, c60])).
% 7.70/7.88 cnf(c3,axiom,X66!=X67|~empty(X66)|empty(X67),theory(equality)).
% 7.70/7.88 cnf(symmetry,axiom,X46!=X45|X45=X46,theory(equality)).
% 7.70/7.88 cnf(c83,plain,empty_set=intersection(skolem0002,skolem0003),inference(resolution,[status(thm)],[c9, symmetry])).
% 7.70/7.88 cnf(c100,plain,~empty(empty_set)|empty(intersection(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c83, c3])).
% 7.70/7.88 cnf(c245,plain,empty(intersection(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c100, c74])).
% 7.70/7.88 cnf(c246,plain,subset(intersection(skolem0002,skolem0003),X164),inference(resolution,[status(thm)],[c245, c109])).
% 7.70/7.88 cnf(c261,plain,~subset(X1030,intersection(skolem0002,skolem0003))|X1030=intersection(skolem0002,skolem0003),inference(resolution,[status(thm)],[c246, c40])).
% 7.70/7.88 cnf(c4977,plain,intersection(skolem0001,skolem0003)=intersection(skolem0002,skolem0003),inference(resolution,[status(thm)],[c261, c219])).
% 7.70/7.88 cnf(c19792,plain,intersection(skolem0001,skolem0003)=empty_set,inference(resolution,[status(thm)],[c4977, c84])).
% 7.70/7.88 cnf(c19829,plain,$false,inference(resolution,[status(thm)],[c19792, c10])).
% 7.70/7.88 % SZS output end CNFRefutation
% 7.70/7.88
% 7.70/7.88 % Initial clauses : 30
% 7.70/7.88 % Processed clauses : 533
% 7.70/7.88 % Factors computed : 36
% 7.70/7.88 % Resolvents computed: 19769
% 7.70/7.88 % Tautologies deleted: 13
% 7.70/7.88 % Forward subsumed : 1395
% 7.70/7.88 % Backward subsumed : 22
% 7.70/7.88 % -------- CPU Time ---------
% 7.70/7.88 % User time : 7.450 s
% 7.70/7.88 % System time : 0.059 s
% 7.70/7.88 % Total time : 7.509 s
%------------------------------------------------------------------------------