%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET643+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:54 EDT 2024
% Result : Theorem 0.73s 0.91s
% Output : Refutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SET643+3 : TPTP v8.1.2. Released v2.2.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 18:38:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.73/0.91 % Version: 1.5
% 0.73/0.91 % SZS status Theorem
% 0.73/0.91 % SZS output start CNFRefutation
% 0.73/0.91 fof(prove_relset_1_5,conjecture,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>ilf_type(cross_product(B,C),relation_type(B,C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_relset_1_5)).
% 0.73/0.91 fof(c11,negated_conjecture,(~(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>ilf_type(cross_product(B,C),relation_type(B,C))))))),inference(assume_negation,[status(cth)],[prove_relset_1_5])).
% 0.73/0.91 fof(c12,negated_conjecture,(?[B]:(ilf_type(B,set_type)&(?[C]:(ilf_type(C,set_type)&~ilf_type(cross_product(B,C),relation_type(B,C)))))),inference(fof_nnf,[status(thm)],[c11])).
% 0.73/0.91 fof(c13,negated_conjecture,(?[X2]:(ilf_type(X2,set_type)&(?[X3]:(ilf_type(X3,set_type)&~ilf_type(cross_product(X2,X3),relation_type(X2,X3)))))),inference(variable_rename,[status(thm)],[c12])).
% 0.73/0.91 fof(c14,negated_conjecture,(ilf_type(skolem0001,set_type)&(ilf_type(skolem0002,set_type)&~ilf_type(cross_product(skolem0001,skolem0002),relation_type(skolem0001,skolem0002)))),inference(skolemize,[status(esa)],[c13])).
% 0.73/0.91 cnf(c17,negated_conjecture,~ilf_type(cross_product(skolem0001,skolem0002),relation_type(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c14])).
% 0.73/0.91 fof(p19,axiom,(![B]:ilf_type(B,set_type)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p19)).
% 0.73/0.91 fof(c18,plain,(![X4]:ilf_type(X4,set_type)),inference(variable_rename,[status(thm)],[p19])).
% 0.73/0.91 cnf(c19,plain,ilf_type(X59,set_type),inference(split_conjunct,[status(thm)],[c18])).
% 0.73/0.91 fof(p4,axiom,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>((![D]:(ilf_type(D,subset_type(cross_product(B,C)))=>ilf_type(D,relation_type(B,C))))&(![E]:(ilf_type(E,relation_type(B,C))=>ilf_type(E,subset_type(cross_product(B,C)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p4)).
% 0.73/0.91 fof(c105,plain,(![B]:(~ilf_type(B,set_type)|(![C]:(~ilf_type(C,set_type)|((![D]:(~ilf_type(D,subset_type(cross_product(B,C)))|ilf_type(D,relation_type(B,C))))&(![E]:(~ilf_type(E,relation_type(B,C))|ilf_type(E,subset_type(cross_product(B,C)))))))))),inference(fof_nnf,[status(thm)],[p4])).
% 0.73/0.91 fof(c107,plain,(![X42]:(![X43]:(![X44]:(![X45]:(~ilf_type(X42,set_type)|(~ilf_type(X43,set_type)|((~ilf_type(X44,subset_type(cross_product(X42,X43)))|ilf_type(X44,relation_type(X42,X43)))&(~ilf_type(X45,relation_type(X42,X43))|ilf_type(X45,subset_type(cross_product(X42,X43))))))))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,(![X42]:(~ilf_type(X42,set_type)|(![X43]:(~ilf_type(X43,set_type)|((![X44]:(~ilf_type(X44,subset_type(cross_product(X42,X43)))|ilf_type(X44,relation_type(X42,X43))))&(![X45]:(~ilf_type(X45,relation_type(X42,X43))|ilf_type(X45,subset_type(cross_product(X42,X43)))))))))),inference(variable_rename,[status(thm)],[c105])).])).
% 0.73/0.91 fof(c108,plain,(![X42]:(![X43]:(![X44]:(![X45]:((~ilf_type(X42,set_type)|(~ilf_type(X43,set_type)|(~ilf_type(X44,subset_type(cross_product(X42,X43)))|ilf_type(X44,relation_type(X42,X43)))))&(~ilf_type(X42,set_type)|(~ilf_type(X43,set_type)|(~ilf_type(X45,relation_type(X42,X43))|ilf_type(X45,subset_type(cross_product(X42,X43))))))))))),inference(distribute,[status(thm)],[c107])).
% 0.73/0.91 cnf(c109,plain,~ilf_type(X328,set_type)|~ilf_type(X327,set_type)|~ilf_type(X329,subset_type(cross_product(X328,X327)))|ilf_type(X329,relation_type(X328,X327)),inference(split_conjunct,[status(thm)],[c108])).
% 0.73/0.91 fof(p7,axiom,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(ilf_type(C,subset_type(B))<=>ilf_type(C,member_type(power_set(B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p7)).
% 0.73/0.91 fof(c90,plain,(![B]:(~ilf_type(B,set_type)|(![C]:(~ilf_type(C,set_type)|((~ilf_type(C,subset_type(B))|ilf_type(C,member_type(power_set(B))))&(~ilf_type(C,member_type(power_set(B)))|ilf_type(C,subset_type(B)))))))),inference(fof_nnf,[status(thm)],[p7])).
% 0.73/0.91 fof(c92,plain,(![X35]:(![X36]:(~ilf_type(X35,set_type)|(~ilf_type(X36,set_type)|((~ilf_type(X36,subset_type(X35))|ilf_type(X36,member_type(power_set(X35))))&(~ilf_type(X36,member_type(power_set(X35)))|ilf_type(X36,subset_type(X35)))))))),inference(shift_quantors,[status(thm)],[fof(c91,plain,(![X35]:(~ilf_type(X35,set_type)|(![X36]:(~ilf_type(X36,set_type)|((~ilf_type(X36,subset_type(X35))|ilf_type(X36,member_type(power_set(X35))))&(~ilf_type(X36,member_type(power_set(X35)))|ilf_type(X36,subset_type(X35)))))))),inference(variable_rename,[status(thm)],[c90])).])).
% 0.73/0.91 fof(c93,plain,(![X35]:(![X36]:((~ilf_type(X35,set_type)|(~ilf_type(X36,set_type)|(~ilf_type(X36,subset_type(X35))|ilf_type(X36,member_type(power_set(X35))))))&(~ilf_type(X35,set_type)|(~ilf_type(X36,set_type)|(~ilf_type(X36,member_type(power_set(X35)))|ilf_type(X36,subset_type(X35)))))))),inference(distribute,[status(thm)],[c92])).
% 0.73/0.91 cnf(c95,plain,~ilf_type(X313,set_type)|~ilf_type(X314,set_type)|~ilf_type(X314,member_type(power_set(X313)))|ilf_type(X314,subset_type(X313)),inference(split_conjunct,[status(thm)],[c93])).
% 0.73/0.91 fof(p12,axiom,(![B]:(ilf_type(B,set_type)=>((~empty(power_set(B)))&ilf_type(power_set(B),set_type)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p12)).
% 0.73/0.91 fof(c59,plain,(![B]:(ilf_type(B,set_type)=>(~empty(power_set(B))&ilf_type(power_set(B),set_type)))),inference(fof_simplification,[status(thm)],[p12])).
% 0.73/0.91 fof(c60,plain,(![B]:(~ilf_type(B,set_type)|(~empty(power_set(B))&ilf_type(power_set(B),set_type)))),inference(fof_nnf,[status(thm)],[c59])).
% 0.73/0.91 fof(c61,plain,(![X23]:(~ilf_type(X23,set_type)|(~empty(power_set(X23))&ilf_type(power_set(X23),set_type)))),inference(variable_rename,[status(thm)],[c60])).
% 0.73/0.91 fof(c62,plain,(![X23]:((~ilf_type(X23,set_type)|~empty(power_set(X23)))&(~ilf_type(X23,set_type)|ilf_type(power_set(X23),set_type)))),inference(distribute,[status(thm)],[c61])).
% 0.73/0.91 cnf(c63,plain,~ilf_type(X81,set_type)|~empty(power_set(X81)),inference(split_conjunct,[status(thm)],[c62])).
% 0.73/0.91 fof(p15,axiom,(![B]:(ilf_type(B,set_type)=>(empty(B)<=>(![C]:(ilf_type(C,set_type)=>(~member(C,B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p15)).
% 0.73/0.91 fof(c38,plain,(![B]:(ilf_type(B,set_type)=>(empty(B)<=>(![C]:(ilf_type(C,set_type)=>~member(C,B)))))),inference(fof_simplification,[status(thm)],[p15])).
% 0.73/0.91 fof(c39,plain,(![B]:(~ilf_type(B,set_type)|((~empty(B)|(![C]:(~ilf_type(C,set_type)|~member(C,B))))&((?[C]:(ilf_type(C,set_type)&member(C,B)))|empty(B))))),inference(fof_nnf,[status(thm)],[c38])).
% 0.73/0.91 fof(c40,plain,(![X16]:(~ilf_type(X16,set_type)|((~empty(X16)|(![X17]:(~ilf_type(X17,set_type)|~member(X17,X16))))&((?[X18]:(ilf_type(X18,set_type)&member(X18,X16)))|empty(X16))))),inference(variable_rename,[status(thm)],[c39])).
% 0.73/0.91 fof(c42,plain,(![X16]:(![X17]:(~ilf_type(X16,set_type)|((~empty(X16)|(~ilf_type(X17,set_type)|~member(X17,X16)))&((ilf_type(skolem0006(X16),set_type)&member(skolem0006(X16),X16))|empty(X16)))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,(![X16]:(~ilf_type(X16,set_type)|((~empty(X16)|(![X17]:(~ilf_type(X17,set_type)|~member(X17,X16))))&((ilf_type(skolem0006(X16),set_type)&member(skolem0006(X16),X16))|empty(X16))))),inference(skolemize,[status(esa)],[c40])).])).
% 0.73/0.91 fof(c43,plain,(![X16]:(![X17]:((~ilf_type(X16,set_type)|(~empty(X16)|(~ilf_type(X17,set_type)|~member(X17,X16))))&((~ilf_type(X16,set_type)|(ilf_type(skolem0006(X16),set_type)|empty(X16)))&(~ilf_type(X16,set_type)|(member(skolem0006(X16),X16)|empty(X16))))))),inference(distribute,[status(thm)],[c42])).
% 0.73/0.91 cnf(c46,plain,~ilf_type(X132,set_type)|member(skolem0006(X132),X132)|empty(X132),inference(split_conjunct,[status(thm)],[c43])).
% 0.73/0.91 cnf(c158,plain,member(skolem0006(X133),X133)|empty(X133),inference(resolution,[status(thm)],[c46, c19])).
% 0.73/0.91 cnf(c160,plain,member(skolem0006(power_set(X168)),power_set(X168))|~ilf_type(X168,set_type),inference(resolution,[status(thm)],[c158, c63])).
% 0.73/0.91 cnf(c170,plain,member(skolem0006(power_set(X171)),power_set(X171)),inference(resolution,[status(thm)],[c160, c19])).
% 0.73/0.91 cnf(c44,plain,~ilf_type(X185,set_type)|~empty(X185)|~ilf_type(X184,set_type)|~member(X184,X185),inference(split_conjunct,[status(thm)],[c43])).
% 0.73/0.91 cnf(c185,plain,~ilf_type(power_set(X408),set_type)|~empty(power_set(X408))|~ilf_type(skolem0006(power_set(X408)),set_type),inference(resolution,[status(thm)],[c44, c170])).
% 0.73/0.91 cnf(c331,plain,~ilf_type(power_set(X409),set_type)|~empty(power_set(X409)),inference(resolution,[status(thm)],[c185, c19])).
% 0.73/0.91 cnf(c332,plain,~empty(power_set(X410)),inference(resolution,[status(thm)],[c331, c19])).
% 0.73/0.91 fof(p13,axiom,(![B]:(ilf_type(B,set_type)=>(![C]:(((~empty(C))&ilf_type(C,set_type))=>(ilf_type(B,member_type(C))<=>member(B,C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p13)).
% 0.73/0.91 fof(c52,plain,(![B]:(ilf_type(B,set_type)=>(![C]:((~empty(C)&ilf_type(C,set_type))=>(ilf_type(B,member_type(C))<=>member(B,C)))))),inference(fof_simplification,[status(thm)],[p13])).
% 0.73/0.91 fof(c53,plain,(![B]:(~ilf_type(B,set_type)|(![C]:((empty(C)|~ilf_type(C,set_type))|((~ilf_type(B,member_type(C))|member(B,C))&(~member(B,C)|ilf_type(B,member_type(C)))))))),inference(fof_nnf,[status(thm)],[c52])).
% 0.73/0.91 fof(c55,plain,(![X21]:(![X22]:(~ilf_type(X21,set_type)|((empty(X22)|~ilf_type(X22,set_type))|((~ilf_type(X21,member_type(X22))|member(X21,X22))&(~member(X21,X22)|ilf_type(X21,member_type(X22)))))))),inference(shift_quantors,[status(thm)],[fof(c54,plain,(![X21]:(~ilf_type(X21,set_type)|(![X22]:((empty(X22)|~ilf_type(X22,set_type))|((~ilf_type(X21,member_type(X22))|member(X21,X22))&(~member(X21,X22)|ilf_type(X21,member_type(X22)))))))),inference(variable_rename,[status(thm)],[c53])).])).
% 0.73/0.91 fof(c56,plain,(![X21]:(![X22]:((~ilf_type(X21,set_type)|((empty(X22)|~ilf_type(X22,set_type))|(~ilf_type(X21,member_type(X22))|member(X21,X22))))&(~ilf_type(X21,set_type)|((empty(X22)|~ilf_type(X22,set_type))|(~member(X21,X22)|ilf_type(X21,member_type(X22)))))))),inference(distribute,[status(thm)],[c55])).
% 0.73/0.91 cnf(c58,plain,~ilf_type(X203,set_type)|empty(X204)|~ilf_type(X204,set_type)|~member(X203,X204)|ilf_type(X203,member_type(X204)),inference(split_conjunct,[status(thm)],[c56])).
% 0.73/0.91 fof(p11,axiom,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(member(B,power_set(C))<=>(![D]:(ilf_type(D,set_type)=>(member(D,B)=>member(D,C))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p11)).
% 0.73/0.91 fof(c65,plain,(![B]:(~ilf_type(B,set_type)|(![C]:(~ilf_type(C,set_type)|((~member(B,power_set(C))|(![D]:(~ilf_type(D,set_type)|(~member(D,B)|member(D,C)))))&((?[D]:(ilf_type(D,set_type)&(member(D,B)&~member(D,C))))|member(B,power_set(C)))))))),inference(fof_nnf,[status(thm)],[p11])).
% 0.73/0.91 fof(c66,plain,(![X24]:(~ilf_type(X24,set_type)|(![X25]:(~ilf_type(X25,set_type)|((~member(X24,power_set(X25))|(![X26]:(~ilf_type(X26,set_type)|(~member(X26,X24)|member(X26,X25)))))&((?[X27]:(ilf_type(X27,set_type)&(member(X27,X24)&~member(X27,X25))))|member(X24,power_set(X25)))))))),inference(variable_rename,[status(thm)],[c65])).
% 0.73/0.91 fof(c68,plain,(![X24]:(![X25]:(![X26]:(~ilf_type(X24,set_type)|(~ilf_type(X25,set_type)|((~member(X24,power_set(X25))|(~ilf_type(X26,set_type)|(~member(X26,X24)|member(X26,X25))))&((ilf_type(skolem0008(X24,X25),set_type)&(member(skolem0008(X24,X25),X24)&~member(skolem0008(X24,X25),X25)))|member(X24,power_set(X25))))))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,(![X24]:(~ilf_type(X24,set_type)|(![X25]:(~ilf_type(X25,set_type)|((~member(X24,power_set(X25))|(![X26]:(~ilf_type(X26,set_type)|(~member(X26,X24)|member(X26,X25)))))&((ilf_type(skolem0008(X24,X25),set_type)&(member(skolem0008(X24,X25),X24)&~member(skolem0008(X24,X25),X25)))|member(X24,power_set(X25)))))))),inference(skolemize,[status(esa)],[c66])).])).
% 0.73/0.91 fof(c69,plain,(![X24]:(![X25]:(![X26]:((~ilf_type(X24,set_type)|(~ilf_type(X25,set_type)|(~member(X24,power_set(X25))|(~ilf_type(X26,set_type)|(~member(X26,X24)|member(X26,X25))))))&((~ilf_type(X24,set_type)|(~ilf_type(X25,set_type)|(ilf_type(skolem0008(X24,X25),set_type)|member(X24,power_set(X25)))))&((~ilf_type(X24,set_type)|(~ilf_type(X25,set_type)|(member(skolem0008(X24,X25),X24)|member(X24,power_set(X25)))))&(~ilf_type(X24,set_type)|(~ilf_type(X25,set_type)|(~member(skolem0008(X24,X25),X25)|member(X24,power_set(X25))))))))))),inference(distribute,[status(thm)],[c68])).
% 0.73/0.91 cnf(c72,plain,~ilf_type(X235,set_type)|~ilf_type(X234,set_type)|member(skolem0008(X235,X234),X235)|member(X235,power_set(X234)),inference(split_conjunct,[status(thm)],[c69])).
% 0.73/0.91 cnf(c213,plain,~ilf_type(X238,set_type)|member(skolem0008(X238,X238),X238)|member(X238,power_set(X238)),inference(factor,[status(thm)],[c72])).
% 0.73/0.91 cnf(c215,plain,member(skolem0008(X239,X239),X239)|member(X239,power_set(X239)),inference(resolution,[status(thm)],[c213, c19])).
% 0.73/0.91 cnf(c73,plain,~ilf_type(X243,set_type)|~ilf_type(X242,set_type)|~member(skolem0008(X243,X242),X242)|member(X243,power_set(X242)),inference(split_conjunct,[status(thm)],[c69])).
% 0.73/0.91 cnf(c227,plain,~ilf_type(X244,set_type)|member(X244,power_set(X244)),inference(resolution,[status(thm)],[c73, c215])).
% 0.73/0.91 cnf(c228,plain,member(X245,power_set(X245)),inference(resolution,[status(thm)],[c227, c19])).
% 0.73/0.91 cnf(c230,plain,~ilf_type(X702,set_type)|empty(power_set(X702))|~ilf_type(power_set(X702),set_type)|ilf_type(X702,member_type(power_set(X702))),inference(resolution,[status(thm)],[c228, c58])).
% 0.73/0.91 cnf(c605,plain,~ilf_type(X708,set_type)|empty(power_set(X708))|ilf_type(X708,member_type(power_set(X708))),inference(resolution,[status(thm)],[c230, c19])).
% 0.73/0.91 cnf(c607,plain,empty(power_set(X709))|ilf_type(X709,member_type(power_set(X709))),inference(resolution,[status(thm)],[c605, c19])).
% 0.73/0.91 cnf(c610,plain,ilf_type(X711,member_type(power_set(X711))),inference(resolution,[status(thm)],[c607, c332])).
% 0.73/0.91 cnf(c618,plain,~ilf_type(X712,set_type)|ilf_type(X712,subset_type(X712)),inference(resolution,[status(thm)],[c610, c95])).
% 0.73/0.91 cnf(c619,plain,ilf_type(X713,subset_type(X713)),inference(resolution,[status(thm)],[c618, c19])).
% 0.73/0.91 cnf(c621,plain,~ilf_type(X769,set_type)|~ilf_type(X770,set_type)|ilf_type(cross_product(X769,X770),relation_type(X769,X770)),inference(resolution,[status(thm)],[c619, c109])).
% 0.73/0.91 cnf(c654,plain,~ilf_type(X774,set_type)|ilf_type(cross_product(X774,X773),relation_type(X774,X773)),inference(resolution,[status(thm)],[c621, c19])).
% 0.73/0.91 cnf(c658,plain,ilf_type(cross_product(X778,X779),relation_type(X778,X779)),inference(resolution,[status(thm)],[c654, c19])).
% 0.73/0.91 cnf(c680,plain,$false,inference(resolution,[status(thm)],[c658, c17])).
% 0.73/0.91 % SZS output end CNFRefutation
% 0.73/0.91
% 0.73/0.91 % Initial clauses : 58
% 0.73/0.91 % Processed clauses : 251
% 0.73/0.91 % Factors computed : 26
% 0.73/0.91 % Resolvents computed: 525
% 0.73/0.91 % Tautologies deleted: 10
% 0.73/0.91 % Forward subsumed : 118
% 0.73/0.91 % Backward subsumed : 80
% 0.73/0.91 % -------- CPU Time ---------
% 0.73/0.91 % User time : 0.543 s
% 0.73/0.91 % System time : 0.013 s
% 0.73/0.91 % Total time : 0.556 s
%------------------------------------------------------------------------------