%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU049+1 : TPTP v9.2.1. Bugfixed v4.0.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 : n004.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:10:33 PM UTC 2026
% Result : Theorem 186.74s 142.33s
% Output : CNFRefutation 194.04s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_480)
% Comments :
%------------------------------------------------------------------------------
fof(t117_funct_1,conjecture,
! [X1,X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X1,relation_dom(X2))
=> relation_image(X2,singleton(X1)) = singleton(apply(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t117_funct_1) ).
fof(antisymmetry_r2_hidden,axiom,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(rc1_subset_1,axiom,
! [X1] :
( ~ empty(X1)
=> ? [X2] :
( element(X2,powerset(X1))
& ~ empty(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_subset_1) ).
fof(fc5_relat_1,axiom,
! [X1] :
( ( ~ empty(X1)
& relation(X1) )
=> ~ empty(relation_dom(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_relat_1) ).
fof(fc1_subset_1,axiom,
! [X1] : ~ empty(powerset(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(fc2_subset_1,axiom,
! [X1] : ~ empty(singleton(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(rc2_xboole_0,axiom,
? [X1] : ~ empty(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(rc2_relat_1,axiom,
? [X1] :
( ~ empty(X1)
& relation(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(d12_funct_1,axiom,
! [X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2,X3] :
( X3 = relation_image(X1,X2)
<=> ! [X4] :
( in(X4,X3)
<=> ? [X5] :
( in(X5,relation_dom(X1))
& in(X5,X2)
& X4 = apply(X1,X5) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_funct_1) ).
fof(t2_tarski,axiom,
! [X1,X2] :
( ! [X3] :
( in(X3,X1)
<=> in(X3,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(d1_tarski,axiom,
! [X1,X2] :
( X2 = singleton(X1)
<=> ! [X3] :
( in(X3,X2)
<=> X3 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tarski) ).
fof(t4_subset,axiom,
! [X1,X2,X3] :
( ( in(X1,X2)
& element(X2,powerset(X3)) )
=> element(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [X1,X2,X3] :
~ ( in(X1,X2)
& element(X2,powerset(X3))
& empty(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(t3_subset,axiom,
! [X1,X2] :
( element(X1,powerset(X2))
<=> subset(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(t2_subset,axiom,
! [X1,X2] :
( element(X1,X2)
=> ( empty(X2)
| in(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(t1_subset,axiom,
! [X1,X2] :
( in(X1,X2)
=> element(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(t7_boole,axiom,
! [X1,X2] :
~ ( in(X1,X2)
& empty(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(rc2_subset_1,axiom,
! [X1] :
? [X2] :
( element(X2,powerset(X1))
& empty(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(cc2_funct_1,axiom,
! [X1] :
( ( relation(X1)
& empty(X1)
& function(X1) )
=> ( relation(X1)
& function(X1)
& one_to_one(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_funct_1) ).
fof(existence_m1_subset_1,axiom,
! [X1] :
? [X2] : element(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(fc7_relat_1,axiom,
! [X1] :
( empty(X1)
=> ( empty(relation_dom(X1))
& relation(relation_dom(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_relat_1) ).
fof(t8_boole,axiom,
! [X1,X2] :
~ ( empty(X1)
& X1 != X2
& empty(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
fof(reflexivity_r1_tarski,axiom,
! [X1,X2] : subset(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(cc1_relat_1,axiom,
! [X1] :
( empty(X1)
=> relation(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relat_1) ).
fof(cc1_funct_1,axiom,
! [X1] :
( empty(X1)
=> function(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_funct_1) ).
fof(t6_boole,axiom,
! [X1] :
( empty(X1)
=> X1 = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(rc3_relat_1,axiom,
? [X1] :
( relation(X1)
& relation_empty_yielding(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_relat_1) ).
fof(rc3_funct_1,axiom,
? [X1] :
( relation(X1)
& function(X1)
& one_to_one(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_funct_1) ).
fof(rc2_funct_1,axiom,
? [X1] :
( relation(X1)
& empty(X1)
& function(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_funct_1) ).
fof(rc1_relat_1,axiom,
? [X1] :
( empty(X1)
& relation(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_relat_1) ).
fof(rc1_funct_1,axiom,
? [X1] :
( relation(X1)
& function(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_funct_1) ).
fof(rc1_xboole_0,axiom,
? [X1] : empty(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(fc12_relat_1,axiom,
( empty(empty_set)
& relation(empty_set)
& relation_empty_yielding(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc12_relat_1) ).
fof(fc4_relat_1,axiom,
( empty(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(fc1_xboole_0,axiom,
empty(empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(i_0_35,negated_conjecture,
~ ! [X1,X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X1,relation_dom(X2))
=> relation_image(X2,singleton(X1)) = singleton(apply(X2,X1)) ) ),
inference(assume_negation,[status(cth)],[t117_funct_1]) ).
fof(i_0_36,plain,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden]) ).
fof(i_0_37,plain,
! [X1] :
( ~ empty(X1)
=> ? [X2] :
( element(X2,powerset(X1))
& ~ empty(X2) ) ),
inference(fof_simplification,[status(thm)],[rc1_subset_1]) ).
fof(i_0_38,plain,
! [X1] :
( ( ~ empty(X1)
& relation(X1) )
=> ~ empty(relation_dom(X1)) ),
inference(fof_simplification,[status(thm)],[fc5_relat_1]) ).
fof(i_0_39,plain,
! [X1] : ~ empty(powerset(X1)),
inference(fof_simplification,[status(thm)],[fc1_subset_1]) ).
fof(i_0_40,plain,
! [X1] : ~ empty(singleton(X1)),
inference(fof_simplification,[status(thm)],[fc2_subset_1]) ).
fof(i_0_41,plain,
? [X1] : ~ empty(X1),
inference(fof_simplification,[status(thm)],[rc2_xboole_0]) ).
fof(i_0_42,plain,
? [X1] :
( ~ empty(X1)
& relation(X1) ),
inference(fof_simplification,[status(thm)],[rc2_relat_1]) ).
fof(i_0_43,plain,
! [X66,X67,X68,X69,X71,X72,X73,X74,X76] :
( ( in(esk1_4(X66,X67,X68,X69),relation_dom(X66))
| ~ in(X69,X68)
| X68 != relation_image(X66,X67)
| ~ relation(X66)
| ~ function(X66) )
& ( in(esk1_4(X66,X67,X68,X69),X67)
| ~ in(X69,X68)
| X68 != relation_image(X66,X67)
| ~ relation(X66)
| ~ function(X66) )
& ( X69 = apply(X66,esk1_4(X66,X67,X68,X69))
| ~ in(X69,X68)
| X68 != relation_image(X66,X67)
| ~ relation(X66)
| ~ function(X66) )
& ( ~ in(X72,relation_dom(X66))
| ~ in(X72,X67)
| X71 != apply(X66,X72)
| in(X71,X68)
| X68 != relation_image(X66,X67)
| ~ relation(X66)
| ~ function(X66) )
& ( ~ in(esk2_3(X66,X73,X74),X74)
| ~ in(X76,relation_dom(X66))
| ~ in(X76,X73)
| esk2_3(X66,X73,X74) != apply(X66,X76)
| X74 = relation_image(X66,X73)
| ~ relation(X66)
| ~ function(X66) )
& ( in(esk3_3(X66,X73,X74),relation_dom(X66))
| in(esk2_3(X66,X73,X74),X74)
| X74 = relation_image(X66,X73)
| ~ relation(X66)
| ~ function(X66) )
& ( in(esk3_3(X66,X73,X74),X73)
| in(esk2_3(X66,X73,X74),X74)
| X74 = relation_image(X66,X73)
| ~ relation(X66)
| ~ function(X66) )
& ( esk2_3(X66,X73,X74) = apply(X66,esk3_3(X66,X73,X74))
| in(esk2_3(X66,X73,X74),X74)
| X74 = relation_image(X66,X73)
| ~ relation(X66)
| ~ function(X66) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d12_funct_1])])])])])]) ).
fof(i_0_44,plain,
! [X110,X111] :
( ( ~ in(esk18_2(X110,X111),X110)
| ~ in(esk18_2(X110,X111),X111)
| X110 = X111 )
& ( in(esk18_2(X110,X111),X110)
| in(esk18_2(X110,X111),X111)
| X110 = X111 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_tarski])])])]) ).
fof(i_0_45,plain,
! [X78,X79,X80,X81,X82,X83] :
( ( ~ in(X80,X79)
| X80 = X78
| X79 != singleton(X78) )
& ( X81 != X78
| in(X81,X79)
| X79 != singleton(X78) )
& ( ~ in(esk4_2(X82,X83),X83)
| esk4_2(X82,X83) != X82
| X83 = singleton(X82) )
& ( in(esk4_2(X82,X83),X83)
| esk4_2(X82,X83) = X82
| X83 = singleton(X82) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d1_tarski])])])])])]) ).
fof(i_0_46,plain,
! [X115,X116,X117] :
( ~ in(X115,X116)
| ~ element(X116,powerset(X117))
| element(X115,X117) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t4_subset])]) ).
fof(i_0_47,plain,
! [X118,X119,X120] :
( ~ in(X118,X119)
| ~ element(X119,powerset(X120))
| ~ empty(X120) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_subset])]) ).
fof(i_0_48,negated_conjecture,
( relation(esk17_0)
& function(esk17_0)
& in(esk16_0,relation_dom(esk17_0))
& relation_image(esk17_0,singleton(esk16_0)) != singleton(apply(esk17_0,esk16_0)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_35])])]) ).
fof(i_0_49,plain,
! [X113,X114] :
( ( ~ element(X113,powerset(X114))
| subset(X113,X114) )
& ( ~ subset(X113,X114)
| element(X113,powerset(X114)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_subset])]) ).
fof(i_0_50,plain,
! [X61,X62] :
( ~ in(X61,X62)
| ~ in(X62,X61) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_36])]) ).
fof(i_0_51,plain,
! [X108,X109] :
( ~ element(X108,X109)
| empty(X109)
| in(X108,X109) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_subset])]) ).
fof(i_0_52,plain,
! [X106,X107] :
( ~ in(X106,X107)
| element(X106,X107) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t1_subset])]) ).
fof(i_0_53,plain,
! [X93] :
( ( element(esk8_1(X93),powerset(X93))
| empty(X93) )
& ( ~ empty(esk8_1(X93))
| empty(X93) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_37])])])]) ).
fof(i_0_54,plain,
! [X122,X123] :
( ~ in(X122,X123)
| ~ empty(X123) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_boole])]) ).
fof(i_0_55,plain,
! [X89] :
( empty(X89)
| ~ relation(X89)
| ~ empty(relation_dom(X89)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_38])]) ).
fof(i_0_56,plain,
! [X98] :
( element(esk12_1(X98),powerset(X98))
& empty(esk12_1(X98)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_subset_1])]) ).
fof(i_0_57,plain,
! [X65] :
( ( relation(X65)
| ~ relation(X65)
| ~ empty(X65)
| ~ function(X65) )
& ( function(X65)
| ~ relation(X65)
| ~ empty(X65)
| ~ function(X65) )
& ( one_to_one(X65)
| ~ relation(X65)
| ~ empty(X65)
| ~ function(X65) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc2_funct_1])])]) ).
fof(i_0_58,plain,
! [X85] : element(esk5_1(X85),X85),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m1_subset_1])]) ).
fof(i_0_59,plain,
! [X90] :
( ( empty(relation_dom(X90))
| ~ empty(X90) )
& ( relation(relation_dom(X90))
| ~ empty(X90) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fc7_relat_1])])]) ).
fof(i_0_60,plain,
! [X87] : ~ empty(powerset(X87)),
inference(variable_rename,[status(thm)],[i_0_39]) ).
fof(i_0_61,plain,
! [X88] : ~ empty(singleton(X88)),
inference(variable_rename,[status(thm)],[i_0_40]) ).
fof(i_0_62,plain,
! [X124,X125] :
( ~ empty(X124)
| X124 = X125
| ~ empty(X125) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t8_boole])]) ).
fof(i_0_63,plain,
! [X103] : subset(X103,X103),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])]) ).
fof(i_0_64,plain,
! [X64] :
( ~ empty(X64)
| relation(X64) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc1_relat_1])]) ).
fof(i_0_65,plain,
! [X63] :
( ~ empty(X63)
| function(X63) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc1_funct_1])]) ).
fof(i_0_66,plain,
! [X121] :
( ~ empty(X121)
| X121 = empty_set ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(i_0_67,plain,
~ empty(esk13_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_41])]) ).
fof(i_0_68,plain,
( ~ empty(esk11_0)
& relation(esk11_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_42])]) ).
fof(i_0_69,plain,
( relation(esk15_0)
& relation_empty_yielding(esk15_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc3_relat_1])]) ).
fof(i_0_70,plain,
( relation(esk14_0)
& function(esk14_0)
& one_to_one(esk14_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc3_funct_1])]) ).
fof(i_0_71,plain,
( relation(esk10_0)
& empty(esk10_0)
& function(esk10_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_funct_1])]) ).
fof(i_0_72,plain,
( empty(esk7_0)
& relation(esk7_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_relat_1])]) ).
fof(i_0_73,plain,
( relation(esk6_0)
& function(esk6_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_funct_1])]) ).
fof(i_0_74,plain,
empty(esk9_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_xboole_0])]) ).
cnf(i_0_75,plain,
( in(esk1_4(X1,X2,X3,X4),relation_dom(X1))
| ~ in(X4,X3)
| X3 != relation_image(X1,X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_76,plain,
( X1 = apply(X2,esk1_4(X2,X3,X4,X1))
| ~ in(X1,X4)
| X4 != relation_image(X2,X3)
| ~ relation(X2)
| ~ function(X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_77,plain,
( in(esk1_4(X1,X2,X3,X4),X2)
| ~ in(X4,X3)
| X3 != relation_image(X1,X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_78,plain,
( X3 = relation_image(X1,X2)
| ~ in(esk2_3(X1,X2,X3),X3)
| ~ in(X4,relation_dom(X1))
| ~ in(X4,X2)
| esk2_3(X1,X2,X3) != apply(X1,X4)
| ~ relation(X1)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_79,plain,
( esk2_3(X1,X2,X3) = apply(X1,esk3_3(X1,X2,X3))
| in(esk2_3(X1,X2,X3),X3)
| X3 = relation_image(X1,X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_80,plain,
( in(esk3_3(X1,X2,X3),relation_dom(X1))
| in(esk2_3(X1,X2,X3),X3)
| X3 = relation_image(X1,X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_81,plain,
( in(esk3_3(X1,X2,X3),X2)
| in(esk2_3(X1,X2,X3),X3)
| X3 = relation_image(X1,X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_82,plain,
( in(X4,X5)
| ~ in(X1,relation_dom(X2))
| ~ in(X1,X3)
| X4 != apply(X2,X1)
| X5 != relation_image(X2,X3)
| ~ relation(X2)
| ~ function(X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_83,plain,
( X1 = X2
| ~ in(esk18_2(X1,X2),X1)
| ~ in(esk18_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_84,plain,
( X2 = singleton(X1)
| ~ in(esk4_2(X1,X2),X2)
| esk4_2(X1,X2) != X1 ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_85,plain,
( in(esk18_2(X1,X2),X1)
| in(esk18_2(X1,X2),X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_86,plain,
( element(X1,X3)
| ~ in(X1,X2)
| ~ element(X2,powerset(X3)) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_87,plain,
( ~ in(X1,X2)
| ~ element(X2,powerset(X3))
| ~ empty(X3) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_88,negated_conjecture,
relation_image(esk17_0,singleton(esk16_0)) != singleton(apply(esk17_0,esk16_0)),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_89,plain,
( in(esk4_2(X1,X2),X2)
| esk4_2(X1,X2) = X1
| X2 = singleton(X1) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_90,plain,
( subset(X1,X2)
| ~ element(X1,powerset(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_91,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_92,plain,
( element(X1,powerset(X2))
| ~ subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_93,plain,
( empty(X2)
| in(X1,X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_94,plain,
( element(X1,X2)
| ~ in(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_95,plain,
( X1 = X3
| ~ in(X1,X2)
| X2 != singleton(X3) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_96,plain,
( element(esk8_1(X1),powerset(X1))
| empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_97,plain,
( ~ in(X1,X2)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_98,plain,
( empty(X1)
| ~ relation(X1)
| ~ empty(relation_dom(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_99,plain,
element(esk12_1(X1),powerset(X1)),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_100,plain,
( in(X1,X3)
| X1 != X2
| X3 != singleton(X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_101,plain,
( one_to_one(X1)
| ~ relation(X1)
| ~ empty(X1)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_102,plain,
( empty(X1)
| ~ empty(esk8_1(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_103,plain,
element(esk5_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_104,plain,
( relation(relation_dom(X1))
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_105,plain,
( empty(relation_dom(X1))
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_106,plain,
~ empty(powerset(X1)),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_107,plain,
~ empty(singleton(X1)),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_108,plain,
( X1 = X2
| ~ empty(X1)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_109,negated_conjecture,
in(esk16_0,relation_dom(esk17_0)),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_110,plain,
subset(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_111,plain,
( relation(X1)
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_112,plain,
( function(X1)
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_113,plain,
empty(esk12_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_114,plain,
( X1 = empty_set
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_115,plain,
~ empty(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_116,plain,
~ empty(esk11_0),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_117,plain,
relation_empty_yielding(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_118,plain,
relation_empty_yielding(empty_set),
inference(split_conjunct,[status(thm)],[fc12_relat_1]),
[final] ).
cnf(i_0_119,plain,
one_to_one(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_120,negated_conjecture,
relation(esk17_0),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_121,plain,
relation(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_122,plain,
relation(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_123,plain,
relation(esk11_0),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_124,plain,
relation(esk10_0),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_125,plain,
relation(esk7_0),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_126,plain,
relation(esk6_0),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_127,plain,
relation(empty_set),
inference(split_conjunct,[status(thm)],[fc4_relat_1]),
[final] ).
cnf(i_0_128,plain,
relation(empty_set),
inference(split_conjunct,[status(thm)],[fc12_relat_1]),
[final] ).
cnf(i_0_129,negated_conjecture,
function(esk17_0),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_130,plain,
function(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_131,plain,
function(esk10_0),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_132,plain,
function(esk6_0),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_133,plain,
empty(esk10_0),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_134,plain,
empty(esk9_0),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_135,plain,
empty(esk7_0),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_136,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc4_relat_1]),
[final] ).
cnf(i_0_137,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc1_xboole_0]),
[final] ).
cnf(i_0_138,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc12_relat_1]),
[final] ).
cnf(i_0_139,axiom,
X1 = X1 ).
cnf(i_0_140,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_141,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_142,axiom,
( X1 != X2
| relation_image(X1,X3) = relation_image(X2,X3) ) ).
cnf(i_0_143,axiom,
( X1 != X2
| relation_image(X3,X1) = relation_image(X3,X2) ) ).
cnf(i_0_144,axiom,
( X1 != X2
| apply(X1,X3) = apply(X2,X3) ) ).
cnf(i_0_145,axiom,
( X1 != X2
| apply(X3,X1) = apply(X3,X2) ) ).
cnf(i_0_146,axiom,
( X1 != X2
| esk2_3(X1,X3,X4) = esk2_3(X2,X3,X4) ) ).
cnf(i_0_147,axiom,
( X1 != X2
| esk2_3(X3,X1,X4) = esk2_3(X3,X2,X4) ) ).
cnf(i_0_148,axiom,
( X1 != X2
| esk2_3(X3,X4,X1) = esk2_3(X3,X4,X2) ) ).
cnf(i_0_149,axiom,
( X1 != X2
| singleton(X1) = singleton(X2) ) ).
cnf(i_0_150,axiom,
( X1 != X2
| esk4_2(X1,X3) = esk4_2(X2,X3) ) ).
cnf(i_0_151,axiom,
( X1 != X2
| esk4_2(X3,X1) = esk4_2(X3,X2) ) ).
cnf(i_0_152,axiom,
( X1 != X2
| ~ in(X1,X3)
| in(X2,X3) ) ).
cnf(i_0_153,axiom,
( X1 != X2
| ~ in(X3,X1)
| in(X3,X2) ) ).
cnf(i_0_154,axiom,
( X1 != X2
| ~ relation(X1)
| relation(X2) ) ).
cnf(i_0_155,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_156,axiom,
( X1 != X2
| ~ element(X1,X3)
| element(X2,X3) ) ).
cnf(i_0_157,axiom,
( X1 != X2
| ~ element(X3,X1)
| element(X3,X2) ) ).
cnf(i_0_158,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_159,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_160,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_161,axiom,
( X1 != X2
| ~ one_to_one(X1)
| one_to_one(X2) ) ).
cnf(i_0_162,axiom,
( X1 != X2
| ~ relation_empty_yielding(X1)
| relation_empty_yielding(X2) ) ).
cnf(i_0_1350,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1352,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1354,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1387,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_1469,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1473,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1475,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1477,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1514,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_1591,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1595,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1597,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1599,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1633,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_1684,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1690,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1692,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1694,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1799,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1805,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1807,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1809,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1827,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_1843,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_1955,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_1958,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1960,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1964,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1968,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_1971,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2004,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2107,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2109,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2111,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2117,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2198,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2200,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2202,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2208,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2275,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2283,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2295,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2297,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2301,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2305,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2387,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2389,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2393,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2397,plain,
X1 = esk4_2(X1,esk7_0),
inference(rename_variables,[],[i_0_480]) ).
cnf(i_0_2476,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2486,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2563,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2569,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2646,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2654,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_2699,plain,
~ in(X1,esk5_1(singleton(esk10_0))),
inference(rename_variables,[],[i_0_484]) ).
cnf(i_0_502,plain,
one_to_one(esk4_2(esk14_0,esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_501,i_0_240,i_0_196]) ).
cnf(i_0_504,plain,
relation_empty_yielding(esk4_2(esk15_0,esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_501,i_0_503,i_0_240,i_0_196,i_0_197]) ).
cnf(i_0_506,plain,
relation_empty_yielding(esk4_2(empty_set,esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_501,i_0_503,i_0_505,i_0_240,i_0_196,i_0_197,i_0_242]) ).
cnf(i_0_508,plain,
one_to_one(esk4_2(esk10_0,esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241]) ).
cnf(i_0_510,plain,
esk12_1(X1) = esk5_1(powerset(esk7_0)),
inference(scs_inference,[],[i_0_352,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140]) ).
cnf(i_0_511,plain,
relation_empty_yielding(esk4_2(relation_image(esk17_0,empty_set),esk7_0)),
inference(scs_inference,[],[i_0_352,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_509,i_0_402,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140,i_0_162]) ).
cnf(i_0_513,plain,
singleton(singleton(esk4_2(X1,esk7_0))) != X1,
inference(scs_inference,[],[i_0_352,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_509,i_0_512,i_0_297,i_0_402,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140,i_0_162,i_0_141]) ).
cnf(i_0_515,plain,
esk9_0 != singleton(X1),
inference(scs_inference,[],[i_0_352,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_509,i_0_512,i_0_297,i_0_402,i_0_134,i_0_107,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140,i_0_162,i_0_141,i_0_158]) ).
cnf(i_0_516,plain,
one_to_one(esk4_2(esk7_0,esk7_0)),
inference(scs_inference,[],[i_0_352,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_509,i_0_512,i_0_228,i_0_297,i_0_402,i_0_134,i_0_107,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140,i_0_162,i_0_141,i_0_158,i_0_161]) ).
cnf(i_0_518,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(scs_inference,[],[i_0_280,i_0_352,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_509,i_0_512,i_0_249,i_0_228,i_0_297,i_0_402,i_0_134,i_0_107,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140,i_0_162,i_0_141,i_0_158,i_0_161,i_0_153]) ).
cnf(i_0_520,plain,
function(esk4_2(relation_image(esk17_0,empty_set),esk7_0)),
inference(scs_inference,[],[i_0_280,i_0_352,i_0_449,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_509,i_0_512,i_0_517,i_0_249,i_0_228,i_0_297,i_0_402,i_0_134,i_0_107,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140,i_0_162,i_0_141,i_0_158,i_0_161,i_0_153,i_0_155]) ).
cnf(i_0_522,plain,
relation(relation_image(esk17_0,empty_set)),
inference(scs_inference,[],[i_0_321,i_0_280,i_0_352,i_0_449,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_509,i_0_512,i_0_517,i_0_488,i_0_249,i_0_228,i_0_297,i_0_402,i_0_134,i_0_107,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140,i_0_162,i_0_141,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154]) ).
cnf(i_0_523,plain,
esk4_2(X1,esk9_0) = X1,
inference(scs_inference,[],[i_0_321,i_0_280,i_0_352,i_0_449,i_0_480,i_0_501,i_0_503,i_0_505,i_0_507,i_0_509,i_0_512,i_0_517,i_0_488,i_0_249,i_0_347,i_0_228,i_0_297,i_0_402,i_0_134,i_0_107,i_0_240,i_0_196,i_0_197,i_0_242,i_0_241,i_0_140,i_0_162,i_0_141,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154,i_0_89]) ).
cnf(i_0_534,plain,
singleton(esk4_2(singleton(X1),esk7_0)) != X1,
inference(scs_inference,[],[i_0_513,i_0_149]) ).
cnf(i_0_535,plain,
singleton(singleton(esk4_2(X1,esk7_0))) != X1,
inference(rename_variables,[],[i_0_513]) ).
cnf(i_0_536,plain,
X1 = esk4_2(X1,esk9_0),
inference(scs_inference,[],[i_0_513,i_0_523,i_0_149,i_0_140]) ).
cnf(i_0_537,plain,
relation_empty_yielding(esk5_1(singleton(esk4_2(esk15_0,esk7_0)))),
inference(scs_inference,[],[i_0_296,i_0_513,i_0_523,i_0_504,i_0_149,i_0_140,i_0_162]) ).
cnf(i_0_539,plain,
esk7_0 != esk13_0,
inference(scs_inference,[],[i_0_296,i_0_513,i_0_523,i_0_504,i_0_135,i_0_115,i_0_149,i_0_140,i_0_162,i_0_158]) ).
cnf(i_0_540,plain,
one_to_one(esk5_1(singleton(relation_image(esk17_0,empty_set)))),
inference(scs_inference,[],[i_0_296,i_0_538,i_0_513,i_0_523,i_0_483,i_0_504,i_0_135,i_0_115,i_0_149,i_0_140,i_0_162,i_0_158,i_0_161]) ).
cnf(i_0_542,plain,
~ in(singleton(X1),X1),
inference(scs_inference,[],[i_0_296,i_0_538,i_0_541,i_0_294,i_0_513,i_0_523,i_0_483,i_0_504,i_0_135,i_0_115,i_0_149,i_0_140,i_0_162,i_0_158,i_0_161,i_0_153]) ).
cnf(i_0_544,plain,
function(esk5_1(singleton(esk4_2(esk14_0,esk7_0)))),
inference(scs_inference,[],[i_0_296,i_0_538,i_0_541,i_0_294,i_0_513,i_0_523,i_0_500,i_0_483,i_0_504,i_0_135,i_0_115,i_0_149,i_0_140,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155]) ).
cnf(i_0_546,plain,
relation(esk5_1(singleton(relation_image(esk17_0,empty_set)))),
inference(scs_inference,[],[i_0_296,i_0_538,i_0_541,i_0_545,i_0_294,i_0_513,i_0_522,i_0_523,i_0_500,i_0_483,i_0_504,i_0_135,i_0_115,i_0_149,i_0_140,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154]) ).
cnf(i_0_548,plain,
function(esk4_2(esk14_0,esk9_0)),
inference(scs_inference,[],[i_0_296,i_0_538,i_0_541,i_0_545,i_0_294,i_0_513,i_0_522,i_0_523,i_0_500,i_0_483,i_0_504,i_0_135,i_0_115,i_0_149,i_0_140,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154,i_0_240]) ).
cnf(i_0_549,plain,
one_to_one(esk4_2(esk14_0,esk9_0)),
inference(scs_inference,[],[i_0_296,i_0_538,i_0_541,i_0_545,i_0_294,i_0_513,i_0_522,i_0_523,i_0_500,i_0_483,i_0_504,i_0_135,i_0_115,i_0_149,i_0_140,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154,i_0_240,i_0_196]) ).
cnf(i_0_551,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_552,plain,
singleton(singleton(esk4_2(X1,esk7_0))) != X1,
inference(rename_variables,[],[i_0_513]) ).
cnf(i_0_669,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_693,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_714,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_782,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_786,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_808,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_828,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_863,plain,
singleton(singleton(esk4_2(X1,esk7_0))) != X1,
inference(rename_variables,[],[i_0_513]) ).
cnf(i_0_871,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_875,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_921,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_924,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_928,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_938,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_954,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_958,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1003,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1025,plain,
singleton(singleton(esk4_2(X1,esk7_0))) != X1,
inference(rename_variables,[],[i_0_513]) ).
cnf(i_0_1073,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1077,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1123,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1139,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1151,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1155,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1173,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1221,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1225,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1229,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1295,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1299,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1366,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1382,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1412,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1416,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1420,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1518,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1522,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1566,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1568,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1586,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1602,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1637,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1641,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1705,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1710,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1712,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1721,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1779,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1781,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1826,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_1921,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_1923,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2012,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2016,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2027,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2042,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2054,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2056,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2113,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2115,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2154,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2168,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2180,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2182,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2278,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2371,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2383,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2479,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2481,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2494,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2502,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2539,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2578,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2603,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2608,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2632,plain,
esk4_2(X1,esk9_0) = X1,
inference(rename_variables,[],[i_0_523]) ).
cnf(i_0_2659,plain,
singleton(singleton(esk4_2(X1,esk7_0))) != X1,
inference(rename_variables,[],[i_0_513]) ).
cnf(i_0_2700,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2704,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2751,plain,
~ in(X1,esk5_1(singleton(empty_set))),
inference(rename_variables,[],[i_0_518]) ).
cnf(i_0_2969,plain,
esk12_1(X1) = esk5_1(powerset(esk7_0)),
inference(rename_variables,[],[i_0_510]) ).
cnf(i_0_550,plain,
singleton(singleton(esk4_2(esk14_0,esk7_0))) != esk4_2(esk14_0,esk9_0),
inference(scs_inference,[],[i_0_296,i_0_538,i_0_541,i_0_545,i_0_294,i_0_513,i_0_535,i_0_522,i_0_523,i_0_500,i_0_483,i_0_504,i_0_135,i_0_115,i_0_149,i_0_140,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154,i_0_240,i_0_196,i_0_141]) ).
cnf(i_0_561,plain,
esk4_2(singleton(singleton(X1)),esk7_0) != X1,
inference(scs_inference,[],[i_0_534,i_0_149]) ).
cnf(i_0_562,plain,
singleton(esk4_2(singleton(X1),esk7_0)) != X1,
inference(rename_variables,[],[i_0_534]) ).
cnf(i_0_563,plain,
relation_empty_yielding(esk4_2(esk15_0,esk9_0)),
inference(scs_inference,[],[i_0_536,i_0_534,i_0_149,i_0_197]) ).
cnf(i_0_564,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_566,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_568,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_570,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_572,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_576,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_542]) ).
cnf(i_0_703,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_706,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_708,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_710,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_814,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_819,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_821,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_823,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_926,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_931,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_933,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_935,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1049,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1053,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1055,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1057,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1101,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1105,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1107,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1109,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1179,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1183,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1185,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1187,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1201,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1205,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1207,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1209,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1371,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1375,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1377,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1379,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1393,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1397,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1399,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1401,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1495,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1499,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1501,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1503,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1615,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1619,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1621,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1623,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1735,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1741,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1743,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1745,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1834,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_542]) ).
cnf(i_0_1857,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1863,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1865,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1867,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1879,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1883,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_542]) ).
cnf(i_0_1885,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1887,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_1889,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2008,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2010,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2014,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2018,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2030,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2032,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2036,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2040,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2088,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_542]) ).
cnf(i_0_2157,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2159,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2161,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2165,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2252,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2254,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2256,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2260,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2347,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2349,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2351,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2355,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2439,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_542]) ).
cnf(i_0_2455,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2459,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2461,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_2465,plain,
X1 = esk4_2(X1,esk9_0),
inference(rename_variables,[],[i_0_536]) ).
cnf(i_0_565,plain,
relation(esk4_2(esk17_0,esk9_0)),
inference(scs_inference,[],[i_0_536,i_0_564,i_0_534,i_0_149,i_0_197,i_0_194]) ).
cnf(i_0_567,plain,
function(esk4_2(esk17_0,esk9_0)),
inference(scs_inference,[],[i_0_536,i_0_564,i_0_566,i_0_534,i_0_149,i_0_197,i_0_194,i_0_195]) ).
cnf(i_0_569,plain,
relation_empty_yielding(esk4_2(empty_set,esk9_0)),
inference(scs_inference,[],[i_0_536,i_0_564,i_0_566,i_0_568,i_0_534,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242]) ).
cnf(i_0_571,plain,
one_to_one(esk4_2(esk10_0,esk9_0)),
inference(scs_inference,[],[i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_534,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241]) ).
cnf(i_0_573,plain,
X1 = esk4_2(X1,empty_set),
inference(scs_inference,[],[i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_282,i_0_534,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140]) ).
cnf(i_0_574,plain,
singleton(esk4_2(singleton(X1),empty_set)) != X1,
inference(scs_inference,[],[i_0_542,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_282,i_0_534,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100]) ).
cnf(i_0_578,plain,
relation_empty_yielding(esk4_2(esk4_2(relation_image(esk17_0,empty_set),esk7_0),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_542,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_282,i_0_534,i_0_511,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100,i_0_162]) ).
cnf(i_0_580,plain,
empty_set != esk11_0,
inference(scs_inference,[],[i_0_480,i_0_542,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_282,i_0_534,i_0_511,i_0_138,i_0_116,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100,i_0_162,i_0_158]) ).
cnf(i_0_581,plain,
one_to_one(esk4_2(esk9_0,esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_579,i_0_542,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_282,i_0_319,i_0_534,i_0_511,i_0_138,i_0_116,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100,i_0_162,i_0_158,i_0_161]) ).
cnf(i_0_583,plain,
~ in(relation_dom(esk17_0),esk5_1(singleton(esk4_2(esk16_0,empty_set)))),
inference(scs_inference,[],[i_0_480,i_0_579,i_0_280,i_0_542,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_282,i_0_368,i_0_319,i_0_534,i_0_511,i_0_138,i_0_116,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100,i_0_162,i_0_158,i_0_161,i_0_153]) ).
cnf(i_0_585,plain,
function(esk4_2(esk4_2(relation_image(esk17_0,empty_set),esk7_0),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_579,i_0_582,i_0_280,i_0_542,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_520,i_0_282,i_0_368,i_0_319,i_0_534,i_0_511,i_0_138,i_0_116,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155]) ).
cnf(i_0_587,plain,
relation(esk4_2(esk5_1(singleton(esk17_0)),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_579,i_0_582,i_0_586,i_0_280,i_0_542,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_520,i_0_343,i_0_282,i_0_368,i_0_319,i_0_534,i_0_511,i_0_138,i_0_116,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154]) ).
cnf(i_0_589,plain,
~ in(esk5_1(singleton(singleton(X1))),X1),
inference(scs_inference,[],[i_0_480,i_0_579,i_0_582,i_0_586,i_0_280,i_0_584,i_0_542,i_0_576,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_520,i_0_343,i_0_282,i_0_368,i_0_319,i_0_534,i_0_511,i_0_138,i_0_116,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154,i_0_152]) ).
cnf(i_0_591,plain,
~ empty(esk4_2(singleton(singleton(empty_set)),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_579,i_0_582,i_0_586,i_0_280,i_0_584,i_0_542,i_0_576,i_0_536,i_0_564,i_0_566,i_0_568,i_0_570,i_0_520,i_0_343,i_0_282,i_0_368,i_0_319,i_0_534,i_0_511,i_0_138,i_0_116,i_0_149,i_0_197,i_0_194,i_0_195,i_0_242,i_0_241,i_0_140,i_0_100,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154,i_0_152,i_0_114]) ).
cnf(i_0_603,plain,
esk4_2(singleton(singleton(X1)),empty_set) != X1,
inference(scs_inference,[],[i_0_574,i_0_149]) ).
cnf(i_0_604,plain,
singleton(esk4_2(singleton(X1),empty_set)) != X1,
inference(rename_variables,[],[i_0_574]) ).
cnf(i_0_605,plain,
relation_empty_yielding(esk4_2(esk15_0,empty_set)),
inference(scs_inference,[],[i_0_573,i_0_574,i_0_149,i_0_197]) ).
cnf(i_0_606,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_608,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_610,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_612,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_614,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_616,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_618,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_724,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_729,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_731,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_733,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_844,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_849,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_851,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_853,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_956,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_960,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_962,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_964,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1075,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1079,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1081,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1083,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1227,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1231,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1233,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1235,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1251,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1255,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1257,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1259,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1273,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1277,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1279,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1281,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1297,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1301,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1303,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1305,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1418,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1422,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1424,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1426,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1520,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1524,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1526,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1528,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1544,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1548,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1550,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1552,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1639,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1643,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1645,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1647,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1708,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1714,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1716,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1718,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1830,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1836,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1838,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1840,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1984,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1986,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1990,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_1994,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2131,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2133,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2135,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2141,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2229,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2231,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2233,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2237,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2321,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2323,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2327,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2331,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2411,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2413,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2415,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_2419,plain,
X1 = esk4_2(X1,empty_set),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_607,plain,
relation(esk4_2(esk17_0,empty_set)),
inference(scs_inference,[],[i_0_573,i_0_606,i_0_574,i_0_149,i_0_197,i_0_194]) ).
cnf(i_0_609,plain,
function(esk4_2(esk17_0,empty_set)),
inference(scs_inference,[],[i_0_573,i_0_606,i_0_608,i_0_574,i_0_149,i_0_197,i_0_194,i_0_195]) ).
cnf(i_0_611,plain,
function(esk4_2(esk14_0,empty_set)),
inference(scs_inference,[],[i_0_573,i_0_606,i_0_608,i_0_610,i_0_574,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240]) ).
cnf(i_0_613,plain,
one_to_one(esk4_2(esk14_0,empty_set)),
inference(scs_inference,[],[i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_574,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196]) ).
cnf(i_0_615,plain,
relation_empty_yielding(esk4_2(empty_set,empty_set)),
inference(scs_inference,[],[i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_574,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242]) ).
cnf(i_0_617,plain,
one_to_one(esk4_2(esk10_0,empty_set)),
inference(scs_inference,[],[i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_616,i_0_574,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242,i_0_241]) ).
cnf(i_0_619,plain,
relation_empty_yielding(esk4_2(esk4_2(empty_set,esk7_0),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_616,i_0_574,i_0_506,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242,i_0_241,i_0_162]) ).
cnf(i_0_621,plain,
empty_set != esk4_2(singleton(singleton(empty_set)),esk7_0),
inference(scs_inference,[],[i_0_480,i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_616,i_0_574,i_0_506,i_0_138,i_0_591,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242,i_0_241,i_0_162,i_0_158]) ).
cnf(i_0_622,plain,
one_to_one(esk4_2(esk4_2(esk14_0,esk7_0),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_620,i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_616,i_0_574,i_0_502,i_0_506,i_0_138,i_0_591,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242,i_0_241,i_0_162,i_0_158,i_0_161]) ).
cnf(i_0_624,plain,
~ in(X1,esk5_1(singleton(esk7_0))),
inference(scs_inference,[],[i_0_480,i_0_620,i_0_280,i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_616,i_0_205,i_0_574,i_0_502,i_0_506,i_0_138,i_0_591,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242,i_0_241,i_0_162,i_0_158,i_0_161,i_0_153]) ).
cnf(i_0_626,plain,
function(esk4_2(esk4_2(esk17_0,esk9_0),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_620,i_0_623,i_0_280,i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_616,i_0_567,i_0_205,i_0_574,i_0_502,i_0_506,i_0_138,i_0_591,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242,i_0_241,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155]) ).
cnf(i_0_628,plain,
relation(esk4_2(esk5_1(singleton(esk11_0)),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_620,i_0_623,i_0_627,i_0_280,i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_616,i_0_567,i_0_413,i_0_205,i_0_574,i_0_502,i_0_506,i_0_138,i_0_591,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242,i_0_241,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154]) ).
cnf(i_0_630,plain,
singleton(singleton(esk4_2(X1,empty_set))) != X1,
inference(scs_inference,[],[i_0_480,i_0_620,i_0_623,i_0_627,i_0_280,i_0_573,i_0_606,i_0_608,i_0_610,i_0_612,i_0_614,i_0_616,i_0_567,i_0_413,i_0_205,i_0_574,i_0_502,i_0_506,i_0_138,i_0_591,i_0_149,i_0_197,i_0_194,i_0_195,i_0_240,i_0_196,i_0_242,i_0_241,i_0_162,i_0_158,i_0_161,i_0_153,i_0_155,i_0_154,i_0_150]) ).
cnf(i_0_636,plain,
~ empty(esk4_2(singleton(singleton(empty_set)),empty_set)),
inference(scs_inference,[],[i_0_603,i_0_114]) ).
cnf(i_0_637,plain,
esk4_2(singleton(singleton(X1)),empty_set) != X1,
inference(rename_variables,[],[i_0_603]) ).
cnf(i_0_639,plain,
esk5_1(singleton(esk9_0)) = esk12_1(X1),
inference(scs_inference,[],[i_0_290,i_0_409,i_0_603,i_0_114,i_0_85]) ).
cnf(i_0_643,plain,
relation_empty_yielding(esk4_2(esk4_2(esk4_2(empty_set,esk7_0),esk7_0),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_290,i_0_409,i_0_603,i_0_619,i_0_114,i_0_85,i_0_162]) ).
cnf(i_0_645,plain,
esk10_0 != esk4_2(singleton(singleton(empty_set)),esk7_0),
inference(scs_inference,[],[i_0_480,i_0_290,i_0_409,i_0_603,i_0_619,i_0_133,i_0_591,i_0_114,i_0_85,i_0_162,i_0_158]) ).
cnf(i_0_646,plain,
one_to_one(esk4_2(esk4_2(esk14_0,esk9_0),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_644,i_0_290,i_0_409,i_0_603,i_0_549,i_0_619,i_0_133,i_0_591,i_0_114,i_0_85,i_0_162,i_0_158,i_0_161]) ).
cnf(i_0_648,plain,
function(esk4_2(esk4_2(esk17_0,empty_set),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_644,i_0_647,i_0_290,i_0_409,i_0_609,i_0_603,i_0_549,i_0_619,i_0_133,i_0_591,i_0_114,i_0_85,i_0_162,i_0_158,i_0_161,i_0_155]) ).
cnf(i_0_650,plain,
~ in(X1,relation_image(esk17_0,relation_image(esk17_0,esk12_1(esk10_0)))),
inference(scs_inference,[],[i_0_480,i_0_644,i_0_647,i_0_255,i_0_290,i_0_641,i_0_409,i_0_609,i_0_603,i_0_549,i_0_619,i_0_133,i_0_591,i_0_114,i_0_85,i_0_162,i_0_158,i_0_161,i_0_155,i_0_153]) ).
cnf(i_0_652,plain,
relation(esk4_2(esk5_1(singleton(esk14_0)),esk7_0)),
inference(scs_inference,[],[i_0_480,i_0_644,i_0_647,i_0_649,i_0_255,i_0_290,i_0_641,i_0_409,i_0_609,i_0_433,i_0_603,i_0_549,i_0_619,i_0_133,i_0_591,i_0_114,i_0_85,i_0_162,i_0_158,i_0_161,i_0_155,i_0_153,i_0_154]) ).
cnf(c_0_141,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
i_0_95 ).
cnf(c_0_142,plain,
( in(esk1_4(X1,X2,X3,X4),X2)
| ~ in(X4,X3)
| X3 != relation_image(X1,X2)
| ~ relation(X1)
| ~ function(X1) ),
i_0_77 ).
cnf(c_0_143,plain,
( X1 = apply(X2,esk1_4(X2,X3,X4,X1))
| ~ in(X1,X4)
| X4 != relation_image(X2,X3)
| ~ relation(X2)
| ~ function(X2) ),
i_0_76 ).
cnf(c_0_144,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(er,[status(thm)],[c_0_141]) ).
cnf(c_0_145,plain,
( in(esk1_4(X1,X2,relation_image(X1,X2),X3),X2)
| ~ function(X1)
| ~ relation(X1)
| ~ in(X3,relation_image(X1,X2)) ),
inference(er,[status(thm)],[c_0_142]) ).
cnf(c_0_146,plain,
( apply(X1,esk1_4(X1,X2,relation_image(X1,X2),X3)) = X3
| ~ function(X1)
| ~ relation(X1)
| ~ in(X3,relation_image(X1,X2)) ),
inference(er,[status(thm)],[c_0_143]) ).
cnf(c_0_147,plain,
( esk1_4(X1,singleton(X2),relation_image(X1,singleton(X2)),X3) = X2
| ~ function(X1)
| ~ relation(X1)
| ~ in(X3,relation_image(X1,singleton(X2))) ),
inference(spm,[status(thm)],[c_0_144,c_0_145]) ).
cnf(c_0_148,negated_conjecture,
relation_image(esk17_0,singleton(esk16_0)) != singleton(apply(esk17_0,esk16_0)),
i_0_88 ).
cnf(c_0_149,plain,
( in(esk4_2(X1,X2),X2)
| esk4_2(X1,X2) = X1
| X2 = singleton(X1) ),
i_0_89 ).
cnf(c_0_150,plain,
( apply(X1,X2) = X3
| ~ function(X1)
| ~ relation(X1)
| ~ in(X3,relation_image(X1,singleton(X2))) ),
inference(spm,[status(thm)],[c_0_146,c_0_147]) ).
cnf(c_0_151,negated_conjecture,
( esk4_2(apply(esk17_0,esk16_0),relation_image(esk17_0,singleton(esk16_0))) = apply(esk17_0,esk16_0)
| in(esk4_2(apply(esk17_0,esk16_0),relation_image(esk17_0,singleton(esk16_0))),relation_image(esk17_0,singleton(esk16_0))) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_148,c_0_149])]) ).
cnf(c_0_152,negated_conjecture,
function(esk17_0),
i_0_129 ).
cnf(c_0_153,negated_conjecture,
relation(esk17_0),
i_0_120 ).
cnf(c_0_154,plain,
( X1 = singleton(X2)
| ~ in(esk4_2(X2,X1),X1)
| esk4_2(X2,X1) != X2 ),
i_0_84 ).
cnf(c_0_155,negated_conjecture,
esk4_2(apply(esk17_0,esk16_0),relation_image(esk17_0,singleton(esk16_0))) = apply(esk17_0,esk16_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_150,c_0_151]),c_0_152]),c_0_153])]) ).
cnf(c_0_156,plain,
( in(X1,X2)
| ~ in(X3,relation_dom(X4))
| ~ in(X3,X5)
| X1 != apply(X4,X3)
| X2 != relation_image(X4,X5)
| ~ relation(X4)
| ~ function(X4) ),
i_0_82 ).
cnf(c_0_157,plain,
( in(X1,X2)
| X1 != X3
| X2 != singleton(X3) ),
i_0_100 ).
cnf(c_0_158,plain,
~ in(apply(esk17_0,esk16_0),relation_image(esk17_0,singleton(esk16_0))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_154,c_0_155]),c_0_148]) ).
cnf(c_0_159,plain,
( in(apply(X1,X2),relation_image(X1,X3))
| ~ function(X1)
| ~ relation(X1)
| ~ in(X2,relation_dom(X1))
| ~ in(X2,X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_156])]) ).
cnf(c_0_160,negated_conjecture,
in(esk16_0,relation_dom(esk17_0)),
i_0_109 ).
cnf(c_0_161,plain,
in(X1,singleton(X1)),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_157])]) ).
cnf(c_0_162,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_158,c_0_159]),c_0_152]),c_0_153]),c_0_160]),c_0_161])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU049+1 : TPTP v9.2.1. Bugfixed v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n004.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 02:42:02 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 186.74/142.33 % Version : CSE_E---1.7
% 186.74/142.33 % Problem : theBenchmark.p
% 186.74/142.33 % SZS status Theorem for theBenchmark.p
% 186.74/142.33 % SZS output start CNFRefutation
% See solution above
% 194.04/149.64 % Total time : 141.967s
%------------------------------------------------------------------------------