%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET662+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:56 EDT 2024
% Result : Theorem 0.83s 1.05s
% Output : Refutation 0.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET662+3 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n024.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 18:37:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.83/1.05 % Version: 1.5
% 0.83/1.05 % SZS status Theorem
% 0.83/1.05 % SZS output start CNFRefutation
% 0.83/1.05 fof(prove_relset_1_25,conjecture,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>ilf_type(empty_set,relation_type(B,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_relset_1_25)).
% 0.83/1.05 fof(c12,negated_conjecture,(~(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>ilf_type(empty_set,relation_type(B,C))))))),inference(assume_negation,[status(cth)],[prove_relset_1_25])).
% 0.83/1.05 fof(c13,negated_conjecture,(?[B]:(ilf_type(B,set_type)&(?[C]:(ilf_type(C,set_type)&~ilf_type(empty_set,relation_type(B,C)))))),inference(fof_nnf,[status(thm)],[c12])).
% 0.83/1.05 fof(c14,negated_conjecture,(?[X2]:(ilf_type(X2,set_type)&(?[X3]:(ilf_type(X3,set_type)&~ilf_type(empty_set,relation_type(X2,X3)))))),inference(variable_rename,[status(thm)],[c13])).
% 0.83/1.05 fof(c15,negated_conjecture,(ilf_type(skolem0001,set_type)&(ilf_type(skolem0002,set_type)&~ilf_type(empty_set,relation_type(skolem0001,skolem0002)))),inference(skolemize,[status(esa)],[c14])).
% 0.83/1.05 cnf(c18,negated_conjecture,~ilf_type(empty_set,relation_type(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c15])).
% 0.83/1.05 fof(p20,axiom,(![B]:ilf_type(B,set_type)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p20)).
% 0.83/1.05 fof(c19,plain,(![X4]:ilf_type(X4,set_type)),inference(variable_rename,[status(thm)],[p20])).
% 0.83/1.05 cnf(c20,plain,ilf_type(X52,set_type),inference(split_conjunct,[status(thm)],[c19])).
% 0.83/1.05 fof(p2,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/sandbox/benchmark/theBenchmark.p', p2)).
% 0.83/1.05 fof(c116,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)],[p2])).
% 0.83/1.05 fof(c118,plain,(![X45]:(![X46]:(![X47]:(![X48]:(~ilf_type(X45,set_type)|(~ilf_type(X46,set_type)|((~ilf_type(X47,subset_type(cross_product(X45,X46)))|ilf_type(X47,relation_type(X45,X46)))&(~ilf_type(X48,relation_type(X45,X46))|ilf_type(X48,subset_type(cross_product(X45,X46))))))))))),inference(shift_quantors,[status(thm)],[fof(c117,plain,(![X45]:(~ilf_type(X45,set_type)|(![X46]:(~ilf_type(X46,set_type)|((![X47]:(~ilf_type(X47,subset_type(cross_product(X45,X46)))|ilf_type(X47,relation_type(X45,X46))))&(![X48]:(~ilf_type(X48,relation_type(X45,X46))|ilf_type(X48,subset_type(cross_product(X45,X46)))))))))),inference(variable_rename,[status(thm)],[c116])).])).
% 0.83/1.05 fof(c119,plain,(![X45]:(![X46]:(![X47]:(![X48]:((~ilf_type(X45,set_type)|(~ilf_type(X46,set_type)|(~ilf_type(X47,subset_type(cross_product(X45,X46)))|ilf_type(X47,relation_type(X45,X46)))))&(~ilf_type(X45,set_type)|(~ilf_type(X46,set_type)|(~ilf_type(X48,relation_type(X45,X46))|ilf_type(X48,subset_type(cross_product(X45,X46))))))))))),inference(distribute,[status(thm)],[c118])).
% 0.83/1.05 cnf(c120,plain,~ilf_type(X353,set_type)|~ilf_type(X352,set_type)|~ilf_type(X351,subset_type(cross_product(X353,X352)))|ilf_type(X351,relation_type(X353,X352)),inference(split_conjunct,[status(thm)],[c119])).
% 0.83/1.05 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/sandbox/benchmark/theBenchmark.p', p7)).
% 0.83/1.05 fof(c95,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.83/1.05 fof(c97,plain,(![X37]:(![X38]:(~ilf_type(X37,set_type)|(~ilf_type(X38,set_type)|((~ilf_type(X38,subset_type(X37))|ilf_type(X38,member_type(power_set(X37))))&(~ilf_type(X38,member_type(power_set(X37)))|ilf_type(X38,subset_type(X37)))))))),inference(shift_quantors,[status(thm)],[fof(c96,plain,(![X37]:(~ilf_type(X37,set_type)|(![X38]:(~ilf_type(X38,set_type)|((~ilf_type(X38,subset_type(X37))|ilf_type(X38,member_type(power_set(X37))))&(~ilf_type(X38,member_type(power_set(X37)))|ilf_type(X38,subset_type(X37)))))))),inference(variable_rename,[status(thm)],[c95])).])).
% 0.83/1.05 fof(c98,plain,(![X37]:(![X38]:((~ilf_type(X37,set_type)|(~ilf_type(X38,set_type)|(~ilf_type(X38,subset_type(X37))|ilf_type(X38,member_type(power_set(X37))))))&(~ilf_type(X37,set_type)|(~ilf_type(X38,set_type)|(~ilf_type(X38,member_type(power_set(X37)))|ilf_type(X38,subset_type(X37)))))))),inference(distribute,[status(thm)],[c97])).
% 0.83/1.05 cnf(c100,plain,~ilf_type(X327,set_type)|~ilf_type(X326,set_type)|~ilf_type(X326,member_type(power_set(X327)))|ilf_type(X326,subset_type(X327)),inference(split_conjunct,[status(thm)],[c98])).
% 0.83/1.05 fof(p11,axiom,(![B]:(ilf_type(B,set_type)=>(empty(B)<=>(![C]:(ilf_type(C,set_type)=>(~member(C,B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p11)).
% 0.83/1.05 fof(c70,plain,(![B]:(ilf_type(B,set_type)=>(empty(B)<=>(![C]:(ilf_type(C,set_type)=>~member(C,B)))))),inference(fof_simplification,[status(thm)],[p11])).
% 0.83/1.05 fof(c71,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)],[c70])).
% 0.83/1.05 fof(c72,plain,(![X27]:(~ilf_type(X27,set_type)|((~empty(X27)|(![X28]:(~ilf_type(X28,set_type)|~member(X28,X27))))&((?[X29]:(ilf_type(X29,set_type)&member(X29,X27)))|empty(X27))))),inference(variable_rename,[status(thm)],[c71])).
% 0.83/1.05 fof(c74,plain,(![X27]:(![X28]:(~ilf_type(X27,set_type)|((~empty(X27)|(~ilf_type(X28,set_type)|~member(X28,X27)))&((ilf_type(skolem0008(X27),set_type)&member(skolem0008(X27),X27))|empty(X27)))))),inference(shift_quantors,[status(thm)],[fof(c73,plain,(![X27]:(~ilf_type(X27,set_type)|((~empty(X27)|(![X28]:(~ilf_type(X28,set_type)|~member(X28,X27))))&((ilf_type(skolem0008(X27),set_type)&member(skolem0008(X27),X27))|empty(X27))))),inference(skolemize,[status(esa)],[c72])).])).
% 0.83/1.05 fof(c75,plain,(![X27]:(![X28]:((~ilf_type(X27,set_type)|(~empty(X27)|(~ilf_type(X28,set_type)|~member(X28,X27))))&((~ilf_type(X27,set_type)|(ilf_type(skolem0008(X27),set_type)|empty(X27)))&(~ilf_type(X27,set_type)|(member(skolem0008(X27),X27)|empty(X27))))))),inference(distribute,[status(thm)],[c74])).
% 0.83/1.05 cnf(c76,plain,~ilf_type(X183,set_type)|~empty(X183)|~ilf_type(X182,set_type)|~member(X182,X183),inference(split_conjunct,[status(thm)],[c75])).
% 0.83/1.05 fof(p4,axiom,(![B]:(ilf_type(B,set_type)=>(~member(B,empty_set)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p4)).
% 0.83/1.05 fof(c107,plain,(![B]:(ilf_type(B,set_type)=>~member(B,empty_set))),inference(fof_simplification,[status(thm)],[p4])).
% 0.83/1.05 fof(c108,plain,(![B]:(~ilf_type(B,set_type)|~member(B,empty_set))),inference(fof_nnf,[status(thm)],[c107])).
% 0.83/1.05 fof(c109,plain,(![X41]:(~ilf_type(X41,set_type)|~member(X41,empty_set))),inference(variable_rename,[status(thm)],[c108])).
% 0.83/1.05 cnf(c110,plain,~ilf_type(X75,set_type)|~member(X75,empty_set),inference(split_conjunct,[status(thm)],[c109])).
% 0.83/1.05 fof(p12,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/sandbox/benchmark/theBenchmark.p', p12)).
% 0.83/1.05 fof(c61,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)],[p12])).
% 0.83/1.05 fof(c62,plain,(![X23]:(~ilf_type(X23,set_type)|(![X24]:(~ilf_type(X24,set_type)|((~member(X23,power_set(X24))|(![X25]:(~ilf_type(X25,set_type)|(~member(X25,X23)|member(X25,X24)))))&((?[X26]:(ilf_type(X26,set_type)&(member(X26,X23)&~member(X26,X24))))|member(X23,power_set(X24)))))))),inference(variable_rename,[status(thm)],[c61])).
% 0.83/1.05 fof(c64,plain,(![X23]:(![X24]:(![X25]:(~ilf_type(X23,set_type)|(~ilf_type(X24,set_type)|((~member(X23,power_set(X24))|(~ilf_type(X25,set_type)|(~member(X25,X23)|member(X25,X24))))&((ilf_type(skolem0007(X23,X24),set_type)&(member(skolem0007(X23,X24),X23)&~member(skolem0007(X23,X24),X24)))|member(X23,power_set(X24))))))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,(![X23]:(~ilf_type(X23,set_type)|(![X24]:(~ilf_type(X24,set_type)|((~member(X23,power_set(X24))|(![X25]:(~ilf_type(X25,set_type)|(~member(X25,X23)|member(X25,X24)))))&((ilf_type(skolem0007(X23,X24),set_type)&(member(skolem0007(X23,X24),X23)&~member(skolem0007(X23,X24),X24)))|member(X23,power_set(X24)))))))),inference(skolemize,[status(esa)],[c62])).])).
% 0.83/1.05 fof(c65,plain,(![X23]:(![X24]:(![X25]:((~ilf_type(X23,set_type)|(~ilf_type(X24,set_type)|(~member(X23,power_set(X24))|(~ilf_type(X25,set_type)|(~member(X25,X23)|member(X25,X24))))))&((~ilf_type(X23,set_type)|(~ilf_type(X24,set_type)|(ilf_type(skolem0007(X23,X24),set_type)|member(X23,power_set(X24)))))&((~ilf_type(X23,set_type)|(~ilf_type(X24,set_type)|(member(skolem0007(X23,X24),X23)|member(X23,power_set(X24)))))&(~ilf_type(X23,set_type)|(~ilf_type(X24,set_type)|(~member(skolem0007(X23,X24),X24)|member(X23,power_set(X24))))))))))),inference(distribute,[status(thm)],[c64])).
% 0.83/1.05 cnf(c68,plain,~ilf_type(X260,set_type)|~ilf_type(X261,set_type)|member(skolem0007(X260,X261),X260)|member(X260,power_set(X261)),inference(split_conjunct,[status(thm)],[c65])).
% 0.83/1.05 cnf(c227,plain,~ilf_type(X264,set_type)|member(skolem0007(X264,X265),X264)|member(X264,power_set(X265)),inference(resolution,[status(thm)],[c68, c20])).
% 0.83/1.05 cnf(c240,plain,member(skolem0007(X267,X266),X267)|member(X267,power_set(X266)),inference(resolution,[status(thm)],[c227, c20])).
% 0.83/1.05 cnf(c246,plain,member(empty_set,power_set(X268))|~ilf_type(skolem0007(empty_set,X268),set_type),inference(resolution,[status(thm)],[c240, c110])).
% 0.83/1.05 cnf(c252,plain,member(empty_set,power_set(X271)),inference(resolution,[status(thm)],[c246, c20])).
% 0.83/1.05 cnf(c257,plain,~ilf_type(power_set(X292),set_type)|~empty(power_set(X292))|~ilf_type(empty_set,set_type),inference(resolution,[status(thm)],[c252, c76])).
% 0.83/1.05 cnf(c278,plain,~empty(power_set(X293))|~ilf_type(empty_set,set_type),inference(resolution,[status(thm)],[c257, c20])).
% 0.83/1.05 cnf(c279,plain,~empty(power_set(X294)),inference(resolution,[status(thm)],[c278, c20])).
% 0.83/1.05 fof(p14,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/sandbox/benchmark/theBenchmark.p', p14)).
% 0.83/1.05 fof(c48,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)],[p14])).
% 0.83/1.05 fof(c49,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)],[c48])).
% 0.83/1.05 fof(c51,plain,(![X20]:(![X21]:(~ilf_type(X20,set_type)|((empty(X21)|~ilf_type(X21,set_type))|((~ilf_type(X20,member_type(X21))|member(X20,X21))&(~member(X20,X21)|ilf_type(X20,member_type(X21)))))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,(![X20]:(~ilf_type(X20,set_type)|(![X21]:((empty(X21)|~ilf_type(X21,set_type))|((~ilf_type(X20,member_type(X21))|member(X20,X21))&(~member(X20,X21)|ilf_type(X20,member_type(X21)))))))),inference(variable_rename,[status(thm)],[c49])).])).
% 0.83/1.05 fof(c52,plain,(![X20]:(![X21]:((~ilf_type(X20,set_type)|((empty(X21)|~ilf_type(X21,set_type))|(~ilf_type(X20,member_type(X21))|member(X20,X21))))&(~ilf_type(X20,set_type)|((empty(X21)|~ilf_type(X21,set_type))|(~member(X20,X21)|ilf_type(X20,member_type(X21)))))))),inference(distribute,[status(thm)],[c51])).
% 0.83/1.05 cnf(c54,plain,~ilf_type(X227,set_type)|empty(X226)|~ilf_type(X226,set_type)|~member(X227,X226)|ilf_type(X227,member_type(X226)),inference(split_conjunct,[status(thm)],[c52])).
% 0.83/1.05 cnf(c258,plain,~ilf_type(empty_set,set_type)|empty(power_set(X791))|~ilf_type(power_set(X791),set_type)|ilf_type(empty_set,member_type(power_set(X791))),inference(resolution,[status(thm)],[c252, c54])).
% 0.83/1.05 cnf(c645,plain,~ilf_type(empty_set,set_type)|empty(power_set(X792))|ilf_type(empty_set,member_type(power_set(X792))),inference(resolution,[status(thm)],[c258, c20])).
% 0.83/1.05 cnf(c646,plain,empty(power_set(X793))|ilf_type(empty_set,member_type(power_set(X793))),inference(resolution,[status(thm)],[c645, c20])).
% 0.83/1.05 cnf(c647,plain,ilf_type(empty_set,member_type(power_set(X794))),inference(resolution,[status(thm)],[c646, c279])).
% 0.83/1.05 cnf(c654,plain,~ilf_type(X807,set_type)|~ilf_type(empty_set,set_type)|ilf_type(empty_set,subset_type(X807)),inference(resolution,[status(thm)],[c647, c100])).
% 0.83/1.05 cnf(c661,plain,~ilf_type(X809,set_type)|ilf_type(empty_set,subset_type(X809)),inference(resolution,[status(thm)],[c654, c20])).
% 0.83/1.05 cnf(c663,plain,ilf_type(empty_set,subset_type(X810)),inference(resolution,[status(thm)],[c661, c20])).
% 0.83/1.05 cnf(c664,plain,~ilf_type(X864,set_type)|~ilf_type(X863,set_type)|ilf_type(empty_set,relation_type(X864,X863)),inference(resolution,[status(thm)],[c663, c120])).
% 0.83/1.05 cnf(c713,plain,~ilf_type(X869,set_type)|ilf_type(empty_set,relation_type(X869,X870)),inference(resolution,[status(thm)],[c664, c20])).
% 0.83/1.05 cnf(c719,plain,ilf_type(empty_set,relation_type(X871,X872)),inference(resolution,[status(thm)],[c713, c20])).
% 0.83/1.05 cnf(c721,plain,$false,inference(resolution,[status(thm)],[c719, c18])).
% 0.83/1.05 % SZS output end CNFRefutation
% 0.83/1.05
% 0.83/1.05 % Initial clauses : 56
% 0.83/1.05 % Processed clauses : 294
% 0.83/1.05 % Factors computed : 36
% 0.83/1.05 % Resolvents computed: 561
% 0.83/1.05 % Tautologies deleted: 10
% 0.83/1.05 % Forward subsumed : 143
% 0.83/1.05 % Backward subsumed : 96
% 0.83/1.05 % -------- CPU Time ---------
% 0.83/1.05 % User time : 0.684 s
% 0.83/1.05 % System time : 0.015 s
% 0.83/1.05 % Total time : 0.699 s
%------------------------------------------------------------------------------