%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET664+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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 43.92s 44.09s
% Output : Refutation 43.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SET664+3 : TPTP v8.1.2. Released v2.2.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 18:53:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 43.92/44.09 % Version: 1.5
% 43.92/44.09 % SZS status Theorem
% 43.92/44.09 % SZS output start CNFRefutation
% 43.92/44.09 fof(prove_relset_1_27,conjecture,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,relation_type(C,B))=>(ilf_type(D,relation_type(C,empty_set))=>D=empty_set))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_relset_1_27)).
% 43.92/44.09 fof(c16,negated_conjecture,(~(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,relation_type(C,B))=>(ilf_type(D,relation_type(C,empty_set))=>D=empty_set)))))))),inference(assume_negation,[status(cth)],[prove_relset_1_27])).
% 43.92/44.09 fof(c17,negated_conjecture,(?[B]:(ilf_type(B,set_type)&(?[C]:(ilf_type(C,set_type)&(?[D]:(ilf_type(D,relation_type(C,B))&(ilf_type(D,relation_type(C,empty_set))&D!=empty_set))))))),inference(fof_nnf,[status(thm)],[c16])).
% 43.92/44.09 fof(c18,negated_conjecture,(?[X2]:(ilf_type(X2,set_type)&(?[X3]:(ilf_type(X3,set_type)&(?[X4]:(ilf_type(X4,relation_type(X3,X2))&(ilf_type(X4,relation_type(X3,empty_set))&X4!=empty_set))))))),inference(variable_rename,[status(thm)],[c17])).
% 43.92/44.09 fof(c19,negated_conjecture,(ilf_type(skolem0001,set_type)&(ilf_type(skolem0002,set_type)&(ilf_type(skolem0003,relation_type(skolem0002,skolem0001))&(ilf_type(skolem0003,relation_type(skolem0002,empty_set))&skolem0003!=empty_set)))),inference(skolemize,[status(esa)],[c18])).
% 43.92/44.09 cnf(c24,negated_conjecture,skolem0003!=empty_set,inference(split_conjunct,[status(thm)],[c19])).
% 43.92/44.09 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)).
% 43.92/44.09 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])).
% 43.92/44.09 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])).
% 43.92/44.09 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])).
% 43.92/44.09 cnf(c187,plain,~ilf_type(X247,binary_relation_type)|range_of(X247)!=empty_set|X247=empty_set,inference(split_conjunct,[status(thm)],[c185])).
% 43.92/44.09 fof(p33,axiom,(![B]:ilf_type(B,set_type)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p33)).
% 43.92/44.09 fof(c25,plain,(![X5]:ilf_type(X5,set_type)),inference(variable_rename,[status(thm)],[p33])).
% 43.92/44.09 cnf(c26,plain,ilf_type(X81,set_type),inference(split_conjunct,[status(thm)],[c25])).
% 43.92/44.09 fof(p1,axiom,(![B]:(ilf_type(B,set_type)=>(subset(B,empty_set)=>B=empty_set))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p1)).
% 43.92/44.09 fof(c188,plain,(![B]:(~ilf_type(B,set_type)|(~subset(B,empty_set)|B=empty_set))),inference(fof_nnf,[status(thm)],[p1])).
% 43.92/44.09 fof(c189,plain,(![X79]:(~ilf_type(X79,set_type)|(~subset(X79,empty_set)|X79=empty_set))),inference(variable_rename,[status(thm)],[c188])).
% 43.92/44.09 cnf(c190,plain,~ilf_type(X223,set_type)|~subset(X223,empty_set)|X223=empty_set,inference(split_conjunct,[status(thm)],[c189])).
% 43.92/44.09 cnf(c23,negated_conjecture,ilf_type(skolem0003,relation_type(skolem0002,empty_set)),inference(split_conjunct,[status(thm)],[c19])).
% 43.92/44.09 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)).
% 43.92/44.09 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])).
% 43.92/44.09 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])).])).
% 43.92/44.09 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])).
% 43.92/44.09 cnf(c182,plain,~ilf_type(X471,set_type)|~ilf_type(X473,set_type)|~ilf_type(X472,relation_type(X471,X473))|subset(range_of(X472),X473),inference(split_conjunct,[status(thm)],[c180])).
% 43.92/44.09 cnf(c664,plain,~ilf_type(skolem0002,set_type)|~ilf_type(empty_set,set_type)|subset(range_of(skolem0003),empty_set),inference(resolution,[status(thm)],[c182, c23])).
% 43.92/44.09 cnf(c23106,plain,~ilf_type(skolem0002,set_type)|subset(range_of(skolem0003),empty_set),inference(resolution,[status(thm)],[c664, c26])).
% 43.92/44.09 cnf(c23107,plain,subset(range_of(skolem0003),empty_set),inference(resolution,[status(thm)],[c23106, c26])).
% 43.92/44.09 cnf(c23108,plain,~ilf_type(range_of(skolem0003),set_type)|range_of(skolem0003)=empty_set,inference(resolution,[status(thm)],[c23107, c190])).
% 43.92/44.09 cnf(c23110,plain,range_of(skolem0003)=empty_set,inference(resolution,[status(thm)],[c23108, c26])).
% 43.92/44.09 cnf(c23145,plain,~ilf_type(skolem0003,binary_relation_type)|skolem0003=empty_set,inference(resolution,[status(thm)],[c23110, c187])).
% 43.92/44.09 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)).
% 43.92/44.09 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])).
% 43.92/44.09 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])).
% 43.92/44.09 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])).
% 43.92/44.09 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])).
% 43.92/44.09 cnf(c283,plain,~ilf_type(X275,set_type)|~relation_like(X275)|ilf_type(X275,binary_relation_type),inference(factor,[status(thm)],[c134])).
% 43.92/44.09 cnf(c285,plain,~relation_like(X278)|ilf_type(X278,binary_relation_type),inference(resolution,[status(thm)],[c283, c26])).
% 43.92/44.09 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)).
% 43.92/44.09 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])).
% 43.92/44.09 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])).])).
% 43.92/44.09 cnf(c46,plain,~ilf_type(X246,set_type)|~ilf_type(X245,set_type)|~ilf_type(X244,subset_type(cross_product(X246,X245)))|relation_like(X244),inference(split_conjunct,[status(thm)],[c45])).
% 43.92/44.09 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)).
% 43.92/44.09 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])).
% 43.92/44.09 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])).])).
% 43.92/44.09 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])).
% 43.92/44.09 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])).
% 43.92/44.09 cnf(c652,plain,~ilf_type(skolem0002,set_type)|~ilf_type(empty_set,set_type)|ilf_type(skolem0003,subset_type(cross_product(skolem0002,empty_set))),inference(resolution,[status(thm)],[c170, c23])).
% 43.92/44.09 cnf(c22519,plain,~ilf_type(skolem0002,set_type)|ilf_type(skolem0003,subset_type(cross_product(skolem0002,empty_set))),inference(resolution,[status(thm)],[c652, c26])).
% 43.92/44.09 cnf(c72613,plain,ilf_type(skolem0003,subset_type(cross_product(skolem0002,empty_set))),inference(resolution,[status(thm)],[c22519, c26])).
% 43.92/44.09 cnf(c72617,plain,~ilf_type(skolem0002,set_type)|~ilf_type(empty_set,set_type)|relation_like(skolem0003),inference(resolution,[status(thm)],[c72613, c46])).
% 43.92/44.09 cnf(c72618,plain,~ilf_type(skolem0002,set_type)|relation_like(skolem0003),inference(resolution,[status(thm)],[c72617, c26])).
% 43.92/44.09 cnf(c72619,plain,relation_like(skolem0003),inference(resolution,[status(thm)],[c72618, c26])).
% 43.92/44.09 cnf(c72687,plain,ilf_type(skolem0003,binary_relation_type),inference(resolution,[status(thm)],[c72619, c285])).
% 43.92/44.09 cnf(c72696,plain,skolem0003=empty_set,inference(resolution,[status(thm)],[c72687, c23145])).
% 43.92/44.09 cnf(c72749,plain,$false,inference(resolution,[status(thm)],[c72696, c24])).
% 43.92/44.09 % SZS output end CNFRefutation
% 43.92/44.09
% 43.92/44.09 % Initial clauses : 84
% 43.92/44.09 % Processed clauses : 1661
% 43.92/44.09 % Factors computed : 105
% 43.92/44.09 % Resolvents computed: 72577
% 43.92/44.09 % Tautologies deleted: 13
% 43.92/44.09 % Forward subsumed : 1347
% 43.92/44.09 % Backward subsumed : 204
% 43.92/44.09 % -------- CPU Time ---------
% 43.92/44.09 % User time : 43.545 s
% 43.92/44.09 % System time : 0.178 s
% 43.92/44.09 % Total time : 43.724 s
%------------------------------------------------------------------------------