%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET663+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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 44.14s 44.31s
% Output : Refutation 44.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET663+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 : n012.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 19:41:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 44.14/44.31 % Version: 1.5
% 44.14/44.31 % SZS status Theorem
% 44.14/44.31 % SZS output start CNFRefutation
% 44.14/44.31 fof(prove_relset_1_26,conjecture,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,relation_type(B,C))=>(ilf_type(D,relation_type(empty_set,C))=>D=empty_set))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_relset_1_26)).
% 44.14/44.31 fof(c16,negated_conjecture,(~(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,relation_type(B,C))=>(ilf_type(D,relation_type(empty_set,C))=>D=empty_set)))))))),inference(assume_negation,[status(cth)],[prove_relset_1_26])).
% 44.14/44.31 fof(c17,negated_conjecture,(?[B]:(ilf_type(B,set_type)&(?[C]:(ilf_type(C,set_type)&(?[D]:(ilf_type(D,relation_type(B,C))&(ilf_type(D,relation_type(empty_set,C))&D!=empty_set))))))),inference(fof_nnf,[status(thm)],[c16])).
% 44.14/44.31 fof(c18,negated_conjecture,(?[X2]:(ilf_type(X2,set_type)&(?[X3]:(ilf_type(X3,set_type)&(?[X4]:(ilf_type(X4,relation_type(X2,X3))&(ilf_type(X4,relation_type(empty_set,X3))&X4!=empty_set))))))),inference(variable_rename,[status(thm)],[c17])).
% 44.14/44.31 fof(c19,negated_conjecture,(ilf_type(skolem0001,set_type)&(ilf_type(skolem0002,set_type)&(ilf_type(skolem0003,relation_type(skolem0001,skolem0002))&(ilf_type(skolem0003,relation_type(empty_set,skolem0002))&skolem0003!=empty_set)))),inference(skolemize,[status(esa)],[c18])).
% 44.14/44.31 cnf(c24,negated_conjecture,skolem0003!=empty_set,inference(split_conjunct,[status(thm)],[c19])).
% 44.14/44.31 fof(p2,axiom,(![B]:(ilf_type(B,binary_relation_type)=>((domain_of(B)=empty_set|range_of(B)=empty_set)=>B=empty_set))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p2)).
% 44.14/44.31 fof(c183,plain,(![B]:(~ilf_type(B,binary_relation_type)|((domain_of(B)!=empty_set&range_of(B)!=empty_set)|B=empty_set))),inference(fof_nnf,[status(thm)],[p2])).
% 44.14/44.31 fof(c184,plain,(![X78]:(~ilf_type(X78,binary_relation_type)|((domain_of(X78)!=empty_set&range_of(X78)!=empty_set)|X78=empty_set))),inference(variable_rename,[status(thm)],[c183])).
% 44.14/44.31 fof(c185,plain,(![X78]:((~ilf_type(X78,binary_relation_type)|(domain_of(X78)!=empty_set|X78=empty_set))&(~ilf_type(X78,binary_relation_type)|(range_of(X78)!=empty_set|X78=empty_set)))),inference(distribute,[status(thm)],[c184])).
% 44.14/44.31 cnf(c186,plain,~ilf_type(X243,binary_relation_type)|domain_of(X243)!=empty_set|X243=empty_set,inference(split_conjunct,[status(thm)],[c185])).
% 44.14/44.31 fof(p33,axiom,(![B]:ilf_type(B,set_type)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p33)).
% 44.14/44.31 fof(c25,plain,(![X5]:ilf_type(X5,set_type)),inference(variable_rename,[status(thm)],[p33])).
% 44.14/44.31 cnf(c26,plain,ilf_type(X81,set_type),inference(split_conjunct,[status(thm)],[c25])).
% 44.14/44.31 fof(p1,axiom,(![B]:(ilf_type(B,set_type)=>(subset(B,empty_set)=>B=empty_set))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p1)).
% 44.14/44.31 fof(c188,plain,(![B]:(~ilf_type(B,set_type)|(~subset(B,empty_set)|B=empty_set))),inference(fof_nnf,[status(thm)],[p1])).
% 44.14/44.31 fof(c189,plain,(![X79]:(~ilf_type(X79,set_type)|(~subset(X79,empty_set)|X79=empty_set))),inference(variable_rename,[status(thm)],[c188])).
% 44.14/44.31 cnf(c190,plain,~ilf_type(X223,set_type)|~subset(X223,empty_set)|X223=empty_set,inference(split_conjunct,[status(thm)],[c189])).
% 44.14/44.31 cnf(c23,negated_conjecture,ilf_type(skolem0003,relation_type(empty_set,skolem0002)),inference(split_conjunct,[status(thm)],[c19])).
% 44.14/44.31 fof(p3,axiom,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,relation_type(B,C))=>(subset(domain_of(D),B)&subset(range_of(D),C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p3)).
% 44.14/44.31 fof(c177,plain,(![B]:(~ilf_type(B,set_type)|(![C]:(~ilf_type(C,set_type)|(![D]:(~ilf_type(D,relation_type(B,C))|(subset(domain_of(D),B)&subset(range_of(D),C)))))))),inference(fof_nnf,[status(thm)],[p3])).
% 44.14/44.31 fof(c179,plain,(![X75]:(![X76]:(![X77]:(~ilf_type(X75,set_type)|(~ilf_type(X76,set_type)|(~ilf_type(X77,relation_type(X75,X76))|(subset(domain_of(X77),X75)&subset(range_of(X77),X76)))))))),inference(shift_quantors,[status(thm)],[fof(c178,plain,(![X75]:(~ilf_type(X75,set_type)|(![X76]:(~ilf_type(X76,set_type)|(![X77]:(~ilf_type(X77,relation_type(X75,X76))|(subset(domain_of(X77),X75)&subset(range_of(X77),X76)))))))),inference(variable_rename,[status(thm)],[c177])).])).
% 44.14/44.31 fof(c180,plain,(![X75]:(![X76]:(![X77]:((~ilf_type(X75,set_type)|(~ilf_type(X76,set_type)|(~ilf_type(X77,relation_type(X75,X76))|subset(domain_of(X77),X75))))&(~ilf_type(X75,set_type)|(~ilf_type(X76,set_type)|(~ilf_type(X77,relation_type(X75,X76))|subset(range_of(X77),X76)))))))),inference(distribute,[status(thm)],[c179])).
% 44.14/44.31 cnf(c181,plain,~ilf_type(X469,set_type)|~ilf_type(X467,set_type)|~ilf_type(X468,relation_type(X469,X467))|subset(domain_of(X468),X469),inference(split_conjunct,[status(thm)],[c180])).
% 44.14/44.31 cnf(c663,plain,~ilf_type(empty_set,set_type)|~ilf_type(skolem0002,set_type)|subset(domain_of(skolem0003),empty_set),inference(resolution,[status(thm)],[c181, c23])).
% 44.14/44.31 cnf(c22989,plain,~ilf_type(empty_set,set_type)|subset(domain_of(skolem0003),empty_set),inference(resolution,[status(thm)],[c663, c26])).
% 44.14/44.31 cnf(c22990,plain,subset(domain_of(skolem0003),empty_set),inference(resolution,[status(thm)],[c22989, c26])).
% 44.14/44.31 cnf(c22991,plain,~ilf_type(domain_of(skolem0003),set_type)|domain_of(skolem0003)=empty_set,inference(resolution,[status(thm)],[c22990, c190])).
% 44.14/44.31 cnf(c22993,plain,domain_of(skolem0003)=empty_set,inference(resolution,[status(thm)],[c22991, c26])).
% 44.14/44.31 cnf(c23073,plain,~ilf_type(skolem0003,binary_relation_type)|skolem0003=empty_set,inference(resolution,[status(thm)],[c22993, c186])).
% 44.14/44.31 fof(p13,axiom,(![B]:(ilf_type(B,set_type)=>(ilf_type(B,binary_relation_type)<=>(relation_like(B)&ilf_type(B,set_type))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p13)).
% 44.14/44.31 fof(c129,plain,(![B]:(~ilf_type(B,set_type)|((~ilf_type(B,binary_relation_type)|(relation_like(B)&ilf_type(B,set_type)))&((~relation_like(B)|~ilf_type(B,set_type))|ilf_type(B,binary_relation_type))))),inference(fof_nnf,[status(thm)],[p13])).
% 44.14/44.31 fof(c130,plain,(![X54]:(~ilf_type(X54,set_type)|((~ilf_type(X54,binary_relation_type)|(relation_like(X54)&ilf_type(X54,set_type)))&((~relation_like(X54)|~ilf_type(X54,set_type))|ilf_type(X54,binary_relation_type))))),inference(variable_rename,[status(thm)],[c129])).
% 44.14/44.31 fof(c131,plain,(![X54]:(((~ilf_type(X54,set_type)|(~ilf_type(X54,binary_relation_type)|relation_like(X54)))&(~ilf_type(X54,set_type)|(~ilf_type(X54,binary_relation_type)|ilf_type(X54,set_type))))&(~ilf_type(X54,set_type)|((~relation_like(X54)|~ilf_type(X54,set_type))|ilf_type(X54,binary_relation_type))))),inference(distribute,[status(thm)],[c130])).
% 44.14/44.31 cnf(c134,plain,~ilf_type(X274,set_type)|~relation_like(X274)|~ilf_type(X274,set_type)|ilf_type(X274,binary_relation_type),inference(split_conjunct,[status(thm)],[c131])).
% 44.14/44.31 cnf(c283,plain,~ilf_type(X275,set_type)|~relation_like(X275)|ilf_type(X275,binary_relation_type),inference(factor,[status(thm)],[c134])).
% 44.14/44.31 cnf(c285,plain,~relation_like(X278)|ilf_type(X278,binary_relation_type),inference(resolution,[status(thm)],[c283, c26])).
% 44.14/44.31 fof(p28,axiom,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,subset_type(cross_product(B,C)))=>relation_like(D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p28)).
% 44.14/44.31 fof(c43,plain,(![B]:(~ilf_type(B,set_type)|(![C]:(~ilf_type(C,set_type)|(![D]:(~ilf_type(D,subset_type(cross_product(B,C)))|relation_like(D))))))),inference(fof_nnf,[status(thm)],[p28])).
% 44.14/44.31 fof(c45,plain,(![X18]:(![X19]:(![X20]:(~ilf_type(X18,set_type)|(~ilf_type(X19,set_type)|(~ilf_type(X20,subset_type(cross_product(X18,X19)))|relation_like(X20))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,(![X18]:(~ilf_type(X18,set_type)|(![X19]:(~ilf_type(X19,set_type)|(![X20]:(~ilf_type(X20,subset_type(cross_product(X18,X19)))|relation_like(X20))))))),inference(variable_rename,[status(thm)],[c43])).])).
% 44.14/44.31 cnf(c46,plain,~ilf_type(X245,set_type)|~ilf_type(X246,set_type)|~ilf_type(X244,subset_type(cross_product(X245,X246)))|relation_like(X244),inference(split_conjunct,[status(thm)],[c45])).
% 44.14/44.31 cnf(c22,negated_conjecture,ilf_type(skolem0003,relation_type(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c19])).
% 44.14/44.31 fof(p6,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', p6)).
% 44.14/44.31 fof(c165,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)],[p6])).
% 44.14/44.31 fof(c167,plain,(![X70]:(![X71]:(![X72]:(![X73]:(~ilf_type(X70,set_type)|(~ilf_type(X71,set_type)|((~ilf_type(X72,subset_type(cross_product(X70,X71)))|ilf_type(X72,relation_type(X70,X71)))&(~ilf_type(X73,relation_type(X70,X71))|ilf_type(X73,subset_type(cross_product(X70,X71))))))))))),inference(shift_quantors,[status(thm)],[fof(c166,plain,(![X70]:(~ilf_type(X70,set_type)|(![X71]:(~ilf_type(X71,set_type)|((![X72]:(~ilf_type(X72,subset_type(cross_product(X70,X71)))|ilf_type(X72,relation_type(X70,X71))))&(![X73]:(~ilf_type(X73,relation_type(X70,X71))|ilf_type(X73,subset_type(cross_product(X70,X71)))))))))),inference(variable_rename,[status(thm)],[c165])).])).
% 44.14/44.31 fof(c168,plain,(![X70]:(![X71]:(![X72]:(![X73]:((~ilf_type(X70,set_type)|(~ilf_type(X71,set_type)|(~ilf_type(X72,subset_type(cross_product(X70,X71)))|ilf_type(X72,relation_type(X70,X71)))))&(~ilf_type(X70,set_type)|(~ilf_type(X71,set_type)|(~ilf_type(X73,relation_type(X70,X71))|ilf_type(X73,subset_type(cross_product(X70,X71))))))))))),inference(distribute,[status(thm)],[c167])).
% 44.14/44.31 cnf(c170,plain,~ilf_type(X465,set_type)|~ilf_type(X464,set_type)|~ilf_type(X466,relation_type(X465,X464))|ilf_type(X466,subset_type(cross_product(X465,X464))),inference(split_conjunct,[status(thm)],[c168])).
% 44.14/44.31 cnf(c652,plain,~ilf_type(skolem0001,set_type)|~ilf_type(skolem0002,set_type)|ilf_type(skolem0003,subset_type(cross_product(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c170, c22])).
% 44.14/44.31 cnf(c22663,plain,~ilf_type(skolem0001,set_type)|ilf_type(skolem0003,subset_type(cross_product(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c652, c26])).
% 44.14/44.31 cnf(c72003,plain,ilf_type(skolem0003,subset_type(cross_product(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c22663, c26])).
% 44.14/44.31 cnf(c72007,plain,~ilf_type(skolem0001,set_type)|~ilf_type(skolem0002,set_type)|relation_like(skolem0003),inference(resolution,[status(thm)],[c72003, c46])).
% 44.14/44.31 cnf(c72179,plain,~ilf_type(skolem0001,set_type)|relation_like(skolem0003),inference(resolution,[status(thm)],[c72007, c26])).
% 44.14/44.31 cnf(c72180,plain,relation_like(skolem0003),inference(resolution,[status(thm)],[c72179, c26])).
% 44.14/44.31 cnf(c72181,plain,ilf_type(skolem0003,binary_relation_type),inference(resolution,[status(thm)],[c72180, c285])).
% 44.14/44.31 cnf(c72192,plain,skolem0003=empty_set,inference(resolution,[status(thm)],[c72181, c23073])).
% 44.14/44.31 cnf(c72300,plain,$false,inference(resolution,[status(thm)],[c72192, c24])).
% 44.14/44.31 % SZS output end CNFRefutation
% 44.14/44.31
% 44.14/44.31 % Initial clauses : 84
% 44.14/44.31 % Processed clauses : 1670
% 44.14/44.31 % Factors computed : 107
% 44.14/44.31 % Resolvents computed: 72239
% 44.14/44.31 % Tautologies deleted: 13
% 44.14/44.31 % Forward subsumed : 1347
% 44.14/44.31 % Backward subsumed : 212
% 44.14/44.31 % -------- CPU Time ---------
% 44.14/44.31 % User time : 43.771 s
% 44.14/44.31 % System time : 0.195 s
% 44.14/44.31 % Total time : 43.966 s
%------------------------------------------------------------------------------