%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET665+3 : TPTP v9.2.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n017.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:16 PM UTC 2026
% Result : Theorem 136.32s 101.41s
% Output : CNFRefutation 137.12s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_142)
% Comments :
%------------------------------------------------------------------------------
fof(p23,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/sandbox2/benchmark/theBenchmark.p',p23) ).
fof(p25,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ( empty(X1)
<=> ! [X2] :
( ilf_type(X2,set_type)
=> ~ member(X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p25) ).
fof(prove_relset_1_28,conjecture,
! [X1] :
( ilf_type(X1,set_type)
=> subset(identity_relation_of(X1),cross_product(X1,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_relset_1_28) ).
fof(p24,axiom,
! [X1] :
( ( ~ empty(X1)
& ilf_type(X1,set_type) )
=> ? [X2] : ilf_type(X2,member_type(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p24) ).
fof(p11,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ( ilf_type(X1,binary_relation_type)
<=> ( relation_like(X1)
& ilf_type(X1,set_type) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p11) ).
fof(p22,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ( ~ empty(power_set(X1))
& ilf_type(power_set(X1),set_type) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p22) ).
fof(p5,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ! [X3] :
( ilf_type(X3,set_type)
=> ( member(X3,cross_product(X1,X2))
<=> ? [X4] :
( ilf_type(X4,set_type)
& ? [X5] :
( ilf_type(X5,set_type)
& member(X4,X1)
& member(X5,X2)
& X3 = ordered_pair(X4,X5) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p5) ).
fof(p1,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/sandbox2/benchmark/theBenchmark.p',p1) ).
fof(p3,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ! [X3] :
( ilf_type(X3,set_type)
=> ! [X4] :
( ilf_type(X4,set_type)
=> ( member(ordered_pair(X1,X2),cross_product(X3,X4))
<=> ( member(X1,X3)
& member(X2,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3) ).
fof(p13,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/sandbox2/benchmark/theBenchmark.p',p13) ).
fof(p20,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/sandbox2/benchmark/theBenchmark.p',p20) ).
fof(p7,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/sandbox2/benchmark/theBenchmark.p',p7) ).
fof(p2,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/sandbox2/benchmark/theBenchmark.p',p2) ).
fof(p19,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/sandbox2/benchmark/theBenchmark.p',p19) ).
fof(p21,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/sandbox2/benchmark/theBenchmark.p',p21) ).
fof(p9,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/sandbox2/benchmark/theBenchmark.p',p9) ).
fof(p17,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/sandbox2/benchmark/theBenchmark.p',p17) ).
fof(p14,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ? [X3] : ilf_type(X3,relation_type(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p14) ).
fof(p4,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ilf_type(cross_product(X1,X2),relation_type(X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4) ).
fof(p6,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ilf_type(cross_product(X1,X2),set_type) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p6) ).
fof(p10,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ! [X2] :
( ilf_type(X2,set_type)
=> ilf_type(ordered_pair(X1,X2),set_type) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10) ).
fof(p18,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ? [X2] : ilf_type(X2,subset_type(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p18) ).
fof(p8,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> ilf_type(identity_relation_of(X1),binary_relation_type) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p8) ).
fof(p15,axiom,
! [X1] :
( ilf_type(X1,set_type)
=> subset(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p15) ).
fof(p16,axiom,
! [X1] :
( ilf_type(X1,binary_relation_type)
=> subset(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p16) ).
fof(p26,axiom,
! [X1] :
( ( empty(X1)
& ilf_type(X1,set_type) )
=> relation_like(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p26) ).
fof(p27,axiom,
! [X1] : ilf_type(X1,set_type),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p27) ).
fof(p12,axiom,
? [X1] : ilf_type(X1,binary_relation_type),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p12) ).
fof(i_0_28,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)],[p23]) ).
fof(i_0_29,plain,
! [X1] :
( ilf_type(X1,set_type)
=> ( empty(X1)
<=> ! [X2] :
( ilf_type(X2,set_type)
=> ~ member(X2,X1) ) ) ),
inference(fof_simplification,[status(thm)],[p25]) ).
fof(i_0_30,negated_conjecture,
~ ! [X1] :
( ilf_type(X1,set_type)
=> subset(identity_relation_of(X1),cross_product(X1,X1)) ),
inference(assume_negation,[status(cth)],[prove_relset_1_28]) ).
fof(i_0_31,plain,
! [X1] :
( ( ~ empty(X1)
& ilf_type(X1,set_type) )
=> ? [X2] : ilf_type(X2,member_type(X1)) ),
inference(fof_simplification,[status(thm)],[p24]) ).
fof(i_0_32,plain,
! [X104] :
( ( relation_like(X104)
| ~ ilf_type(X104,binary_relation_type)
| ~ ilf_type(X104,set_type) )
& ( ilf_type(X104,set_type)
| ~ ilf_type(X104,binary_relation_type)
| ~ ilf_type(X104,set_type) )
& ( ~ relation_like(X104)
| ~ ilf_type(X104,set_type)
| ilf_type(X104,binary_relation_type)
| ~ ilf_type(X104,set_type) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p11])])]) ).
fof(i_0_33,plain,
! [X1] :
( ilf_type(X1,set_type)
=> ( ~ empty(power_set(X1))
& ilf_type(power_set(X1),set_type) ) ),
inference(fof_simplification,[status(thm)],[p22]) ).
fof(i_0_34,plain,
! [X85,X86,X87,X90,X91] :
( ( ilf_type(esk3_3(X85,X86,X87),set_type)
| ~ member(X87,cross_product(X85,X86))
| ~ ilf_type(X87,set_type)
| ~ ilf_type(X86,set_type)
| ~ ilf_type(X85,set_type) )
& ( ilf_type(esk4_3(X85,X86,X87),set_type)
| ~ member(X87,cross_product(X85,X86))
| ~ ilf_type(X87,set_type)
| ~ ilf_type(X86,set_type)
| ~ ilf_type(X85,set_type) )
& ( member(esk3_3(X85,X86,X87),X85)
| ~ member(X87,cross_product(X85,X86))
| ~ ilf_type(X87,set_type)
| ~ ilf_type(X86,set_type)
| ~ ilf_type(X85,set_type) )
& ( member(esk4_3(X85,X86,X87),X86)
| ~ member(X87,cross_product(X85,X86))
| ~ ilf_type(X87,set_type)
| ~ ilf_type(X86,set_type)
| ~ ilf_type(X85,set_type) )
& ( X87 = ordered_pair(esk3_3(X85,X86,X87),esk4_3(X85,X86,X87))
| ~ member(X87,cross_product(X85,X86))
| ~ ilf_type(X87,set_type)
| ~ ilf_type(X86,set_type)
| ~ ilf_type(X85,set_type) )
& ( ~ ilf_type(X90,set_type)
| ~ ilf_type(X91,set_type)
| ~ member(X90,X85)
| ~ member(X91,X86)
| X87 != ordered_pair(X90,X91)
| member(X87,cross_product(X85,X86))
| ~ ilf_type(X87,set_type)
| ~ ilf_type(X86,set_type)
| ~ ilf_type(X85,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)],[p5])])])])]) ).
fof(i_0_35,plain,
! [X70,X71,X72,X73] :
( ( ~ subset(X70,X71)
| ~ ilf_type(X72,set_type)
| ~ ilf_type(X73,set_type)
| ~ member(ordered_pair(X72,X73),X70)
| member(ordered_pair(X72,X73),X71)
| ~ ilf_type(X71,binary_relation_type)
| ~ ilf_type(X70,binary_relation_type) )
& ( ilf_type(esk1_2(X70,X71),set_type)
| subset(X70,X71)
| ~ ilf_type(X71,binary_relation_type)
| ~ ilf_type(X70,binary_relation_type) )
& ( ilf_type(esk2_2(X70,X71),set_type)
| subset(X70,X71)
| ~ ilf_type(X71,binary_relation_type)
| ~ ilf_type(X70,binary_relation_type) )
& ( member(ordered_pair(esk1_2(X70,X71),esk2_2(X70,X71)),X70)
| subset(X70,X71)
| ~ ilf_type(X71,binary_relation_type)
| ~ ilf_type(X70,binary_relation_type) )
& ( ~ member(ordered_pair(esk1_2(X70,X71),esk2_2(X70,X71)),X71)
| subset(X70,X71)
| ~ ilf_type(X71,binary_relation_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)],[p1])])])])]) ).
fof(i_0_36,plain,
! [X79,X80,X81,X82] :
( ( member(X79,X81)
| ~ member(ordered_pair(X79,X80),cross_product(X81,X82))
| ~ ilf_type(X82,set_type)
| ~ ilf_type(X81,set_type)
| ~ ilf_type(X80,set_type)
| ~ ilf_type(X79,set_type) )
& ( member(X80,X82)
| ~ member(ordered_pair(X79,X80),cross_product(X81,X82))
| ~ ilf_type(X82,set_type)
| ~ ilf_type(X81,set_type)
| ~ ilf_type(X80,set_type)
| ~ ilf_type(X79,set_type) )
& ( ~ member(X79,X81)
| ~ member(X80,X82)
| member(ordered_pair(X79,X80),cross_product(X81,X82))
| ~ ilf_type(X82,set_type)
| ~ ilf_type(X81,set_type)
| ~ ilf_type(X80,set_type)
| ~ ilf_type(X79,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_37,plain,
! [X106,X107,X108,X109] :
( ( ~ ilf_type(X108,subset_type(cross_product(X106,X107)))
| ilf_type(X108,relation_type(X106,X107))
| ~ ilf_type(X107,set_type)
| ~ ilf_type(X106,set_type) )
& ( ~ ilf_type(X109,relation_type(X106,X107))
| ilf_type(X109,subset_type(cross_product(X106,X107)))
| ~ ilf_type(X107,set_type)
| ~ ilf_type(X106,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p13])])])]) ).
fof(i_0_38,plain,
! [X126,X127,X128] :
( ~ ilf_type(X126,set_type)
| ~ ilf_type(X127,set_type)
| ~ ilf_type(X128,subset_type(cross_product(X126,X127)))
| relation_like(X128) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p20])])]) ).
fof(i_0_39,plain,
! [X94,X95,X96] :
( ( member(X95,X94)
| ~ member(ordered_pair(X95,X96),identity_relation_of(X94))
| ~ ilf_type(X96,set_type)
| ~ ilf_type(X95,set_type)
| ~ ilf_type(X94,set_type) )
& ( X95 = X96
| ~ member(ordered_pair(X95,X96),identity_relation_of(X94))
| ~ ilf_type(X96,set_type)
| ~ ilf_type(X95,set_type)
| ~ ilf_type(X94,set_type) )
& ( ~ member(X95,X94)
| X95 != X96
| member(ordered_pair(X95,X96),identity_relation_of(X94))
| ~ ilf_type(X96,set_type)
| ~ ilf_type(X95,set_type)
| ~ ilf_type(X94,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p7])])])]) ).
fof(i_0_40,plain,
! [X76,X77,X78] :
( ( member(X77,X76)
| ~ member(ordered_pair(X77,X78),identity_relation_of(X76))
| ~ ilf_type(X78,set_type)
| ~ ilf_type(X77,set_type)
| ~ ilf_type(X76,set_type) )
& ( X77 = X78
| ~ member(ordered_pair(X77,X78),identity_relation_of(X76))
| ~ ilf_type(X78,set_type)
| ~ ilf_type(X77,set_type)
| ~ ilf_type(X76,set_type) )
& ( ~ member(X77,X76)
| X77 != X78
| member(ordered_pair(X77,X78),identity_relation_of(X76))
| ~ ilf_type(X78,set_type)
| ~ ilf_type(X77,set_type)
| ~ ilf_type(X76,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_41,plain,
! [X119,X120,X124,X125] :
( ( ilf_type(esk9_2(X119,X120),set_type)
| ~ member(X120,X119)
| ~ ilf_type(X120,set_type)
| ~ relation_like(X119)
| ~ ilf_type(X119,set_type) )
& ( ilf_type(esk10_2(X119,X120),set_type)
| ~ member(X120,X119)
| ~ ilf_type(X120,set_type)
| ~ relation_like(X119)
| ~ ilf_type(X119,set_type) )
& ( X120 = ordered_pair(esk9_2(X119,X120),esk10_2(X119,X120))
| ~ member(X120,X119)
| ~ ilf_type(X120,set_type)
| ~ relation_like(X119)
| ~ ilf_type(X119,set_type) )
& ( ilf_type(esk11_1(X119),set_type)
| relation_like(X119)
| ~ ilf_type(X119,set_type) )
& ( member(esk11_1(X119),X119)
| relation_like(X119)
| ~ ilf_type(X119,set_type) )
& ( ~ ilf_type(X124,set_type)
| ~ ilf_type(X125,set_type)
| esk11_1(X119) != ordered_pair(X124,X125)
| relation_like(X119)
| ~ ilf_type(X119,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)],[p19])])])])]) ).
fof(i_0_42,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(esk12_2(X129,X130),set_type)
| member(X129,power_set(X130))
| ~ ilf_type(X130,set_type)
| ~ ilf_type(X129,set_type) )
& ( member(esk12_2(X129,X130),X129)
| member(X129,power_set(X130))
| ~ ilf_type(X130,set_type)
| ~ ilf_type(X129,set_type) )
& ( ~ member(esk12_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)],[p21])])])])]) ).
fof(i_0_43,plain,
! [X98,X99,X100] :
( ( ~ subset(X98,X99)
| ~ ilf_type(X100,set_type)
| ~ member(X100,X98)
| member(X100,X99)
| ~ ilf_type(X99,set_type)
| ~ ilf_type(X98,set_type) )
& ( ilf_type(esk5_2(X98,X99),set_type)
| subset(X98,X99)
| ~ ilf_type(X99,set_type)
| ~ ilf_type(X98,set_type) )
& ( member(esk5_2(X98,X99),X98)
| subset(X98,X99)
| ~ ilf_type(X99,set_type)
| ~ ilf_type(X98,set_type) )
& ( ~ member(esk5_2(X98,X99),X99)
| subset(X98,X99)
| ~ ilf_type(X99,set_type)
| ~ ilf_type(X98,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)],[p9])])])])]) ).
fof(i_0_44,plain,
! [X115,X116] :
( ( ~ ilf_type(X116,subset_type(X115))
| ilf_type(X116,member_type(power_set(X115)))
| ~ ilf_type(X116,set_type)
| ~ ilf_type(X115,set_type) )
& ( ~ ilf_type(X116,member_type(power_set(X115)))
| ilf_type(X116,subset_type(X115))
| ~ ilf_type(X116,set_type)
| ~ ilf_type(X115,set_type) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p17])])])]) ).
fof(i_0_45,plain,
! [X110,X111] :
( ~ ilf_type(X110,set_type)
| ~ ilf_type(X111,set_type)
| ilf_type(esk7_2(X110,X111),relation_type(X111,X110)) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p14])])])]) ).
fof(i_0_46,plain,
! [X83,X84] :
( ~ ilf_type(X83,set_type)
| ~ ilf_type(X84,set_type)
| ilf_type(cross_product(X83,X84),relation_type(X83,X84)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p4])])]) ).
fof(i_0_47,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_28])])])]) ).
fof(i_0_48,plain,
! [X92,X93] :
( ~ ilf_type(X92,set_type)
| ~ ilf_type(X93,set_type)
| ilf_type(cross_product(X92,X93),set_type) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p6])])]) ).
fof(i_0_49,plain,
! [X102,X103] :
( ~ ilf_type(X102,set_type)
| ~ ilf_type(X103,set_type)
| ilf_type(ordered_pair(X102,X103),set_type) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p10])])]) ).
fof(i_0_50,plain,
! [X138,X139] :
( ( ~ empty(X138)
| ~ ilf_type(X139,set_type)
| ~ member(X139,X138)
| ~ ilf_type(X138,set_type) )
& ( ilf_type(esk14_1(X138),set_type)
| empty(X138)
| ~ ilf_type(X138,set_type) )
& ( member(esk14_1(X138),X138)
| empty(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)],[i_0_29])])])])]) ).
fof(i_0_51,negated_conjecture,
( ilf_type(esk15_0,set_type)
& ~ subset(identity_relation_of(esk15_0),cross_product(esk15_0,esk15_0)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_30])])]) ).
fof(i_0_52,plain,
! [X136] :
( empty(X136)
| ~ ilf_type(X136,set_type)
| ilf_type(esk13_1(X136),member_type(X136)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_31])])]) ).
fof(i_0_53,plain,
! [X117] :
( ~ ilf_type(X117,set_type)
| ilf_type(esk8_1(X117),subset_type(X117)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p18])])]) ).
cnf(i_0_54,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_32]) ).
fof(i_0_55,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_33])])]) ).
fof(i_0_56,plain,
! [X97] :
( ~ ilf_type(X97,set_type)
| ilf_type(identity_relation_of(X97),binary_relation_type) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p8])]) ).
fof(i_0_57,plain,
! [X113] :
( ~ ilf_type(X113,set_type)
| subset(X113,X113) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p15])]) ).
fof(i_0_58,plain,
! [X114] :
( ~ ilf_type(X114,binary_relation_type)
| subset(X114,X114) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p16])]) ).
fof(i_0_59,plain,
! [X141] :
( ~ empty(X141)
| ~ ilf_type(X141,set_type)
| relation_like(X141) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p26])]) ).
fof(i_0_60,plain,
! [X142] : ilf_type(X142,set_type),
inference(variable_rename,[status(thm)],[p27]) ).
fof(i_0_61,plain,
ilf_type(esk6_0,binary_relation_type),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[p12])]) ).
cnf(i_0_62,plain,
( X1 = ordered_pair(esk3_3(X2,X3,X1),esk4_3(X2,X3,X1))
| ~ member(X1,cross_product(X2,X3))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_63,plain,
( subset(X1,X2)
| ~ member(ordered_pair(esk1_2(X1,X2),esk2_2(X1,X2)),X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_64,plain,
( member(esk4_3(X1,X2,X3),X2)
| ~ member(X3,cross_product(X1,X2))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_65,plain,
( member(esk3_3(X1,X2,X3),X1)
| ~ member(X3,cross_product(X1,X2))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_66,plain,
( ilf_type(esk4_3(X1,X2,X3),set_type)
| ~ member(X3,cross_product(X1,X2))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_67,plain,
( ilf_type(esk3_3(X1,X2,X3),set_type)
| ~ member(X3,cross_product(X1,X2))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_68,plain,
( member(X5,cross_product(X3,X4))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| ~ member(X1,X3)
| ~ member(X2,X4)
| X5 != ordered_pair(X1,X2)
| ~ ilf_type(X5,set_type)
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X3,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_69,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_35]),
[final] ).
cnf(i_0_70,plain,
( member(X1,X2)
| ~ member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_71,plain,
( member(X1,X2)
| ~ member(ordered_pair(X3,X1),cross_product(X4,X2))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X3,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_72,plain,
( member(ordered_pair(esk1_2(X1,X2),esk2_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_35]),
[final] ).
cnf(i_0_73,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] ).
cnf(i_0_74,plain,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4)
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_75,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] ).
cnf(i_0_76,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_38]),
[final] ).
cnf(i_0_77,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_39]),
[final] ).
cnf(i_0_78,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_40]),
[final] ).
cnf(i_0_79,plain,
( X1 = ordered_pair(esk9_2(X2,X1),esk10_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_41]),
[final] ).
cnf(i_0_80,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_39]),
[final] ).
cnf(i_0_81,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_40]),
[final] ).
cnf(i_0_82,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_39]),
[final] ).
cnf(i_0_83,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_40]),
[final] ).
cnf(i_0_84,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_42]),
[final] ).
cnf(i_0_85,plain,
( member(X1,power_set(X2))
| ~ member(esk12_2(X1,X2),X2)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_86,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_43]),
[final] ).
cnf(i_0_87,plain,
( subset(X1,X2)
| ~ member(esk5_2(X1,X2),X2)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_88,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_44]),
[final] ).
cnf(i_0_89,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_41]),
[final] ).
cnf(i_0_90,plain,
( ilf_type(esk9_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_41]),
[final] ).
cnf(i_0_91,plain,
( ilf_type(esk7_2(X1,X2),relation_type(X2,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_92,plain,
( ilf_type(cross_product(X1,X2),relation_type(X1,X2))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_93,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_44]),
[final] ).
cnf(i_0_94,plain,
( member(esk12_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_42]),
[final] ).
cnf(i_0_95,plain,
( ilf_type(esk12_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_42]),
[final] ).
cnf(i_0_96,plain,
( member(esk5_2(X1,X2),X1)
| subset(X1,X2)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_97,plain,
( relation_like(X3)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X2,set_type)
| esk11_1(X3) != ordered_pair(X1,X2)
| ~ ilf_type(X3,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_98,plain,
( ilf_type(esk5_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_43]),
[final] ).
cnf(i_0_99,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_35]),
[final] ).
cnf(i_0_100,plain,
( ilf_type(esk1_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_35]),
[final] ).
cnf(i_0_101,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_47]),
[final] ).
cnf(i_0_102,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_47]),
[final] ).
cnf(i_0_103,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_48]),
[final] ).
cnf(i_0_104,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_49]),
[final] ).
cnf(i_0_105,plain,
( ~ empty(X1)
| ~ ilf_type(X2,set_type)
| ~ member(X2,X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_106,negated_conjecture,
~ subset(identity_relation_of(esk15_0),cross_product(esk15_0,esk15_0)),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_107,plain,
( empty(X1)
| ilf_type(esk13_1(X1),member_type(X1))
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_108,plain,
( ilf_type(esk8_1(X1),subset_type(X1))
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_109,plain,
( member(esk14_1(X1),X1)
| empty(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_110,plain,
( member(esk11_1(X1),X1)
| relation_like(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_111,plain,
( relation_like(X1)
| ~ ilf_type(X1,binary_relation_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_112,plain,
( ilf_type(esk14_1(X1),set_type)
| empty(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_113,plain,
( ilf_type(esk11_1(X1),set_type)
| relation_like(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_114,plain,
( ilf_type(X1,binary_relation_type)
| ~ relation_like(X1)
| ~ ilf_type(X1,set_type) ),
inference(cn,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_115,plain,
( ilf_type(power_set(X1),set_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_116,plain,
( ilf_type(identity_relation_of(X1),binary_relation_type)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_117,plain,
( ~ empty(power_set(X1))
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_118,plain,
( subset(X1,X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_119,plain,
( subset(X1,X1)
| ~ ilf_type(X1,binary_relation_type) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_120,plain,
( relation_like(X1)
| ~ empty(X1)
| ~ ilf_type(X1,set_type) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_121,plain,
ilf_type(X1,set_type),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_122,negated_conjecture,
ilf_type(esk15_0,set_type),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_123,plain,
ilf_type(esk6_0,binary_relation_type),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_124,axiom,
X1 = X1 ).
cnf(i_0_125,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_126,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_127,axiom,
( X1 != X2
| ordered_pair(X1,X3) = ordered_pair(X2,X3) ) ).
cnf(i_0_128,axiom,
( X1 != X2
| ordered_pair(X3,X1) = ordered_pair(X3,X2) ) ).
cnf(i_0_129,axiom,
( X1 != X2
| esk11_1(X1) = esk11_1(X2) ) ).
cnf(i_0_130,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_131,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_132,axiom,
( X1 != X2
| ~ ilf_type(X1,X3)
| ilf_type(X2,X3) ) ).
cnf(i_0_133,axiom,
( X1 != X2
| ~ ilf_type(X3,X1)
| ilf_type(X3,X2) ) ).
cnf(i_0_134,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_135,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_136,axiom,
( X1 != X2
| ~ relation_like(X1)
| relation_like(X2) ) ).
cnf(i_0_137,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_13443,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_13551,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_13568,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13584,plain,
ilf_type(esk6_0,binary_relation_type),
inference(equality_inference,[],[13581]) ).
cnf(i_0_13603,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13612,plain,
ilf_type(esk6_0,binary_relation_type),
inference(equality_inference,[],[13607]) ).
cnf(i_0_13633,plain,
ilf_type(X1,set_type),
inference(equality_inference,[],[13615]) ).
cnf(i_0_13649,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_13651,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13671,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13685,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_13700,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_13715,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13747,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13770,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13773,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13803,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_13852,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13943,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_13949,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13955,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13970,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_13977,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_13994,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14028,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14041,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14077,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14090,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14094,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14096,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14101,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14136,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14166,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14218,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14243,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14297,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14321,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14330,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14359,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14368,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14383,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14436,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14443,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14453,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14461,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14462,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14496,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14576,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14649,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14672,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14673,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14681,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14685,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14687,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14718,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14728,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14733,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14757,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14773,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14878,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_14908,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14919,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_14971,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_15016,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_15038,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_15056,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_15061,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_15071,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_15089,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_15091,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_15113,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_15139,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_15145,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_15171,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_15192,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(rename_variables,[],[i_0_13130]) ).
cnf(i_0_183,plain,
~ subset(identity_relation_of(esk15_0),cross_product(esk15_0,esk15_0)),
inference(equality_inference,[],[159]) ).
cnf(i_0_184,plain,
identity_relation_of(esk15_0) != cross_product(esk15_0,esk15_0),
inference(scs_inference,[],[i_0_142,i_0_159]) ).
cnf(i_0_186,plain,
ilf_type(esk8_1(cross_product(esk15_0,esk15_0)),binary_relation_type),
inference(scs_inference,[],[i_0_142,i_0_156,i_0_121,i_0_159,i_0_114]) ).
cnf(i_0_189,plain,
ilf_type(esk7_2(X1,X1),relation_type(X1,X1)),
inference(scs_inference,[],[i_0_142,i_0_156,i_0_121,i_0_187,i_0_159,i_0_114,i_0_91]) ).
cnf(i_0_191,plain,
ilf_type(esk8_1(cross_product(X1,X1)),relation_type(X1,X1)),
inference(scs_inference,[],[i_0_142,i_0_140,i_0_156,i_0_121,i_0_187,i_0_159,i_0_114,i_0_91,i_0_73]) ).
cnf(i_0_194,plain,
relation_like(esk8_1(cross_product(X1,X1))),
inference(scs_inference,[],[i_0_142,i_0_140,i_0_192,i_0_156,i_0_121,i_0_187,i_0_159,i_0_114,i_0_91,i_0_73,i_0_76]) ).
cnf(i_0_13132,plain,
ilf_type(cross_product(X1,X1),subset_type(cross_product(X1,X1))),
inference(scs_inference,[],[i_0_148,i_0_121,i_0_117,i_0_116,i_0_75]) ).
cnf(i_0_13133,plain,
ilf_type(cross_product(X1,X1),relation_type(X1,X1)),
inference(rename_variables,[],[i_0_148]) ).
cnf(i_0_13537,plain,
ilf_type(esk8_1(X1),subset_type(X1)),
inference(equality_inference,[],[13533]) ).
cnf(i_0_13543,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(equality_inference,[],[13540]) ).
cnf(i_0_13564,plain,
ilf_type(esk8_1(X1),subset_type(X1)),
inference(equality_inference,[],[13558]) ).
cnf(i_0_13630,plain,
relation_like(identity_relation_of(X1)),
inference(rename_variables,[],[i_0_13145]) ).
cnf(i_0_13642,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(equality_inference,[],[13637]) ).
cnf(i_0_13643,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
inference(equality_inference,[],[13638]) ).
cnf(i_0_208,plain,
relation_like(esk8_1(cross_product(esk15_0,esk15_0))),
inference(equality_inference,[],[203]) ).
cnf(i_0_209,plain,
ilf_type(esk8_1(cross_product(X1,X1)),binary_relation_type),
inference(scs_inference,[],[i_0_194,i_0_121,i_0_114]) ).
cnf(i_0_224,plain,
relation_like(esk6_0),
inference(equality_inference,[],[219]) ).
cnf(i_0_13135,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(scs_inference,[],[i_0_148,i_0_121,i_0_117,i_0_116,i_0_75,i_0_197]) ).
cnf(i_0_13148,plain,
ilf_type(esk7_2(X1,X1),subset_type(cross_product(X1,X1))),
inference(scs_inference,[],[i_0_189,i_0_13128,i_0_13130,i_0_121,i_0_13143,i_0_13146,i_0_107,i_0_111,i_0_75]) ).
cnf(i_0_13360,plain,
ilf_type(esk13_1(power_set(X1)),member_type(power_set(X1))),
inference(equality_inference,[],[13346]) ).
cnf(i_0_13421,plain,
ilf_type(esk13_1(power_set(X1)),member_type(power_set(X1))),
inference(equality_inference,[],[13417]) ).
cnf(i_0_15040,plain,
relation_like(identity_relation_of(X1)),
inference(equality_inference,[],[15034]) ).
cnf(i_0_218,plain,
relation_like(esk8_1(cross_product(X1,X1))),
inference(equality_inference,[],[212]) ).
cnf(i_0_13140,plain,
ilf_type(cross_product(X1,X1),relation_type(X1,X1)),
inference(equality_inference,[],[13137]) ).
cnf(i_0_13141,plain,
ilf_type(cross_product(X1,X1),relation_type(X1,X1)),
inference(equality_inference,[],[13138]) ).
cnf(i_0_13156,plain,
ilf_type(esk14_1(power_set(X1)),member_type(power_set(X1))),
inference(scs_inference,[],[i_0_106,i_0_189,i_0_13128,i_0_13130,i_0_13135,i_0_121,i_0_13143,i_0_13146,i_0_13150,i_0_13153,i_0_13149,i_0_13154,i_0_107,i_0_111,i_0_75,i_0_96,i_0_102]) ).
cnf(i_0_13162,plain,
ilf_type(esk13_1(power_set(X1)),subset_type(X1)),
inference(scs_inference,[],[i_0_106,i_0_189,i_0_13128,i_0_13130,i_0_13135,i_0_121,i_0_13143,i_0_13146,i_0_13150,i_0_13153,i_0_13158,i_0_13149,i_0_13154,i_0_13159,i_0_107,i_0_111,i_0_75,i_0_96,i_0_102,i_0_133,i_0_88]) ).
cnf(i_0_13170,plain,
relation_like(cross_product(X1,X1)),
inference(scs_inference,[],[i_0_106,i_0_189,i_0_13128,i_0_13130,i_0_13135,i_0_13132,i_0_121,i_0_13143,i_0_13146,i_0_13150,i_0_13153,i_0_13158,i_0_13164,i_0_13168,i_0_13149,i_0_13154,i_0_13159,i_0_13163,i_0_107,i_0_111,i_0_75,i_0_96,i_0_102,i_0_133,i_0_88,i_0_87,i_0_76]) ).
cnf(i_0_13179,plain,
~ member(identity_relation_of(esk15_0),power_set(cross_product(esk15_0,esk15_0))),
inference(scs_inference,[],[i_0_106,i_0_189,i_0_13128,i_0_13130,i_0_13135,i_0_13132,i_0_184,i_0_121,i_0_13143,i_0_13146,i_0_13150,i_0_13153,i_0_13158,i_0_13164,i_0_13168,i_0_13172,i_0_13176,i_0_13175,i_0_13171,i_0_13177,i_0_13149,i_0_13154,i_0_13159,i_0_13163,i_0_107,i_0_111,i_0_75,i_0_96,i_0_102,i_0_133,i_0_88,i_0_87,i_0_76,i_0_81,i_0_84]) ).
cnf(i_0_13184,plain,
ilf_type(cross_product(X1,X2),relation_type(X1,X2)),
inference(scs_inference,[],[i_0_106,i_0_189,i_0_13128,i_0_13130,i_0_13135,i_0_13132,i_0_184,i_0_121,i_0_13143,i_0_13146,i_0_13150,i_0_13153,i_0_13158,i_0_13164,i_0_13168,i_0_13172,i_0_13176,i_0_13180,i_0_13175,i_0_13181,i_0_13171,i_0_13177,i_0_13149,i_0_13154,i_0_13159,i_0_13163,i_0_107,i_0_111,i_0_75,i_0_96,i_0_102,i_0_133,i_0_88,i_0_87,i_0_76,i_0_81,i_0_84,i_0_92]) ).
cnf(i_0_13186,plain,
ilf_type(esk7_2(X1,X2),relation_type(X2,X1)),
inference(scs_inference,[],[i_0_106,i_0_189,i_0_13128,i_0_13130,i_0_13135,i_0_13132,i_0_184,i_0_121,i_0_13143,i_0_13146,i_0_13150,i_0_13153,i_0_13158,i_0_13164,i_0_13168,i_0_13172,i_0_13176,i_0_13180,i_0_13175,i_0_13181,i_0_13171,i_0_13177,i_0_13149,i_0_13154,i_0_13159,i_0_13163,i_0_107,i_0_111,i_0_75,i_0_96,i_0_102,i_0_133,i_0_88,i_0_87,i_0_76,i_0_81,i_0_84,i_0_92,i_0_91]) ).
cnf(i_0_13227,plain,
relation_like(esk7_2(X1,X1)),
inference(scs_inference,[],[i_0_13148,i_0_121,i_0_76]) ).
cnf(i_0_13343,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13363,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13398,plain,
ilf_type(esk8_1(cross_product(X1,X1)),relation_type(X1,X1)),
inference(equality_inference,[],[13397]) ).
cnf(i_0_13440,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13469,plain,
ilf_type(esk8_1(cross_product(X1,X1)),relation_type(X1,X1)),
inference(equality_inference,[],[13466]) ).
cnf(i_0_13478,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13523,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13567,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13658,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13677,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13712,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14180,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14231,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14307,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14333,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14372,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14377,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14393,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14421,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14426,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14509,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14560,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14586,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14641,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14656,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14678,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14791,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14888,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_14956,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_15008,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_15051,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_15083,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_15174,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(rename_variables,[],[i_0_13135]) ).
cnf(i_0_13189,plain,
ilf_type(esk7_2(X1,X1),relation_type(X1,X1)),
inference(equality_inference,[],[13161]) ).
cnf(i_0_13190,plain,
~ empty(power_set(X1)),
inference(equality_inference,[],[13188]) ).
cnf(i_0_13191,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(scs_inference,[],[i_0_13170,i_0_121,i_0_114]) ).
cnf(i_0_13237,plain,
ilf_type(esk8_1(X1),member_type(power_set(X1))),
inference(scs_inference,[],[i_0_13184,i_0_13148,i_0_184,i_0_140,i_0_121,i_0_13229,i_0_13233,i_0_13228,i_0_13234,i_0_76,i_0_81,i_0_133,i_0_93]) ).
cnf(i_0_13241,plain,
ilf_type(cross_product(X1,X2),subset_type(cross_product(X1,X2))),
inference(scs_inference,[],[i_0_13184,i_0_13148,i_0_184,i_0_140,i_0_121,i_0_13229,i_0_13233,i_0_13228,i_0_13234,i_0_13239,i_0_76,i_0_81,i_0_133,i_0_93,i_0_75]) ).
cnf(i_0_13251,plain,
ilf_type(esk7_2(X1,X1),binary_relation_type),
inference(scs_inference,[],[i_0_13227,i_0_121,i_0_114]) ).
cnf(i_0_13405,plain,
ilf_type(esk7_2(X1,X1),subset_type(cross_product(X1,X1))),
inference(equality_inference,[],[13402]) ).
cnf(i_0_13476,plain,
ilf_type(esk7_2(X1,X1),subset_type(cross_product(X1,X1))),
inference(equality_inference,[],[13472]) ).
cnf(i_0_13510,plain,
ilf_type(esk8_1(cross_product(X1,X1)),binary_relation_type),
inference(equality_inference,[],[13506]) ).
cnf(i_0_13553,plain,
ilf_type(esk8_1(cross_product(X1,X1)),binary_relation_type),
inference(equality_inference,[],[13544]) ).
cnf(i_0_13219,plain,
member(esk14_1(power_set(X1)),power_set(X1)),
inference(equality_inference,[],[13218]) ).
cnf(i_0_13246,plain,
ilf_type(cross_product(X1,X2),relation_type(X1,X2)),
inference(equality_inference,[],[13236]) ).
cnf(i_0_13250,plain,
ilf_type(esk7_2(X1,X2),relation_type(X2,X1)),
inference(equality_inference,[],[13249]) ).
cnf(i_0_13263,plain,
~ empty(identity_relation_of(esk15_0)),
inference(scs_inference,[],[i_0_121,i_0_13254]) ).
cnf(i_0_13265,plain,
member(esk14_1(identity_relation_of(esk15_0)),identity_relation_of(esk15_0)),
inference(scs_inference,[],[i_0_121,i_0_13264,i_0_13254,i_0_13257]) ).
cnf(i_0_13267,plain,
ilf_type(esk13_1(identity_relation_of(esk15_0)),member_type(identity_relation_of(esk15_0))),
inference(scs_inference,[],[i_0_121,i_0_13264,i_0_13266,i_0_13254,i_0_13257,i_0_13259]) ).
cnf(i_0_13368,plain,
ilf_type(esk14_1(power_set(X1)),member_type(power_set(X1))),
inference(equality_inference,[],[13362]) ).
cnf(i_0_13438,plain,
ilf_type(esk14_1(power_set(X1)),member_type(power_set(X1))),
inference(equality_inference,[],[13424]) ).
cnf(i_0_13463,plain,
ilf_type(esk13_1(power_set(X1)),subset_type(X1)),
inference(equality_inference,[],[13459]) ).
cnf(i_0_13484,plain,
ilf_type(esk7_2(X1,X2),relation_type(X2,X1)),
inference(equality_inference,[],[13480]) ).
cnf(i_0_13485,plain,
ilf_type(esk7_2(X1,X1),subset_type(cross_product(X1,X1))),
inference(equality_inference,[],[13481]) ).
cnf(i_0_13520,plain,
ilf_type(cross_product(X1,X2),relation_type(X1,X2)),
inference(equality_inference,[],[13514]) ).
cnf(i_0_13521,plain,
ilf_type(cross_product(X1,X2),relation_type(X1,X2)),
inference(equality_inference,[],[13515]) ).
cnf(i_0_13530,plain,
ilf_type(esk13_1(power_set(X1)),subset_type(X1)),
inference(equality_inference,[],[13525]) ).
cnf(i_0_13604,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_13804,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_13972,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14042,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14134,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14298,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14360,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14437,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14650,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14759,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14969,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14994,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_14997,plain,
relation_like(cross_product(X1,X1)),
inference(equality_inference,[],[14988]) ).
cnf(i_0_15018,plain,
relation_like(esk7_2(X1,X1)),
inference(equality_inference,[],[15012]) ).
cnf(i_0_15072,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(rename_variables,[],[i_0_13191]) ).
cnf(i_0_13272,plain,
~ empty(identity_relation_of(esk15_0)),
inference(equality_inference,[],[13271]) ).
cnf(i_0_13280,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(equality_inference,[],[13276]) ).
cnf(i_0_13318,plain,
ilf_type(esk8_1(X1),member_type(power_set(X1))),
inference(equality_inference,[],[13317]) ).
cnf(i_0_13334,plain,
ilf_type(cross_product(X1,X2),subset_type(cross_product(X1,X2))),
inference(equality_inference,[],[13332]) ).
cnf(i_0_13335,plain,
ilf_type(cross_product(X1,X2),subset_type(cross_product(X1,X2))),
inference(equality_inference,[],[13333]) ).
cnf(i_0_13414,plain,
ilf_type(esk8_1(X1),member_type(power_set(X1))),
inference(equality_inference,[],[13410]) ).
cnf(i_0_13577,plain,
ilf_type(esk7_2(X1,X1),binary_relation_type),
inference(equality_inference,[],[13571]) ).
cnf(i_0_13591,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(equality_inference,[],[13585]) ).
cnf(i_0_13592,plain,
ilf_type(cross_product(X1,X1),binary_relation_type),
inference(equality_inference,[],[13586]) ).
cnf(i_0_13606,plain,
ilf_type(esk7_2(X1,X1),binary_relation_type),
inference(equality_inference,[],[13600]) ).
cnf(i_0_13285,plain,
member(esk14_1(identity_relation_of(esk15_0)),identity_relation_of(esk15_0)),
inference(equality_inference,[],[13284]) ).
cnf(i_0_13286,plain,
ilf_type(esk14_1(identity_relation_of(esk15_0)),member_type(identity_relation_of(esk15_0))),
inference(scs_inference,[],[i_0_121,i_0_13281]) ).
cnf(i_0_13328,plain,
member(esk14_1(identity_relation_of(esk15_0)),identity_relation_of(esk15_0)),
inference(equality_inference,[],[13325]) ).
cnf(i_0_13329,plain,
member(esk14_1(identity_relation_of(esk15_0)),identity_relation_of(esk15_0)),
inference(equality_inference,[],[13326]) ).
cnf(i_0_13446,plain,
ilf_type(esk13_1(identity_relation_of(esk15_0)),member_type(identity_relation_of(esk15_0))),
inference(equality_inference,[],[13442]) ).
cnf(i_0_13503,plain,
ilf_type(esk13_1(identity_relation_of(esk15_0)),member_type(identity_relation_of(esk15_0))),
inference(equality_inference,[],[13492]) ).
cnf(i_0_13393,plain,
ilf_type(esk14_1(identity_relation_of(esk15_0)),member_type(identity_relation_of(esk15_0))),
inference(equality_inference,[],[13389]) ).
cnf(i_0_13448,plain,
ilf_type(esk14_1(identity_relation_of(esk15_0)),member_type(identity_relation_of(esk15_0))),
inference(equality_inference,[],[13447]) ).
cnf(c_0_13580,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) ),
i_0_80 ).
cnf(c_0_13581,plain,
ilf_type(X1,set_type),
i_0_121 ).
cnf(c_0_13582,plain,
( relation_like(X1)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X1,subset_type(cross_product(X2,X3))) ),
i_0_76 ).
cnf(c_0_13583,plain,
( X1 = X2
| ~ member(ordered_pair(X1,X2),identity_relation_of(X3)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_13580,c_0_13581]),c_0_13581]),c_0_13581])]) ).
cnf(c_0_13584,plain,
( member(ordered_pair(esk1_2(X1,X2),esk2_2(X1,X2)),X1)
| subset(X1,X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type) ),
i_0_72 ).
cnf(c_0_13585,plain,
ilf_type(identity_relation_of(X1),binary_relation_type),
i_0_13568 ).
cnf(c_0_13586,plain,
( ilf_type(X1,binary_relation_type)
| ~ relation_like(X1)
| ~ ilf_type(X1,set_type) ),
i_0_114 ).
cnf(c_0_13587,plain,
( relation_like(X1)
| ~ ilf_type(X1,subset_type(cross_product(X2,X3))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_13582,c_0_13581]),c_0_13581])]) ).
cnf(c_0_13588,plain,
ilf_type(cross_product(X1,X2),subset_type(cross_product(X1,X2))),
i_0_13241 ).
cnf(c_0_13589,plain,
( subset(X1,X2)
| ~ member(ordered_pair(esk1_2(X1,X2),esk2_2(X1,X2)),X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ ilf_type(X1,binary_relation_type) ),
i_0_63 ).
cnf(c_0_13590,plain,
( esk2_2(identity_relation_of(X1),X2) = esk1_2(identity_relation_of(X1),X2)
| subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,binary_relation_type) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13583,c_0_13584]),c_0_13585])]) ).
cnf(c_0_13591,plain,
( member(ordered_pair(X1,X2),cross_product(X3,X4))
| ~ member(X1,X3)
| ~ member(X2,X4)
| ~ ilf_type(X4,set_type)
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type) ),
i_0_74 ).
cnf(c_0_13592,plain,
( ilf_type(X1,binary_relation_type)
| ~ relation_like(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13586,c_0_13581])]) ).
cnf(c_0_13593,plain,
relation_like(cross_product(X1,X2)),
inference(spm,[status(thm)],[c_0_13587,c_0_13588]) ).
cnf(c_0_13594,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) ),
i_0_77 ).
cnf(c_0_13595,plain,
( subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,binary_relation_type)
| ~ member(ordered_pair(esk1_2(identity_relation_of(X1),X2),esk1_2(identity_relation_of(X1),X2)),X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13589,c_0_13590]),c_0_13585])]) ).
cnf(c_0_13596,plain,
( member(ordered_pair(X1,X2),cross_product(X3,X4))
| ~ member(X2,X4)
| ~ member(X1,X3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_13591,c_0_13581]),c_0_13581]),c_0_13581]),c_0_13581])]) ).
cnf(c_0_13597,plain,
ilf_type(cross_product(X1,X2),binary_relation_type),
inference(spm,[status(thm)],[c_0_13592,c_0_13593]) ).
cnf(c_0_13598,plain,
( member(X1,X2)
| ~ member(ordered_pair(X1,X3),identity_relation_of(X2)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_13594,c_0_13581]),c_0_13581]),c_0_13581])]) ).
cnf(c_0_13599,plain,
( subset(identity_relation_of(X1),cross_product(X2,X3))
| ~ member(esk1_2(identity_relation_of(X1),cross_product(X2,X3)),X3)
| ~ member(esk1_2(identity_relation_of(X1),cross_product(X2,X3)),X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13595,c_0_13596]),c_0_13597])]) ).
cnf(c_0_13600,plain,
( subset(identity_relation_of(X1),X2)
| member(esk1_2(identity_relation_of(X1),X2),X1)
| ~ ilf_type(X2,binary_relation_type) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13598,c_0_13584]),c_0_13585])]) ).
cnf(c_0_13601,plain,
( subset(identity_relation_of(X1),cross_product(X2,X1))
| ~ member(esk1_2(identity_relation_of(X1),cross_product(X2,X1)),X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13599,c_0_13600]),c_0_13597])]) ).
cnf(c_0_13602,negated_conjecture,
~ subset(identity_relation_of(esk15_0),cross_product(esk15_0,esk15_0)),
i_0_106 ).
cnf(c_0_13603,plain,
subset(identity_relation_of(X1),cross_product(X1,X1)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13601,c_0_13600]),c_0_13597])]) ).
cnf(c_0_13604,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13602,c_0_13603])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET665+3 : TPTP v9.2.1. Released v2.2.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n017.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 02:29:28 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 136.32/101.41 % Version : CSE_E---1.7
% 136.32/101.41 % Problem : theBenchmark.p
% 136.32/101.41 % SZS status Theorem for theBenchmark.p
% 136.32/101.41 % SZS output start CNFRefutation
% See solution above
% 137.12/102.25 % Total time : 101.045s
%------------------------------------------------------------------------------