%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET658+3 : TPTP v9.2.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n025.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 : Tue May 5 05:08:15 PM UTC 2026
% Result : Theorem 0.30s 1.62s
% Output : CNFRefutation 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET658+3 : TPTP v9.2.1. Released v2.2.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n025.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 02:31:13 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.30/1.62 % Version : CSE_E---1.7
% 0.30/1.62 % Problem : theBenchmark.p
% 0.30/1.62 % SZS status Theorem for theBenchmark.p
% 0.30/1.62 % SZS output start CNFRefutation
% 0.30/1.62 fof(p20, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:((~(empty(X2))&ilf_type(X2,set_type))=>(ilf_type(X1,member_type(X2))<=>member(X1,X2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p20)).
% 0.30/1.62 fof(prove_relset_1_20, conjecture, ![X1]:(ilf_type(X1,binary_relation_type)=>ilf_type(X1,relation_type(domain_of(X1),range_of(X1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_relset_1_20)).
% 0.30/1.62 fof(p22, axiom, ![X1]:(ilf_type(X1,set_type)=>(empty(X1)<=>![X2]:(ilf_type(X2,set_type)=>~(member(X2,X1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p22)).
% 0.30/1.62 fof(p21, axiom, ![X1]:((~(empty(X1))&ilf_type(X1,set_type))=>?[X2]:ilf_type(X2,member_type(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p21)).
% 0.30/1.62 fof(p6, axiom, ![X1]:(ilf_type(X1,set_type)=>(ilf_type(X1,binary_relation_type)<=>(relation_like(X1)&ilf_type(X1,set_type)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p6)).
% 0.30/1.62 fof(p19, axiom, ![X1]:(ilf_type(X1,set_type)=>(~(empty(power_set(X1)))&ilf_type(power_set(X1),set_type))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p19)).
% 0.30/1.62 fof(p27, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>ilf_type(range(X1,X2,X3),subset_type(X2))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p27)).
% 0.30/1.62 fof(p25, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>ilf_type(domain(X1,X2,X3),subset_type(X1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p25)).
% 0.30/1.62 fof(p8, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(![X3]:(ilf_type(X3,subset_type(cross_product(X1,X2)))=>ilf_type(X3,relation_type(X1,X2)))&![X4]:(ilf_type(X4,relation_type(X1,X2))=>ilf_type(X4,subset_type(cross_product(X1,X2))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p8)).
% 0.30/1.62 fof(p4, axiom, ![X1]:(ilf_type(X1,binary_relation_type)=>![X2]:(ilf_type(X2,set_type)=>(member(X2,range_of(X1))<=>?[X3]:(ilf_type(X3,set_type)&member(ordered_pair(X3,X2),X1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p4)).
% 0.30/1.62 fof(p2, axiom, ![X1]:(ilf_type(X1,binary_relation_type)=>![X2]:(ilf_type(X2,set_type)=>(member(X2,domain_of(X1))<=>?[X3]:(ilf_type(X3,set_type)&member(ordered_pair(X2,X3),X1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p2)).
% 0.30/1.62 fof(p26, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>range(X1,X2,X3)=range_of(X3)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p26)).
% 0.30/1.62 fof(p24, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>domain(X1,X2,X3)=domain_of(X3)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p24)).
% 0.30/1.62 fof(p17, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,subset_type(cross_product(X1,X2)))=>relation_like(X3)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p17)).
% 0.30/1.62 fof(p16, axiom, ![X1]:(ilf_type(X1,set_type)=>(relation_like(X1)<=>![X2]:(ilf_type(X2,set_type)=>(member(X2,X1)=>?[X3]:(ilf_type(X3,set_type)&?[X4]:(ilf_type(X4,set_type)&X2=ordered_pair(X3,X4))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p16)).
% 0.30/1.62 fof(p18, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(member(X1,power_set(X2))<=>![X3]:(ilf_type(X3,set_type)=>(member(X3,X1)=>member(X3,X2)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p18)).
% 0.30/1.62 fof(p1, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,binary_relation_type)=>(subset(domain_of(X2),X1)=>ilf_type(X2,relation_type(X1,range_of(X2)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p1)).
% 0.30/1.62 fof(p14, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(subset(X1,X2)<=>![X3]:(ilf_type(X3,set_type)=>(member(X3,X1)=>member(X3,X2)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p14)).
% 0.30/1.62 fof(p12, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(ilf_type(X2,subset_type(X1))<=>ilf_type(X2,member_type(power_set(X1)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p12)).
% 0.30/1.62 fof(p9, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>?[X3]:ilf_type(X3,relation_type(X2,X1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p9)).
% 0.30/1.62 fof(p10, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>ilf_type(cross_product(X1,X2),set_type))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p10)).
% 0.30/1.62 fof(p11, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>ilf_type(ordered_pair(X1,X2),set_type))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p11)).
% 0.30/1.62 fof(p13, axiom, ![X1]:(ilf_type(X1,set_type)=>?[X2]:ilf_type(X2,subset_type(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p13)).
% 0.30/1.62 fof(p5, axiom, ![X1]:(ilf_type(X1,binary_relation_type)=>ilf_type(range_of(X1),set_type)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p5)).
% 0.30/1.62 fof(p3, axiom, ![X1]:(ilf_type(X1,binary_relation_type)=>ilf_type(domain_of(X1),set_type)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p3)).
% 0.30/1.62 fof(p15, axiom, ![X1]:(ilf_type(X1,set_type)=>subset(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p15)).
% 0.30/1.62 fof(p23, axiom, ![X1]:((empty(X1)&ilf_type(X1,set_type))=>relation_like(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p23)).
% 0.30/1.62 fof(p28, axiom, ![X1]:ilf_type(X1,set_type), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p28)).
% 0.30/1.62 fof(p7, axiom, ?[X1]:ilf_type(X1,binary_relation_type), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p7)).
% 0.30/1.62 fof(i_0_29, plain, ![X1]:(ilf_type(X1,set_type)=>![X2]:((~empty(X2)&ilf_type(X2,set_type))=>(ilf_type(X1,member_type(X2))<=>member(X1,X2)))), inference(fof_simplification,[status(thm)],[p20])).
% 0.30/1.62 fof(i_0_30, negated_conjecture, ~(![X1]:(ilf_type(X1,binary_relation_type)=>ilf_type(X1,relation_type(domain_of(X1),range_of(X1))))), inference(assume_negation,[status(cth)],[prove_relset_1_20])).
% 0.30/1.62 fof(i_0_31, plain, ![X1]:(ilf_type(X1,set_type)=>(empty(X1)<=>![X2]:(ilf_type(X2,set_type)=>~member(X2,X1)))), inference(fof_simplification,[status(thm)],[p22])).
% 0.30/1.62 fof(i_0_32, plain, ![X1]:((~empty(X1)&ilf_type(X1,set_type))=>?[X2]:ilf_type(X2,member_type(X1))), inference(fof_simplification,[status(thm)],[p21])).
% 0.30/1.62 fof(i_0_33, plain, ![X80]:(((relation_like(X80)|~ilf_type(X80,binary_relation_type)|~ilf_type(X80,set_type))&(ilf_type(X80,set_type)|~ilf_type(X80,binary_relation_type)|~ilf_type(X80,set_type)))&(~relation_like(X80)|~ilf_type(X80,set_type)|ilf_type(X80,binary_relation_type)|~ilf_type(X80,set_type))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p6])])])).
% 0.30/1.62 fof(i_0_34, plain, ![X1]:(ilf_type(X1,set_type)=>(~empty(power_set(X1))&ilf_type(power_set(X1),set_type))), inference(fof_simplification,[status(thm)],[p19])).
% 0.30/1.62 fof(i_0_35, plain, ![X134, X135, X136]:(~ilf_type(X134,set_type)|(~ilf_type(X135,set_type)|(~ilf_type(X136,relation_type(X134,X135))|ilf_type(range(X134,X135,X136),subset_type(X135))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p27])])])).
% 0.30/1.62 fof(i_0_36, plain, ![X128, X129, X130]:(~ilf_type(X128,set_type)|(~ilf_type(X129,set_type)|(~ilf_type(X130,relation_type(X128,X129))|ilf_type(domain(X128,X129,X130),subset_type(X128))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p25])])])).
% 0.30/1.62 fof(i_0_37, plain, ![X82, X83, X84, X85]:((~ilf_type(X84,subset_type(cross_product(X82,X83)))|ilf_type(X84,relation_type(X82,X83))|~ilf_type(X83,set_type)|~ilf_type(X82,set_type))&(~ilf_type(X85,relation_type(X82,X83))|ilf_type(X85,subset_type(cross_product(X82,X83)))|~ilf_type(X83,set_type)|~ilf_type(X82,set_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p8])])])])).
% 0.30/1.62 fof(i_0_38, plain, ![X75, X76, X78]:(((ilf_type(esk2_2(X75,X76),set_type)|~member(X76,range_of(X75))|~ilf_type(X76,set_type)|~ilf_type(X75,binary_relation_type))&(member(ordered_pair(esk2_2(X75,X76),X76),X75)|~member(X76,range_of(X75))|~ilf_type(X76,set_type)|~ilf_type(X75,binary_relation_type)))&(~ilf_type(X78,set_type)|~member(ordered_pair(X78,X76),X75)|member(X76,range_of(X75))|~ilf_type(X76,set_type)|~ilf_type(X75,binary_relation_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p4])])])])])).
% 0.30/1.62 fof(i_0_39, plain, ![X70, X71, X73]:(((ilf_type(esk1_2(X70,X71),set_type)|~member(X71,domain_of(X70))|~ilf_type(X71,set_type)|~ilf_type(X70,binary_relation_type))&(member(ordered_pair(X71,esk1_2(X70,X71)),X70)|~member(X71,domain_of(X70))|~ilf_type(X71,set_type)|~ilf_type(X70,binary_relation_type)))&(~ilf_type(X73,set_type)|~member(ordered_pair(X71,X73),X70)|member(X71,domain_of(X70))|~ilf_type(X71,set_type)|~ilf_type(X70,binary_relation_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p2])])])])])).
% 0.30/1.62 fof(i_0_40, plain, ![X131, X132, X133]:(~ilf_type(X131,set_type)|(~ilf_type(X132,set_type)|(~ilf_type(X133,relation_type(X131,X132))|range(X131,X132,X133)=range_of(X133)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p26])])])).
% 0.30/1.62 fof(i_0_41, plain, ![X125, X126, X127]:(~ilf_type(X125,set_type)|(~ilf_type(X126,set_type)|(~ilf_type(X127,relation_type(X125,X126))|domain(X125,X126,X127)=domain_of(X127)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p24])])])).
% 0.30/1.62 fof(i_0_42, plain, ![X109, X110, X111]:(~ilf_type(X109,set_type)|(~ilf_type(X110,set_type)|(~ilf_type(X111,subset_type(cross_product(X109,X110)))|relation_like(X111)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p17])])])).
% 0.30/1.62 fof(i_0_43, plain, ![X102, X103, X107, X108]:(((ilf_type(esk7_2(X102,X103),set_type)|~member(X103,X102)|~ilf_type(X103,set_type)|~relation_like(X102)|~ilf_type(X102,set_type))&((ilf_type(esk8_2(X102,X103),set_type)|~member(X103,X102)|~ilf_type(X103,set_type)|~relation_like(X102)|~ilf_type(X102,set_type))&(X103=ordered_pair(esk7_2(X102,X103),esk8_2(X102,X103))|~member(X103,X102)|~ilf_type(X103,set_type)|~relation_like(X102)|~ilf_type(X102,set_type))))&((ilf_type(esk9_1(X102),set_type)|relation_like(X102)|~ilf_type(X102,set_type))&((member(esk9_1(X102),X102)|relation_like(X102)|~ilf_type(X102,set_type))&(~ilf_type(X107,set_type)|(~ilf_type(X108,set_type)|esk9_1(X102)!=ordered_pair(X107,X108))|relation_like(X102)|~ilf_type(X102,set_type))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p16])])])])])).
% 0.30/1.62 fof(i_0_44, plain, ![X112, X113, X114]:((~member(X112,power_set(X113))|(~ilf_type(X114,set_type)|(~member(X114,X112)|member(X114,X113)))|~ilf_type(X113,set_type)|~ilf_type(X112,set_type))&((ilf_type(esk10_2(X112,X113),set_type)|member(X112,power_set(X113))|~ilf_type(X113,set_type)|~ilf_type(X112,set_type))&((member(esk10_2(X112,X113),X112)|member(X112,power_set(X113))|~ilf_type(X113,set_type)|~ilf_type(X112,set_type))&(~member(esk10_2(X112,X113),X113)|member(X112,power_set(X113))|~ilf_type(X113,set_type)|~ilf_type(X112,set_type))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p18])])])])])).
% 0.30/1.62 fof(i_0_45, plain, ![X68, X69]:(~ilf_type(X68,set_type)|(~ilf_type(X69,binary_relation_type)|(~subset(domain_of(X69),X68)|ilf_type(X69,relation_type(X68,range_of(X69)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p1])])])).
% 0.30/1.62 fof(i_0_46, plain, ![X97, X98, X99]:((~subset(X97,X98)|(~ilf_type(X99,set_type)|(~member(X99,X97)|member(X99,X98)))|~ilf_type(X98,set_type)|~ilf_type(X97,set_type))&((ilf_type(esk6_2(X97,X98),set_type)|subset(X97,X98)|~ilf_type(X98,set_type)|~ilf_type(X97,set_type))&((member(esk6_2(X97,X98),X97)|subset(X97,X98)|~ilf_type(X98,set_type)|~ilf_type(X97,set_type))&(~member(esk6_2(X97,X98),X98)|subset(X97,X98)|~ilf_type(X98,set_type)|~ilf_type(X97,set_type))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p14])])])])])).
% 0.30/1.62 fof(i_0_47, plain, ![X93, X94]:((~ilf_type(X94,subset_type(X93))|ilf_type(X94,member_type(power_set(X93)))|~ilf_type(X94,set_type)|~ilf_type(X93,set_type))&(~ilf_type(X94,member_type(power_set(X93)))|ilf_type(X94,subset_type(X93))|~ilf_type(X94,set_type)|~ilf_type(X93,set_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p12])])])])).
% 0.30/1.62 fof(i_0_48, plain, ![X86, X87]:(~ilf_type(X86,set_type)|(~ilf_type(X87,set_type)|ilf_type(esk4_2(X86,X87),relation_type(X87,X86)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p9])])])])).
% 0.30/1.62 fof(i_0_49, plain, ![X117, X118]:((~ilf_type(X117,member_type(X118))|member(X117,X118)|(empty(X118)|~ilf_type(X118,set_type))|~ilf_type(X117,set_type))&(~member(X117,X118)|ilf_type(X117,member_type(X118))|(empty(X118)|~ilf_type(X118,set_type))|~ilf_type(X117,set_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_29])])])])).
% 0.30/1.62 fof(i_0_50, negated_conjecture, (ilf_type(esk13_0,binary_relation_type)&~ilf_type(esk13_0,relation_type(domain_of(esk13_0),range_of(esk13_0)))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_30])])])).
% 0.30/1.62 fof(i_0_51, plain, ![X89, X90]:(~ilf_type(X89,set_type)|(~ilf_type(X90,set_type)|ilf_type(cross_product(X89,X90),set_type))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p10])])])).
% 0.30/1.62 fof(i_0_52, plain, ![X91, X92]:(~ilf_type(X91,set_type)|(~ilf_type(X92,set_type)|ilf_type(ordered_pair(X91,X92),set_type))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p11])])])).
% 0.30/1.62 fof(i_0_53, plain, ![X121, X122]:((~empty(X121)|(~ilf_type(X122,set_type)|~member(X122,X121))|~ilf_type(X121,set_type))&((ilf_type(esk12_1(X121),set_type)|empty(X121)|~ilf_type(X121,set_type))&(member(esk12_1(X121),X121)|empty(X121)|~ilf_type(X121,set_type)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_31])])])])])).
% 0.30/1.62 fof(i_0_54, plain, ![X119]:(empty(X119)|~ilf_type(X119,set_type)|ilf_type(esk11_1(X119),member_type(X119))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_32])])])).
% 0.30/1.62 fof(i_0_55, plain, ![X95]:(~ilf_type(X95,set_type)|ilf_type(esk5_1(X95),subset_type(X95))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p13])])])).
% 0.30/1.62 cnf(i_0_56, plain, (ilf_type(X1,binary_relation_type)|~relation_like(X1)|~ilf_type(X1,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_33])).
% 0.30/1.62 fof(i_0_57, plain, ![X116]:((~empty(power_set(X116))|~ilf_type(X116,set_type))&(ilf_type(power_set(X116),set_type)|~ilf_type(X116,set_type))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_34])])])).
% 0.30/1.62 fof(i_0_58, plain, ![X79]:(~ilf_type(X79,binary_relation_type)|ilf_type(range_of(X79),set_type)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p5])])).
% 0.30/1.62 fof(i_0_59, plain, ![X74]:(~ilf_type(X74,binary_relation_type)|ilf_type(domain_of(X74),set_type)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p3])])).
% 0.30/1.62 fof(i_0_60, plain, ![X101]:(~ilf_type(X101,set_type)|subset(X101,X101)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p15])])).
% 0.30/1.62 fof(i_0_61, plain, ![X124]:(~empty(X124)|~ilf_type(X124,set_type)|relation_like(X124)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p23])])).
% 0.30/1.62 fof(i_0_62, plain, ![X137]:ilf_type(X137,set_type), inference(variable_rename,[status(thm)],[p28])).
% 0.30/1.62 fof(i_0_63, plain, ilf_type(esk3_0,binary_relation_type), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[p7])])).
% 0.30/1.62 cnf(i_0_64, plain, (ilf_type(range(X1,X2,X3),subset_type(X2))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))), inference(split_conjunct,[status(thm)],[i_0_35]), ['final']).
% 0.30/1.62 cnf(i_0_65, plain, (ilf_type(domain(X1,X2,X3),subset_type(X1))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))), inference(split_conjunct,[status(thm)],[i_0_36]), ['final']).
% 0.30/1.62 cnf(i_0_66, plain, (ilf_type(X1,relation_type(X2,X3))|~ilf_type(X1,subset_type(cross_product(X2,X3)))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_37]), ['final']).
% 0.30/1.62 cnf(i_0_67, plain, (ilf_type(X1,subset_type(cross_product(X2,X3)))|~ilf_type(X1,relation_type(X2,X3))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_37]), ['final']).
% 0.30/1.62 cnf(i_0_68, plain, (member(ordered_pair(esk2_2(X1,X2),X2),X1)|~member(X2,range_of(X1))|~ilf_type(X2,set_type)|~ilf_type(X1,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_38]), ['final']).
% 0.30/1.62 cnf(i_0_69, plain, (member(ordered_pair(X1,esk1_2(X2,X1)),X2)|~member(X1,domain_of(X2))|~ilf_type(X1,set_type)|~ilf_type(X2,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_39]), ['final']).
% 0.30/1.62 cnf(i_0_70, plain, (range(X1,X2,X3)=range_of(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))), inference(split_conjunct,[status(thm)],[i_0_40]), ['final']).
% 0.30/1.62 cnf(i_0_71, plain, (domain(X1,X2,X3)=domain_of(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))), inference(split_conjunct,[status(thm)],[i_0_41]), ['final']).
% 0.30/1.62 cnf(i_0_72, plain, (relation_like(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,subset_type(cross_product(X1,X2)))), inference(split_conjunct,[status(thm)],[i_0_42]), ['final']).
% 0.30/1.62 cnf(i_0_73, plain, (member(X2,range_of(X3))|~ilf_type(X1,set_type)|~member(ordered_pair(X1,X2),X3)|~ilf_type(X2,set_type)|~ilf_type(X3,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_38]), ['final']).
% 0.30/1.62 cnf(i_0_74, plain, (member(X2,domain_of(X3))|~ilf_type(X1,set_type)|~member(ordered_pair(X2,X1),X3)|~ilf_type(X2,set_type)|~ilf_type(X3,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_39]), ['final']).
% 0.30/1.62 cnf(i_0_75, plain, (X1=ordered_pair(esk7_2(X2,X1),esk8_2(X2,X1))|~member(X1,X2)|~ilf_type(X1,set_type)|~relation_like(X2)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.30/1.62 cnf(i_0_76, plain, (member(X3,X2)|~member(X1,power_set(X2))|~ilf_type(X3,set_type)|~member(X3,X1)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.30/1.62 cnf(i_0_77, plain, (ilf_type(X2,relation_type(X1,range_of(X2)))|~ilf_type(X1,set_type)|~ilf_type(X2,binary_relation_type)|~subset(domain_of(X2),X1)), inference(split_conjunct,[status(thm)],[i_0_45]), ['final']).
% 0.30/1.62 cnf(i_0_78, plain, (member(X1,power_set(X2))|~member(esk10_2(X1,X2),X2)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.30/1.62 cnf(i_0_79, plain, (member(X3,X2)|~subset(X1,X2)|~ilf_type(X3,set_type)|~member(X3,X1)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.30/1.62 cnf(i_0_80, plain, (subset(X1,X2)|~member(esk6_2(X1,X2),X2)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.30/1.62 cnf(i_0_81, plain, (ilf_type(X1,subset_type(X2))|~ilf_type(X1,member_type(power_set(X2)))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.30/1.62 cnf(i_0_82, plain, (ilf_type(esk2_2(X1,X2),set_type)|~member(X2,range_of(X1))|~ilf_type(X2,set_type)|~ilf_type(X1,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_38]), ['final']).
% 0.30/1.62 cnf(i_0_83, plain, (ilf_type(esk1_2(X1,X2),set_type)|~member(X2,domain_of(X1))|~ilf_type(X2,set_type)|~ilf_type(X1,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_39]), ['final']).
% 0.30/1.62 cnf(i_0_84, plain, (ilf_type(esk8_2(X1,X2),set_type)|~member(X2,X1)|~ilf_type(X2,set_type)|~relation_like(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.30/1.62 cnf(i_0_85, plain, (ilf_type(esk7_2(X1,X2),set_type)|~member(X2,X1)|~ilf_type(X2,set_type)|~relation_like(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.30/1.62 cnf(i_0_86, plain, (ilf_type(esk4_2(X1,X2),relation_type(X2,X1))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.30/1.62 cnf(i_0_87, plain, (ilf_type(X1,member_type(power_set(X2)))|~ilf_type(X1,subset_type(X2))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.30/1.62 cnf(i_0_88, plain, (member(esk10_2(X1,X2),X1)|member(X1,power_set(X2))|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.30/1.62 cnf(i_0_89, plain, (ilf_type(esk10_2(X1,X2),set_type)|member(X1,power_set(X2))|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.30/1.62 cnf(i_0_90, plain, (member(esk6_2(X1,X2),X1)|subset(X1,X2)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.30/1.62 cnf(i_0_91, plain, (relation_like(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|esk9_1(X3)!=ordered_pair(X1,X2)|~ilf_type(X3,set_type)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.30/1.62 cnf(i_0_92, plain, (ilf_type(esk6_2(X1,X2),set_type)|subset(X1,X2)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.30/1.62 cnf(i_0_93, plain, (member(X1,X2)|empty(X2)|~ilf_type(X1,member_type(X2))|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.30/1.62 cnf(i_0_94, plain, (ilf_type(X1,member_type(X2))|empty(X2)|~member(X1,X2)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.30/1.62 cnf(i_0_95, negated_conjecture, (~ilf_type(esk13_0,relation_type(domain_of(esk13_0),range_of(esk13_0)))), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.30/1.62 cnf(i_0_96, plain, (ilf_type(cross_product(X1,X2),set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.30/1.62 cnf(i_0_97, plain, (ilf_type(ordered_pair(X1,X2),set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.30/1.62 cnf(i_0_98, plain, (~empty(X1)|~ilf_type(X2,set_type)|~member(X2,X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.30/1.62 cnf(i_0_99, plain, (empty(X1)|ilf_type(esk11_1(X1),member_type(X1))|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.30/1.62 cnf(i_0_100, plain, (ilf_type(esk5_1(X1),subset_type(X1))|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.30/1.62 cnf(i_0_101, plain, (member(esk12_1(X1),X1)|empty(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.30/1.62 cnf(i_0_102, plain, (member(esk9_1(X1),X1)|relation_like(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.30/1.62 cnf(i_0_103, plain, (relation_like(X1)|~ilf_type(X1,binary_relation_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_33]), ['final']).
% 0.30/1.62 cnf(i_0_104, plain, (ilf_type(esk12_1(X1),set_type)|empty(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.30/1.62 cnf(i_0_105, plain, (ilf_type(esk9_1(X1),set_type)|relation_like(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.30/1.62 cnf(i_0_106, plain, (ilf_type(X1,binary_relation_type)|~relation_like(X1)|~ilf_type(X1,set_type)), inference(cn,[status(thm)],[i_0_56]), ['final']).
% 0.30/1.62 cnf(i_0_107, plain, (ilf_type(power_set(X1),set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.30/1.62 cnf(i_0_108, plain, (ilf_type(range_of(X1),set_type)|~ilf_type(X1,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.30/1.62 cnf(i_0_109, plain, (ilf_type(domain_of(X1),set_type)|~ilf_type(X1,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.30/1.62 cnf(i_0_110, plain, (~empty(power_set(X1))|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.30/1.62 cnf(i_0_111, plain, (subset(X1,X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.30/1.62 cnf(i_0_112, plain, (relation_like(X1)|~empty(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.30/1.62 cnf(i_0_113, plain, (ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.30/1.62 cnf(i_0_114, negated_conjecture, (ilf_type(esk13_0,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.30/1.62 cnf(i_0_115, plain, (ilf_type(esk3_0,binary_relation_type)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.30/1.62 cnf(i_0_116, axiom, (X1=X1)).
% 0.30/1.62 cnf(i_0_117, axiom, (X1=X2|X2!=X1)).
% 0.30/1.62 cnf(i_0_118, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.30/1.62 cnf(i_0_119, axiom, (X1!=X2|range(X1,X3,X4)=range(X2,X3,X4))).
% 0.30/1.62 cnf(i_0_120, axiom, (X1!=X2|range(X3,X1,X4)=range(X3,X2,X4))).
% 0.30/1.62 cnf(i_0_121, axiom, (X1!=X2|range(X3,X4,X1)=range(X3,X4,X2))).
% 0.30/1.62 cnf(i_0_122, axiom, (X1!=X2|domain_of(X1)=domain_of(X2))).
% 0.30/1.62 cnf(i_0_123, axiom, (X1!=X2|esk9_1(X1)=esk9_1(X2))).
% 0.30/1.62 cnf(i_0_124, axiom, (X1!=X2|domain(X1,X3,X4)=domain(X2,X3,X4))).
% 0.30/1.62 cnf(i_0_125, axiom, (X1!=X2|domain(X3,X1,X4)=domain(X3,X2,X4))).
% 0.30/1.62 cnf(i_0_126, axiom, (X1!=X2|domain(X3,X4,X1)=domain(X3,X4,X2))).
% 0.30/1.62 cnf(i_0_127, axiom, (X1!=X2|ordered_pair(X1,X3)=ordered_pair(X2,X3))).
% 0.30/1.62 cnf(i_0_128, axiom, (X1!=X2|ordered_pair(X3,X1)=ordered_pair(X3,X2))).
% 0.30/1.62 cnf(i_0_129, axiom, (X1!=X2|range_of(X1)=range_of(X2))).
% 0.30/1.62 cnf(i_0_130, axiom, (X1!=X2|~ilf_type(X1,X3)|ilf_type(X2,X3))).
% 0.30/1.62 cnf(i_0_131, axiom, (X1!=X2|~ilf_type(X3,X1)|ilf_type(X3,X2))).
% 0.30/1.62 cnf(i_0_132, axiom, (X1!=X2|~member(X1,X3)|member(X2,X3))).
% 0.30/1.62 cnf(i_0_133, axiom, (X1!=X2|~member(X3,X1)|member(X3,X2))).
% 0.30/1.62 cnf(i_0_134, axiom, (X1!=X2|~relation_like(X1)|relation_like(X2))).
% 0.30/1.62 cnf(i_0_135, axiom, (X1!=X2|~subset(X1,X3)|subset(X2,X3))).
% 0.30/1.62 cnf(i_0_136, axiom, (X1!=X2|~subset(X3,X1)|subset(X3,X2))).
% 0.30/1.62 cnf(i_0_137, axiom, (X1!=X2|~empty(X1)|empty(X2))).
% 0.40/1.77 cnf(i_0_116, axiom, (X1=X1)).
% 0.40/1.77 cnf(i_0_117, axiom, (X1=X2|X2!=X1)).
% 0.40/1.77 cnf(i_0_118, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.40/1.77 cnf(i_0_119, axiom, (X1!=X2|range(X1,X3,X4)=range(X2,X3,X4))).
% 0.40/1.77 cnf(i_0_120, axiom, (X1!=X2|range(X3,X1,X4)=range(X3,X2,X4))).
% 0.40/1.77 cnf(i_0_121, axiom, (X1!=X2|range(X3,X4,X1)=range(X3,X4,X2))).
% 0.40/1.77 cnf(i_0_122, axiom, (X1!=X2|domain_of(X1)=domain_of(X2))).
% 0.40/1.77 cnf(i_0_123, axiom, (X1!=X2|esk9_1(X1)=esk9_1(X2))).
% 0.40/1.77 cnf(i_0_124, axiom, (X1!=X2|domain(X1,X3,X4)=domain(X2,X3,X4))).
% 0.40/1.77 cnf(i_0_125, axiom, (X1!=X2|domain(X3,X1,X4)=domain(X3,X2,X4))).
% 0.40/1.77 cnf(i_0_126, axiom, (X1!=X2|domain(X3,X4,X1)=domain(X3,X4,X2))).
% 0.40/1.77 cnf(i_0_127, axiom, (X1!=X2|ordered_pair(X1,X3)=ordered_pair(X2,X3))).
% 0.40/1.77 cnf(i_0_128, axiom, (X1!=X2|ordered_pair(X3,X1)=ordered_pair(X3,X2))).
% 0.40/1.77 cnf(i_0_129, axiom, (X1!=X2|range_of(X1)=range_of(X2))).
% 0.40/1.77 cnf(i_0_130, axiom, (X1!=X2|~ilf_type(X1,X3)|ilf_type(X2,X3))).
% 0.40/1.77 cnf(i_0_131, axiom, (X1!=X2|~ilf_type(X3,X1)|ilf_type(X3,X2))).
% 0.40/1.77 cnf(i_0_132, axiom, (X1!=X2|~member(X1,X3)|member(X2,X3))).
% 0.40/1.77 cnf(i_0_133, axiom, (X1!=X2|~member(X3,X1)|member(X3,X2))).
% 0.40/1.77 cnf(i_0_134, axiom, (X1!=X2|~relation_like(X1)|relation_like(X2))).
% 0.40/1.77 cnf(i_0_135, axiom, (X1!=X2|~subset(X1,X3)|subset(X2,X3))).
% 0.40/1.77 cnf(i_0_136, axiom, (X1!=X2|~subset(X3,X1)|subset(X3,X2))).
% 0.40/1.77 cnf(i_0_137, axiom, (X1!=X2|~empty(X1)|empty(X2))).
% 0.40/1.77 cnf(i_0_138, plain, (ilf_type(esk5_1(X1),subset_type(X1))), inference(scs_inference,[],[i_0_113,i_0_100])).
% 0.40/1.77 cnf(i_0_139, plain, (~ilf_type(X1,set_type)|ilf_type(esk5_1(X1),subset_type(X1))), inference(rename_variables,[],[i_0_100])).
% 0.40/1.77 cnf(i_0_140, plain, (subset(X1,X1)), inference(scs_inference,[],[i_0_113,i_0_100,i_0_111])).
% 0.40/1.77 cnf(i_0_141, plain, (~ilf_type(X1,set_type)|subset(X1,X1)), inference(rename_variables,[],[i_0_111])).
% 0.40/1.77 cnf(i_0_142, plain, (relation_like(esk13_0)), inference(scs_inference,[],[i_0_114,i_0_113,i_0_100,i_0_111,i_0_103])).
% 0.40/1.77 cnf(i_0_143, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_144, plain, (~ilf_type(X1,binary_relation_type)|~ilf_type(X1,set_type)|relation_like(X1)), inference(rename_variables,[],[i_0_103])).
% 0.40/1.77 cnf(i_0_145, plain, (binary_relation_type!=relation_type(domain_of(esk13_0),range_of(esk13_0))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_100,i_0_111,i_0_103,i_0_131])).
% 0.40/1.77 cnf(i_0_146, plain, (ilf_type(esk4_2(X1,X1),relation_type(X1,X1))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86])).
% 0.40/1.77 cnf(i_0_147, plain, (~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|ilf_type(esk4_2(X1,X2),relation_type(X2,X1))), inference(rename_variables,[],[i_0_86])).
% 0.40/1.77 cnf(i_0_148, plain, (ilf_type(range(X1,X1,esk4_2(X1,X1)),subset_type(X1))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64])).
% 0.40/1.77 cnf(i_0_149, plain, (~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))|ilf_type(range(X1,X2,X3),subset_type(X2))), inference(rename_variables,[],[i_0_64])).
% 0.40/1.77 cnf(i_0_150, plain, (~subset(domain_of(esk13_0),domain_of(esk13_0))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77])).
% 0.40/1.77 cnf(i_0_151, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_152, plain, (ilf_type(X1,relation_type(X2,range_of(X1)))|~ilf_type(X2,set_type)|~ilf_type(X1,binary_relation_type)|~subset(domain_of(X1),X2)), inference(rename_variables,[],[i_0_77])).
% 0.40/1.77 cnf(i_0_153, plain, (member(esk6_2(domain_of(esk13_0),domain_of(esk13_0)),domain_of(esk13_0))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90])).
% 0.40/1.77 cnf(i_0_154, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_155, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_156, plain, (~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|member(esk6_2(X2,X1),X2)|subset(X2,X1)), inference(rename_variables,[],[i_0_90])).
% 0.40/1.77 cnf(i_0_157, plain, (~empty(domain_of(esk13_0))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_154,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98])).
% 0.40/1.77 cnf(i_0_158, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_159, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_160, plain, (~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~member(X2,X1)|~empty(X1)), inference(rename_variables,[],[i_0_98])).
% 0.40/1.77 cnf(i_0_161, plain, (ilf_type(esk6_2(domain_of(esk13_0),domain_of(esk13_0)),member_type(domain_of(esk13_0)))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_159,i_0_154,i_0_158,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98,i_0_94])).
% 0.40/1.77 cnf(i_0_162, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_163, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_164, plain, (~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|ilf_type(X2,member_type(X1))|empty(X1)|~member(X2,X1)), inference(rename_variables,[],[i_0_94])).
% 0.40/1.77 cnf(i_0_165, plain, (X1!=esk13_0|~ilf_type(X1,relation_type(domain_of(esk13_0),range_of(esk13_0)))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_159,i_0_154,i_0_158,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98,i_0_94,i_0_130])).
% 0.40/1.77 cnf(i_0_166, plain, (member(esk12_1(domain_of(esk13_0)),domain_of(esk13_0))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_159,i_0_163,i_0_154,i_0_158,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98,i_0_94,i_0_130,i_0_101])).
% 0.40/1.77 cnf(i_0_167, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_168, plain, (~ilf_type(X1,set_type)|member(esk12_1(X1),X1)|empty(X1)), inference(rename_variables,[],[i_0_101])).
% 0.40/1.77 cnf(i_0_169, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_113])).
% 0.40/1.77 cnf(i_0_170, plain, (relation_like(X1)|member(esk9_1(X1),X1)), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_159,i_0_163,i_0_167,i_0_169,i_0_154,i_0_158,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98,i_0_94,i_0_130,i_0_101,i_0_80,i_0_102])).
% 0.40/1.77 cnf(i_0_171, plain, (~ilf_type(X1,set_type)|member(esk9_1(X1),X1)|relation_like(X1)), inference(rename_variables,[],[i_0_102])).
% 0.40/1.77 cnf(i_0_172, plain, (~empty(X1)|relation_like(X1)), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_159,i_0_163,i_0_167,i_0_169,i_0_154,i_0_158,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98,i_0_94,i_0_130,i_0_101,i_0_80,i_0_102,i_0_112])).
% 0.40/1.77 cnf(i_0_173, plain, (~ilf_type(X1,set_type)|~empty(X1)|relation_like(X1)), inference(rename_variables,[],[i_0_112])).
% 0.40/1.77 cnf(i_0_174, plain, (relation_like(X1)|esk13_0!=X1), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_159,i_0_163,i_0_167,i_0_169,i_0_154,i_0_158,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98,i_0_94,i_0_130,i_0_101,i_0_80,i_0_102,i_0_112,i_0_134])).
% 0.40/1.77 cnf(i_0_175, plain, (X1!=domain_of(esk13_0)|~subset(X1,domain_of(esk13_0))), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_159,i_0_163,i_0_167,i_0_169,i_0_154,i_0_158,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98,i_0_94,i_0_130,i_0_101,i_0_80,i_0_102,i_0_112,i_0_134,i_0_135])).
% 0.40/1.77 cnf(i_0_176, plain, (X1!=domain_of(esk13_0)|~subset(domain_of(esk13_0),X1)), inference(scs_inference,[],[i_0_95,i_0_114,i_0_113,i_0_143,i_0_151,i_0_155,i_0_159,i_0_163,i_0_167,i_0_169,i_0_154,i_0_158,i_0_100,i_0_111,i_0_103,i_0_131,i_0_86,i_0_64,i_0_77,i_0_90,i_0_98,i_0_94,i_0_130,i_0_101,i_0_80,i_0_102,i_0_112,i_0_134,i_0_135,i_0_136])).
% 0.40/1.77 cnf(i_0_177, plain, (~ilf_type(esk13_0,relation_type(domain_of(esk13_0),range_of(esk13_0)))), inference(equality_inference,[],[165])).
% 0.40/1.77 cnf(i_0_178, plain, (relation_like(esk13_0)), inference(equality_inference,[],[174])).
% 0.40/1.77 cnf(i_0_179, plain, (~subset(domain_of(esk13_0),domain_of(esk13_0))), inference(equality_inference,[],[175])).
% 0.40/1.77 cnf(i_0_180, plain, (~subset(domain_of(esk13_0),domain_of(esk13_0))), inference(equality_inference,[],[176])).
% 0.40/1.77 cnf(i_0_181,plain, ($false), inference(scs_inference,[],[i_0+150, i_0_140]), ['proof']).
% 0.40/1.77 % SZS output end CNFRefutation
% 0.40/1.77 % Total time : 1.271s
%------------------------------------------------------------------------------