%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU422+1 : TPTP v9.2.1. Released v3.4.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 : n018.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:12:15 PM UTC 2026
% Result : Theorem 210.13s 128.43s
% Output : CNFRefutation 214.93s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_651)
% Comments :
%------------------------------------------------------------------------------
fof(fraenkel_a_2_0_relset_2,axiom,
! [X1,X2,X3] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X3,k1_zfmisc_1(X2)) )
=> ( r2_hidden(X1,a_2_0_relset_2(X2,X3))
<=> ? [X4] :
( m1_subset_1(X4,X2)
& X1 = k1_tarski(X4)
& r2_hidden(X4,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fraenkel_a_2_0_relset_2) ).
fof(t16_relset_2,conjecture,
! [X1] :
( ~ v1_xboole_0(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> m1_subset_1(a_2_0_relset_2(X1,X2),k1_zfmisc_1(k1_zfmisc_1(X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_relset_2) ).
fof(antisymmetry_r2_hidden,axiom,
! [X1,X2] :
( r2_hidden(X1,X2)
=> ~ r2_hidden(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(rc1_subset_1,axiom,
! [X1] :
( ~ v1_xboole_0(X1)
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& ~ v1_xboole_0(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_subset_1) ).
fof(fc2_subset_1,axiom,
! [X1] : ~ v1_xboole_0(k1_tarski(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(fc1_subset_1,axiom,
! [X1] : ~ v1_xboole_0(k1_zfmisc_1(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(rc2_relat_1,axiom,
? [X1] :
( ~ v1_xboole_0(X1)
& v1_relat_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(t2_tarski,axiom,
! [X1,X2] :
( ! [X3] :
( r2_hidden(X3,X1)
<=> r2_hidden(X3,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(d3_tarski,axiom,
! [X1,X2] :
( r1_tarski(X1,X2)
<=> ! [X3] :
( r2_hidden(X3,X1)
=> r2_hidden(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(t4_subset,axiom,
! [X1,X2,X3] :
( ( r2_hidden(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(X3)) )
=> m1_subset_1(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [X1,X2,X3] :
~ ( r2_hidden(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(X3))
& v1_xboole_0(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(t37_zfmisc_1,axiom,
! [X1,X2] :
( r1_tarski(k1_tarski(X1),X2)
<=> r2_hidden(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_zfmisc_1) ).
fof(t3_subset,axiom,
! [X1,X2] :
( m1_subset_1(X1,k1_zfmisc_1(X2))
<=> r1_tarski(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(t2_subset,axiom,
! [X1,X2] :
( m1_subset_1(X1,X2)
=> ( v1_xboole_0(X2)
| r2_hidden(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(t1_subset,axiom,
! [X1,X2] :
( r2_hidden(X1,X2)
=> m1_subset_1(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(t7_boole,axiom,
! [X1,X2] :
~ ( r2_hidden(X1,X2)
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(rc2_subset_1,axiom,
! [X1] :
? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(existence_m1_subset_1,axiom,
! [X1] :
? [X2] : m1_subset_1(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(t8_boole,axiom,
! [X1,X2] :
~ ( v1_xboole_0(X1)
& X1 != X2
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
fof(reflexivity_r1_tarski,axiom,
! [X1,X2] : r1_tarski(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(cc1_relat_1,axiom,
! [X1] :
( v1_xboole_0(X1)
=> v1_relat_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relat_1) ).
fof(t6_boole,axiom,
! [X1] :
( v1_xboole_0(X1)
=> X1 = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(rc3_relat_1,axiom,
? [X1] :
( v1_relat_1(X1)
& v3_relat_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_relat_1) ).
fof(rc1_relat_1,axiom,
? [X1] :
( v1_xboole_0(X1)
& v1_relat_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_relat_1) ).
fof(fc12_relat_1,axiom,
( v1_xboole_0(k1_xboole_0)
& v1_relat_1(k1_xboole_0)
& v3_relat_1(k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc12_relat_1) ).
fof(fc4_relat_1,axiom,
( v1_xboole_0(k1_xboole_0)
& v1_relat_1(k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(i_0_26,plain,
! [X1,X2,X3] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X3,k1_zfmisc_1(X2)) )
=> ( r2_hidden(X1,a_2_0_relset_2(X2,X3))
<=> ? [X4] :
( m1_subset_1(X4,X2)
& X1 = k1_tarski(X4)
& r2_hidden(X4,X3) ) ) ),
inference(fof_simplification,[status(thm)],[fraenkel_a_2_0_relset_2]) ).
fof(i_0_27,negated_conjecture,
~ ! [X1] :
( ~ v1_xboole_0(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> m1_subset_1(a_2_0_relset_2(X1,X2),k1_zfmisc_1(k1_zfmisc_1(X1))) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t16_relset_2])]) ).
fof(i_0_28,plain,
! [X1,X2] :
( r2_hidden(X1,X2)
=> ~ r2_hidden(X2,X1) ),
inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden]) ).
fof(i_0_29,plain,
! [X1] :
( ~ v1_xboole_0(X1)
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& ~ v1_xboole_0(X2) ) ),
inference(fof_simplification,[status(thm)],[rc1_subset_1]) ).
fof(i_0_30,plain,
! [X1] : ~ v1_xboole_0(k1_tarski(X1)),
inference(fof_simplification,[status(thm)],[fc2_subset_1]) ).
fof(i_0_31,plain,
! [X1] : ~ v1_xboole_0(k1_zfmisc_1(X1)),
inference(fof_simplification,[status(thm)],[fc1_subset_1]) ).
fof(i_0_32,plain,
? [X1] :
( ~ v1_xboole_0(X1)
& v1_relat_1(X1) ),
inference(fof_simplification,[status(thm)],[rc2_relat_1]) ).
fof(i_0_33,plain,
! [X67,X68,X69,X71] :
( ( m1_subset_1(esk5_3(X67,X68,X69),X68)
| ~ r2_hidden(X67,a_2_0_relset_2(X68,X69))
| v1_xboole_0(X68)
| ~ m1_subset_1(X69,k1_zfmisc_1(X68)) )
& ( X67 = k1_tarski(esk5_3(X67,X68,X69))
| ~ r2_hidden(X67,a_2_0_relset_2(X68,X69))
| v1_xboole_0(X68)
| ~ m1_subset_1(X69,k1_zfmisc_1(X68)) )
& ( r2_hidden(esk5_3(X67,X68,X69),X69)
| ~ r2_hidden(X67,a_2_0_relset_2(X68,X69))
| v1_xboole_0(X68)
| ~ m1_subset_1(X69,k1_zfmisc_1(X68)) )
& ( ~ m1_subset_1(X71,X68)
| X67 != k1_tarski(X71)
| ~ r2_hidden(X71,X69)
| r2_hidden(X67,a_2_0_relset_2(X68,X69))
| v1_xboole_0(X68)
| ~ m1_subset_1(X69,k1_zfmisc_1(X68)) ) ),
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_26])])])])]) ).
fof(i_0_34,plain,
! [X84,X85] :
( ( ~ r2_hidden(esk11_2(X84,X85),X84)
| ~ r2_hidden(esk11_2(X84,X85),X85)
| X84 = X85 )
& ( r2_hidden(esk11_2(X84,X85),X84)
| r2_hidden(esk11_2(X84,X85),X85)
| X84 = X85 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_tarski])])])]) ).
fof(i_0_35,plain,
! [X57,X58,X59,X60,X61] :
( ( ~ r1_tarski(X57,X58)
| ~ r2_hidden(X59,X57)
| r2_hidden(X59,X58) )
& ( r2_hidden(esk3_2(X60,X61),X60)
| r1_tarski(X60,X61) )
& ( ~ r2_hidden(esk3_2(X60,X61),X61)
| r1_tarski(X60,X61) ) ),
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)],[d3_tarski])])])])])]) ).
fof(i_0_36,negated_conjecture,
( ~ v1_xboole_0(esk1_0)
& m1_subset_1(esk2_0,k1_zfmisc_1(esk1_0))
& ~ m1_subset_1(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(k1_zfmisc_1(esk1_0))) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_27])])]) ).
fof(i_0_37,plain,
! [X91,X92,X93] :
( ~ r2_hidden(X91,X92)
| ~ m1_subset_1(X92,k1_zfmisc_1(X93))
| m1_subset_1(X91,X93) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t4_subset])]) ).
fof(i_0_38,plain,
! [X94,X95,X96] :
( ~ r2_hidden(X94,X95)
| ~ m1_subset_1(X95,k1_zfmisc_1(X96))
| ~ v1_xboole_0(X96) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_subset])]) ).
fof(i_0_39,plain,
! [X87,X88] :
( ( ~ r1_tarski(k1_tarski(X87),X88)
| r2_hidden(X87,X88) )
& ( ~ r2_hidden(X87,X88)
| r1_tarski(k1_tarski(X87),X88) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t37_zfmisc_1])]) ).
fof(i_0_40,plain,
! [X89,X90] :
( ( ~ m1_subset_1(X89,k1_zfmisc_1(X90))
| r1_tarski(X89,X90) )
& ( ~ r1_tarski(X89,X90)
| m1_subset_1(X89,k1_zfmisc_1(X90)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_subset])]) ).
fof(i_0_41,plain,
! [X54,X55] :
( ~ r2_hidden(X54,X55)
| ~ r2_hidden(X55,X54) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_28])]) ).
fof(i_0_42,plain,
! [X82,X83] :
( ~ m1_subset_1(X82,X83)
| v1_xboole_0(X83)
| r2_hidden(X82,X83) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_subset])]) ).
fof(i_0_43,plain,
! [X80,X81] :
( ~ r2_hidden(X80,X81)
| m1_subset_1(X80,X81) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t1_subset])]) ).
fof(i_0_44,plain,
! [X73] :
( ( m1_subset_1(esk7_1(X73),k1_zfmisc_1(X73))
| v1_xboole_0(X73) )
& ( ~ v1_xboole_0(esk7_1(X73))
| v1_xboole_0(X73) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_29])])])]) ).
fof(i_0_45,plain,
! [X98,X99] :
( ~ r2_hidden(X98,X99)
| ~ v1_xboole_0(X99) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_boole])]) ).
fof(i_0_46,plain,
! [X76] :
( m1_subset_1(esk9_1(X76),k1_zfmisc_1(X76))
& v1_xboole_0(esk9_1(X76)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_subset_1])]) ).
fof(i_0_47,plain,
! [X63] : m1_subset_1(esk4_1(X63),X63),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m1_subset_1])]) ).
fof(i_0_48,plain,
! [X66] : ~ v1_xboole_0(k1_tarski(X66)),
inference(variable_rename,[status(thm)],[i_0_30]) ).
fof(i_0_49,plain,
! [X65] : ~ v1_xboole_0(k1_zfmisc_1(X65)),
inference(variable_rename,[status(thm)],[i_0_31]) ).
fof(i_0_50,plain,
! [X100,X101] :
( ~ v1_xboole_0(X100)
| X100 = X101
| ~ v1_xboole_0(X101) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t8_boole])]) ).
fof(i_0_51,plain,
! [X79] : r1_tarski(X79,X79),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])]) ).
fof(i_0_52,plain,
! [X56] :
( ~ v1_xboole_0(X56)
| v1_relat_1(X56) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc1_relat_1])]) ).
fof(i_0_53,plain,
! [X97] :
( ~ v1_xboole_0(X97)
| X97 = k1_xboole_0 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(i_0_54,plain,
( ~ v1_xboole_0(esk8_0)
& v1_relat_1(esk8_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_32])]) ).
fof(i_0_55,plain,
( v1_relat_1(esk10_0)
& v3_relat_1(esk10_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc3_relat_1])]) ).
fof(i_0_56,plain,
( v1_xboole_0(esk6_0)
& v1_relat_1(esk6_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_relat_1])]) ).
cnf(i_0_57,plain,
( r2_hidden(esk5_3(X1,X2,X3),X3)
| v1_xboole_0(X2)
| ~ r2_hidden(X1,a_2_0_relset_2(X2,X3))
| ~ m1_subset_1(X3,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_58,plain,
( m1_subset_1(esk5_3(X1,X2,X3),X2)
| v1_xboole_0(X2)
| ~ r2_hidden(X1,a_2_0_relset_2(X2,X3))
| ~ m1_subset_1(X3,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_59,plain,
( X1 = k1_tarski(esk5_3(X1,X2,X3))
| v1_xboole_0(X2)
| ~ r2_hidden(X1,a_2_0_relset_2(X2,X3))
| ~ m1_subset_1(X3,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_60,plain,
( r2_hidden(X3,a_2_0_relset_2(X2,X4))
| v1_xboole_0(X2)
| ~ m1_subset_1(X1,X2)
| X3 != k1_tarski(X1)
| ~ r2_hidden(X1,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_61,plain,
( X1 = X2
| ~ r2_hidden(esk11_2(X1,X2),X1)
| ~ r2_hidden(esk11_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_62,plain,
( r2_hidden(esk11_2(X1,X2),X1)
| r2_hidden(esk11_2(X1,X2),X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_63,plain,
( r1_tarski(X1,X2)
| ~ r2_hidden(esk3_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_64,negated_conjecture,
~ m1_subset_1(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(k1_zfmisc_1(esk1_0))),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_65,plain,
( m1_subset_1(X1,X3)
| ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3)) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_66,plain,
( ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| ~ v1_xboole_0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_67,plain,
( r2_hidden(X3,X2)
| ~ r1_tarski(X1,X2)
| ~ r2_hidden(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_68,plain,
( r2_hidden(esk3_2(X1,X2),X1)
| r1_tarski(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_69,plain,
( r2_hidden(X1,X2)
| ~ r1_tarski(k1_tarski(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_70,plain,
( r1_tarski(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_71,plain,
( ~ r2_hidden(X1,X2)
| ~ r2_hidden(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_72,plain,
( r1_tarski(k1_tarski(X1),X2)
| ~ r2_hidden(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_73,plain,
( m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r1_tarski(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_74,plain,
( v1_xboole_0(X2)
| r2_hidden(X1,X2)
| ~ m1_subset_1(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_75,plain,
( m1_subset_1(X1,X2)
| ~ r2_hidden(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_76,plain,
( m1_subset_1(esk7_1(X1),k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_77,plain,
( ~ r2_hidden(X1,X2)
| ~ v1_xboole_0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_78,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_79,plain,
( v1_xboole_0(X1)
| ~ v1_xboole_0(esk7_1(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_80,plain,
m1_subset_1(esk4_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_81,plain,
~ v1_xboole_0(k1_tarski(X1)),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_82,plain,
~ v1_xboole_0(k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_83,plain,
( X1 = X2
| ~ v1_xboole_0(X1)
| ~ v1_xboole_0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_84,negated_conjecture,
m1_subset_1(esk2_0,k1_zfmisc_1(esk1_0)),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_85,plain,
r1_tarski(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_86,plain,
( v1_relat_1(X1)
| ~ v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_87,plain,
v1_xboole_0(esk9_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_88,plain,
( X1 = k1_xboole_0
| ~ v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_89,plain,
~ v1_xboole_0(esk8_0),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_90,negated_conjecture,
~ v1_xboole_0(esk1_0),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_91,plain,
v3_relat_1(esk10_0),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_92,plain,
v3_relat_1(k1_xboole_0),
inference(split_conjunct,[status(thm)],[fc12_relat_1]),
[final] ).
cnf(i_0_93,plain,
v1_relat_1(esk10_0),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_94,plain,
v1_relat_1(esk8_0),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_95,plain,
v1_relat_1(esk6_0),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_96,plain,
v1_relat_1(k1_xboole_0),
inference(split_conjunct,[status(thm)],[fc4_relat_1]),
[final] ).
cnf(i_0_97,plain,
v1_relat_1(k1_xboole_0),
inference(split_conjunct,[status(thm)],[fc12_relat_1]),
[final] ).
cnf(i_0_98,plain,
v1_xboole_0(esk6_0),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_99,plain,
v1_xboole_0(k1_xboole_0),
inference(split_conjunct,[status(thm)],[fc4_relat_1]),
[final] ).
cnf(i_0_100,plain,
v1_xboole_0(k1_xboole_0),
inference(split_conjunct,[status(thm)],[fc12_relat_1]),
[final] ).
cnf(i_0_101,axiom,
X1 = X1 ).
cnf(i_0_102,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_103,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_104,axiom,
( X1 != X2
| k1_tarski(X1) = k1_tarski(X2) ) ).
cnf(i_0_105,axiom,
( X1 != X2
| ~ r2_hidden(X1,X3)
| r2_hidden(X2,X3) ) ).
cnf(i_0_106,axiom,
( X1 != X2
| ~ r2_hidden(X3,X1)
| r2_hidden(X3,X2) ) ).
cnf(i_0_107,axiom,
( X1 != X2
| ~ v1_xboole_0(X1)
| v1_xboole_0(X2) ) ).
cnf(i_0_108,axiom,
( X1 != X2
| ~ m1_subset_1(X1,X3)
| m1_subset_1(X2,X3) ) ).
cnf(i_0_109,axiom,
( X1 != X2
| ~ m1_subset_1(X3,X1)
| m1_subset_1(X3,X2) ) ).
cnf(i_0_110,axiom,
( X1 != X2
| ~ r1_tarski(X1,X3)
| r1_tarski(X2,X3) ) ).
cnf(i_0_111,axiom,
( X1 != X2
| ~ r1_tarski(X3,X1)
| r1_tarski(X3,X2) ) ).
cnf(i_0_112,axiom,
( X1 != X2
| ~ v1_relat_1(X1)
| v1_relat_1(X2) ) ).
cnf(i_0_113,axiom,
( X1 != X2
| ~ v3_relat_1(X1)
| v3_relat_1(X2) ) ).
cnf(i_0_698,plain,
esk8_0 != esk4_1(k1_zfmisc_1(esk6_0)),
inference(scs_inference,[],[i_0_651,i_0_614,i_0_413,i_0_612,i_0_622,i_0_484,i_0_532,i_0_512,i_0_616,i_0_626,i_0_563,i_0_325,i_0_577,i_0_159,i_0_168,i_0_166,i_0_122,i_0_497,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_104,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_67,i_0_103]) ).
cnf(i_0_699,plain,
esk4_1(k1_zfmisc_1(esk6_0)) != esk7_1(a_2_0_relset_2(esk1_0,esk2_0)),
inference(scs_inference,[],[i_0_651,i_0_614,i_0_413,i_0_612,i_0_622,i_0_484,i_0_532,i_0_512,i_0_508,i_0_645,i_0_616,i_0_626,i_0_563,i_0_325,i_0_577,i_0_159,i_0_168,i_0_166,i_0_122,i_0_497,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_104,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_67,i_0_103,i_0_107]) ).
cnf(i_0_700,plain,
r1_tarski(k1_tarski(k1_tarski(k1_xboole_0)),k1_tarski(k1_tarski(esk6_0))),
inference(scs_inference,[],[i_0_651,i_0_614,i_0_413,i_0_612,i_0_622,i_0_484,i_0_532,i_0_512,i_0_508,i_0_645,i_0_616,i_0_626,i_0_563,i_0_325,i_0_577,i_0_159,i_0_168,i_0_166,i_0_122,i_0_497,i_0_82,i_0_85,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_104,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_67,i_0_103,i_0_107,i_0_110]) ).
cnf(i_0_702,plain,
r2_hidden(esk4_1(k1_zfmisc_1(k1_xboole_0)),k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_651,i_0_614,i_0_413,i_0_612,i_0_622,i_0_484,i_0_532,i_0_512,i_0_653,i_0_508,i_0_645,i_0_616,i_0_626,i_0_563,i_0_325,i_0_577,i_0_159,i_0_168,i_0_166,i_0_122,i_0_497,i_0_82,i_0_85,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_104,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_67,i_0_103,i_0_107,i_0_110,i_0_106]) ).
cnf(i_0_703,plain,
r2_hidden(esk6_0,k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_651,i_0_614,i_0_413,i_0_612,i_0_622,i_0_484,i_0_532,i_0_512,i_0_594,i_0_653,i_0_508,i_0_645,i_0_616,i_0_626,i_0_563,i_0_301,i_0_325,i_0_577,i_0_159,i_0_168,i_0_166,i_0_122,i_0_497,i_0_82,i_0_85,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_104,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_67,i_0_103,i_0_107,i_0_110,i_0_106,i_0_105]) ).
cnf(i_0_704,plain,
r2_hidden(k1_tarski(esk6_0),a_2_0_relset_2(k1_tarski(esk6_0),k1_tarski(k1_xboole_0))),
inference(scs_inference,[],[i_0_651,i_0_614,i_0_413,i_0_612,i_0_622,i_0_484,i_0_532,i_0_512,i_0_594,i_0_653,i_0_508,i_0_645,i_0_616,i_0_626,i_0_563,i_0_301,i_0_325,i_0_577,i_0_159,i_0_694,i_0_168,i_0_166,i_0_122,i_0_497,i_0_81,i_0_82,i_0_85,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_104,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_67,i_0_103,i_0_107,i_0_110,i_0_106,i_0_105,i_0_114]) ).
cnf(i_0_708,plain,
~ v1_xboole_0(a_2_0_relset_2(k1_tarski(esk6_0),k1_tarski(k1_xboole_0))),
inference(scs_inference,[],[i_0_651,i_0_614,i_0_413,i_0_612,i_0_622,i_0_484,i_0_532,i_0_512,i_0_594,i_0_653,i_0_508,i_0_645,i_0_616,i_0_626,i_0_563,i_0_301,i_0_325,i_0_577,i_0_159,i_0_694,i_0_168,i_0_166,i_0_122,i_0_497,i_0_81,i_0_82,i_0_85,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_104,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_67,i_0_103,i_0_107,i_0_110,i_0_106,i_0_105,i_0_114,i_0_77]) ).
cnf(i_0_1384,plain,
r2_hidden(k1_xboole_0,k1_tarski(esk9_1(X1))),
inference(scs_inference,[],[i_0_647,i_0_69]) ).
cnf(i_0_1486,plain,
r1_tarski(k1_tarski(k1_xboole_0),k1_tarski(esk9_1(X1))),
inference(rename_variables,[],[i_0_647]) ).
cnf(i_0_721,plain,
r1_tarski(k1_tarski(esk11_2(esk8_0,k1_xboole_0)),esk8_0),
inference(scs_inference,[],[i_0_689,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72]) ).
cnf(i_0_723,plain,
~ r1_tarski(k1_tarski(esk1_0),esk3_2(esk1_0,esk6_0)),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69]) ).
cnf(i_0_725,plain,
m1_subset_1(k1_tarski(esk3_2(esk1_0,esk6_0)),k1_zfmisc_1(esk1_0)),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_668,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73]) ).
cnf(i_0_727,plain,
~ r2_hidden(k1_tarski(k1_tarski(esk8_0)),k1_zfmisc_1(esk8_0)),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_579,i_0_668,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75]) ).
cnf(i_0_729,plain,
~ m1_subset_1(k1_tarski(k1_tarski(esk1_0)),k1_zfmisc_1(esk2_0)),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_579,i_0_668,i_0_670,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70]) ).
cnf(i_0_731,plain,
r2_hidden(esk3_2(k1_zfmisc_1(X1),esk6_0),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_579,i_0_668,i_0_670,i_0_324,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68]) ).
cnf(i_0_733,plain,
~ r2_hidden(esk8_0,esk11_2(esk8_0,k1_xboole_0)),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_579,i_0_668,i_0_670,i_0_324,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71]) ).
cnf(i_0_735,plain,
a_2_0_relset_2(esk1_0,esk9_1(esk1_0)) != k1_tarski(esk6_0),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_579,i_0_368,i_0_668,i_0_670,i_0_324,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102]) ).
cnf(i_0_736,plain,
~ m1_subset_1(k1_tarski(k1_xboole_0),k1_zfmisc_1(a_2_0_relset_2(esk1_0,esk2_0))),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_535,i_0_579,i_0_702,i_0_368,i_0_668,i_0_670,i_0_324,i_0_117,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65]) ).
cnf(i_0_738,plain,
~ m1_subset_1(k1_tarski(k1_tarski(k1_xboole_0)),k1_tarski(esk6_0)),
inference(scs_inference,[],[i_0_680,i_0_689,i_0_535,i_0_579,i_0_640,i_0_702,i_0_368,i_0_668,i_0_670,i_0_324,i_0_117,i_0_81,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74]) ).
cnf(i_0_741,plain,
r2_hidden(esk11_2(k1_zfmisc_1(X1),esk6_0),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_683,i_0_680,i_0_689,i_0_535,i_0_579,i_0_640,i_0_702,i_0_368,i_0_668,i_0_670,i_0_324,i_0_117,i_0_124,i_0_81,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62]) ).
cnf(i_0_744,plain,
m1_subset_1(esk4_1(k1_zfmisc_1(k1_xboole_0)),k1_tarski(esk6_0)),
inference(scs_inference,[],[i_0_637,i_0_683,i_0_680,i_0_689,i_0_535,i_0_579,i_0_640,i_0_702,i_0_368,i_0_668,i_0_670,i_0_324,i_0_117,i_0_328,i_0_124,i_0_81,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108]) ).
cnf(i_0_745,plain,
m1_subset_1(k1_xboole_0,k1_tarski(esk9_1(esk6_0))),
inference(scs_inference,[],[i_0_637,i_0_683,i_0_680,i_0_689,i_0_535,i_0_579,i_0_640,i_0_702,i_0_368,i_0_682,i_0_668,i_0_670,i_0_324,i_0_117,i_0_328,i_0_124,i_0_81,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109]) ).
cnf(i_0_746,plain,
esk9_1(X1) != esk7_1(a_2_0_relset_2(esk1_0,esk2_0)),
inference(scs_inference,[],[i_0_637,i_0_683,i_0_680,i_0_689,i_0_535,i_0_579,i_0_640,i_0_702,i_0_368,i_0_682,i_0_668,i_0_670,i_0_699,i_0_324,i_0_117,i_0_278,i_0_328,i_0_124,i_0_81,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_103]) ).
cnf(i_0_747,plain,
r1_tarski(k1_tarski(esk9_1(esk6_0)),k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_637,i_0_683,i_0_680,i_0_689,i_0_535,i_0_579,i_0_640,i_0_702,i_0_368,i_0_682,i_0_668,i_0_670,i_0_699,i_0_324,i_0_117,i_0_595,i_0_278,i_0_328,i_0_124,i_0_81,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_103,i_0_110]) ).
cnf(i_0_748,plain,
esk8_0 != a_2_0_relset_2(esk8_0,esk9_1(esk8_0)),
inference(scs_inference,[],[i_0_637,i_0_683,i_0_680,i_0_689,i_0_535,i_0_579,i_0_640,i_0_702,i_0_368,i_0_493,i_0_682,i_0_668,i_0_670,i_0_699,i_0_324,i_0_117,i_0_595,i_0_278,i_0_328,i_0_124,i_0_81,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106]) ).
cnf(i_0_750,plain,
esk11_2(esk8_0,k1_xboole_0) != k1_tarski(esk8_0),
inference(scs_inference,[],[i_0_637,i_0_683,i_0_680,i_0_689,i_0_535,i_0_579,i_0_640,i_0_702,i_0_368,i_0_493,i_0_682,i_0_668,i_0_670,i_0_699,i_0_324,i_0_117,i_0_595,i_0_278,i_0_328,i_0_124,i_0_122,i_0_81,i_0_90,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106,i_0_105]) ).
cnf(i_0_760,plain,
~ r2_hidden(esk3_2(k1_tarski(esk1_0),esk3_2(esk1_0,esk6_0)),esk3_2(esk1_0,esk6_0)),
inference(scs_inference,[],[i_0_723,i_0_715,i_0_79,i_0_76,i_0_63]) ).
cnf(i_0_764,plain,
~ r1_tarski(k1_tarski(esk8_0),esk11_2(esk8_0,k1_xboole_0)),
inference(scs_inference,[],[i_0_723,i_0_715,i_0_733,i_0_654,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69]) ).
cnf(i_0_766,plain,
m1_subset_1(k1_tarski(esk9_1(esk6_0)),k1_zfmisc_1(k1_tarski(k1_xboole_0))),
inference(scs_inference,[],[i_0_723,i_0_715,i_0_733,i_0_747,i_0_654,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73]) ).
cnf(i_0_768,plain,
~ r2_hidden(k1_tarski(k1_tarski(esk1_0)),k1_zfmisc_1(esk2_0)),
inference(scs_inference,[],[i_0_723,i_0_715,i_0_733,i_0_729,i_0_747,i_0_654,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75]) ).
cnf(i_0_770,plain,
~ m1_subset_1(k1_tarski(esk1_0),k1_zfmisc_1(esk3_2(esk1_0,esk6_0))),
inference(scs_inference,[],[i_0_723,i_0_715,i_0_733,i_0_729,i_0_747,i_0_654,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70]) ).
cnf(i_0_772,plain,
r2_hidden(esk3_2(k1_tarski(esk1_0),esk3_2(esk1_0,esk6_0)),k1_tarski(esk1_0)),
inference(scs_inference,[],[i_0_723,i_0_715,i_0_733,i_0_729,i_0_747,i_0_654,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68]) ).
cnf(i_0_774,plain,
~ r2_hidden(k1_zfmisc_1(X1),esk3_2(k1_zfmisc_1(X1),esk6_0)),
inference(scs_inference,[],[i_0_723,i_0_715,i_0_733,i_0_731,i_0_729,i_0_747,i_0_654,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71]) ).
cnf(i_0_776,plain,
k1_tarski(esk8_0) != esk11_2(esk8_0,k1_xboole_0),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_715,i_0_733,i_0_731,i_0_729,i_0_747,i_0_654,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102]) ).
cnf(i_0_777,plain,
~ m1_subset_1(k1_tarski(esk8_0),k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0))),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_715,i_0_733,i_0_731,i_0_729,i_0_747,i_0_654,i_0_524,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65]) ).
cnf(i_0_780,plain,
~ m1_subset_1(esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),k1_zfmisc_1(esk1_0)),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_654,i_0_524,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74]) ).
cnf(i_0_783,plain,
r2_hidden(esk11_2(k1_zfmisc_1(X1),k1_xboole_0),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_627,i_0_654,i_0_524,i_0_166,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62]) ).
cnf(i_0_786,plain,
~ r2_hidden(k1_tarski(k1_tarski(k1_xboole_0)),k1_tarski(esk9_1(esk6_0))),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_627,i_0_654,i_0_524,i_0_166,i_0_122,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67]) ).
cnf(i_0_789,plain,
m1_subset_1(esk4_1(k1_zfmisc_1(k1_xboole_0)),k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_639,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_627,i_0_654,i_0_524,i_0_236,i_0_166,i_0_122,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108]) ).
cnf(i_0_791,plain,
m1_subset_1(esk4_1(esk9_1(X1)),k1_xboole_0),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_639,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_627,i_0_654,i_0_524,i_0_451,i_0_236,i_0_166,i_0_122,i_0_80,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109]) ).
cnf(i_0_793,plain,
a_2_0_relset_2(esk1_0,esk2_0) != k1_tarski(esk6_0),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_639,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_418,i_0_627,i_0_654,i_0_524,i_0_451,i_0_236,i_0_682,i_0_166,i_0_122,i_0_80,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103]) ).
cnf(i_0_795,plain,
r2_hidden(esk4_1(k1_zfmisc_1(k1_xboole_0)),k1_tarski(esk9_1(esk6_0))),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_639,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_418,i_0_627,i_0_654,i_0_524,i_0_653,i_0_451,i_0_236,i_0_682,i_0_166,i_0_122,i_0_80,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106]) ).
cnf(i_0_796,plain,
r2_hidden(k1_xboole_0,k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_639,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_418,i_0_627,i_0_654,i_0_524,i_0_653,i_0_451,i_0_236,i_0_682,i_0_166,i_0_122,i_0_213,i_0_80,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106,i_0_105]) ).
cnf(i_0_799,plain,
~ r2_hidden(X1,a_2_0_relset_2(esk7_1(esk1_0),esk6_0)),
inference(scs_inference,[],[i_0_723,i_0_750,i_0_639,i_0_715,i_0_733,i_0_731,i_0_719,i_0_729,i_0_747,i_0_418,i_0_647,i_0_627,i_0_654,i_0_524,i_0_653,i_0_451,i_0_236,i_0_457,i_0_682,i_0_124,i_0_166,i_0_122,i_0_213,i_0_80,i_0_82,i_0_119,i_0_79,i_0_76,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106,i_0_105,i_0_110,i_0_57]) ).
cnf(i_0_839,plain,
esk9_1(X1) != esk7_1(a_2_0_relset_2(esk1_0,esk2_0)),
inference(rename_variables,[],[i_0_746]) ).
cnf(i_0_805,plain,
r1_tarski(k1_tarski(k1_xboole_0),k1_tarski(esk9_1(X1))),
inference(equality_inference,[],[798]) ).
cnf(i_0_806,plain,
~ r2_hidden(esk3_2(k1_tarski(esk8_0),esk11_2(esk8_0,k1_xboole_0)),esk11_2(esk8_0,k1_xboole_0)),
inference(scs_inference,[],[i_0_764,i_0_63]) ).
cnf(i_0_808,plain,
r1_tarski(k1_tarski(k1_xboole_0),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_63,i_0_72]) ).
cnf(i_0_810,plain,
~ r1_tarski(k1_tarski(esk1_0),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_63,i_0_72,i_0_69]) ).
cnf(i_0_812,plain,
m1_subset_1(k1_tarski(esk11_2(esk8_0,k1_xboole_0)),k1_zfmisc_1(esk8_0)),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_721,i_0_63,i_0_72,i_0_69,i_0_73]) ).
cnf(i_0_814,plain,
~ r2_hidden(k1_tarski(esk1_0),k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0))),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_469,i_0_721,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75]) ).
cnf(i_0_816,plain,
~ m1_subset_1(k1_tarski(esk8_0),k1_zfmisc_1(esk11_2(esk8_0,k1_xboole_0))),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_469,i_0_721,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70]) ).
cnf(i_0_818,plain,
r2_hidden(esk3_2(k1_tarski(esk8_0),esk11_2(esk8_0,k1_xboole_0)),k1_tarski(esk8_0)),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_469,i_0_721,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68]) ).
cnf(i_0_820,plain,
~ r2_hidden(k1_zfmisc_1(X1),esk11_2(k1_zfmisc_1(X1),esk6_0)),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_741,i_0_469,i_0_721,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71]) ).
cnf(i_0_822,plain,
a_2_0_relset_2(esk1_0,esk9_1(esk1_0)) != k1_zfmisc_1(k1_xboole_0),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_741,i_0_407,i_0_469,i_0_721,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102]) ).
cnf(i_0_823,plain,
~ m1_subset_1(k1_tarski(esk9_1(esk6_0)),k1_zfmisc_1(a_2_0_relset_2(esk1_0,esk2_0))),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_741,i_0_407,i_0_469,i_0_721,i_0_795,i_0_535,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65]) ).
cnf(i_0_825,plain,
~ m1_subset_1(k1_tarski(esk7_1(esk1_0)),esk7_1(esk1_0)),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_741,i_0_407,i_0_469,i_0_721,i_0_795,i_0_535,i_0_715,i_0_122,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74]) ).
cnf(i_0_828,plain,
r2_hidden(esk11_2(esk9_1(X1),esk8_0),esk8_0),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_741,i_0_407,i_0_469,i_0_721,i_0_795,i_0_443,i_0_535,i_0_715,i_0_202,i_0_122,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62]) ).
cnf(i_0_832,plain,
~ r2_hidden(k1_tarski(esk8_0),k1_tarski(esk11_2(esk8_0,k1_xboole_0))),
inference(scs_inference,[],[i_0_764,i_0_796,i_0_569,i_0_741,i_0_407,i_0_469,i_0_721,i_0_795,i_0_443,i_0_535,i_0_715,i_0_202,i_0_122,i_0_826,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67]) ).
cnf(i_0_835,plain,
m1_subset_1(esk4_1(k1_zfmisc_1(esk6_0)),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_764,i_0_586,i_0_796,i_0_569,i_0_741,i_0_407,i_0_469,i_0_721,i_0_795,i_0_443,i_0_535,i_0_715,i_0_315,i_0_202,i_0_122,i_0_826,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108]) ).
cnf(i_0_836,plain,
k1_zfmisc_1(esk1_0) != k1_zfmisc_1(k1_xboole_0),
inference(scs_inference,[],[i_0_764,i_0_586,i_0_796,i_0_569,i_0_741,i_0_567,i_0_407,i_0_469,i_0_721,i_0_795,i_0_443,i_0_474,i_0_535,i_0_715,i_0_315,i_0_202,i_0_122,i_0_826,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109]) ).
cnf(i_0_838,plain,
esk6_0 != esk7_1(a_2_0_relset_2(esk1_0,esk2_0)),
inference(scs_inference,[],[i_0_764,i_0_586,i_0_796,i_0_569,i_0_741,i_0_567,i_0_407,i_0_746,i_0_469,i_0_721,i_0_795,i_0_443,i_0_474,i_0_535,i_0_715,i_0_189,i_0_315,i_0_202,i_0_122,i_0_826,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103]) ).
cnf(i_0_840,plain,
k1_zfmisc_1(X1) != a_2_0_relset_2(esk7_1(esk1_0),esk6_0),
inference(scs_inference,[],[i_0_764,i_0_586,i_0_796,i_0_569,i_0_741,i_0_567,i_0_407,i_0_746,i_0_469,i_0_799,i_0_721,i_0_795,i_0_443,i_0_474,i_0_535,i_0_715,i_0_189,i_0_315,i_0_202,i_0_122,i_0_826,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106]) ).
cnf(i_0_841,plain,
~ r2_hidden(X1,a_2_0_relset_2(esk7_1(esk1_0),esk6_0)),
inference(rename_variables,[],[i_0_799]) ).
cnf(i_0_842,plain,
r2_hidden(esk4_1(k1_zfmisc_1(esk6_0)),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_764,i_0_586,i_0_796,i_0_569,i_0_741,i_0_567,i_0_407,i_0_746,i_0_469,i_0_799,i_0_721,i_0_795,i_0_443,i_0_474,i_0_535,i_0_715,i_0_189,i_0_315,i_0_202,i_0_122,i_0_826,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106,i_0_105]) ).
cnf(i_0_843,plain,
~ r2_hidden(X1,a_2_0_relset_2(esk7_1(esk1_0),k1_xboole_0)),
inference(scs_inference,[],[i_0_764,i_0_586,i_0_796,i_0_569,i_0_741,i_0_567,i_0_407,i_0_746,i_0_469,i_0_799,i_0_721,i_0_795,i_0_443,i_0_474,i_0_535,i_0_715,i_0_189,i_0_315,i_0_202,i_0_166,i_0_122,i_0_826,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106,i_0_105,i_0_57]) ).
cnf(i_0_847,plain,
~ m1_subset_1(k1_zfmisc_1(X1),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_764,i_0_586,i_0_796,i_0_569,i_0_741,i_0_567,i_0_407,i_0_746,i_0_469,i_0_799,i_0_721,i_0_795,i_0_443,i_0_474,i_0_535,i_0_715,i_0_189,i_0_315,i_0_202,i_0_166,i_0_122,i_0_826,i_0_100,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106,i_0_105,i_0_57,i_0_66]) ).
cnf(i_0_1386,plain,
~ r2_hidden(k1_tarski(esk1_0),k1_zfmisc_1(esk3_2(esk1_0,esk6_0))),
inference(scs_inference,[],[i_0_770,i_0_647,i_0_69,i_0_75]) ).
cnf(i_0_1657,plain,
~ r2_hidden(X1,a_2_0_relset_2(esk7_1(esk1_0),esk6_0)),
inference(rename_variables,[],[i_0_799]) ).
cnf(i_0_852,plain,
~ r2_hidden(esk3_2(k1_tarski(esk1_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_810,i_0_63]) ).
cnf(i_0_854,plain,
r1_tarski(k1_tarski(k1_tarski(esk6_0)),a_2_0_relset_2(k1_tarski(esk6_0),k1_tarski(k1_xboole_0))),
inference(scs_inference,[],[i_0_810,i_0_704,i_0_63,i_0_72]) ).
cnf(i_0_856,plain,
~ r1_tarski(k1_tarski(esk8_0),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_810,i_0_618,i_0_704,i_0_63,i_0_72,i_0_69]) ).
cnf(i_0_858,plain,
m1_subset_1(k1_tarski(k1_xboole_0),k1_zfmisc_1(k1_zfmisc_1(X1))),
inference(scs_inference,[],[i_0_808,i_0_810,i_0_618,i_0_704,i_0_63,i_0_72,i_0_69,i_0_73]) ).
cnf(i_0_860,plain,
~ r2_hidden(k1_zfmisc_1(X1),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_618,i_0_704,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75]) ).
cnf(i_0_862,plain,
~ m1_subset_1(k1_tarski(esk6_0),k1_zfmisc_1(a_2_0_relset_2(esk1_0,esk2_0))),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_618,i_0_704,i_0_455,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70]) ).
cnf(i_0_864,plain,
r2_hidden(esk3_2(k1_tarski(esk1_0),k1_zfmisc_1(k1_xboole_0)),k1_tarski(esk1_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_618,i_0_704,i_0_455,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68]) ).
cnf(i_0_866,plain,
~ r2_hidden(k1_zfmisc_1(X1),esk11_2(k1_zfmisc_1(X1),k1_xboole_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_618,i_0_783,i_0_704,i_0_455,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71]) ).
cnf(i_0_868,plain,
k1_zfmisc_1(k1_xboole_0) != k1_zfmisc_1(esk1_0),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_704,i_0_455,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102]) ).
cnf(i_0_869,plain,
~ m1_subset_1(k1_tarski(k1_zfmisc_1(X1)),k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0))),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_704,i_0_455,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65]) ).
cnf(i_0_872,plain,
~ m1_subset_1(k1_xboole_0,a_2_0_relset_2(esk1_0,esk2_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_333,i_0_704,i_0_455,i_0_497,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74]) ).
cnf(i_0_874,plain,
r2_hidden(esk11_2(esk8_0,esk9_1(X1)),esk8_0),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_333,i_0_503,i_0_704,i_0_455,i_0_497,i_0_202,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62]) ).
cnf(i_0_877,plain,
~ r2_hidden(esk8_0,k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_333,i_0_503,i_0_704,i_0_455,i_0_497,i_0_202,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67]) ).
cnf(i_0_878,plain,
r1_tarski(k1_tarski(k1_xboole_0),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_808]) ).
cnf(i_0_880,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_333,i_0_503,i_0_704,i_0_455,i_0_256,i_0_497,i_0_202,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108]) ).
cnf(i_0_881,plain,
m1_subset_1(esk4_1(esk6_0),esk9_1(X1)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_476,i_0_333,i_0_503,i_0_704,i_0_455,i_0_256,i_0_278,i_0_497,i_0_202,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109]) ).
cnf(i_0_882,plain,
esk4_1(k1_zfmisc_1(k1_xboole_0)) != esk7_1(a_2_0_relset_2(esk1_0,esk2_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_476,i_0_838,i_0_333,i_0_503,i_0_704,i_0_455,i_0_256,i_0_278,i_0_302,i_0_497,i_0_202,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103]) ).
cnf(i_0_883,plain,
a_2_0_relset_2(k1_tarski(k1_xboole_0),k1_tarski(esk6_0)) != esk9_1(X1),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_476,i_0_838,i_0_762,i_0_333,i_0_503,i_0_704,i_0_455,i_0_311,i_0_256,i_0_278,i_0_302,i_0_497,i_0_202,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_111]) ).
cnf(i_0_885,plain,
r2_hidden(esk4_1(k1_tarski(esk6_0)),k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_476,i_0_838,i_0_762,i_0_333,i_0_503,i_0_704,i_0_455,i_0_311,i_0_370,i_0_256,i_0_278,i_0_302,i_0_577,i_0_497,i_0_202,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_111,i_0_106]) ).
cnf(i_0_887,plain,
r2_hidden(esk6_0,k1_tarski(esk9_1(esk6_0))),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_476,i_0_838,i_0_762,i_0_333,i_0_503,i_0_704,i_0_455,i_0_795,i_0_311,i_0_370,i_0_314,i_0_256,i_0_278,i_0_302,i_0_577,i_0_497,i_0_202,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_111,i_0_106,i_0_105]) ).
cnf(i_0_888,plain,
m1_subset_1(esk5_3(k1_tarski(esk6_0),k1_tarski(esk6_0),k1_tarski(k1_xboole_0)),k1_tarski(esk6_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_476,i_0_672,i_0_838,i_0_762,i_0_333,i_0_503,i_0_704,i_0_455,i_0_795,i_0_311,i_0_370,i_0_314,i_0_256,i_0_278,i_0_302,i_0_577,i_0_497,i_0_202,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_111,i_0_106,i_0_105,i_0_58]) ).
cnf(i_0_891,plain,
r2_hidden(esk5_3(k1_tarski(esk6_0),k1_tarski(esk6_0),k1_tarski(k1_xboole_0)),k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_808,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_476,i_0_672,i_0_838,i_0_762,i_0_333,i_0_503,i_0_704,i_0_455,i_0_795,i_0_311,i_0_370,i_0_314,i_0_256,i_0_278,i_0_302,i_0_577,i_0_497,i_0_202,i_0_81,i_0_889,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_111,i_0_106,i_0_105,i_0_58,i_0_57]) ).
cnf(i_0_895,plain,
r1_tarski(k1_tarski(k1_xboole_0),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_808]) ).
cnf(i_0_936,plain,
~ r2_hidden(X1,a_2_0_relset_2(esk7_1(esk1_0),k1_xboole_0)),
inference(rename_variables,[],[i_0_843]) ).
cnf(i_0_976,plain,
r1_tarski(k1_tarski(k1_xboole_0),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_808]) ).
cnf(i_0_1170,plain,
r1_tarski(k1_tarski(k1_xboole_0),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_808]) ).
cnf(i_0_1414,plain,
~ r1_tarski(k1_tarski(k1_tarski(esk1_0)),k1_zfmisc_1(esk3_2(esk1_0,esk6_0))),
inference(scs_inference,[],[i_0_1386,i_0_69]) ).
cnf(i_0_1416,plain,
m1_subset_1(k1_xboole_0,k1_tarski(esk9_1(X1))),
inference(scs_inference,[],[i_0_1386,i_0_1384,i_0_69,i_0_75]) ).
cnf(i_0_1802,plain,
~ r2_hidden(X1,a_2_0_relset_2(esk7_1(esk1_0),k1_xboole_0)),
inference(rename_variables,[],[i_0_843]) ).
cnf(i_0_894,plain,
k1_tarski(k1_xboole_0) != k1_tarski(esk1_0),
inference(scs_inference,[],[i_0_808,i_0_878,i_0_847,i_0_810,i_0_836,i_0_618,i_0_783,i_0_534,i_0_476,i_0_672,i_0_838,i_0_762,i_0_333,i_0_503,i_0_704,i_0_455,i_0_795,i_0_311,i_0_370,i_0_314,i_0_256,i_0_278,i_0_302,i_0_577,i_0_497,i_0_202,i_0_81,i_0_889,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_111,i_0_106,i_0_105,i_0_58,i_0_57,i_0_110]) ).
cnf(i_0_901,plain,
~ r2_hidden(esk3_2(k1_tarski(esk8_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_856,i_0_63]) ).
cnf(i_0_903,plain,
r1_tarski(k1_tarski(esk11_2(esk1_0,esk6_0)),esk1_0),
inference(scs_inference,[],[i_0_856,i_0_539,i_0_63,i_0_72]) ).
cnf(i_0_905,plain,
~ r1_tarski(k1_tarski(k1_zfmisc_1(X1)),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_539,i_0_63,i_0_72,i_0_69]) ).
cnf(i_0_907,plain,
m1_subset_1(k1_tarski(esk3_2(esk8_0,k1_xboole_0)),k1_zfmisc_1(esk8_0)),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_539,i_0_563,i_0_63,i_0_72,i_0_69,i_0_73]) ).
cnf(i_0_909,plain,
~ r2_hidden(k1_tarski(k1_xboole_0),k1_zfmisc_1(a_2_0_relset_2(esk1_0,esk2_0))),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_736,i_0_539,i_0_563,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75]) ).
cnf(i_0_911,plain,
~ m1_subset_1(k1_zfmisc_1(esk1_0),k1_zfmisc_1(esk9_1(esk6_0))),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_736,i_0_539,i_0_178,i_0_563,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70]) ).
cnf(i_0_913,plain,
r2_hidden(esk3_2(k1_tarski(esk8_0),k1_zfmisc_1(k1_xboole_0)),k1_tarski(esk8_0)),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_736,i_0_539,i_0_178,i_0_563,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68]) ).
cnf(i_0_932,plain,
m1_subset_1(esk4_1(esk6_0),esk9_1(X1)),
inference(rename_variables,[],[i_0_881]) ).
cnf(i_0_940,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_1105,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_1178,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_1276,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_1404,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_1436,plain,
m1_subset_1(k1_tarski(k1_xboole_0),k1_zfmisc_1(k1_zfmisc_1(X1))),
inference(rename_variables,[],[i_0_858]) ).
cnf(i_0_1560,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_1706,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_1875,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_2062,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_2246,plain,
m1_subset_1(esk9_1(X1),k1_zfmisc_1(X2)),
inference(rename_variables,[],[i_0_880]) ).
cnf(i_0_917,plain,
k1_tarski(esk1_0) != k1_tarski(k1_xboole_0),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_894,i_0_891,i_0_736,i_0_539,i_0_178,i_0_563,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102]) ).
cnf(i_0_920,plain,
~ m1_subset_1(esk8_0,k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_894,i_0_877,i_0_891,i_0_692,i_0_736,i_0_539,i_0_178,i_0_563,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74]) ).
cnf(i_0_923,plain,
r2_hidden(esk11_2(esk1_0,esk9_1(X1)),esk1_0),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_894,i_0_877,i_0_891,i_0_692,i_0_736,i_0_546,i_0_539,i_0_178,i_0_563,i_0_202,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62]) ).
cnf(i_0_927,plain,
~ r2_hidden(k1_tarski(esk1_0),k1_tarski(esk3_2(esk1_0,esk6_0))),
inference(scs_inference,[],[i_0_860,i_0_856,i_0_894,i_0_877,i_0_891,i_0_692,i_0_736,i_0_546,i_0_539,i_0_178,i_0_668,i_0_563,i_0_202,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67]) ).
cnf(i_0_931,plain,
m1_subset_1(esk4_1(esk6_0),esk4_1(k1_zfmisc_1(k1_xboole_0))),
inference(scs_inference,[],[i_0_860,i_0_881,i_0_856,i_0_894,i_0_877,i_0_891,i_0_888,i_0_738,i_0_692,i_0_736,i_0_546,i_0_539,i_0_178,i_0_668,i_0_563,i_0_236,i_0_202,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109]) ).
cnf(i_0_933,plain,
k1_xboole_0 != esk7_1(a_2_0_relset_2(esk1_0,esk2_0)),
inference(scs_inference,[],[i_0_860,i_0_881,i_0_856,i_0_894,i_0_877,i_0_891,i_0_888,i_0_738,i_0_692,i_0_736,i_0_882,i_0_546,i_0_539,i_0_178,i_0_668,i_0_338,i_0_563,i_0_236,i_0_202,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103]) ).
cnf(i_0_935,plain,
k1_tarski(k1_xboole_0) != a_2_0_relset_2(esk7_1(esk1_0),k1_xboole_0),
inference(scs_inference,[],[i_0_860,i_0_881,i_0_856,i_0_894,i_0_877,i_0_891,i_0_888,i_0_738,i_0_692,i_0_843,i_0_736,i_0_882,i_0_854,i_0_546,i_0_539,i_0_178,i_0_668,i_0_338,i_0_563,i_0_626,i_0_236,i_0_202,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106]) ).
cnf(i_0_937,plain,
esk5_3(k1_tarski(esk6_0),k1_tarski(esk6_0),k1_tarski(k1_xboole_0)) != esk8_0,
inference(scs_inference,[],[i_0_860,i_0_881,i_0_856,i_0_894,i_0_877,i_0_891,i_0_888,i_0_738,i_0_692,i_0_843,i_0_736,i_0_882,i_0_854,i_0_546,i_0_539,i_0_178,i_0_668,i_0_338,i_0_563,i_0_626,i_0_236,i_0_202,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106,i_0_105]) ).
cnf(i_0_938,plain,
~ r2_hidden(X1,a_2_0_relset_2(esk7_1(k1_tarski(X2)),esk9_1(X3))),
inference(scs_inference,[],[i_0_880,i_0_860,i_0_881,i_0_856,i_0_894,i_0_877,i_0_891,i_0_888,i_0_738,i_0_606,i_0_692,i_0_843,i_0_736,i_0_882,i_0_854,i_0_546,i_0_539,i_0_178,i_0_668,i_0_338,i_0_563,i_0_626,i_0_236,i_0_202,i_0_925,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106,i_0_105,i_0_57]) ).
cnf(i_0_942,plain,
esk4_1(k1_zfmisc_1(esk6_0)) != esk7_1(k1_tarski(X1)),
inference(scs_inference,[],[i_0_880,i_0_860,i_0_881,i_0_856,i_0_894,i_0_877,i_0_891,i_0_888,i_0_738,i_0_606,i_0_692,i_0_843,i_0_736,i_0_882,i_0_854,i_0_546,i_0_539,i_0_178,i_0_668,i_0_645,i_0_338,i_0_563,i_0_626,i_0_236,i_0_202,i_0_925,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106,i_0_105,i_0_57,i_0_107]) ).
cnf(i_0_943,plain,
~ r2_hidden(esk3_2(k1_tarski(k1_zfmisc_1(X1)),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_905,i_0_63]) ).
cnf(i_0_945,plain,
r1_tarski(k1_tarski(esk4_1(esk1_0)),esk1_0),
inference(scs_inference,[],[i_0_905,i_0_175,i_0_63,i_0_72]) ).
cnf(i_0_947,plain,
~ r1_tarski(k1_tarski(esk1_0),k1_zfmisc_1(esk6_0)),
inference(scs_inference,[],[i_0_674,i_0_905,i_0_175,i_0_63,i_0_72,i_0_69]) ).
cnf(i_0_949,plain,
m1_subset_1(k1_tarski(esk11_2(esk1_0,esk6_0)),k1_zfmisc_1(esk1_0)),
inference(scs_inference,[],[i_0_674,i_0_905,i_0_903,i_0_175,i_0_63,i_0_72,i_0_69,i_0_73]) ).
cnf(i_0_951,plain,
~ r2_hidden(k1_tarski(esk8_0),k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0))),
inference(scs_inference,[],[i_0_674,i_0_905,i_0_777,i_0_903,i_0_175,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75]) ).
cnf(i_0_953,plain,
~ m1_subset_1(k1_zfmisc_1(X1),k1_zfmisc_1(esk6_0)),
inference(scs_inference,[],[i_0_674,i_0_905,i_0_777,i_0_903,i_0_324,i_0_175,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70]) ).
cnf(i_0_955,plain,
r2_hidden(esk3_2(k1_zfmisc_1(X1),k1_xboole_0),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_674,i_0_905,i_0_777,i_0_903,i_0_346,i_0_324,i_0_175,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68]) ).
cnf(i_0_957,plain,
~ r2_hidden(k1_tarski(esk1_0),esk3_2(k1_tarski(esk1_0),k1_zfmisc_1(k1_xboole_0))),
inference(scs_inference,[],[i_0_674,i_0_905,i_0_864,i_0_777,i_0_903,i_0_346,i_0_324,i_0_175,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71]) ).
cnf(i_0_959,plain,
esk9_1(X1) != a_2_0_relset_2(k1_tarski(k1_xboole_0),k1_tarski(esk6_0)),
inference(scs_inference,[],[i_0_674,i_0_883,i_0_905,i_0_864,i_0_777,i_0_903,i_0_346,i_0_324,i_0_175,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102]) ).
cnf(i_0_960,plain,
~ m1_subset_1(k1_tarski(esk8_0),k1_zfmisc_1(k1_tarski(k1_xboole_0))),
inference(scs_inference,[],[i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_777,i_0_903,i_0_346,i_0_324,i_0_175,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65]) ).
cnf(i_0_963,plain,
~ m1_subset_1(esk3_2(k1_tarski(esk1_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)),
inference(scs_inference,[],[i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_852,i_0_777,i_0_903,i_0_346,i_0_324,i_0_175,i_0_82,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74]) ).
cnf(i_0_966,plain,
r2_hidden(esk11_2(k1_tarski(X1),k1_xboole_0),k1_tarski(X1)),
inference(scs_inference,[],[i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_852,i_0_777,i_0_903,i_0_323,i_0_346,i_0_324,i_0_175,i_0_166,i_0_82,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62]) ).
cnf(i_0_969,plain,
~ r2_hidden(k1_tarski(esk1_0),k1_tarski(esk11_2(esk1_0,esk6_0))),
inference(scs_inference,[],[i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_852,i_0_777,i_0_903,i_0_323,i_0_346,i_0_324,i_0_175,i_0_166,i_0_82,i_0_122,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67]) ).
cnf(i_0_972,plain,
m1_subset_1(esk9_1(X1),k1_tarski(esk6_0)),
inference(scs_inference,[],[i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_744,i_0_852,i_0_777,i_0_903,i_0_323,i_0_346,i_0_324,i_0_175,i_0_256,i_0_166,i_0_82,i_0_122,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108]) ).
cnf(i_0_973,plain,
m1_subset_1(esk4_1(k1_zfmisc_1(esk6_0)),k1_tarski(esk9_1(esk6_0))),
inference(scs_inference,[],[i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_472,i_0_744,i_0_852,i_0_777,i_0_903,i_0_323,i_0_346,i_0_324,i_0_175,i_0_256,i_0_682,i_0_166,i_0_82,i_0_122,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109]) ).
cnf(i_0_974,plain,
k1_tarski(esk1_0) != k1_tarski(esk9_1(X1)),
inference(scs_inference,[],[i_0_917,i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_472,i_0_744,i_0_852,i_0_777,i_0_903,i_0_323,i_0_346,i_0_324,i_0_526,i_0_175,i_0_256,i_0_682,i_0_166,i_0_82,i_0_122,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103]) ).
cnf(i_0_975,plain,
k1_tarski(k1_xboole_0) != k1_tarski(k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_917,i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_472,i_0_744,i_0_852,i_0_777,i_0_903,i_0_323,i_0_346,i_0_324,i_0_808,i_0_526,i_0_175,i_0_256,i_0_682,i_0_166,i_0_82,i_0_122,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110]) ).
cnf(i_0_977,plain,
r2_hidden(esk6_0,k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_917,i_0_674,i_0_920,i_0_883,i_0_905,i_0_864,i_0_472,i_0_744,i_0_852,i_0_777,i_0_903,i_0_842,i_0_323,i_0_346,i_0_324,i_0_808,i_0_301,i_0_526,i_0_175,i_0_256,i_0_682,i_0_166,i_0_82,i_0_122,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110,i_0_105]) ).
cnf(i_0_980,plain,
~ r2_hidden(esk3_2(k1_tarski(esk1_0),k1_zfmisc_1(esk6_0)),k1_zfmisc_1(esk6_0)),
inference(scs_inference,[],[i_0_947,i_0_63]) ).
cnf(i_0_1014,plain,
r2_hidden(esk3_2(k1_zfmisc_1(X1),k1_xboole_0),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_955]) ).
cnf(i_0_982,plain,
r1_tarski(k1_tarski(esk6_0),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_947,i_0_977,i_0_63,i_0_72]) ).
cnf(i_0_984,plain,
~ r1_tarski(k1_tarski(k1_zfmisc_1(X1)),esk11_2(k1_zfmisc_1(X1),esk9_1(X2))),
inference(scs_inference,[],[i_0_947,i_0_977,i_0_624,i_0_63,i_0_72,i_0_69]) ).
cnf(i_0_986,plain,
m1_subset_1(k1_tarski(esk4_1(esk1_0)),k1_zfmisc_1(esk1_0)),
inference(scs_inference,[],[i_0_947,i_0_977,i_0_624,i_0_945,i_0_63,i_0_72,i_0_69,i_0_73]) ).
cnf(i_0_988,plain,
~ r2_hidden(k1_zfmisc_1(X1),k1_zfmisc_1(esk6_0)),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_624,i_0_945,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75]) ).
cnf(i_0_990,plain,
~ m1_subset_1(k1_tarski(esk9_1(X1)),k1_zfmisc_1(a_2_0_relset_2(esk1_0,esk2_0))),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_624,i_0_945,i_0_393,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70]) ).
cnf(i_0_992,plain,
r2_hidden(esk3_2(k1_tarski(esk1_0),k1_zfmisc_1(esk6_0)),k1_tarski(esk1_0)),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_624,i_0_945,i_0_393,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68]) ).
cnf(i_0_994,plain,
~ r2_hidden(k1_zfmisc_1(X1),esk3_2(k1_zfmisc_1(X1),k1_xboole_0)),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_955,i_0_624,i_0_945,i_0_393,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71]) ).
cnf(i_0_996,plain,
k1_tarski(esk9_1(X1)) != k1_tarski(esk1_0),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_955,i_0_624,i_0_974,i_0_945,i_0_393,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102]) ).
cnf(i_0_997,plain,
m1_subset_1(esk4_1(k1_tarski(esk6_0)),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_955,i_0_885,i_0_624,i_0_858,i_0_974,i_0_945,i_0_393,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65]) ).
cnf(i_0_999,plain,
~ m1_subset_1(k1_tarski(esk1_0),k1_tarski(esk3_2(esk1_0,k1_xboole_0))),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_955,i_0_885,i_0_624,i_0_858,i_0_974,i_0_599,i_0_945,i_0_393,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74]) ).
cnf(i_0_1002,plain,
r2_hidden(esk11_2(k1_xboole_0,esk7_1(esk8_0)),esk7_1(esk8_0)),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_955,i_0_885,i_0_624,i_0_858,i_0_974,i_0_599,i_0_945,i_0_488,i_0_393,i_0_166,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62]) ).
cnf(i_0_1005,plain,
~ r2_hidden(k1_tarski(esk1_0),k1_tarski(esk4_1(esk1_0))),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_955,i_0_885,i_0_624,i_0_858,i_0_974,i_0_599,i_0_945,i_0_488,i_0_393,i_0_166,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67]) ).
cnf(i_0_1008,plain,
k1_tarski(esk3_2(esk1_0,esk6_0)) != esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),
inference(scs_inference,[],[i_0_953,i_0_947,i_0_977,i_0_955,i_0_725,i_0_780,i_0_885,i_0_624,i_0_858,i_0_974,i_0_599,i_0_945,i_0_488,i_0_393,i_0_166,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108]) ).
cnf(i_0_1009,plain,
m1_subset_1(esk9_1(X1),k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_953,i_0_972,i_0_947,i_0_977,i_0_955,i_0_725,i_0_780,i_0_885,i_0_624,i_0_858,i_0_974,i_0_599,i_0_945,i_0_488,i_0_393,i_0_577,i_0_166,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109]) ).
cnf(i_0_1010,plain,
k1_xboole_0 != esk7_1(k1_tarski(X1)),
inference(scs_inference,[],[i_0_953,i_0_972,i_0_947,i_0_977,i_0_955,i_0_725,i_0_780,i_0_885,i_0_624,i_0_858,i_0_974,i_0_599,i_0_945,i_0_942,i_0_488,i_0_393,i_0_325,i_0_577,i_0_166,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103]) ).
cnf(i_0_1011,plain,
r2_hidden(esk11_2(k1_tarski(esk6_0),k1_xboole_0),k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_953,i_0_972,i_0_947,i_0_977,i_0_955,i_0_966,i_0_725,i_0_780,i_0_885,i_0_624,i_0_858,i_0_974,i_0_599,i_0_945,i_0_942,i_0_488,i_0_393,i_0_325,i_0_577,i_0_166,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106]) ).
cnf(i_0_1012,plain,
r2_hidden(esk11_2(k1_tarski(X1),k1_xboole_0),k1_tarski(X1)),
inference(rename_variables,[],[i_0_966]) ).
cnf(i_0_1013,plain,
esk3_2(k1_zfmisc_1(esk8_0),k1_xboole_0) != k1_tarski(k1_tarski(esk8_0)),
inference(scs_inference,[],[i_0_953,i_0_972,i_0_947,i_0_977,i_0_955,i_0_966,i_0_725,i_0_780,i_0_727,i_0_885,i_0_624,i_0_858,i_0_974,i_0_599,i_0_945,i_0_942,i_0_488,i_0_393,i_0_325,i_0_577,i_0_166,i_0_122,i_0_81,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_65,i_0_74,i_0_62,i_0_67,i_0_108,i_0_109,i_0_103,i_0_106,i_0_105]) ).
cnf(i_0_1235,plain,
r2_hidden(esk11_2(k1_tarski(X1),k1_xboole_0),k1_tarski(X1)),
inference(rename_variables,[],[i_0_966]) ).
cnf(i_0_1439,plain,
~ r1_tarski(esk3_2(k1_tarski(esk1_0),k1_zfmisc_1(k1_xboole_0)),k1_xboole_0),
inference(scs_inference,[],[i_0_963,i_0_73]) ).
cnf(i_0_1759,plain,
~ r1_tarski(k1_tarski(esk8_0),k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_960,i_0_73]) ).
cnf(i_0_1761,plain,
r2_hidden(esk3_2(k1_tarski(esk8_0),k1_tarski(k1_xboole_0)),k1_tarski(esk8_0)),
inference(scs_inference,[],[i_0_960,i_0_73,i_0_68]) ).
cnf(i_0_1763,plain,
~ r2_hidden(k1_tarski(esk8_0),k1_zfmisc_1(k1_tarski(k1_xboole_0))),
inference(scs_inference,[],[i_0_960,i_0_73,i_0_68,i_0_75]) ).
cnf(i_0_1025,plain,
~ r1_tarski(k1_tarski(k1_zfmisc_1(X1)),k1_zfmisc_1(esk6_0)),
inference(scs_inference,[],[i_0_988,i_0_393,i_0_131,i_0_63,i_0_72,i_0_69]) ).
cnf(i_0_1027,plain,
m1_subset_1(k1_tarski(esk6_0),k1_zfmisc_1(k1_zfmisc_1(X1))),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_393,i_0_131,i_0_63,i_0_72,i_0_69,i_0_73]) ).
cnf(i_0_1029,plain,
~ r2_hidden(k1_tarski(esk6_0),k1_zfmisc_1(a_2_0_relset_2(esk1_0,esk2_0))),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_862,i_0_393,i_0_131,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75]) ).
cnf(i_0_1031,plain,
~ m1_subset_1(k1_zfmisc_1(X1),k1_zfmisc_1(a_2_0_relset_2(esk1_0,esk2_0))),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_862,i_0_389,i_0_393,i_0_131,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70]) ).
cnf(i_0_1033,plain,
r2_hidden(esk3_2(k1_tarski(X1),k1_xboole_0),k1_tarski(X1)),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_862,i_0_336,i_0_389,i_0_393,i_0_131,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68]) ).
cnf(i_0_1035,plain,
~ r2_hidden(k1_tarski(esk1_0),esk3_2(k1_tarski(esk1_0),k1_zfmisc_1(esk6_0))),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_992,i_0_862,i_0_336,i_0_389,i_0_393,i_0_131,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71]) ).
cnf(i_0_1037,plain,
k1_tarski(k1_zfmisc_1(X1)) != k1_tarski(k1_xboole_0),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_992,i_0_862,i_0_975,i_0_336,i_0_389,i_0_393,i_0_131,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102]) ).
cnf(i_0_1038,plain,
~ m1_subset_1(k1_tarski(esk1_0),k1_zfmisc_1(esk6_0)),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_992,i_0_862,i_0_975,i_0_336,i_0_389,i_0_393,i_0_131,i_0_98,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66]) ).
cnf(i_0_1040,plain,
~ m1_subset_1(k1_tarski(k1_zfmisc_1(X1)),k1_zfmisc_1(k1_zfmisc_1(esk6_0))),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_992,i_0_862,i_0_975,i_0_953,i_0_336,i_0_389,i_0_393,i_0_131,i_0_98,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65]) ).
cnf(i_0_1043,plain,
~ m1_subset_1(k1_tarski(esk8_0),k1_tarski(esk3_2(esk8_0,k1_xboole_0))),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_992,i_0_862,i_0_975,i_0_695,i_0_953,i_0_336,i_0_389,i_0_393,i_0_131,i_0_98,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74]) ).
cnf(i_0_1046,plain,
~ r2_hidden(k1_zfmisc_1(X1),k1_tarski(esk6_0)),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_992,i_0_862,i_0_975,i_0_695,i_0_953,i_0_336,i_0_389,i_0_393,i_0_131,i_0_98,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74,i_0_67]) ).
cnf(i_0_1047,plain,
r1_tarski(k1_tarski(esk6_0),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_982]) ).
cnf(i_0_1049,plain,
m1_subset_1(esk6_0,k1_tarski(k1_xboole_0)),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_992,i_0_789,i_0_862,i_0_975,i_0_695,i_0_953,i_0_336,i_0_389,i_0_393,i_0_314,i_0_131,i_0_98,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74,i_0_67,i_0_108]) ).
cnf(i_0_1050,plain,
m1_subset_1(esk9_1(X1),k1_tarski(esk9_1(esk6_0))),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_992,i_0_789,i_0_862,i_0_975,i_0_695,i_0_953,i_0_972,i_0_336,i_0_389,i_0_393,i_0_314,i_0_682,i_0_131,i_0_98,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74,i_0_67,i_0_108,i_0_109]) ).
cnf(i_0_1051,plain,
k1_tarski(esk6_0) != k1_tarski(esk1_0),
inference(scs_inference,[],[i_0_982,i_0_988,i_0_996,i_0_992,i_0_789,i_0_862,i_0_975,i_0_695,i_0_953,i_0_972,i_0_336,i_0_389,i_0_393,i_0_314,i_0_461,i_0_682,i_0_131,i_0_98,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74,i_0_67,i_0_108,i_0_109,i_0_103]) ).
cnf(i_0_1052,plain,
k1_tarski(esk9_1(X1)) != k1_tarski(esk1_0),
inference(rename_variables,[],[i_0_996]) ).
cnf(i_0_1092,plain,
m1_subset_1(esk4_1(k1_tarski(esk6_0)),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_997]) ).
cnf(i_0_1753,plain,
r1_tarski(k1_tarski(esk6_0),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_982]) ).
cnf(i_0_1053,plain,
r1_tarski(k1_tarski(esk9_1(esk6_0)),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_982,i_0_1047,i_0_988,i_0_996,i_0_992,i_0_789,i_0_862,i_0_975,i_0_695,i_0_953,i_0_972,i_0_336,i_0_389,i_0_393,i_0_314,i_0_461,i_0_682,i_0_131,i_0_98,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110]) ).
cnf(i_0_1054,plain,
k1_tarski(esk1_0) != k1_zfmisc_1(esk6_0),
inference(scs_inference,[],[i_0_982,i_0_1047,i_0_988,i_0_996,i_0_992,i_0_789,i_0_980,i_0_862,i_0_975,i_0_695,i_0_953,i_0_972,i_0_336,i_0_389,i_0_393,i_0_314,i_0_461,i_0_682,i_0_131,i_0_98,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106]) ).
cnf(i_0_1055,plain,
r2_hidden(k1_xboole_0,k1_tarski(esk9_1(esk6_0))),
inference(scs_inference,[],[i_0_982,i_0_1047,i_0_988,i_0_996,i_0_992,i_0_789,i_0_980,i_0_862,i_0_975,i_0_695,i_0_887,i_0_953,i_0_972,i_0_336,i_0_389,i_0_393,i_0_314,i_0_461,i_0_514,i_0_682,i_0_131,i_0_98,i_0_81,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106,i_0_105]) ).
cnf(i_0_1056,plain,
r2_hidden(k1_tarski(esk6_0),a_2_0_relset_2(k1_tarski(k1_xboole_0),k1_tarski(k1_xboole_0))),
inference(scs_inference,[],[i_0_982,i_0_1047,i_0_988,i_0_996,i_0_992,i_0_789,i_0_980,i_0_862,i_0_975,i_0_695,i_0_887,i_0_703,i_0_953,i_0_972,i_0_692,i_0_336,i_0_389,i_0_393,i_0_314,i_0_461,i_0_514,i_0_682,i_0_131,i_0_98,i_0_81,i_0_1044,i_0_119,i_0_63,i_0_72,i_0_69,i_0_73,i_0_75,i_0_70,i_0_68,i_0_71,i_0_102,i_0_66,i_0_65,i_0_74,i_0_67,i_0_108,i_0_109,i_0_103,i_0_110,i_0_106,i_0_105,i_0_114]) ).
cnf(c_0_797,plain,
( m1_subset_1(X1,X2)
| ~ r2_hidden(X1,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(X2)) ),
i_0_65 ).
cnf(c_0_798,plain,
( m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r1_tarski(X1,X2) ),
i_0_73 ).
cnf(c_0_799,plain,
~ v1_xboole_0(k1_zfmisc_1(X1)),
i_0_82 ).
cnf(c_0_800,plain,
( v1_xboole_0(X1)
| r2_hidden(X2,X1)
| ~ m1_subset_1(X2,X1) ),
i_0_74 ).
cnf(c_0_801,plain,
~ m1_subset_1(esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),k1_zfmisc_1(esk1_0)),
i_0_780 ).
cnf(c_0_802,plain,
( m1_subset_1(X1,X2)
| ~ r1_tarski(X3,X2)
| ~ r2_hidden(X1,X3) ),
inference(spm,[status(thm)],[c_0_797,c_0_798]) ).
cnf(c_0_803,plain,
( r2_hidden(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(spm,[status(thm)],[c_0_799,c_0_800]) ).
cnf(c_0_804,plain,
( r1_tarski(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
i_0_70 ).
cnf(c_0_805,negated_conjecture,
m1_subset_1(esk2_0,k1_zfmisc_1(esk1_0)),
i_0_84 ).
cnf(c_0_806,negated_conjecture,
~ v1_xboole_0(esk1_0),
i_0_90 ).
cnf(c_0_807,plain,
( r2_hidden(esk5_3(X1,X2,X3),X3)
| v1_xboole_0(X2)
| ~ r2_hidden(X1,a_2_0_relset_2(X2,X3))
| ~ m1_subset_1(X3,k1_zfmisc_1(X2)) ),
i_0_57 ).
cnf(c_0_808,plain,
( ~ r1_tarski(X1,k1_zfmisc_1(esk1_0))
| ~ r2_hidden(esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),X1) ),
inference(spm,[status(thm)],[c_0_801,c_0_802]) ).
cnf(c_0_809,plain,
( r1_tarski(k1_tarski(X1),X2)
| ~ r2_hidden(X1,X2) ),
i_0_72 ).
cnf(c_0_810,plain,
( r2_hidden(X1,k1_zfmisc_1(X2))
| ~ r1_tarski(X1,X2) ),
inference(spm,[status(thm)],[c_0_803,c_0_798]) ).
cnf(c_0_811,plain,
( r2_hidden(X1,X2)
| ~ r1_tarski(X3,X2)
| ~ r2_hidden(X1,X3) ),
i_0_67 ).
cnf(c_0_812,negated_conjecture,
r1_tarski(esk2_0,esk1_0),
inference(spm,[status(thm)],[c_0_804,c_0_805]) ).
cnf(c_0_813,negated_conjecture,
( r2_hidden(esk5_3(X1,esk1_0,X2),X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(esk1_0))
| ~ r2_hidden(X1,a_2_0_relset_2(esk1_0,X2)) ),
inference(spm,[status(thm)],[c_0_806,c_0_807]) ).
cnf(c_0_814,plain,
( X1 = k1_tarski(esk5_3(X1,X2,X3))
| v1_xboole_0(X2)
| ~ r2_hidden(X1,a_2_0_relset_2(X2,X3))
| ~ m1_subset_1(X3,k1_zfmisc_1(X2)) ),
i_0_59 ).
cnf(c_0_815,negated_conjecture,
~ m1_subset_1(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(k1_zfmisc_1(esk1_0))),
i_0_64 ).
cnf(c_0_816,plain,
( ~ r2_hidden(esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),k1_tarski(X1))
| ~ r2_hidden(X1,k1_zfmisc_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_808,c_0_809]) ).
cnf(c_0_817,plain,
( r2_hidden(k1_tarski(X1),k1_zfmisc_1(X2))
| ~ r2_hidden(X1,X2) ),
inference(spm,[status(thm)],[c_0_810,c_0_809]) ).
cnf(c_0_818,negated_conjecture,
( r2_hidden(X1,esk1_0)
| ~ r2_hidden(X1,esk2_0) ),
inference(spm,[status(thm)],[c_0_811,c_0_812]) ).
cnf(c_0_819,negated_conjecture,
( r2_hidden(esk5_3(X1,esk1_0,esk2_0),esk2_0)
| ~ r2_hidden(X1,a_2_0_relset_2(esk1_0,esk2_0)) ),
inference(spm,[status(thm)],[c_0_813,c_0_805]) ).
cnf(c_0_820,negated_conjecture,
( k1_tarski(esk5_3(X1,esk1_0,X2)) = X1
| ~ m1_subset_1(X2,k1_zfmisc_1(esk1_0))
| ~ r2_hidden(X1,a_2_0_relset_2(esk1_0,X2)) ),
inference(spm,[status(thm)],[c_0_806,c_0_814]) ).
cnf(c_0_821,negated_conjecture,
~ r1_tarski(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),
inference(spm,[status(thm)],[c_0_815,c_0_798]) ).
cnf(c_0_822,plain,
( r2_hidden(esk3_2(X1,X2),X1)
| r1_tarski(X1,X2) ),
i_0_68 ).
cnf(c_0_823,plain,
( ~ r2_hidden(esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),k1_tarski(k1_tarski(X1)))
| ~ r2_hidden(X1,esk1_0) ),
inference(spm,[status(thm)],[c_0_816,c_0_817]) ).
cnf(c_0_824,negated_conjecture,
( r2_hidden(esk5_3(X1,esk1_0,esk2_0),esk1_0)
| ~ r2_hidden(X1,a_2_0_relset_2(esk1_0,esk2_0)) ),
inference(spm,[status(thm)],[c_0_818,c_0_819]) ).
cnf(c_0_825,negated_conjecture,
( k1_tarski(esk5_3(X1,esk1_0,esk2_0)) = X1
| ~ r2_hidden(X1,a_2_0_relset_2(esk1_0,esk2_0)) ),
inference(spm,[status(thm)],[c_0_820,c_0_805]) ).
cnf(c_0_826,negated_conjecture,
r2_hidden(esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),a_2_0_relset_2(esk1_0,esk2_0)),
inference(spm,[status(thm)],[c_0_821,c_0_822]) ).
cnf(c_0_827,plain,
( r2_hidden(X1,X2)
| ~ r1_tarski(k1_tarski(X1),X2) ),
i_0_69 ).
cnf(c_0_828,plain,
r1_tarski(X1,X1),
i_0_85 ).
cnf(c_0_829,plain,
( ~ r2_hidden(esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),k1_tarski(k1_tarski(esk5_3(X1,esk1_0,esk2_0))))
| ~ r2_hidden(X1,a_2_0_relset_2(esk1_0,esk2_0)) ),
inference(spm,[status(thm)],[c_0_823,c_0_824]) ).
cnf(c_0_830,negated_conjecture,
k1_tarski(esk5_3(esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),esk1_0,esk2_0)) = esk3_2(a_2_0_relset_2(esk1_0,esk2_0),k1_zfmisc_1(esk1_0)),
inference(spm,[status(thm)],[c_0_825,c_0_826]) ).
cnf(c_0_831,plain,
r2_hidden(X1,k1_tarski(X1)),
inference(spm,[status(thm)],[c_0_827,c_0_828]) ).
cnf(c_0_832,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_829,c_0_826]),c_0_830]),c_0_831])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU422+1 : TPTP v9.2.1. Released v3.4.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 : n018.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 03:08:47 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 210.13/128.43 % Version : CSE_E---1.7
% 210.13/128.43 % Problem : theBenchmark.p
% 210.13/128.43 % SZS status Theorem for theBenchmark.p
% 210.13/128.43 % SZS output start CNFRefutation
% See solution above
% 214.93/133.25 % Total time : 127.343s
%------------------------------------------------------------------------------