%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET629+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:53 EDT 2024
% Result : Theorem 0.46s 0.68s
% Output : Refutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET629+3 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n028.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 18:51:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.46/0.68 % Version: 1.5
% 0.46/0.68 % SZS status Theorem
% 0.46/0.68 % SZS output start CNFRefutation
% 0.46/0.68 fof(prove_intersection_and_difference_disjoint,conjecture,(![B]:(![C]:disjoint(intersection(B,C),difference(B,C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_intersection_and_difference_disjoint)).
% 0.46/0.68 fof(c5,negated_conjecture,(~(![B]:(![C]:disjoint(intersection(B,C),difference(B,C))))),inference(assume_negation,[status(cth)],[prove_intersection_and_difference_disjoint])).
% 0.46/0.68 fof(c6,negated_conjecture,(?[B]:(?[C]:~disjoint(intersection(B,C),difference(B,C)))),inference(fof_nnf,[status(thm)],[c5])).
% 0.46/0.68 fof(c7,negated_conjecture,(?[X2]:(?[X3]:~disjoint(intersection(X2,X3),difference(X2,X3)))),inference(variable_rename,[status(thm)],[c6])).
% 0.46/0.68 fof(c8,negated_conjecture,~disjoint(intersection(skolem0001,skolem0002),difference(skolem0001,skolem0002)),inference(skolemize,[status(esa)],[c7])).
% 0.46/0.68 cnf(c9,negated_conjecture,~disjoint(intersection(skolem0001,skolem0002),difference(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c8])).
% 0.46/0.68 fof(difference_defn,axiom,(![B]:(![C]:(![D]:(member(D,difference(B,C))<=>(member(D,B)&(~member(D,C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', difference_defn)).
% 0.46/0.68 fof(c41,plain,(![B]:(![C]:(![D]:(member(D,difference(B,C))<=>(member(D,B)&~member(D,C)))))),inference(fof_simplification,[status(thm)],[difference_defn])).
% 0.46/0.68 fof(c42,plain,(![B]:(![C]:(![D]:((~member(D,difference(B,C))|(member(D,B)&~member(D,C)))&((~member(D,B)|member(D,C))|member(D,difference(B,C))))))),inference(fof_nnf,[status(thm)],[c41])).
% 0.46/0.68 fof(c43,plain,((![B]:(![C]:(![D]:(~member(D,difference(B,C))|(member(D,B)&~member(D,C))))))&(![B]:(![C]:(![D]:((~member(D,B)|member(D,C))|member(D,difference(B,C))))))),inference(shift_quantors,[status(thm)],[c42])).
% 0.46/0.68 fof(c45,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:((~member(X27,difference(X25,X26))|(member(X27,X25)&~member(X27,X26)))&((~member(X30,X28)|member(X30,X29))|member(X30,difference(X28,X29)))))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,((![X25]:(![X26]:(![X27]:(~member(X27,difference(X25,X26))|(member(X27,X25)&~member(X27,X26))))))&(![X28]:(![X29]:(![X30]:((~member(X30,X28)|member(X30,X29))|member(X30,difference(X28,X29))))))),inference(variable_rename,[status(thm)],[c43])).])).
% 0.46/0.68 fof(c46,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(((~member(X27,difference(X25,X26))|member(X27,X25))&(~member(X27,difference(X25,X26))|~member(X27,X26)))&((~member(X30,X28)|member(X30,X29))|member(X30,difference(X28,X29)))))))))),inference(distribute,[status(thm)],[c45])).
% 0.46/0.68 cnf(c48,plain,~member(X86,difference(X85,X84))|~member(X86,X84),inference(split_conjunct,[status(thm)],[c46])).
% 0.46/0.68 fof(symmetry_of_intersect,axiom,(![B]:(![C]:(intersect(B,C)=>intersect(C,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', symmetry_of_intersect)).
% 0.46/0.68 fof(c20,plain,(![B]:(![C]:(~intersect(B,C)|intersect(C,B)))),inference(fof_nnf,[status(thm)],[symmetry_of_intersect])).
% 0.46/0.68 fof(c21,plain,(![X11]:(![X12]:(~intersect(X11,X12)|intersect(X12,X11)))),inference(variable_rename,[status(thm)],[c20])).
% 0.46/0.68 cnf(c22,plain,~intersect(X41,X42)|intersect(X42,X41),inference(split_conjunct,[status(thm)],[c21])).
% 0.46/0.68 fof(disjoint_defn,axiom,(![B]:(![C]:(disjoint(B,C)<=>(~intersect(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', disjoint_defn)).
% 0.46/0.68 fof(c25,plain,(![B]:(![C]:(disjoint(B,C)<=>~intersect(B,C)))),inference(fof_simplification,[status(thm)],[disjoint_defn])).
% 0.46/0.68 fof(c26,plain,(![B]:(![C]:((~disjoint(B,C)|~intersect(B,C))&(intersect(B,C)|disjoint(B,C))))),inference(fof_nnf,[status(thm)],[c25])).
% 0.46/0.68 fof(c27,plain,((![B]:(![C]:(~disjoint(B,C)|~intersect(B,C))))&(![B]:(![C]:(intersect(B,C)|disjoint(B,C))))),inference(shift_quantors,[status(thm)],[c26])).
% 0.46/0.68 fof(c29,plain,(![X15]:(![X16]:(![X17]:(![X18]:((~disjoint(X15,X16)|~intersect(X15,X16))&(intersect(X17,X18)|disjoint(X17,X18))))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,((![X15]:(![X16]:(~disjoint(X15,X16)|~intersect(X15,X16))))&(![X17]:(![X18]:(intersect(X17,X18)|disjoint(X17,X18))))),inference(variable_rename,[status(thm)],[c27])).])).
% 0.46/0.68 cnf(c31,plain,intersect(X49,X48)|disjoint(X49,X48),inference(split_conjunct,[status(thm)],[c29])).
% 0.46/0.68 cnf(c61,plain,disjoint(X54,X53)|intersect(X53,X54),inference(resolution,[status(thm)],[c31, c22])).
% 0.46/0.68 fof(intersect_defn,axiom,(![B]:(![C]:(intersect(B,C)<=>(?[D]:(member(D,B)&member(D,C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', intersect_defn)).
% 0.46/0.68 fof(c32,plain,(![B]:(![C]:((~intersect(B,C)|(?[D]:(member(D,B)&member(D,C))))&((![D]:(~member(D,B)|~member(D,C)))|intersect(B,C))))),inference(fof_nnf,[status(thm)],[intersect_defn])).
% 0.46/0.68 fof(c33,plain,((![B]:(![C]:(~intersect(B,C)|(?[D]:(member(D,B)&member(D,C))))))&(![B]:(![C]:((![D]:(~member(D,B)|~member(D,C)))|intersect(B,C))))),inference(shift_quantors,[status(thm)],[c32])).
% 0.46/0.68 fof(c34,plain,((![X19]:(![X20]:(~intersect(X19,X20)|(?[X21]:(member(X21,X19)&member(X21,X20))))))&(![X22]:(![X23]:((![X24]:(~member(X24,X22)|~member(X24,X23)))|intersect(X22,X23))))),inference(variable_rename,[status(thm)],[c33])).
% 0.46/0.68 fof(c36,plain,(![X19]:(![X20]:(![X22]:(![X23]:(![X24]:((~intersect(X19,X20)|(member(skolem0004(X19,X20),X19)&member(skolem0004(X19,X20),X20)))&((~member(X24,X22)|~member(X24,X23))|intersect(X22,X23)))))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,((![X19]:(![X20]:(~intersect(X19,X20)|(member(skolem0004(X19,X20),X19)&member(skolem0004(X19,X20),X20)))))&(![X22]:(![X23]:((![X24]:(~member(X24,X22)|~member(X24,X23)))|intersect(X22,X23))))),inference(skolemize,[status(esa)],[c34])).])).
% 0.46/0.68 fof(c37,plain,(![X19]:(![X20]:(![X22]:(![X23]:(![X24]:(((~intersect(X19,X20)|member(skolem0004(X19,X20),X19))&(~intersect(X19,X20)|member(skolem0004(X19,X20),X20)))&((~member(X24,X22)|~member(X24,X23))|intersect(X22,X23)))))))),inference(distribute,[status(thm)],[c36])).
% 0.46/0.68 cnf(c38,plain,~intersect(X77,X78)|member(skolem0004(X77,X78),X77),inference(split_conjunct,[status(thm)],[c37])).
% 0.46/0.68 cnf(c75,plain,member(skolem0004(X98,X97),X98)|disjoint(X97,X98),inference(resolution,[status(thm)],[c38, c61])).
% 0.46/0.68 cnf(c83,plain,disjoint(X284,difference(X285,X286))|~member(skolem0004(difference(X285,X286),X284),X286),inference(resolution,[status(thm)],[c75, c48])).
% 0.46/0.68 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.46/0.68 fof(c50,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.46/0.68 fof(c51,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)],[c50])).
% 0.46/0.68 fof(c53,plain,(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:((~member(X33,intersection(X31,X32))|(member(X33,X31)&member(X33,X32)))&((~member(X36,X34)|~member(X36,X35))|member(X36,intersection(X34,X35)))))))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,((![X31]:(![X32]:(![X33]:(~member(X33,intersection(X31,X32))|(member(X33,X31)&member(X33,X32))))))&(![X34]:(![X35]:(![X36]:((~member(X36,X34)|~member(X36,X35))|member(X36,intersection(X34,X35))))))),inference(variable_rename,[status(thm)],[c51])).])).
% 0.46/0.68 fof(c54,plain,(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(((~member(X33,intersection(X31,X32))|member(X33,X31))&(~member(X33,intersection(X31,X32))|member(X33,X32)))&((~member(X36,X34)|~member(X36,X35))|member(X36,intersection(X34,X35)))))))))),inference(distribute,[status(thm)],[c53])).
% 0.46/0.68 cnf(c56,plain,~member(X94,intersection(X95,X96))|member(X94,X96),inference(split_conjunct,[status(thm)],[c54])).
% 0.46/0.68 cnf(c39,plain,~intersect(X79,X80)|member(skolem0004(X79,X80),X80),inference(split_conjunct,[status(thm)],[c37])).
% 0.46/0.68 cnf(c77,plain,member(skolem0004(X102,X101),X101)|disjoint(X101,X102),inference(resolution,[status(thm)],[c39, c61])).
% 0.46/0.68 cnf(c91,plain,disjoint(intersection(X380,X378),X379)|member(skolem0004(X379,intersection(X380,X378)),X378),inference(resolution,[status(thm)],[c77, c56])).
% 0.46/0.68 cnf(c555,plain,disjoint(intersection(X382,X381),difference(X383,X381)),inference(resolution,[status(thm)],[c91, c83])).
% 0.46/0.68 cnf(c567,plain,$false,inference(resolution,[status(thm)],[c555, c9])).
% 0.46/0.68 % SZS output end CNFRefutation
% 0.46/0.68
% 0.46/0.68 % Initial clauses : 26
% 0.46/0.68 % Processed clauses : 80
% 0.46/0.68 % Factors computed : 7
% 0.46/0.68 % Resolvents computed: 504
% 0.46/0.68 % Tautologies deleted: 3
% 0.46/0.68 % Forward subsumed : 86
% 0.46/0.68 % Backward subsumed : 0
% 0.46/0.68 % -------- CPU Time ---------
% 0.46/0.68 % User time : 0.295 s
% 0.46/0.68 % System time : 0.020 s
% 0.46/0.68 % Total time : 0.315 s
%------------------------------------------------------------------------------