%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET628+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:52 EDT 2024
% Result : Theorem 0.54s 0.72s
% Output : Refutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET628+3 : TPTP v8.1.2. Released v2.2.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.36 % Computer : n021.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:24:53 EDT 2024
% 0.16/0.36 % CPUTime :
% 0.54/0.72 % Version: 1.5
% 0.54/0.72 % SZS status Theorem
% 0.54/0.72 % SZS output start CNFRefutation
% 0.54/0.72 fof(prove_th110,conjecture,(![B]:(intersect(B,B)<=>not_equal(B,empty_set))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th110)).
% 0.54/0.72 fof(c4,negated_conjecture,(~(![B]:(intersect(B,B)<=>not_equal(B,empty_set)))),inference(assume_negation,[status(cth)],[prove_th110])).
% 0.54/0.72 fof(c5,negated_conjecture,(?[B]:((~intersect(B,B)|~not_equal(B,empty_set))&(intersect(B,B)|not_equal(B,empty_set)))),inference(fof_nnf,[status(thm)],[c4])).
% 0.54/0.72 fof(c6,negated_conjecture,(?[X2]:((~intersect(X2,X2)|~not_equal(X2,empty_set))&(intersect(X2,X2)|not_equal(X2,empty_set)))),inference(variable_rename,[status(thm)],[c5])).
% 0.54/0.72 fof(c7,negated_conjecture,((~intersect(skolem0001,skolem0001)|~not_equal(skolem0001,empty_set))&(intersect(skolem0001,skolem0001)|not_equal(skolem0001,empty_set))),inference(skolemize,[status(esa)],[c6])).
% 0.54/0.72 cnf(c8,negated_conjecture,~intersect(skolem0001,skolem0001)|~not_equal(skolem0001,empty_set),inference(split_conjunct,[status(thm)],[c7])).
% 0.54/0.72 fof(not_equal_defn,axiom,(![B]:(![C]:(not_equal(B,C)<=>B!=C))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', not_equal_defn)).
% 0.54/0.72 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.54/0.72 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.54/0.72 fof(c24,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~not_equal(X9,X10)|X9!=X10)&(X11=X12|not_equal(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X9]:(![X10]:(~not_equal(X9,X10)|X9!=X10)))&(![X11]:(![X12]:(X11=X12|not_equal(X11,X12))))),inference(variable_rename,[status(thm)],[c22])).])).
% 0.54/0.72 cnf(c25,plain,~not_equal(X40,X39)|X40!=X39,inference(split_conjunct,[status(thm)],[c24])).
% 0.54/0.72 cnf(symmetry,axiom,X32!=X31|X31=X32,theory(equality)).
% 0.54/0.72 cnf(c26,plain,X43=X42|not_equal(X43,X42),inference(split_conjunct,[status(thm)],[c24])).
% 0.54/0.72 cnf(c55,plain,not_equal(X54,X55)|X55=X54,inference(resolution,[status(thm)],[c26, symmetry])).
% 0.54/0.72 cnf(c59,plain,not_equal(X62,X61)|~not_equal(X61,X62),inference(resolution,[status(thm)],[c55, c25])).
% 0.54/0.72 fof(empty_set_defn,axiom,(![B]:(~member(B,empty_set))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', empty_set_defn)).
% 0.54/0.72 fof(c37,plain,(![B]:~member(B,empty_set)),inference(fof_simplification,[status(thm)],[empty_set_defn])).
% 0.54/0.72 fof(c38,plain,(![X20]:~member(X20,empty_set)),inference(variable_rename,[status(thm)],[c37])).
% 0.54/0.72 cnf(c39,plain,~member(X28,empty_set),inference(split_conjunct,[status(thm)],[c38])).
% 0.54/0.72 fof(empty_defn,axiom,(![B]:(empty(B)<=>(![C]:(~member(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', empty_defn)).
% 0.54/0.72 fof(c10,plain,(![B]:(empty(B)<=>(![C]:~member(C,B)))),inference(fof_simplification,[status(thm)],[empty_defn])).
% 0.54/0.72 fof(c11,plain,(![B]:((~empty(B)|(![C]:~member(C,B)))&((?[C]:member(C,B))|empty(B)))),inference(fof_nnf,[status(thm)],[c10])).
% 0.54/0.72 fof(c12,plain,((![B]:(~empty(B)|(![C]:~member(C,B))))&(![B]:((?[C]:member(C,B))|empty(B)))),inference(shift_quantors,[status(thm)],[c11])).
% 0.54/0.72 fof(c13,plain,((![X3]:(~empty(X3)|(![X4]:~member(X4,X3))))&(![X5]:((?[X6]:member(X6,X5))|empty(X5)))),inference(variable_rename,[status(thm)],[c12])).
% 0.54/0.72 fof(c15,plain,(![X3]:(![X4]:(![X5]:((~empty(X3)|~member(X4,X3))&(member(skolem0002(X5),X5)|empty(X5)))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,((![X3]:(~empty(X3)|(![X4]:~member(X4,X3))))&(![X5]:(member(skolem0002(X5),X5)|empty(X5)))),inference(skolemize,[status(esa)],[c13])).])).
% 0.54/0.72 cnf(c17,plain,member(skolem0002(X69),X69)|empty(X69),inference(split_conjunct,[status(thm)],[c15])).
% 0.54/0.72 cnf(c63,plain,empty(empty_set),inference(resolution,[status(thm)],[c17, c39])).
% 0.54/0.72 cnf(c3,axiom,X75!=X76|~empty(X75)|empty(X76),theory(equality)).
% 0.54/0.72 cnf(c68,plain,~empty(X79)|empty(X78)|not_equal(X79,X78),inference(resolution,[status(thm)],[c3, c26])).
% 0.54/0.72 cnf(c71,plain,empty(X80)|not_equal(empty_set,X80),inference(resolution,[status(thm)],[c68, c63])).
% 0.54/0.72 cnf(c78,plain,empty(X81)|not_equal(X81,empty_set),inference(resolution,[status(thm)],[c71, c59])).
% 0.54/0.72 cnf(c82,plain,empty(skolem0001)|~intersect(skolem0001,skolem0001),inference(resolution,[status(thm)],[c78, c8])).
% 0.54/0.72 fof(intersect_defn,axiom,(![B]:(![C]:(intersect(B,C)<=>(?[D]:(member(D,B)&member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', intersect_defn)).
% 0.54/0.72 fof(c40,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.54/0.72 fof(c41,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)],[c40])).
% 0.54/0.72 fof(c42,plain,((![X21]:(![X22]:(~intersect(X21,X22)|(?[X23]:(member(X23,X21)&member(X23,X22))))))&(![X24]:(![X25]:((![X26]:(~member(X26,X24)|~member(X26,X25)))|intersect(X24,X25))))),inference(variable_rename,[status(thm)],[c41])).
% 0.54/0.72 fof(c44,plain,(![X21]:(![X22]:(![X24]:(![X25]:(![X26]:((~intersect(X21,X22)|(member(skolem0004(X21,X22),X21)&member(skolem0004(X21,X22),X22)))&((~member(X26,X24)|~member(X26,X25))|intersect(X24,X25)))))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,((![X21]:(![X22]:(~intersect(X21,X22)|(member(skolem0004(X21,X22),X21)&member(skolem0004(X21,X22),X22)))))&(![X24]:(![X25]:((![X26]:(~member(X26,X24)|~member(X26,X25)))|intersect(X24,X25))))),inference(skolemize,[status(esa)],[c42])).])).
% 0.54/0.72 fof(c45,plain,(![X21]:(![X22]:(![X24]:(![X25]:(![X26]:(((~intersect(X21,X22)|member(skolem0004(X21,X22),X21))&(~intersect(X21,X22)|member(skolem0004(X21,X22),X22)))&((~member(X26,X24)|~member(X26,X25))|intersect(X24,X25)))))))),inference(distribute,[status(thm)],[c44])).
% 0.54/0.72 cnf(c48,plain,~member(X98,X97)|~member(X98,X96)|intersect(X97,X96),inference(split_conjunct,[status(thm)],[c45])).
% 0.54/0.72 cnf(c98,plain,~member(X100,X99)|intersect(X99,X99),inference(factor,[status(thm)],[c48])).
% 0.54/0.72 cnf(c100,plain,intersect(X101,X101)|empty(X101),inference(resolution,[status(thm)],[c98, c17])).
% 0.54/0.72 cnf(c104,plain,empty(skolem0001),inference(resolution,[status(thm)],[c100, c82])).
% 0.54/0.72 cnf(c16,plain,~empty(X30)|~member(X29,X30),inference(split_conjunct,[status(thm)],[c15])).
% 0.54/0.72 cnf(c9,negated_conjecture,intersect(skolem0001,skolem0001)|not_equal(skolem0001,empty_set),inference(split_conjunct,[status(thm)],[c7])).
% 0.54/0.72 cnf(c46,plain,~intersect(X87,X86)|member(skolem0004(X87,X86),X87),inference(split_conjunct,[status(thm)],[c45])).
% 0.54/0.72 cnf(c94,plain,member(skolem0004(skolem0001,skolem0001),skolem0001)|not_equal(skolem0001,empty_set),inference(resolution,[status(thm)],[c46, c9])).
% 0.54/0.72 cnf(c324,plain,not_equal(skolem0001,empty_set)|~empty(skolem0001),inference(resolution,[status(thm)],[c94, c16])).
% 0.54/0.72 cnf(c336,plain,not_equal(skolem0001,empty_set),inference(resolution,[status(thm)],[c324, c104])).
% 0.54/0.72 cnf(c347,plain,~intersect(skolem0001,skolem0001),inference(resolution,[status(thm)],[c336, c8])).
% 0.54/0.72 fof(equal_member_defn,axiom,(![B]:(![C]:(B=C<=>(![D]:(member(D,B)<=>member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_member_defn)).
% 0.54/0.72 fof(c27,plain,(![B]:(![C]:((B!=C|(![D]:((~member(D,B)|member(D,C))&(~member(D,C)|member(D,B)))))&((?[D]:((~member(D,B)|~member(D,C))&(member(D,B)|member(D,C))))|B=C)))),inference(fof_nnf,[status(thm)],[equal_member_defn])).
% 0.54/0.72 fof(c28,plain,((![B]:(![C]:(B!=C|((![D]:(~member(D,B)|member(D,C)))&(![D]:(~member(D,C)|member(D,B)))))))&(![B]:(![C]:((?[D]:((~member(D,B)|~member(D,C))&(member(D,B)|member(D,C))))|B=C)))),inference(shift_quantors,[status(thm)],[c27])).
% 0.54/0.72 fof(c29,plain,((![X13]:(![X14]:(X13!=X14|((![X15]:(~member(X15,X13)|member(X15,X14)))&(![X16]:(~member(X16,X14)|member(X16,X13)))))))&(![X17]:(![X18]:((?[X19]:((~member(X19,X17)|~member(X19,X18))&(member(X19,X17)|member(X19,X18))))|X17=X18)))),inference(variable_rename,[status(thm)],[c28])).
% 0.54/0.72 fof(c31,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((X13!=X14|((~member(X15,X13)|member(X15,X14))&(~member(X16,X14)|member(X16,X13))))&(((~member(skolem0003(X17,X18),X17)|~member(skolem0003(X17,X18),X18))&(member(skolem0003(X17,X18),X17)|member(skolem0003(X17,X18),X18)))|X17=X18)))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X13]:(![X14]:(X13!=X14|((![X15]:(~member(X15,X13)|member(X15,X14)))&(![X16]:(~member(X16,X14)|member(X16,X13)))))))&(![X17]:(![X18]:(((~member(skolem0003(X17,X18),X17)|~member(skolem0003(X17,X18),X18))&(member(skolem0003(X17,X18),X17)|member(skolem0003(X17,X18),X18)))|X17=X18)))),inference(skolemize,[status(esa)],[c29])).])).
% 0.54/0.72 fof(c32,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(((X13!=X14|(~member(X15,X13)|member(X15,X14)))&(X13!=X14|(~member(X16,X14)|member(X16,X13))))&(((~member(skolem0003(X17,X18),X17)|~member(skolem0003(X17,X18),X18))|X17=X18)&((member(skolem0003(X17,X18),X17)|member(skolem0003(X17,X18),X18))|X17=X18))))))))),inference(distribute,[status(thm)],[c31])).
% 0.54/0.72 cnf(c36,plain,member(skolem0003(X107,X108),X107)|member(skolem0003(X107,X108),X108)|X107=X108,inference(split_conjunct,[status(thm)],[c32])).
% 0.54/0.72 cnf(c128,plain,member(skolem0003(X323,X322),X322)|X323=X322|intersect(X323,X323),inference(resolution,[status(thm)],[c36, c98])).
% 0.54/0.72 cnf(c584,plain,X324=empty_set|intersect(X324,X324),inference(resolution,[status(thm)],[c128, c39])).
% 0.54/0.72 cnf(c638,plain,skolem0001=empty_set,inference(resolution,[status(thm)],[c584, c347])).
% 0.54/0.72 cnf(c654,plain,~not_equal(skolem0001,empty_set),inference(resolution,[status(thm)],[c638, c25])).
% 0.54/0.72 cnf(c678,plain,$false,inference(resolution,[status(thm)],[c654, c336])).
% 0.54/0.72 % SZS output end CNFRefutation
% 0.54/0.72
% 0.54/0.72 % Initial clauses : 22
% 0.54/0.72 % Processed clauses : 91
% 0.54/0.72 % Factors computed : 24
% 0.54/0.72 % Resolvents computed: 637
% 0.54/0.72 % Tautologies deleted: 8
% 0.54/0.72 % Forward subsumed : 109
% 0.54/0.72 % Backward subsumed : 9
% 0.54/0.72 % -------- CPU Time ---------
% 0.54/0.72 % User time : 0.336 s
% 0.54/0.72 % System time : 0.017 s
% 0.54/0.72 % Total time : 0.353 s
%------------------------------------------------------------------------------