%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET581+3 : TPTP v8.1.2. Released v2.2.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:39:45 EDT 2024
% Result : Theorem 0.90s 1.14s
% Output : Refutation 0.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET581+3 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 18:14:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.90/1.14 % Version: 1.5
% 0.90/1.14 % SZS status Theorem
% 0.90/1.14 % SZS output start CNFRefutation
% 0.90/1.14 fof(prove_th24,conjecture,(![B]:(![C]:(![D]:((member(B,C)&member(B,D))=>not_equal(intersection(C,D),empty_set))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_th24)).
% 0.90/1.14 fof(c4,negated_conjecture,(~(![B]:(![C]:(![D]:((member(B,C)&member(B,D))=>not_equal(intersection(C,D),empty_set)))))),inference(assume_negation,[status(cth)],[prove_th24])).
% 0.90/1.14 fof(c5,negated_conjecture,(?[B]:(?[C]:(?[D]:((member(B,C)&member(B,D))&~not_equal(intersection(C,D),empty_set))))),inference(fof_nnf,[status(thm)],[c4])).
% 0.90/1.14 fof(c6,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((member(X2,X3)&member(X2,X4))&~not_equal(intersection(X3,X4),empty_set))))),inference(variable_rename,[status(thm)],[c5])).
% 0.90/1.14 fof(c7,negated_conjecture,((member(skolem0001,skolem0002)&member(skolem0001,skolem0003))&~not_equal(intersection(skolem0002,skolem0003),empty_set)),inference(skolemize,[status(esa)],[c6])).
% 0.90/1.14 cnf(c10,negated_conjecture,~not_equal(intersection(skolem0002,skolem0003),empty_set),inference(split_conjunct,[status(thm)],[c7])).
% 0.90/1.14 fof(empty_set_defn,axiom,(![B]:(~member(B,empty_set))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', empty_set_defn)).
% 0.90/1.14 fof(c37,plain,(![B]:~member(B,empty_set)),inference(fof_simplification,[status(thm)],[empty_set_defn])).
% 0.90/1.14 fof(c38,plain,(![X22]:~member(X22,empty_set)),inference(variable_rename,[status(thm)],[c37])).
% 0.90/1.14 cnf(c39,plain,~member(X30,empty_set),inference(split_conjunct,[status(thm)],[c38])).
% 0.90/1.14 fof(empty_defn,axiom,(![B]:(empty(B)<=>(![C]:(~member(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', empty_defn)).
% 0.90/1.14 fof(c11,plain,(![B]:(empty(B)<=>(![C]:~member(C,B)))),inference(fof_simplification,[status(thm)],[empty_defn])).
% 0.90/1.14 fof(c12,plain,(![B]:((~empty(B)|(![C]:~member(C,B)))&((?[C]:member(C,B))|empty(B)))),inference(fof_nnf,[status(thm)],[c11])).
% 0.90/1.14 fof(c13,plain,((![B]:(~empty(B)|(![C]:~member(C,B))))&(![B]:((?[C]:member(C,B))|empty(B)))),inference(shift_quantors,[status(thm)],[c12])).
% 0.90/1.14 fof(c14,plain,((![X5]:(~empty(X5)|(![X6]:~member(X6,X5))))&(![X7]:((?[X8]:member(X8,X7))|empty(X7)))),inference(variable_rename,[status(thm)],[c13])).
% 0.90/1.14 fof(c16,plain,(![X5]:(![X6]:(![X7]:((~empty(X5)|~member(X6,X5))&(member(skolem0004(X7),X7)|empty(X7)))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,((![X5]:(~empty(X5)|(![X6]:~member(X6,X5))))&(![X7]:(member(skolem0004(X7),X7)|empty(X7)))),inference(skolemize,[status(esa)],[c14])).])).
% 0.90/1.14 cnf(c18,plain,member(skolem0004(X69),X69)|empty(X69),inference(split_conjunct,[status(thm)],[c16])).
% 0.90/1.14 cnf(c71,plain,empty(empty_set),inference(resolution,[status(thm)],[c18, c39])).
% 0.90/1.14 cnf(symmetry,axiom,X33!=X34|X34=X33,theory(equality)).
% 0.90/1.14 fof(not_equal_defn,axiom,(![B]:(![C]:(not_equal(B,C)<=>B!=C))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', not_equal_defn)).
% 0.90/1.14 fof(c21,plain,(![B]:(![C]:((~not_equal(B,C)|B!=C)&(B=C|not_equal(B,C))))),inference(fof_nnf,[status(thm)],[not_equal_defn])).
% 0.90/1.14 fof(c22,plain,((![B]:(![C]:(~not_equal(B,C)|B!=C)))&(![B]:(![C]:(B=C|not_equal(B,C))))),inference(shift_quantors,[status(thm)],[c21])).
% 0.90/1.14 fof(c24,plain,(![X11]:(![X12]:(![X13]:(![X14]:((~not_equal(X11,X12)|X11!=X12)&(X13=X14|not_equal(X13,X14))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X11]:(![X12]:(~not_equal(X11,X12)|X11!=X12)))&(![X13]:(![X14]:(X13=X14|not_equal(X13,X14))))),inference(variable_rename,[status(thm)],[c22])).])).
% 0.90/1.14 cnf(c26,plain,X43=X42|not_equal(X43,X42),inference(split_conjunct,[status(thm)],[c24])).
% 0.90/1.14 cnf(c54,plain,not_equal(X48,X49)|X49=X48,inference(resolution,[status(thm)],[c26, symmetry])).
% 0.90/1.14 cnf(c3,axiom,X75!=X76|~empty(X75)|empty(X76),theory(equality)).
% 0.90/1.14 cnf(c81,plain,~empty(X81)|empty(X80)|not_equal(X80,X81),inference(resolution,[status(thm)],[c3, c54])).
% 0.90/1.14 cnf(c91,plain,empty(X82)|not_equal(X82,empty_set),inference(resolution,[status(thm)],[c81, c71])).
% 0.90/1.14 cnf(c97,plain,empty(intersection(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c91, c10])).
% 0.90/1.14 fof(commutativity_of_intersection,axiom,(![B]:(![C]:intersection(B,C)=intersection(C,B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', commutativity_of_intersection)).
% 0.90/1.14 fof(c19,plain,(![X9]:(![X10]:intersection(X9,X10)=intersection(X10,X9))),inference(variable_rename,[status(thm)],[commutativity_of_intersection])).
% 0.90/1.14 cnf(c20,plain,intersection(X78,X79)=intersection(X79,X78),inference(split_conjunct,[status(thm)],[c19])).
% 0.90/1.14 cnf(c88,plain,~empty(intersection(X197,X198))|empty(intersection(X198,X197)),inference(resolution,[status(thm)],[c20, c3])).
% 0.90/1.14 cnf(c414,plain,empty(intersection(skolem0003,skolem0002)),inference(resolution,[status(thm)],[c88, c97])).
% 0.90/1.14 cnf(c17,plain,~empty(X31)|~member(X32,X31),inference(split_conjunct,[status(thm)],[c16])).
% 0.90/1.14 cnf(c9,negated_conjecture,member(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c7])).
% 0.90/1.14 cnf(c8,negated_conjecture,member(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c7])).
% 0.90/1.14 fof(intersection_defn,axiom,(![B]:(![C]:(![D]:(member(D,intersection(B,C))<=>(member(D,B)&member(D,C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', intersection_defn)).
% 0.90/1.14 fof(c40,plain,(![B]:(![C]:(![D]:((~member(D,intersection(B,C))|(member(D,B)&member(D,C)))&((~member(D,B)|~member(D,C))|member(D,intersection(B,C))))))),inference(fof_nnf,[status(thm)],[intersection_defn])).
% 0.90/1.14 fof(c41,plain,((![B]:(![C]:(![D]:(~member(D,intersection(B,C))|(member(D,B)&member(D,C))))))&(![B]:(![C]:(![D]:((~member(D,B)|~member(D,C))|member(D,intersection(B,C))))))),inference(shift_quantors,[status(thm)],[c40])).
% 0.90/1.14 fof(c43,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:((~member(X25,intersection(X23,X24))|(member(X25,X23)&member(X25,X24)))&((~member(X28,X26)|~member(X28,X27))|member(X28,intersection(X26,X27)))))))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,((![X23]:(![X24]:(![X25]:(~member(X25,intersection(X23,X24))|(member(X25,X23)&member(X25,X24))))))&(![X26]:(![X27]:(![X28]:((~member(X28,X26)|~member(X28,X27))|member(X28,intersection(X26,X27))))))),inference(variable_rename,[status(thm)],[c41])).])).
% 0.90/1.14 fof(c44,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(((~member(X25,intersection(X23,X24))|member(X25,X23))&(~member(X25,intersection(X23,X24))|member(X25,X24)))&((~member(X28,X26)|~member(X28,X27))|member(X28,intersection(X26,X27)))))))))),inference(distribute,[status(thm)],[c43])).
% 0.90/1.14 cnf(c47,plain,~member(X114,X113)|~member(X114,X112)|member(X114,intersection(X113,X112)),inference(split_conjunct,[status(thm)],[c44])).
% 0.90/1.14 cnf(c188,plain,~member(skolem0001,X509)|member(skolem0001,intersection(X509,skolem0002)),inference(resolution,[status(thm)],[c47, c8])).
% 0.90/1.14 cnf(c2477,plain,member(skolem0001,intersection(skolem0003,skolem0002)),inference(resolution,[status(thm)],[c188, c9])).
% 0.90/1.14 cnf(c2632,plain,~empty(intersection(skolem0003,skolem0002)),inference(resolution,[status(thm)],[c2477, c17])).
% 0.90/1.14 cnf(c2669,plain,$false,inference(resolution,[status(thm)],[c2632, c414])).
% 0.90/1.14 % SZS output end CNFRefutation
% 0.90/1.14
% 0.90/1.14 % Initial clauses : 23
% 0.90/1.14 % Processed clauses : 207
% 0.90/1.14 % Factors computed : 27
% 0.90/1.14 % Resolvents computed: 2599
% 0.90/1.14 % Tautologies deleted: 7
% 0.90/1.14 % Forward subsumed : 334
% 0.90/1.14 % Backward subsumed : 0
% 0.90/1.14 % -------- CPU Time ---------
% 0.90/1.14 % User time : 0.773 s
% 0.90/1.14 % System time : 0.019 s
% 0.90/1.14 % Total time : 0.792 s
%------------------------------------------------------------------------------