%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET173+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:20 EDT 2024
% Result : Theorem 51.29s 51.51s
% Output : Refutation 51.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET173+3 : TPTP v8.1.2. Released v2.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.36 % Computer : n013.cluster.edu
% 0.16/0.36 % Model : x86_64 x86_64
% 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.36 % Memory : 8042.1875MB
% 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.36 % CPULimit : 300
% 0.16/0.36 % WCLimit : 300
% 0.16/0.36 % DateTime : Wed May 8 19:41:08 EDT 2024
% 0.16/0.36 % CPUTime :
% 51.29/51.51 % Version: 1.5
% 51.29/51.51 % SZS status Theorem
% 51.29/51.51 % SZS output start CNFRefutation
% 51.29/51.51 fof(prove_absorbtion_for_intersection,conjecture,(![B]:(![C]:intersection(B,union(B,C))=B)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_absorbtion_for_intersection)).
% 51.29/51.51 fof(c4,negated_conjecture,(~(![B]:(![C]:intersection(B,union(B,C))=B))),inference(assume_negation,[status(cth)],[prove_absorbtion_for_intersection])).
% 51.29/51.51 fof(c5,negated_conjecture,(?[B]:(?[C]:intersection(B,union(B,C))!=B)),inference(fof_nnf,[status(thm)],[c4])).
% 51.29/51.51 fof(c6,negated_conjecture,(?[X2]:(?[X3]:intersection(X2,union(X2,X3))!=X2)),inference(variable_rename,[status(thm)],[c5])).
% 51.29/51.51 fof(c7,negated_conjecture,intersection(skolem0001,union(skolem0001,skolem0002))!=skolem0001,inference(skolemize,[status(esa)],[c6])).
% 51.29/51.51 cnf(c8,negated_conjecture,intersection(skolem0001,union(skolem0001,skolem0002))!=skolem0001,inference(split_conjunct,[status(thm)],[c7])).
% 51.29/51.51 cnf(transitivity,axiom,X46!=X45|X45!=X47|X46=X47,theory(equality)).
% 51.29/51.51 fof(commutativity_of_intersection,axiom,(![B]:(![C]:intersection(B,C)=intersection(C,B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', commutativity_of_intersection)).
% 51.29/51.51 fof(c30,plain,(![X18]:(![X19]:intersection(X18,X19)=intersection(X19,X18))),inference(variable_rename,[status(thm)],[commutativity_of_intersection])).
% 51.29/51.51 cnf(c31,plain,intersection(X59,X60)=intersection(X60,X59),inference(split_conjunct,[status(thm)],[c30])).
% 51.29/51.51 cnf(c66,plain,X137!=intersection(X135,X136)|X137=intersection(X136,X135),inference(resolution,[status(thm)],[c31, transitivity])).
% 51.29/51.51 cnf(reflexivity,axiom,X38=X38,theory(equality)).
% 51.29/51.51 fof(commutativity_of_union,axiom,(![B]:(![C]:union(B,C)=union(C,B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', commutativity_of_union)).
% 51.29/51.51 fof(c32,plain,(![X20]:(![X21]:union(X20,X21)=union(X21,X20))),inference(variable_rename,[status(thm)],[commutativity_of_union])).
% 51.29/51.51 cnf(c33,plain,union(X61,X62)=union(X62,X61),inference(split_conjunct,[status(thm)],[c32])).
% 51.29/51.51 cnf(c1,axiom,X71!=X70|X69!=X72|intersection(X71,X69)=intersection(X70,X72),theory(equality)).
% 51.29/51.51 cnf(c77,plain,X224!=X223|intersection(X224,union(X222,X221))=intersection(X223,union(X221,X222)),inference(resolution,[status(thm)],[c1, c33])).
% 51.29/51.51 cnf(c240,plain,intersection(X1390,union(X1391,X1389))=intersection(X1390,union(X1389,X1391)),inference(resolution,[status(thm)],[c77, reflexivity])).
% 51.29/51.51 cnf(c5966,plain,intersection(X2561,union(X2562,X2560))=intersection(union(X2560,X2562),X2561),inference(resolution,[status(thm)],[c240, c66])).
% 51.29/51.51 cnf(symmetry,axiom,X41!=X40|X40=X41,theory(equality)).
% 51.29/51.51 fof(equal_defn,axiom,(![B]:(![C]:(B=C<=>(subset(B,C)&subset(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_defn)).
% 51.29/51.51 fof(c34,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])).
% 51.29/51.51 fof(c35,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)],[c34])).
% 51.29/51.51 fof(c37,plain,(![X22]:(![X23]:(![X24]:(![X25]:((X22!=X23|(subset(X22,X23)&subset(X23,X22)))&((~subset(X24,X25)|~subset(X25,X24))|X24=X25)))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X22]:(![X23]:(X22!=X23|(subset(X22,X23)&subset(X23,X22)))))&(![X24]:(![X25]:((~subset(X24,X25)|~subset(X25,X24))|X24=X25)))),inference(variable_rename,[status(thm)],[c35])).])).
% 51.29/51.51 fof(c38,plain,(![X22]:(![X23]:(![X24]:(![X25]:(((X22!=X23|subset(X22,X23))&(X22!=X23|subset(X23,X22)))&((~subset(X24,X25)|~subset(X25,X24))|X24=X25)))))),inference(distribute,[status(thm)],[c37])).
% 51.29/51.51 cnf(c41,plain,~subset(X113,X114)|~subset(X114,X113)|X113=X114,inference(split_conjunct,[status(thm)],[c38])).
% 51.29/51.51 fof(subset_defn,axiom,(![B]:(![C]:(subset(B,C)<=>(![D]:(member(D,B)=>member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', subset_defn)).
% 51.29/51.51 fof(c21,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])).
% 51.29/51.51 fof(c22,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)],[c21])).
% 51.29/51.51 fof(c23,plain,((![X12]:(![X13]:(~subset(X12,X13)|(![X14]:(~member(X14,X12)|member(X14,X13))))))&(![X15]:(![X16]:((?[X17]:(member(X17,X15)&~member(X17,X16)))|subset(X15,X16))))),inference(variable_rename,[status(thm)],[c22])).
% 51.29/51.51 fof(c25,plain,(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((~subset(X12,X13)|(~member(X14,X12)|member(X14,X13)))&((member(skolem0004(X15,X16),X15)&~member(skolem0004(X15,X16),X16))|subset(X15,X16)))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X12]:(![X13]:(~subset(X12,X13)|(![X14]:(~member(X14,X12)|member(X14,X13))))))&(![X15]:(![X16]:((member(skolem0004(X15,X16),X15)&~member(skolem0004(X15,X16),X16))|subset(X15,X16))))),inference(skolemize,[status(esa)],[c23])).])).
% 51.29/51.51 fof(c26,plain,(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((~subset(X12,X13)|(~member(X14,X12)|member(X14,X13)))&((member(skolem0004(X15,X16),X15)|subset(X15,X16))&(~member(skolem0004(X15,X16),X16)|subset(X15,X16))))))))),inference(distribute,[status(thm)],[c25])).
% 51.29/51.51 cnf(c29,plain,~member(skolem0004(X81,X82),X82)|subset(X81,X82),inference(split_conjunct,[status(thm)],[c26])).
% 51.29/51.51 cnf(c28,plain,member(skolem0004(X79,X80),X79)|subset(X79,X80),inference(split_conjunct,[status(thm)],[c26])).
% 51.29/51.51 fof(intersection_defn,axiom,(![B]:(![C]:(![D]:(member(D,intersection(B,C))<=>(member(D,B)&member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', intersection_defn)).
% 51.29/51.51 fof(c42,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])).
% 51.29/51.51 fof(c43,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)],[c42])).
% 51.29/51.51 fof(c45,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~member(X28,intersection(X26,X27))|(member(X28,X26)&member(X28,X27)))&((~member(X31,X29)|~member(X31,X30))|member(X31,intersection(X29,X30)))))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,((![X26]:(![X27]:(![X28]:(~member(X28,intersection(X26,X27))|(member(X28,X26)&member(X28,X27))))))&(![X29]:(![X30]:(![X31]:((~member(X31,X29)|~member(X31,X30))|member(X31,intersection(X29,X30))))))),inference(variable_rename,[status(thm)],[c43])).])).
% 51.29/51.51 fof(c46,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(((~member(X28,intersection(X26,X27))|member(X28,X26))&(~member(X28,intersection(X26,X27))|member(X28,X27)))&((~member(X31,X29)|~member(X31,X30))|member(X31,intersection(X29,X30)))))))))),inference(distribute,[status(thm)],[c45])).
% 51.29/51.51 cnf(c48,plain,~member(X93,intersection(X92,X91))|member(X93,X91),inference(split_conjunct,[status(thm)],[c46])).
% 51.29/51.51 cnf(c82,plain,member(skolem0004(intersection(X263,X264),X265),X264)|subset(intersection(X263,X264),X265),inference(resolution,[status(thm)],[c48, c28])).
% 51.29/51.51 cnf(c336,plain,subset(intersection(X275,X276),X276),inference(resolution,[status(thm)],[c82, c29])).
% 51.29/51.51 cnf(c358,plain,~subset(X702,intersection(X703,X702))|X702=intersection(X703,X702),inference(resolution,[status(thm)],[c336, c41])).
% 51.29/51.51 fof(union_defn,axiom,(![B]:(![C]:(![D]:(member(D,union(B,C))<=>(member(D,B)|member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', union_defn)).
% 51.29/51.51 fof(c50,plain,(![B]:(![C]:(![D]:((~member(D,union(B,C))|(member(D,B)|member(D,C)))&((~member(D,B)&~member(D,C))|member(D,union(B,C))))))),inference(fof_nnf,[status(thm)],[union_defn])).
% 51.29/51.51 fof(c51,plain,((![B]:(![C]:(![D]:(~member(D,union(B,C))|(member(D,B)|member(D,C))))))&(![B]:(![C]:(![D]:((~member(D,B)&~member(D,C))|member(D,union(B,C))))))),inference(shift_quantors,[status(thm)],[c50])).
% 51.29/51.51 fof(c53,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:((~member(X34,union(X32,X33))|(member(X34,X32)|member(X34,X33)))&((~member(X37,X35)&~member(X37,X36))|member(X37,union(X35,X36)))))))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,((![X32]:(![X33]:(![X34]:(~member(X34,union(X32,X33))|(member(X34,X32)|member(X34,X33))))))&(![X35]:(![X36]:(![X37]:((~member(X37,X35)&~member(X37,X36))|member(X37,union(X35,X36))))))),inference(variable_rename,[status(thm)],[c51])).])).
% 51.29/51.51 fof(c54,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:((~member(X34,union(X32,X33))|(member(X34,X32)|member(X34,X33)))&((~member(X37,X35)|member(X37,union(X35,X36)))&(~member(X37,X36)|member(X37,union(X35,X36))))))))))),inference(distribute,[status(thm)],[c53])).
% 51.29/51.51 cnf(c57,plain,~member(X97,X98)|member(X97,union(X99,X98)),inference(split_conjunct,[status(thm)],[c54])).
% 51.29/51.51 cnf(c84,plain,member(skolem0004(X174,X175),union(X173,X174))|subset(X174,X175),inference(resolution,[status(thm)],[c57, c28])).
% 51.29/51.51 cnf(c49,plain,~member(X152,X151)|~member(X152,X150)|member(X152,intersection(X151,X150)),inference(split_conjunct,[status(thm)],[c46])).
% 51.29/51.51 cnf(c146,plain,~member(skolem0004(X727,X729),X728)|member(skolem0004(X727,X729),intersection(X728,X727))|subset(X727,X729),inference(resolution,[status(thm)],[c49, c28])).
% 51.29/51.51 cnf(c2684,plain,member(skolem0004(X7073,X7072),intersection(union(X7071,X7073),X7073))|subset(X7073,X7072),inference(resolution,[status(thm)],[c146, c84])).
% 51.29/51.51 cnf(c65551,plain,subset(X7074,intersection(union(X7075,X7074),X7074)),inference(resolution,[status(thm)],[c2684, c29])).
% 51.29/51.51 cnf(c65610,plain,X7076=intersection(union(X7077,X7076),X7076),inference(resolution,[status(thm)],[c65551, c358])).
% 51.29/51.51 cnf(c65685,plain,intersection(union(X7079,X7080),X7080)=X7080,inference(resolution,[status(thm)],[c65610, symmetry])).
% 51.29/51.51 cnf(c65868,plain,X7705!=intersection(union(X7704,X7703),X7703)|X7705=X7703,inference(resolution,[status(thm)],[c65685, transitivity])).
% 51.29/51.51 cnf(c76535,plain,intersection(X7715,union(X7715,X7714))=X7715,inference(resolution,[status(thm)],[c65868, c5966])).
% 51.29/51.51 cnf(c77009,plain,$false,inference(resolution,[status(thm)],[c76535, c8])).
% 51.29/51.51 % SZS output end CNFRefutation
% 51.29/51.51
% 51.29/51.51 % Initial clauses : 27
% 51.29/51.51 % Processed clauses : 1033
% 51.29/51.51 % Factors computed : 121
% 51.29/51.51 % Resolvents computed: 76918
% 51.29/51.51 % Tautologies deleted: 4
% 51.29/51.51 % Forward subsumed : 2500
% 51.29/51.51 % Backward subsumed : 31
% 51.29/51.51 % -------- CPU Time ---------
% 51.29/51.51 % User time : 50.941 s
% 51.29/51.51 % System time : 0.193 s
% 51.29/51.51 % Total time : 51.134 s
%------------------------------------------------------------------------------