%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET677+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 : n023.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:18 PM UTC 2026
% Result : Theorem 0.35s 1.61s
% Output : CNFRefutation 0.65s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 119)
% Comments :
%------------------------------------------------------------------------------
fof(prove_relset_1_44,conjecture,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,identity_relation_of_type(X1))
=> ( subset(identity_relation_of(X1),X2)
=> ( X1 = domain(X1,X1,X2)
& X1 = range(X1,X1,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_relset_1_44) ).
fof(p24,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',p24) ).
fof(p28,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',p28) ).
fof(p25,axiom,
! [X1] :
( ( ~ empty(X1)
& ilf_type(X1,set_type) )
=> ? [X2] : ilf_type(X2,member_type(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p25) ).
fof(p12,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',p12) ).
fof(p23,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',p23) ).
fof(p7,axiom,
! [X1] :
( ilf_type(X1,binary_relation_type)
=> ! [X2] :
( ilf_type(X2,binary_relation_type)
=> ( subset(X1,X2)
<=> ! [X3] :
( ilf_type(X3,set_type)
=> ! [X4] :
( ilf_type(X4,set_type)
=> ( member(ordered_pair(X3,X4),X1)
=> member(ordered_pair(X3,X4),X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p7) ).
fof(p1,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ! [X3] :
( ilf_type(X3,relation_type(X2,X1))
=> ( subset(identity_relation_of(X2),X3)
=> ( X2 = domain(X2,X1,X3)
& subset(X2,range(X2,X1,X3)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p1) ).
fof(p2,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ! [X3] :
( ilf_type(X3,relation_type(X1,X2))
=> ( subset(identity_relation_of(X2),X3)
=> ( subset(X2,domain(X1,X2,X3))
& X2 = range(X1,X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2) ).
fof(p33,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',p33) ).
fof(p31,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',p31) ).
fof(p14,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',p14) ).
fof(p32,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',p32) ).
fof(p30,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',p30) ).
fof(p27,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',p27) ).
fof(p3,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ! [X3] :
( ilf_type(X3,set_type)
=> ( member(ordered_pair(X2,X3),identity_relation_of(X1))
<=> ( member(X2,X1)
& X2 = X3 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3) ).
fof(p26,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',p26) ).
fof(p22,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',p22) ).
fof(p5,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ( ilf_type(X2,identity_relation_of_type(X1))
<=> ilf_type(X2,relation_type(X1,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5) ).
fof(p18,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',p18) ).
fof(p16,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',p16) ).
fof(p15,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',p15) ).
fof(p8,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ( X1 = X2
<=> ( subset(X1,X2)
& subset(X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p8) ).
fof(p21,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',p21) ).
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) ).
fof(p17,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ? [X2] : ilf_type(X2,subset_type(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p17) ).
fof(p6,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ? [X2] : ilf_type(X2,identity_relation_of_type(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6) ).
fof(p10,axiom,
! [X1] :
( ilf_type(X1,binary_relation_type)
=> ilf_type(range_of(X1),set_type) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p10) ).
fof(p9,axiom,
! [X1] :
( ilf_type(X1,binary_relation_type)
=> ilf_type(domain_of(X1),set_type) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9) ).
fof(p4,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ilf_type(identity_relation_of(X1),binary_relation_type) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4) ).
fof(p20,axiom,
! [X1] :
( ilf_type(X1,binary_relation_type)
=> subset(X1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p20) ).
fof(p19,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> subset(X1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19) ).
fof(p29,axiom,
! [X1] :
( ( empty(X1)
& ilf_type(X1,set_type) )
=> relation_like(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p29) ).
fof(p34,axiom,
! [X1] : ilf_type(X1,set_type),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p34) ).
fof(p13,axiom,
? [X1] : ilf_type(X1,binary_relation_type),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p13) ).
fof(i_0_35,negated_conjecture,
~ ! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,identity_relation_of_type(X1))
=> ( subset(identity_relation_of(X1),X2)
=> ( X1 = domain(X1,X1,X2)
& X1 = range(X1,X1,X2) ) ) ) ),
inference(assume_negation,[status(cth)],[prove_relset_1_44]) ).
fof(i_0_36,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)],[p24]) ).
fof(i_0_37,plain,
! [X1] :
( ilf_type(X1,set_type)
=> ( empty(X1)
<=> ! [X2] :
( ilf_type(X2,set_type)
=> ~ member(X2,X1) ) ) ),
inference(fof_simplification,[status(thm)],[p28]) ).
fof(i_0_38,plain,
! [X1] :
( ( ~ empty(X1)
& ilf_type(X1,set_type) )
=> ? [X2] : ilf_type(X2,member_type(X1)) ),
inference(fof_simplification,[status(thm)],[p25]) ).
fof(i_0_39,plain,
! [X108] :
( ( relation_like(X108)
| ~ ilf_type(X108,binary_relation_type)
| ~ ilf_type(X108,set_type) )
& ( ilf_type(X108,set_type)
| ~ ilf_type(X108,binary_relation_type)
| ~ ilf_type(X108,set_type) )
& ( ~ relation_like(X108)
| ~ ilf_type(X108,set_type)
| ilf_type(X108,binary_relation_type)
| ~ ilf_type(X108,set_type) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p12])])]) ).
fof(i_0_40,plain,
! [X1] :
( ilf_type(X1,set_type)
=> ( ~ empty(power_set(X1))
& ilf_type(power_set(X1),set_type) ) ),
inference(fof_simplification,[status(thm)],[p23]) ).
fof(i_0_41,plain,
! [X96,X97,X98,X99] :
( ( ~ subset(X96,X97)
| ~ ilf_type(X98,set_type)
| ~ ilf_type(X99,set_type)
| ~ member(ordered_pair(X98,X99),X96)
| member(ordered_pair(X98,X99),X97)
| ~ ilf_type(X97,binary_relation_type)
| ~ ilf_type(X96,binary_relation_type) )
& ( ilf_type(esk2_2(X96,X97),set_type)
| subset(X96,X97)
| ~ ilf_type(X97,binary_relation_type)
| ~ ilf_type(X96,binary_relation_type) )
& ( ilf_type(esk3_2(X96,X97),set_type)
| subset(X96,X97)
| ~ ilf_type(X97,binary_relation_type)
| ~ ilf_type(X96,binary_relation_type) )
& ( member(ordered_pair(esk2_2(X96,X97),esk3_2(X96,X97)),X96)
| subset(X96,X97)
| ~ ilf_type(X97,binary_relation_type)
| ~ ilf_type(X96,binary_relation_type) )
& ( ~ member(ordered_pair(esk2_2(X96,X97),esk3_2(X96,X97)),X97)
| subset(X96,X97)
| ~ ilf_type(X97,binary_relation_type)
| ~ ilf_type(X96,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)],[p7])])])])]) ).
fof(i_0_42,plain,
! [X82,X83,X84] :
( ( X83 = domain(X83,X82,X84)
| ~ subset(identity_relation_of(X83),X84)
| ~ ilf_type(X84,relation_type(X83,X82))
| ~ ilf_type(X83,set_type)
| ~ ilf_type(X82,set_type) )
& ( subset(X83,range(X83,X82,X84))
| ~ subset(identity_relation_of(X83),X84)
| ~ ilf_type(X84,relation_type(X83,X82))
| ~ 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)],[p1])])])]) ).
fof(i_0_43,plain,
! [X85,X86,X87] :
( ( subset(X86,domain(X85,X86,X87))
| ~ subset(identity_relation_of(X86),X87)
| ~ ilf_type(X87,relation_type(X85,X86))
| ~ ilf_type(X86,set_type)
| ~ ilf_type(X85,set_type) )
& ( X86 = range(X85,X86,X87)
| ~ subset(identity_relation_of(X86),X87)
| ~ ilf_type(X87,relation_type(X85,X86))
| ~ ilf_type(X86,set_type)
| ~ ilf_type(X85,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p2])])])]) ).
fof(i_0_44,plain,
! [X161,X162,X163] :
( ~ ilf_type(X161,set_type)
| ~ ilf_type(X162,set_type)
| ~ ilf_type(X163,relation_type(X161,X162))
| ilf_type(range(X161,X162,X163),subset_type(X162)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p33])])]) ).
fof(i_0_45,plain,
! [X155,X156,X157] :
( ~ ilf_type(X155,set_type)
| ~ ilf_type(X156,set_type)
| ~ ilf_type(X157,relation_type(X155,X156))
| ilf_type(domain(X155,X156,X157),subset_type(X155)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p31])])]) ).
fof(i_0_46,plain,
! [X110,X111,X112,X113] :
( ( ~ ilf_type(X112,subset_type(cross_product(X110,X111)))
| ilf_type(X112,relation_type(X110,X111))
| ~ ilf_type(X111,set_type)
| ~ ilf_type(X110,set_type) )
& ( ~ ilf_type(X113,relation_type(X110,X111))
| ilf_type(X113,subset_type(cross_product(X110,X111)))
| ~ ilf_type(X111,set_type)
| ~ ilf_type(X110,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p14])])])]) ).
fof(i_0_47,plain,
! [X158,X159,X160] :
( ~ ilf_type(X158,set_type)
| ~ ilf_type(X159,set_type)
| ~ ilf_type(X160,relation_type(X158,X159))
| range(X158,X159,X160) = range_of(X160) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p32])])]) ).
fof(i_0_48,plain,
! [X152,X153,X154] :
( ~ ilf_type(X152,set_type)
| ~ ilf_type(X153,set_type)
| ~ ilf_type(X154,relation_type(X152,X153))
| domain(X152,X153,X154) = domain_of(X154) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p30])])]) ).
fof(i_0_49,plain,
! [X145,X146,X147] :
( ~ ilf_type(X145,set_type)
| ~ ilf_type(X146,set_type)
| ~ ilf_type(X147,subset_type(cross_product(X145,X146)))
| relation_like(X147) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p27])])]) ).
fof(i_0_50,negated_conjecture,
( ilf_type(esk14_0,set_type)
& ilf_type(esk15_0,identity_relation_of_type(esk14_0))
& subset(identity_relation_of(esk14_0),esk15_0)
& ( esk14_0 != domain(esk14_0,esk14_0,esk15_0)
| esk14_0 != range(esk14_0,esk14_0,esk15_0) ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_35])])]) ).
fof(i_0_51,plain,
! [X88,X89,X90] :
( ( member(X89,X88)
| ~ member(ordered_pair(X89,X90),identity_relation_of(X88))
| ~ ilf_type(X90,set_type)
| ~ ilf_type(X89,set_type)
| ~ ilf_type(X88,set_type) )
& ( X89 = X90
| ~ member(ordered_pair(X89,X90),identity_relation_of(X88))
| ~ ilf_type(X90,set_type)
| ~ ilf_type(X89,set_type)
| ~ ilf_type(X88,set_type) )
& ( ~ member(X89,X88)
| X89 != X90
| member(ordered_pair(X89,X90),identity_relation_of(X88))
| ~ ilf_type(X90,set_type)
| ~ ilf_type(X89,set_type)
| ~ ilf_type(X88,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p3])])])]) ).
fof(i_0_52,plain,
! [X138,X139,X143,X144] :
( ( ilf_type(esk10_2(X138,X139),set_type)
| ~ member(X139,X138)
| ~ ilf_type(X139,set_type)
| ~ relation_like(X138)
| ~ ilf_type(X138,set_type) )
& ( ilf_type(esk11_2(X138,X139),set_type)
| ~ member(X139,X138)
| ~ ilf_type(X139,set_type)
| ~ relation_like(X138)
| ~ ilf_type(X138,set_type) )
& ( X139 = ordered_pair(esk10_2(X138,X139),esk11_2(X138,X139))
| ~ member(X139,X138)
| ~ ilf_type(X139,set_type)
| ~ relation_like(X138)
| ~ ilf_type(X138,set_type) )
& ( ilf_type(esk12_1(X138),set_type)
| relation_like(X138)
| ~ ilf_type(X138,set_type) )
& ( member(esk12_1(X138),X138)
| relation_like(X138)
| ~ ilf_type(X138,set_type) )
& ( ~ ilf_type(X143,set_type)
| ~ ilf_type(X144,set_type)
| esk12_1(X138) != ordered_pair(X143,X144)
| relation_like(X138)
| ~ ilf_type(X138,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)],[p26])])])])]) ).
fof(i_0_53,plain,
! [X129,X130,X131] :
( ( ~ member(X129,power_set(X130))
| ~ ilf_type(X131,set_type)
| ~ member(X131,X129)
| member(X131,X130)
| ~ ilf_type(X130,set_type)
| ~ ilf_type(X129,set_type) )
& ( ilf_type(esk8_2(X129,X130),set_type)
| member(X129,power_set(X130))
| ~ ilf_type(X130,set_type)
| ~ ilf_type(X129,set_type) )
& ( member(esk8_2(X129,X130),X129)
| member(X129,power_set(X130))
| ~ ilf_type(X130,set_type)
| ~ ilf_type(X129,set_type) )
& ( ~ member(esk8_2(X129,X130),X130)
| member(X129,power_set(X130))
| ~ ilf_type(X130,set_type)
| ~ ilf_type(X129,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)],[p22])])])])]) ).
fof(i_0_54,plain,
! [X92,X93] :
( ( ~ ilf_type(X93,identity_relation_of_type(X92))
| ilf_type(X93,relation_type(X92,X92))
| ~ ilf_type(X93,set_type)
| ~ ilf_type(X92,set_type) )
& ( ~ ilf_type(X93,relation_type(X92,X92))
| ilf_type(X93,identity_relation_of_type(X92))
| ~ ilf_type(X93,set_type)
| ~ ilf_type(X92,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p5])])])]) ).
fof(i_0_55,plain,
! [X121,X122,X123] :
( ( ~ subset(X121,X122)
| ~ ilf_type(X123,set_type)
| ~ member(X123,X121)
| member(X123,X122)
| ~ ilf_type(X122,set_type)
| ~ ilf_type(X121,set_type) )
& ( ilf_type(esk7_2(X121,X122),set_type)
| subset(X121,X122)
| ~ ilf_type(X122,set_type)
| ~ ilf_type(X121,set_type) )
& ( member(esk7_2(X121,X122),X121)
| subset(X121,X122)
| ~ ilf_type(X122,set_type)
| ~ ilf_type(X121,set_type) )
& ( ~ member(esk7_2(X121,X122),X122)
| subset(X121,X122)
| ~ ilf_type(X122,set_type)
| ~ 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)],[p18])])])])]) ).
fof(i_0_56,plain,
! [X117,X118] :
( ( ~ ilf_type(X118,subset_type(X117))
| ilf_type(X118,member_type(power_set(X117)))
| ~ ilf_type(X118,set_type)
| ~ ilf_type(X117,set_type) )
& ( ~ ilf_type(X118,member_type(power_set(X117)))
| ilf_type(X118,subset_type(X117))
| ~ 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)],[p16])])])]) ).
fof(i_0_57,plain,
! [X114,X115] :
( ~ ilf_type(X114,set_type)
| ~ ilf_type(X115,set_type)
| ilf_type(esk5_2(X114,X115),relation_type(X115,X114)) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p15])])])]) ).
fof(i_0_58,plain,
! [X134,X135] :
( ( ~ ilf_type(X134,member_type(X135))
| member(X134,X135)
| empty(X135)
| ~ ilf_type(X135,set_type)
| ~ ilf_type(X134,set_type) )
& ( ~ member(X134,X135)
| ilf_type(X134,member_type(X135))
| empty(X135)
| ~ ilf_type(X135,set_type)
| ~ ilf_type(X134,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_36])])])]) ).
fof(i_0_59,plain,
! [X102,X103] :
( ( subset(X102,X103)
| X102 != X103
| ~ ilf_type(X103,set_type)
| ~ ilf_type(X102,set_type) )
& ( subset(X103,X102)
| X102 != X103
| ~ ilf_type(X103,set_type)
| ~ ilf_type(X102,set_type) )
& ( ~ subset(X102,X103)
| ~ subset(X103,X102)
| X102 = X103
| ~ ilf_type(X103,set_type)
| ~ ilf_type(X102,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p8])])])]) ).
fof(i_0_60,plain,
! [X127,X128] :
( ~ ilf_type(X127,set_type)
| ~ ilf_type(X128,set_type)
| ilf_type(cross_product(X127,X128),set_type) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p21])])]) ).
fof(i_0_61,plain,
! [X106,X107] :
( ~ ilf_type(X106,set_type)
| ~ ilf_type(X107,set_type)
| ilf_type(ordered_pair(X106,X107),set_type) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p11])])]) ).
fof(i_0_62,plain,
! [X148,X149] :
( ( ~ empty(X148)
| ~ ilf_type(X149,set_type)
| ~ member(X149,X148)
| ~ ilf_type(X148,set_type) )
& ( ilf_type(esk13_1(X148),set_type)
| empty(X148)
| ~ ilf_type(X148,set_type) )
& ( member(esk13_1(X148),X148)
| empty(X148)
| ~ ilf_type(X148,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_37])])])])]) ).
fof(i_0_63,plain,
! [X136] :
( empty(X136)
| ~ ilf_type(X136,set_type)
| ilf_type(esk9_1(X136),member_type(X136)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_38])])]) ).
fof(i_0_64,plain,
! [X119] :
( ~ ilf_type(X119,set_type)
| ilf_type(esk6_1(X119),subset_type(X119)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p17])])]) ).
fof(i_0_65,plain,
! [X94] :
( ~ ilf_type(X94,set_type)
| ilf_type(esk1_1(X94),identity_relation_of_type(X94)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p6])])]) ).
cnf(i_0_66,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_39]) ).
fof(i_0_67,plain,
! [X133] :
( ( ~ empty(power_set(X133))
| ~ ilf_type(X133,set_type) )
& ( ilf_type(power_set(X133),set_type)
| ~ ilf_type(X133,set_type) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_40])])]) ).
fof(i_0_68,plain,
! [X105] :
( ~ ilf_type(X105,binary_relation_type)
| ilf_type(range_of(X105),set_type) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p10])]) ).
fof(i_0_69,plain,
! [X104] :
( ~ ilf_type(X104,binary_relation_type)
| ilf_type(domain_of(X104),set_type) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p9])]) ).
fof(i_0_70,plain,
! [X91] :
( ~ ilf_type(X91,set_type)
| ilf_type(identity_relation_of(X91),binary_relation_type) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p4])]) ).
fof(i_0_71,plain,
! [X126] :
( ~ ilf_type(X126,binary_relation_type)
| subset(X126,X126) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p20])]) ).
fof(i_0_72,plain,
! [X125] :
( ~ ilf_type(X125,set_type)
| subset(X125,X125) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p19])]) ).
fof(i_0_73,plain,
! [X151] :
( ~ empty(X151)
| ~ ilf_type(X151,set_type)
| relation_like(X151) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p29])]) ).
fof(i_0_74,plain,
! [X164] : ilf_type(X164,set_type),
inference(variable_rename,[status(thm)],[p34]) ).
fof(i_0_75,plain,
ilf_type(esk4_0,binary_relation_type),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[p13])]) ).
cnf(i_0_76,plain,
( subset(X1,X2)
| ~ member(ordered_pair(esk2_2(X1,X2),esk3_2(X1,X2)),X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_77,plain,
( subset(X1,range(X1,X2,X3))
| ~ subset(identity_relation_of(X1),X3)
| ~ ilf_type(X3,relation_type(X1,X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_78,plain,
( subset(X1,domain(X2,X1,X3))
| ~ subset(identity_relation_of(X1),X3)
| ~ ilf_type(X3,relation_type(X2,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_79,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_44]),
[final] ).
cnf(i_0_80,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_45]),
[final] ).
cnf(i_0_81,plain,
( member(ordered_pair(X3,X4),X2)
| ~ subset(X1,X2)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X4,set_type)
| ~ member(ordered_pair(X3,X4),X1)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_82,plain,
( member(ordered_pair(esk2_2(X1,X2),esk3_2(X1,X2)),X1)
| subset(X1,X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_83,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_46]),
[final] ).
cnf(i_0_84,plain,
( X1 = range(X2,X1,X3)
| ~ subset(identity_relation_of(X1),X3)
| ~ ilf_type(X3,relation_type(X2,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_85,plain,
( X1 = domain(X1,X2,X3)
| ~ subset(identity_relation_of(X1),X3)
| ~ ilf_type(X3,relation_type(X1,X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_86,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_46]),
[final] ).
cnf(i_0_87,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_47]),
[final] ).
cnf(i_0_88,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_48]),
[final] ).
cnf(i_0_89,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_49]),
[final] ).
cnf(i_0_90,negated_conjecture,
( esk14_0 != domain(esk14_0,esk14_0,esk15_0)
| esk14_0 != range(esk14_0,esk14_0,esk15_0) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_91,plain,
( member(X1,X2)
| ~ member(ordered_pair(X1,X3),identity_relation_of(X2))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_92,plain,
( X1 = ordered_pair(esk10_2(X2,X1),esk11_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_52]),
[final] ).
cnf(i_0_93,plain,
( X1 = X2
| ~ member(ordered_pair(X1,X2),identity_relation_of(X3))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_94,plain,
( member(ordered_pair(X1,X3),identity_relation_of(X2))
| ~ member(X1,X2)
| X1 != X3
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_95,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_53]),
[final] ).
cnf(i_0_96,plain,
( member(X1,power_set(X2))
| ~ member(esk8_2(X1,X2),X2)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_97,plain,
( ilf_type(X1,identity_relation_of_type(X2))
| ~ ilf_type(X1,relation_type(X2,X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_98,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_55]),
[final] ).
cnf(i_0_99,plain,
( subset(X1,X2)
| ~ member(esk7_2(X1,X2),X2)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_100,plain,
( ilf_type(X1,relation_type(X2,X2))
| ~ ilf_type(X1,identity_relation_of_type(X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_101,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_56]),
[final] ).
cnf(i_0_102,plain,
( ilf_type(esk11_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_52]),
[final] ).
cnf(i_0_103,plain,
( ilf_type(esk10_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_52]),
[final] ).
cnf(i_0_104,plain,
( ilf_type(esk5_2(X1,X2),relation_type(X2,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_105,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_56]),
[final] ).
cnf(i_0_106,plain,
( member(esk8_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_53]),
[final] ).
cnf(i_0_107,plain,
( ilf_type(esk8_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_53]),
[final] ).
cnf(i_0_108,plain,
( member(esk7_2(X1,X2),X1)
| subset(X1,X2)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_109,plain,
( relation_like(X3)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| esk12_1(X3) != ordered_pair(X1,X2)
| ~ ilf_type(X3,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_110,plain,
( ilf_type(esk7_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_55]),
[final] ).
cnf(i_0_111,plain,
( ilf_type(esk3_2(X1,X2),set_type)
| subset(X1,X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_112,plain,
( ilf_type(esk2_2(X1,X2),set_type)
| subset(X1,X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_113,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_58]),
[final] ).
cnf(i_0_114,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_58]),
[final] ).
cnf(i_0_115,plain,
( X1 = X2
| ~ subset(X1,X2)
| ~ subset(X2,X1)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_116,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_60]),
[final] ).
cnf(i_0_117,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_61]),
[final] ).
cnf(i_0_118,plain,
( ~ empty(X1)
| ~ ilf_type(X2,set_type)
| ~ member(X2,X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_119,plain,
( subset(X1,X2)
| X1 != X2
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_120,plain,
( subset(X1,X2)
| X2 != X1
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_121,plain,
( empty(X1)
| ilf_type(esk9_1(X1),member_type(X1))
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_122,plain,
( ilf_type(esk6_1(X1),subset_type(X1))
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_123,plain,
( ilf_type(esk1_1(X1),identity_relation_of_type(X1))
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_124,plain,
( member(esk13_1(X1),X1)
| empty(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_125,plain,
( member(esk12_1(X1),X1)
| relation_like(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_126,plain,
( relation_like(X1)
| ~ ilf_type(X1,binary_relation_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_127,plain,
( ilf_type(esk13_1(X1),set_type)
| empty(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_128,plain,
( ilf_type(esk12_1(X1),set_type)
| relation_like(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_129,plain,
( ilf_type(X1,binary_relation_type)
| ~ relation_like(X1)
| ~ ilf_type(X1,set_type) ),
inference(cn,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_130,plain,
( ilf_type(power_set(X1),set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_131,plain,
( ilf_type(range_of(X1),set_type)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_132,plain,
( ilf_type(domain_of(X1),set_type)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_133,plain,
( ilf_type(identity_relation_of(X1),binary_relation_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_134,plain,
( ~ empty(power_set(X1))
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_135,plain,
( subset(X1,X1)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_136,plain,
( subset(X1,X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_137,plain,
( relation_like(X1)
| ~ empty(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_138,negated_conjecture,
subset(identity_relation_of(esk14_0),esk15_0),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_139,negated_conjecture,
ilf_type(esk15_0,identity_relation_of_type(esk14_0)),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_140,plain,
ilf_type(X1,set_type),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_141,negated_conjecture,
ilf_type(esk14_0,set_type),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_142,plain,
ilf_type(esk4_0,binary_relation_type),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_143,axiom,
X1 = X1 ).
cnf(i_0_144,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_145,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_146,axiom,
( X1 != X2
| ordered_pair(X1,X3) = ordered_pair(X2,X3) ) ).
cnf(i_0_147,axiom,
( X1 != X2
| ordered_pair(X3,X1) = ordered_pair(X3,X2) ) ).
cnf(i_0_148,axiom,
( X1 != X2
| range_of(X1) = range_of(X2) ) ).
cnf(i_0_149,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_150,axiom,
( X1 != X2
| esk12_1(X1) = esk12_1(X2) ) ).
cnf(i_0_151,axiom,
( X1 != X2
| range(X1,X3,X4) = range(X2,X3,X4) ) ).
cnf(i_0_152,axiom,
( X1 != X2
| range(X3,X1,X4) = range(X3,X2,X4) ) ).
cnf(i_0_153,axiom,
( X1 != X2
| range(X3,X4,X1) = range(X3,X4,X2) ) ).
cnf(i_0_154,axiom,
( X1 != X2
| domain(X1,X3,X4) = domain(X2,X3,X4) ) ).
cnf(i_0_155,axiom,
( X1 != X2
| domain(X3,X1,X4) = domain(X3,X2,X4) ) ).
cnf(i_0_156,axiom,
( X1 != X2
| domain(X3,X4,X1) = domain(X3,X4,X2) ) ).
cnf(i_0_157,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_158,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_159,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_160,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_161,axiom,
( X1 != X2
| ~ ilf_type(X1,X3)
| ilf_type(X2,X3) ) ).
cnf(i_0_162,axiom,
( X1 != X2
| ~ ilf_type(X3,X1)
| ilf_type(X3,X2) ) ).
cnf(i_0_163,axiom,
( X1 != X2
| ~ relation_like(X1)
| relation_like(X2) ) ).
cnf(i_0_164,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_143_001,axiom,
X1 = X1 ).
cnf(i_0_144_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_145_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_146_004,axiom,
( X1 != X2
| ordered_pair(X1,X3) = ordered_pair(X2,X3) ) ).
cnf(i_0_147_005,axiom,
( X1 != X2
| ordered_pair(X3,X1) = ordered_pair(X3,X2) ) ).
cnf(i_0_148_006,axiom,
( X1 != X2
| range_of(X1) = range_of(X2) ) ).
cnf(i_0_149_007,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_150_008,axiom,
( X1 != X2
| esk12_1(X1) = esk12_1(X2) ) ).
cnf(i_0_151_009,axiom,
( X1 != X2
| range(X1,X3,X4) = range(X2,X3,X4) ) ).
cnf(i_0_152_010,axiom,
( X1 != X2
| range(X3,X1,X4) = range(X3,X2,X4) ) ).
cnf(i_0_153_011,axiom,
( X1 != X2
| range(X3,X4,X1) = range(X3,X4,X2) ) ).
cnf(i_0_154_012,axiom,
( X1 != X2
| domain(X1,X3,X4) = domain(X2,X3,X4) ) ).
cnf(i_0_155_013,axiom,
( X1 != X2
| domain(X3,X1,X4) = domain(X3,X2,X4) ) ).
cnf(i_0_156_014,axiom,
( X1 != X2
| domain(X3,X4,X1) = domain(X3,X4,X2) ) ).
cnf(i_0_157_015,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_158_016,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_159_017,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_160_018,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_161_019,axiom,
( X1 != X2
| ~ ilf_type(X1,X3)
| ilf_type(X2,X3) ) ).
cnf(i_0_162_020,axiom,
( X1 != X2
| ~ ilf_type(X3,X1)
| ilf_type(X3,X2) ) ).
cnf(i_0_163_021,axiom,
( X1 != X2
| ~ relation_like(X1)
| relation_like(X2) ) ).
cnf(i_0_164_022,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_165,plain,
( ~ member(X1,X2)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| member(ordered_pair(X1,X1),identity_relation_of(X2)) ),
inference(equality_inference,[],[94]) ).
cnf(i_0_166,plain,
( subset(X1,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X1,set_type) ),
inference(equality_inference,[],[119]) ).
cnf(i_0_167,plain,
( subset(X1,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X1,set_type) ),
inference(equality_inference,[],[120]) ).
cnf(i_0_168,plain,
ilf_type(esk6_1(X1),subset_type(X1)),
inference(scs_inference,[],[i_0_140,i_0_122]) ).
cnf(i_0_169,plain,
( ~ ilf_type(X1,set_type)
| ilf_type(esk6_1(X1),subset_type(X1)) ),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_170,plain,
ilf_type(esk1_1(X1),identity_relation_of_type(X1)),
inference(scs_inference,[],[i_0_140,i_0_122,i_0_123]) ).
cnf(i_0_171,plain,
( ~ ilf_type(X1,set_type)
| ilf_type(esk1_1(X1),identity_relation_of_type(X1)) ),
inference(rename_variables,[],[i_0_123]) ).
cnf(i_0_172,plain,
subset(esk4_0,esk4_0),
inference(scs_inference,[],[i_0_140,i_0_142,i_0_122,i_0_123,i_0_135]) ).
cnf(i_0_173,plain,
( ~ ilf_type(X1,binary_relation_type)
| subset(X1,X1) ),
inference(rename_variables,[],[i_0_135]) ).
cnf(i_0_174,plain,
subset(X1,X1),
inference(scs_inference,[],[i_0_140,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136]) ).
cnf(i_0_175,plain,
( ~ ilf_type(X1,set_type)
| subset(X1,X1) ),
inference(rename_variables,[],[i_0_136]) ).
cnf(i_0_176,plain,
ilf_type(esk5_2(X1,X1),relation_type(X1,X1)),
inference(scs_inference,[],[i_0_140,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104]) ).
cnf(i_0_177,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ilf_type(esk5_2(X1,X2),relation_type(X2,X1)) ),
inference(rename_variables,[],[i_0_104]) ).
cnf(i_0_178,plain,
relation_like(esk4_0),
inference(scs_inference,[],[i_0_140,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126]) ).
cnf(i_0_179,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_180,plain,
( ~ ilf_type(X1,binary_relation_type)
| ~ ilf_type(X1,set_type)
| relation_like(X1) ),
inference(rename_variables,[],[i_0_126]) ).
cnf(i_0_181,plain,
ilf_type(range(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)),subset_type(esk4_0)),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79]) ).
cnf(i_0_182,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_183,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_184,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_79]) ).
cnf(i_0_185,plain,
ilf_type(domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)),subset_type(esk4_0)),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80]) ).
cnf(i_0_186,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_187,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_188,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| ilf_type(domain(X1,X2,X3),subset_type(X1)) ),
inference(rename_variables,[],[i_0_80]) ).
cnf(i_0_189,plain,
range(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)) = range_of(esk5_2(esk4_0,esk4_0)),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_187,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87]) ).
cnf(i_0_190,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_191,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_192,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| range(X1,X2,X3) = range_of(X3) ),
inference(rename_variables,[],[i_0_87]) ).
cnf(i_0_193,plain,
domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)) = domain_of(esk5_2(esk4_0,esk4_0)),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88]) ).
cnf(i_0_194,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_195,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_196,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| domain(X1,X2,X3) = domain_of(X3) ),
inference(rename_variables,[],[i_0_88]) ).
cnf(i_0_197,plain,
ilf_type(esk5_2(esk4_0,esk4_0),identity_relation_of_type(esk4_0)),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_194,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97]) ).
cnf(i_0_198,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_199,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_200,plain,
( ~ ilf_type(X1,relation_type(X2,X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ilf_type(X1,identity_relation_of_type(X2)) ),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_201,plain,
subset(range(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)),range_of(esk5_2(esk4_0,esk4_0))),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_194,i_0_199,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119]) ).
cnf(i_0_202,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_203,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_204,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| X2 != X1
| subset(X2,X1) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_205,plain,
subset(range_of(esk5_2(esk4_0,esk4_0)),range(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0))),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_194,i_0_199,i_0_202,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120]) ).
cnf(i_0_206,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_207,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_208,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| X2 != X1
| subset(X1,X2) ),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_209,plain,
range_of(esk5_2(esk4_0,esk4_0)) = range(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_194,i_0_199,i_0_202,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144]) ).
cnf(i_0_210,plain,
( X1 = domain_of(esk5_2(esk4_0,esk4_0))
| X1 != domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)) ),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_194,i_0_199,i_0_202,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144,i_0_145]) ).
cnf(i_0_211,plain,
( relation_like(domain_of(esk5_2(esk4_0,esk4_0)))
| esk4_0 != domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)) ),
inference(scs_inference,[],[i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_194,i_0_199,i_0_202,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144,i_0_145,i_0_163]) ).
cnf(i_0_212,plain,
( esk4_0 != domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0))
| ilf_type(esk15_0,relation_type(esk14_0,esk14_0)) ),
inference(scs_inference,[],[i_0_139,i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_207,i_0_194,i_0_199,i_0_202,i_0_206,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144,i_0_145,i_0_163,i_0_100]) ).
cnf(i_0_213,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_214,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_215,plain,
( ~ ilf_type(X1,identity_relation_of_type(X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ilf_type(X1,relation_type(X2,X2)) ),
inference(rename_variables,[],[i_0_100]) ).
cnf(i_0_216,plain,
( esk4_0 != domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0))
| esk14_0 = domain(esk14_0,esk14_0,esk15_0) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_207,i_0_213,i_0_194,i_0_199,i_0_202,i_0_206,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144,i_0_145,i_0_163,i_0_100,i_0_85]) ).
cnf(i_0_217,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_218,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X1,X3))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| X1 = domain(X1,X3,X2) ),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_219,plain,
( esk4_0 != domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0))
| subset(esk14_0,range(esk14_0,esk14_0,esk15_0)) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_207,i_0_213,i_0_217,i_0_194,i_0_199,i_0_202,i_0_206,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144,i_0_145,i_0_163,i_0_100,i_0_85,i_0_77]) ).
cnf(i_0_220,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_221,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X1,X3))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| subset(X1,range(X1,X3,X2)) ),
inference(rename_variables,[],[i_0_77]) ).
cnf(i_0_222,plain,
( esk4_0 != domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0))
| subset(esk14_0,domain(esk14_0,esk14_0,esk15_0)) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_207,i_0_213,i_0_217,i_0_220,i_0_194,i_0_199,i_0_202,i_0_206,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144,i_0_145,i_0_163,i_0_100,i_0_85,i_0_77,i_0_78]) ).
cnf(i_0_223,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_224,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X3,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| subset(X1,domain(X3,X1,X2)) ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_225,plain,
( esk4_0 != domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0))
| esk14_0 = range(esk14_0,esk14_0,esk15_0) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_207,i_0_213,i_0_217,i_0_220,i_0_223,i_0_194,i_0_199,i_0_202,i_0_206,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144,i_0_145,i_0_163,i_0_100,i_0_85,i_0_77,i_0_78,i_0_84]) ).
cnf(i_0_226,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_227,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X3,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| X1 = range(X3,X1,X2) ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_228,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_229,plain,
( ~ member(X1,X1)
| ~ empty(X1)
| esk4_0 != domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0))
| member(esk12_1(esk4_0),esk4_0) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_140,i_0_179,i_0_183,i_0_187,i_0_191,i_0_195,i_0_198,i_0_203,i_0_207,i_0_213,i_0_217,i_0_220,i_0_223,i_0_226,i_0_228,i_0_194,i_0_199,i_0_202,i_0_206,i_0_142,i_0_122,i_0_123,i_0_135,i_0_136,i_0_104,i_0_126,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_120,i_0_144,i_0_145,i_0_163,i_0_100,i_0_85,i_0_77,i_0_78,i_0_84,i_0_90,i_0_125,i_0_129,i_0_118]) ).
cnf(i_0_230,plain,
domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)) = domain_of(esk5_2(esk4_0,esk4_0)),
inference(equality_inference,[],[210]) ).
cnf(i_0_231,plain,
domain_of(esk5_2(esk4_0,esk4_0)) = domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0)),
inference(scs_inference,[],[i_0_193,i_0_144]) ).
cnf(i_0_232,plain,
ilf_type(esk6_1(cross_product(X1,X1)),relation_type(X1,X1)),
inference(scs_inference,[],[i_0_168,i_0_193,i_0_140,i_0_144,i_0_83]) ).
cnf(i_0_233,plain,
ilf_type(esk6_1(X1),subset_type(X1)),
inference(rename_variables,[],[i_0_168]) ).
cnf(i_0_234,plain,
( ~ ilf_type(X1,subset_type(cross_product(X2,X3)))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ilf_type(X1,relation_type(X2,X3)) ),
inference(rename_variables,[],[i_0_83]) ).
cnf(i_0_235,plain,
relation_like(esk6_1(cross_product(X1,X1))),
inference(scs_inference,[],[i_0_168,i_0_233,i_0_193,i_0_140,i_0_144,i_0_83,i_0_89]) ).
cnf(i_0_236,plain,
ilf_type(esk6_1(X1),subset_type(X1)),
inference(rename_variables,[],[i_0_168]) ).
cnf(i_0_237,plain,
( ~ ilf_type(X1,subset_type(cross_product(X2,X3)))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,set_type)
| relation_like(X1) ),
inference(rename_variables,[],[i_0_89]) ).
cnf(i_0_238,plain,
ilf_type(range(X1,X1,esk5_2(X1,X1)),subset_type(X1)),
inference(scs_inference,[],[i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_144,i_0_83,i_0_89,i_0_79]) ).
cnf(i_0_239,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_240,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_241,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_79]) ).
cnf(i_0_242,plain,
ilf_type(domain(X1,X1,esk5_2(X1,X1)),subset_type(X1)),
inference(scs_inference,[],[i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80]) ).
cnf(i_0_243,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_244,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_245,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| ilf_type(domain(X1,X2,X3),subset_type(X1)) ),
inference(rename_variables,[],[i_0_80]) ).
cnf(i_0_246,plain,
range(X1,X1,esk5_2(X1,X1)) = range_of(esk5_2(X1,X1)),
inference(scs_inference,[],[i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87]) ).
cnf(i_0_247,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_248,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_249,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| range(X1,X2,X3) = range_of(X3) ),
inference(rename_variables,[],[i_0_87]) ).
cnf(i_0_250,plain,
domain(X1,X1,esk5_2(X1,X1)) = domain_of(esk5_2(X1,X1)),
inference(scs_inference,[],[i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88]) ).
cnf(i_0_251,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_252,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_253,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| domain(X1,X2,X3) = domain_of(X3) ),
inference(rename_variables,[],[i_0_88]) ).
cnf(i_0_254,plain,
ilf_type(esk5_2(X1,X1),identity_relation_of_type(X1)),
inference(scs_inference,[],[i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_251,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97]) ).
cnf(i_0_255,plain,
ilf_type(esk5_2(X1,X1),relation_type(X1,X1)),
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_256,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_257,plain,
( ~ ilf_type(X1,relation_type(X2,X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ilf_type(X1,identity_relation_of_type(X2)) ),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_258,plain,
ilf_type(esk5_2(X1,X2),relation_type(X2,X1)),
inference(scs_inference,[],[i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_251,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104]) ).
cnf(i_0_259,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ilf_type(esk5_2(X1,X2),relation_type(X2,X1)) ),
inference(rename_variables,[],[i_0_104]) ).
cnf(i_0_260,plain,
( empty(X1)
| member(esk13_1(X1),X1) ),
inference(scs_inference,[],[i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_251,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124]) ).
cnf(i_0_261,plain,
( ~ ilf_type(X1,set_type)
| member(esk13_1(X1),X1)
| empty(X1) ),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_262,plain,
ilf_type(esk15_0,relation_type(esk14_0,esk14_0)),
inference(scs_inference,[],[i_0_139,i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_251,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124,i_0_100]) ).
cnf(i_0_263,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_264,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_265,plain,
( ~ ilf_type(X1,identity_relation_of_type(X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ilf_type(X1,relation_type(X2,X2)) ),
inference(rename_variables,[],[i_0_100]) ).
cnf(i_0_266,plain,
( empty(esk15_0)
| ~ empty(esk15_0) ),
inference(scs_inference,[],[i_0_139,i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_263,i_0_251,i_0_264,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124,i_0_100,i_0_118]) ).
cnf(i_0_267,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_268,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_269,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ member(X2,X1)
| ~ empty(X1) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_270,plain,
( empty(esk15_0)
| ilf_type(esk13_1(esk15_0),member_type(esk15_0)) ),
inference(scs_inference,[],[i_0_139,i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_263,i_0_268,i_0_251,i_0_264,i_0_267,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124,i_0_100,i_0_118,i_0_114]) ).
cnf(i_0_271,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_272,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_273,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_114]) ).
cnf(i_0_274,plain,
( member(ordered_pair(esk13_1(esk15_0),esk13_1(esk15_0)),identity_relation_of(esk15_0))
| empty(esk15_0) ),
inference(scs_inference,[],[i_0_139,i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_263,i_0_268,i_0_272,i_0_251,i_0_264,i_0_267,i_0_271,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124,i_0_100,i_0_118,i_0_114,i_0_165]) ).
cnf(i_0_275,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_276,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_277,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X2,set_type)
| member(ordered_pair(X2,X2),identity_relation_of(X1))
| ~ member(X2,X1) ),
inference(rename_variables,[],[i_0_165]) ).
cnf(i_0_278,plain,
( empty(esk15_0)
| esk14_0 = domain(esk14_0,esk14_0,esk15_0) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_263,i_0_268,i_0_272,i_0_276,i_0_251,i_0_264,i_0_267,i_0_271,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124,i_0_100,i_0_118,i_0_114,i_0_165,i_0_85]) ).
cnf(i_0_279,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_280,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X1,X3))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| X1 = domain(X1,X3,X2) ),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_281,plain,
( empty(esk15_0)
| subset(esk14_0,range(esk14_0,esk14_0,esk15_0)) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_263,i_0_268,i_0_272,i_0_276,i_0_279,i_0_251,i_0_264,i_0_267,i_0_271,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124,i_0_100,i_0_118,i_0_114,i_0_165,i_0_85,i_0_77]) ).
cnf(i_0_282,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_283,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X1,X3))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| subset(X1,range(X1,X3,X2)) ),
inference(rename_variables,[],[i_0_77]) ).
cnf(i_0_284,plain,
( empty(esk15_0)
| subset(esk14_0,domain(esk14_0,esk14_0,esk15_0)) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_263,i_0_268,i_0_272,i_0_276,i_0_279,i_0_282,i_0_251,i_0_264,i_0_267,i_0_271,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124,i_0_100,i_0_118,i_0_114,i_0_165,i_0_85,i_0_77,i_0_78]) ).
cnf(i_0_285,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_286,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X3,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| subset(X1,domain(X3,X1,X2)) ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_287,plain,
( empty(esk15_0)
| esk14_0 = range(esk14_0,esk14_0,esk15_0) ),
inference(scs_inference,[],[i_0_138,i_0_139,i_0_176,i_0_168,i_0_233,i_0_193,i_0_140,i_0_240,i_0_244,i_0_248,i_0_252,i_0_256,i_0_263,i_0_268,i_0_272,i_0_276,i_0_279,i_0_282,i_0_285,i_0_251,i_0_264,i_0_267,i_0_271,i_0_144,i_0_83,i_0_89,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_104,i_0_124,i_0_100,i_0_118,i_0_114,i_0_165,i_0_85,i_0_77,i_0_78,i_0_84]) ).
cnf(i_0_288,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_289,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X3,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| X1 = range(X3,X1,X2) ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_290,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_292,plain,
range_of(esk5_2(X1,X1)) = range(X1,X1,esk5_2(X1,X1)),
inference(scs_inference,[],[i_0_246,i_0_144]) ).
cnf(i_0_293,plain,
ilf_type(esk6_1(cross_product(X1,X1)),binary_relation_type),
inference(scs_inference,[],[i_0_246,i_0_235,i_0_140,i_0_144,i_0_129]) ).
cnf(i_0_294,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_295,plain,
( ~ ilf_type(X1,set_type)
| ilf_type(X1,binary_relation_type)
| ~ relation_like(X1) ),
inference(rename_variables,[],[i_0_129]) ).
cnf(i_0_296,plain,
ilf_type(range(esk14_0,esk14_0,esk15_0),subset_type(esk14_0)),
inference(scs_inference,[],[i_0_262,i_0_246,i_0_235,i_0_140,i_0_294,i_0_144,i_0_129,i_0_79]) ).
cnf(i_0_297,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_298,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_299,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_79]) ).
cnf(i_0_300,plain,
ilf_type(domain(esk14_0,esk14_0,esk15_0),subset_type(esk14_0)),
inference(scs_inference,[],[i_0_262,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_144,i_0_129,i_0_79,i_0_80]) ).
cnf(i_0_301,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_302,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_303,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| ilf_type(domain(X1,X2,X3),subset_type(X1)) ),
inference(rename_variables,[],[i_0_80]) ).
cnf(i_0_304,plain,
range(esk14_0,esk14_0,esk15_0) = range_of(esk15_0),
inference(scs_inference,[],[i_0_262,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87]) ).
cnf(i_0_305,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_306,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_307,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| range(X1,X2,X3) = range_of(X3) ),
inference(rename_variables,[],[i_0_87]) ).
cnf(i_0_308,plain,
domain(esk14_0,esk14_0,esk15_0) = domain_of(esk15_0),
inference(scs_inference,[],[i_0_262,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_306,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87,i_0_88]) ).
cnf(i_0_309,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_310,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_311,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,relation_type(X1,X2))
| domain(X1,X2,X3) = domain_of(X3) ),
inference(rename_variables,[],[i_0_88]) ).
cnf(i_0_312,plain,
ilf_type(esk6_1(cross_product(X1,X1)),identity_relation_of_type(X1)),
inference(scs_inference,[],[i_0_262,i_0_232,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_306,i_0_310,i_0_309,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97]) ).
cnf(i_0_313,plain,
ilf_type(esk6_1(cross_product(X1,X1)),relation_type(X1,X1)),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_314,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_315,plain,
( ~ ilf_type(X1,relation_type(X2,X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ilf_type(X1,identity_relation_of_type(X2)) ),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_316,plain,
subset(domain_of(esk5_2(esk4_0,esk4_0)),domain(esk4_0,esk4_0,esk5_2(esk4_0,esk4_0))),
inference(scs_inference,[],[i_0_231,i_0_262,i_0_232,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_306,i_0_310,i_0_314,i_0_309,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119]) ).
cnf(i_0_317,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_318,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_319,plain,
( ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| X2 != X1
| subset(X2,X1) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_320,plain,
esk14_0 = domain(esk14_0,esk14_0,esk15_0),
inference(scs_inference,[],[i_0_138,i_0_231,i_0_262,i_0_232,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_306,i_0_310,i_0_314,i_0_318,i_0_309,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_85]) ).
cnf(i_0_321,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_322,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X1,X3))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| X1 = domain(X1,X3,X2) ),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_323,plain,
subset(esk14_0,range(esk14_0,esk14_0,esk15_0)),
inference(scs_inference,[],[i_0_138,i_0_231,i_0_262,i_0_232,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_306,i_0_310,i_0_314,i_0_318,i_0_321,i_0_309,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_85,i_0_77]) ).
cnf(i_0_324,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_325,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X1,X3))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| subset(X1,range(X1,X3,X2)) ),
inference(rename_variables,[],[i_0_77]) ).
cnf(i_0_326,plain,
subset(esk14_0,domain(esk14_0,esk14_0,esk15_0)),
inference(scs_inference,[],[i_0_138,i_0_231,i_0_262,i_0_232,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_306,i_0_310,i_0_314,i_0_318,i_0_321,i_0_324,i_0_309,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_85,i_0_77,i_0_78]) ).
cnf(i_0_327,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_328,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X3,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| subset(X1,domain(X3,X1,X2)) ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_329,plain,
esk14_0 = range(esk14_0,esk14_0,esk15_0),
inference(scs_inference,[],[i_0_138,i_0_231,i_0_262,i_0_232,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_306,i_0_310,i_0_314,i_0_318,i_0_321,i_0_324,i_0_327,i_0_309,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_85,i_0_77,i_0_78,i_0_84]) ).
cnf(i_0_330,plain,
ilf_type(X1,set_type),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_331,plain,
( ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X3,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| X1 = range(X3,X1,X2) ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_332,plain,
$false,
inference(scs_inference,[],[i_0_138,i_0_231,i_0_262,i_0_232,i_0_246,i_0_235,i_0_140,i_0_294,i_0_298,i_0_302,i_0_306,i_0_310,i_0_314,i_0_318,i_0_321,i_0_324,i_0_327,i_0_309,i_0_144,i_0_129,i_0_79,i_0_80,i_0_87,i_0_88,i_0_97,i_0_119,i_0_85,i_0_77,i_0_78,i_0_84,i_0_90]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET677+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.14/0.33 % Computer : n023.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 02:32:39 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.35/1.61 % Version : CSE_E---1.7
% 0.35/1.61 % Problem : theBenchmark.p
% 0.35/1.61 % SZS status Theorem for theBenchmark.p
% 0.35/1.61 % SZS output start CNFRefutation
% See solution above
% 0.65/2.02 % Total time : 1.272s
%------------------------------------------------------------------------------