%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU329+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Sun Dec 26 07:23:45 EST 2010
% Result : Theorem 13.07s
% Output : CNFRefutation 13.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 95
% Number of leaves : 2
% Syntax : Number of formulae : 263 ( 9 unt; 0 def)
% Number of atoms : 2198 ( 837 equ)
% Maximal formula atoms : 518 ( 8 avg)
% Number of connectives : 3198 (1263 ~;1726 |; 191 &)
% ( 3 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 87 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 3 con; 0-7 aty)
% Number of variables : 781 ( 34 sgn 90 !; 52 ?)
% Comments :
%------------------------------------------------------------------------------
fof(11,conjecture,
! [X1,X2] :
( ( one_sorted_str(X1)
& element(X2,powerset(powerset(the_carrier(X1)))) )
=> ! [X3] :
? [X4] :
! [X5] :
( in(X5,X4)
<=> ( in(X5,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
& ? [X6,X7] :
( ordered_pair(X6,X7) = X5
& in(X6,complements_of_subsets(the_carrier(X1),X2))
& ! [X8] :
( element(X8,powerset(the_carrier(X1)))
=> ( X8 = X6
=> X7 = subset_complement(the_carrier(X1),X8) ) ) ) ) ) ),
file('/tmp/tmpdXuoT0/sel_SEU329+1.p_1',s1_xboole_0__e4_7_1__tops_2__1) ).
fof(23,axiom,
! [X1,X2] :
( ( one_sorted_str(X1)
& element(X2,powerset(powerset(the_carrier(X1)))) )
=> ! [X3] :
( ! [X4,X5,X6] :
( ( X4 = X5
& ? [X7,X8] :
( ordered_pair(X7,X8) = X5
& in(X7,complements_of_subsets(the_carrier(X1),X2))
& ! [X9] :
( element(X9,powerset(the_carrier(X1)))
=> ( X9 = X7
=> X8 = subset_complement(the_carrier(X1),X9) ) ) )
& X4 = X6
& ? [X10,X11] :
( ordered_pair(X10,X11) = X6
& in(X10,complements_of_subsets(the_carrier(X1),X2))
& ! [X12] :
( element(X12,powerset(the_carrier(X1)))
=> ( X12 = X10
=> X11 = subset_complement(the_carrier(X1),X12) ) ) ) )
=> X5 = X6 )
=> ? [X4] :
! [X5] :
( in(X5,X4)
<=> ? [X6] :
( in(X6,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
& X6 = X5
& ? [X13,X14] :
( ordered_pair(X13,X14) = X5
& in(X13,complements_of_subsets(the_carrier(X1),X2))
& ! [X15] :
( element(X15,powerset(the_carrier(X1)))
=> ( X15 = X13
=> X14 = subset_complement(the_carrier(X1),X15) ) ) ) ) ) ) ),
file('/tmp/tmpdXuoT0/sel_SEU329+1.p_1',s1_tarski__e4_7_1__tops_2__2) ).
fof(35,negated_conjecture,
~ ! [X1,X2] :
( ( one_sorted_str(X1)
& element(X2,powerset(powerset(the_carrier(X1)))) )
=> ! [X3] :
? [X4] :
! [X5] :
( in(X5,X4)
<=> ( in(X5,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
& ? [X6,X7] :
( ordered_pair(X6,X7) = X5
& in(X6,complements_of_subsets(the_carrier(X1),X2))
& ! [X8] :
( element(X8,powerset(the_carrier(X1)))
=> ( X8 = X6
=> X7 = subset_complement(the_carrier(X1),X8) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[11]) ).
fof(73,negated_conjecture,
? [X1,X2] :
( one_sorted_str(X1)
& element(X2,powerset(powerset(the_carrier(X1))))
& ? [X3] :
! [X4] :
? [X5] :
( ( ~ in(X5,X4)
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| ! [X6,X7] :
( ordered_pair(X6,X7) != X5
| ~ in(X6,complements_of_subsets(the_carrier(X1),X2))
| ? [X8] :
( element(X8,powerset(the_carrier(X1)))
& X8 = X6
& X7 != subset_complement(the_carrier(X1),X8) ) ) )
& ( in(X5,X4)
| ( in(X5,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
& ? [X6,X7] :
( ordered_pair(X6,X7) = X5
& in(X6,complements_of_subsets(the_carrier(X1),X2))
& ! [X8] :
( ~ element(X8,powerset(the_carrier(X1)))
| X8 != X6
| X7 = subset_complement(the_carrier(X1),X8) ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[35]) ).
fof(74,negated_conjecture,
? [X9,X10] :
( one_sorted_str(X9)
& element(X10,powerset(powerset(the_carrier(X9))))
& ? [X11] :
! [X12] :
? [X13] :
( ( ~ in(X13,X12)
| ~ in(X13,cartesian_product2(complements_of_subsets(the_carrier(X9),X10),X11))
| ! [X14,X15] :
( ordered_pair(X14,X15) != X13
| ~ in(X14,complements_of_subsets(the_carrier(X9),X10))
| ? [X16] :
( element(X16,powerset(the_carrier(X9)))
& X16 = X14
& X15 != subset_complement(the_carrier(X9),X16) ) ) )
& ( in(X13,X12)
| ( in(X13,cartesian_product2(complements_of_subsets(the_carrier(X9),X10),X11))
& ? [X17,X18] :
( ordered_pair(X17,X18) = X13
& in(X17,complements_of_subsets(the_carrier(X9),X10))
& ! [X19] :
( ~ element(X19,powerset(the_carrier(X9)))
| X19 != X17
| X18 = subset_complement(the_carrier(X9),X19) ) ) ) ) ) ),
inference(variable_rename,[status(thm)],[73]) ).
fof(75,negated_conjecture,
( one_sorted_str(esk2_0)
& element(esk3_0,powerset(powerset(the_carrier(esk2_0))))
& ! [X12] :
( ( ~ in(esk5_1(X12),X12)
| ~ in(esk5_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ! [X14,X15] :
( ordered_pair(X14,X15) != esk5_1(X12)
| ~ in(X14,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ( element(esk6_3(X12,X14,X15),powerset(the_carrier(esk2_0)))
& esk6_3(X12,X14,X15) = X14
& X15 != subset_complement(the_carrier(esk2_0),esk6_3(X12,X14,X15)) ) ) )
& ( in(esk5_1(X12),X12)
| ( in(esk5_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
& ordered_pair(esk7_1(X12),esk8_1(X12)) = esk5_1(X12)
& in(esk7_1(X12),complements_of_subsets(the_carrier(esk2_0),esk3_0))
& ! [X19] :
( ~ element(X19,powerset(the_carrier(esk2_0)))
| X19 != esk7_1(X12)
| esk8_1(X12) = subset_complement(the_carrier(esk2_0),X19) ) ) ) ) ),
inference(skolemize,[status(esa)],[74]) ).
fof(76,negated_conjecture,
! [X12,X14,X15,X19] :
( ( ( ( ~ element(X19,powerset(the_carrier(esk2_0)))
| X19 != esk7_1(X12)
| esk8_1(X12) = subset_complement(the_carrier(esk2_0),X19) )
& ordered_pair(esk7_1(X12),esk8_1(X12)) = esk5_1(X12)
& in(esk7_1(X12),complements_of_subsets(the_carrier(esk2_0),esk3_0))
& in(esk5_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0)) )
| in(esk5_1(X12),X12) )
& ( ordered_pair(X14,X15) != esk5_1(X12)
| ~ in(X14,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ( element(esk6_3(X12,X14,X15),powerset(the_carrier(esk2_0)))
& esk6_3(X12,X14,X15) = X14
& X15 != subset_complement(the_carrier(esk2_0),esk6_3(X12,X14,X15)) )
| ~ in(esk5_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(X12),X12) )
& one_sorted_str(esk2_0)
& element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(shift_quantors,[status(thm)],[75]) ).
fof(77,negated_conjecture,
! [X12,X14,X15,X19] :
( ( ~ element(X19,powerset(the_carrier(esk2_0)))
| X19 != esk7_1(X12)
| esk8_1(X12) = subset_complement(the_carrier(esk2_0),X19)
| in(esk5_1(X12),X12) )
& ( ordered_pair(esk7_1(X12),esk8_1(X12)) = esk5_1(X12)
| in(esk5_1(X12),X12) )
& ( in(esk7_1(X12),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| in(esk5_1(X12),X12) )
& ( in(esk5_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| in(esk5_1(X12),X12) )
& ( element(esk6_3(X12,X14,X15),powerset(the_carrier(esk2_0)))
| ordered_pair(X14,X15) != esk5_1(X12)
| ~ in(X14,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(X12),X12) )
& ( esk6_3(X12,X14,X15) = X14
| ordered_pair(X14,X15) != esk5_1(X12)
| ~ in(X14,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(X12),X12) )
& ( X15 != subset_complement(the_carrier(esk2_0),esk6_3(X12,X14,X15))
| ordered_pair(X14,X15) != esk5_1(X12)
| ~ in(X14,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(X12),X12) )
& one_sorted_str(esk2_0)
& element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(distribute,[status(thm)],[76]) ).
cnf(78,negated_conjecture,
element(esk3_0,powerset(powerset(the_carrier(esk2_0)))),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(79,negated_conjecture,
one_sorted_str(esk2_0),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(80,negated_conjecture,
( ~ in(esk5_1(X1),X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ordered_pair(X2,X3) != esk5_1(X1)
| X3 != subset_complement(the_carrier(esk2_0),esk6_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(81,negated_conjecture,
( esk6_3(X1,X2,X3) = X2
| ~ in(esk5_1(X1),X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ordered_pair(X2,X3) != esk5_1(X1) ),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(82,negated_conjecture,
( element(esk6_3(X1,X2,X3),powerset(the_carrier(esk2_0)))
| ~ in(esk5_1(X1),X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ordered_pair(X2,X3) != esk5_1(X1) ),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(83,negated_conjecture,
( in(esk5_1(X1),X1)
| in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0)) ),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(84,negated_conjecture,
( in(esk5_1(X1),X1)
| in(esk7_1(X1),complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(85,negated_conjecture,
( in(esk5_1(X1),X1)
| ordered_pair(esk7_1(X1),esk8_1(X1)) = esk5_1(X1) ),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(86,negated_conjecture,
( in(esk5_1(X1),X1)
| esk8_1(X1) = subset_complement(the_carrier(esk2_0),X2)
| X2 != esk7_1(X1)
| ~ element(X2,powerset(the_carrier(esk2_0))) ),
inference(split_conjunct,[status(thm)],[77]) ).
fof(133,plain,
! [X1,X2] :
( ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1))))
| ! [X3] :
( ? [X4,X5,X6] :
( X4 = X5
& ? [X7,X8] :
( ordered_pair(X7,X8) = X5
& in(X7,complements_of_subsets(the_carrier(X1),X2))
& ! [X9] :
( ~ element(X9,powerset(the_carrier(X1)))
| X9 != X7
| X8 = subset_complement(the_carrier(X1),X9) ) )
& X4 = X6
& ? [X10,X11] :
( ordered_pair(X10,X11) = X6
& in(X10,complements_of_subsets(the_carrier(X1),X2))
& ! [X12] :
( ~ element(X12,powerset(the_carrier(X1)))
| X12 != X10
| X11 = subset_complement(the_carrier(X1),X12) ) )
& X5 != X6 )
| ? [X4] :
! [X5] :
( ( ~ in(X5,X4)
| ? [X6] :
( in(X6,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
& X6 = X5
& ? [X13,X14] :
( ordered_pair(X13,X14) = X5
& in(X13,complements_of_subsets(the_carrier(X1),X2))
& ! [X15] :
( ~ element(X15,powerset(the_carrier(X1)))
| X15 != X13
| X14 = subset_complement(the_carrier(X1),X15) ) ) ) )
& ( ! [X6] :
( ~ in(X6,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| X6 != X5
| ! [X13,X14] :
( ordered_pair(X13,X14) != X5
| ~ in(X13,complements_of_subsets(the_carrier(X1),X2))
| ? [X15] :
( element(X15,powerset(the_carrier(X1)))
& X15 = X13
& X14 != subset_complement(the_carrier(X1),X15) ) ) )
| in(X5,X4) ) ) ) ),
inference(fof_nnf,[status(thm)],[23]) ).
fof(134,plain,
! [X16,X17] :
( ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16))))
| ! [X18] :
( ? [X19,X20,X21] :
( X19 = X20
& ? [X22,X23] :
( ordered_pair(X22,X23) = X20
& in(X22,complements_of_subsets(the_carrier(X16),X17))
& ! [X24] :
( ~ element(X24,powerset(the_carrier(X16)))
| X24 != X22
| X23 = subset_complement(the_carrier(X16),X24) ) )
& X19 = X21
& ? [X25,X26] :
( ordered_pair(X25,X26) = X21
& in(X25,complements_of_subsets(the_carrier(X16),X17))
& ! [X27] :
( ~ element(X27,powerset(the_carrier(X16)))
| X27 != X25
| X26 = subset_complement(the_carrier(X16),X27) ) )
& X20 != X21 )
| ? [X28] :
! [X29] :
( ( ~ in(X29,X28)
| ? [X30] :
( in(X30,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
& X30 = X29
& ? [X31,X32] :
( ordered_pair(X31,X32) = X29
& in(X31,complements_of_subsets(the_carrier(X16),X17))
& ! [X33] :
( ~ element(X33,powerset(the_carrier(X16)))
| X33 != X31
| X32 = subset_complement(the_carrier(X16),X33) ) ) ) )
& ( ! [X34] :
( ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| ! [X35,X36] :
( ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ? [X37] :
( element(X37,powerset(the_carrier(X16)))
& X37 = X35
& X36 != subset_complement(the_carrier(X16),X37) ) ) )
| in(X29,X28) ) ) ) ),
inference(variable_rename,[status(thm)],[133]) ).
fof(135,plain,
! [X16,X17] :
( ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16))))
| ! [X18] :
( ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
& ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
& in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
& ! [X24] :
( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24) )
& esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
& ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
& in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
& ! [X27] :
( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27) )
& esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18) )
| ! [X29] :
( ( ~ in(X29,esk16_3(X16,X17,X18))
| ( in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
& esk17_4(X16,X17,X18,X29) = X29
& ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
& in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
& ! [X33] :
( ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33) ) ) )
& ( ! [X34] :
( ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| ! [X35,X36] :
( ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ( element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
& esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
& X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36)) ) ) )
| in(X29,esk16_3(X16,X17,X18)) ) ) ) ),
inference(skolemize,[status(esa)],[134]) ).
fof(136,plain,
! [X16,X17,X18,X24,X27,X29,X33,X34,X35,X36] :
( ( ( ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ( element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
& esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
& X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36)) )
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18)) )
& ( ( ( ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33) )
& ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
& in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
& in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
& esk17_4(X16,X17,X18,X29) = X29 )
| ~ in(X29,esk16_3(X16,X17,X18)) ) )
| ( ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27) )
& ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
& in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24) )
& ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
& in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
& esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
& esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
& esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18) )
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) ),
inference(shift_quantors,[status(thm)],[135]) ).
fof(137,plain,
! [X16,X17,X18,X24,X27,X29,X33,X34,X35,X36] :
( ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27)
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24)
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18)
| element(esk20_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27)
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24)
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18)
| esk20_7(X16,X17,X18,X29,X34,X35,X36) = X35
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27)
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24)
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18)
| X36 != subset_complement(the_carrier(X16),esk20_7(X16,X17,X18,X29,X34,X35,X36))
| ordered_pair(X35,X36) != X29
| ~ in(X35,complements_of_subsets(the_carrier(X16),X17))
| ~ in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| X34 != X29
| in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27)
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24)
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18)
| ~ element(X33,powerset(the_carrier(X16)))
| X33 != esk18_4(X16,X17,X18,X29)
| esk19_4(X16,X17,X18,X29) = subset_complement(the_carrier(X16),X33)
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27)
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24)
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18)
| ordered_pair(esk18_4(X16,X17,X18,X29),esk19_4(X16,X17,X18,X29)) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27)
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24)
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18)
| in(esk18_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27)
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24)
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18)
| in(esk17_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X27,powerset(the_carrier(X16)))
| X27 != esk14_3(X16,X17,X18)
| esk15_3(X16,X17,X18) = subset_complement(the_carrier(X16),X27)
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk14_3(X16,X17,X18),esk15_3(X16,X17,X18)) = esk11_3(X16,X17,X18)
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk14_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ~ element(X24,powerset(the_carrier(X16)))
| X24 != esk12_3(X16,X17,X18)
| esk13_3(X16,X17,X18) = subset_complement(the_carrier(X16),X24)
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( ordered_pair(esk12_3(X16,X17,X18),esk13_3(X16,X17,X18)) = esk10_3(X16,X17,X18)
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( in(esk12_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk10_3(X16,X17,X18)
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk9_3(X16,X17,X18) = esk11_3(X16,X17,X18)
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) )
& ( esk10_3(X16,X17,X18) != esk11_3(X16,X17,X18)
| esk17_4(X16,X17,X18,X29) = X29
| ~ in(X29,esk16_3(X16,X17,X18))
| ~ one_sorted_str(X16)
| ~ element(X17,powerset(powerset(the_carrier(X16)))) ) ),
inference(distribute,[status(thm)],[136]) ).
cnf(138,plain,
( esk17_4(X2,X1,X4,X3) = X3
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4))
| esk10_3(X2,X1,X4) != esk11_3(X2,X1,X4) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(139,plain,
( esk17_4(X2,X1,X4,X3) = X3
| esk9_3(X2,X1,X4) = esk11_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(140,plain,
( esk17_4(X2,X1,X4,X3) = X3
| esk9_3(X2,X1,X4) = esk10_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(147,plain,
( in(esk17_4(X2,X1,X4,X3),cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4))
| esk10_3(X2,X1,X4) != esk11_3(X2,X1,X4) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(148,plain,
( in(esk17_4(X2,X1,X4,X3),cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| esk9_3(X2,X1,X4) = esk11_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(149,plain,
( in(esk17_4(X2,X1,X4,X3),cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| esk9_3(X2,X1,X4) = esk10_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(156,plain,
( in(esk18_4(X2,X1,X4,X3),complements_of_subsets(the_carrier(X2),X1))
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4))
| esk10_3(X2,X1,X4) != esk11_3(X2,X1,X4) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(157,plain,
( in(esk18_4(X2,X1,X4,X3),complements_of_subsets(the_carrier(X2),X1))
| esk9_3(X2,X1,X4) = esk11_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(158,plain,
( in(esk18_4(X2,X1,X4,X3),complements_of_subsets(the_carrier(X2),X1))
| esk9_3(X2,X1,X4) = esk10_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(165,plain,
( ordered_pair(esk18_4(X2,X1,X4,X3),esk19_4(X2,X1,X4,X3)) = X3
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4))
| esk10_3(X2,X1,X4) != esk11_3(X2,X1,X4) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(166,plain,
( ordered_pair(esk18_4(X2,X1,X4,X3),esk19_4(X2,X1,X4,X3)) = X3
| esk9_3(X2,X1,X4) = esk11_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(167,plain,
( ordered_pair(esk18_4(X2,X1,X4,X3),esk19_4(X2,X1,X4,X3)) = X3
| esk9_3(X2,X1,X4) = esk10_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(174,plain,
( esk19_4(X2,X1,X4,X3) = subset_complement(the_carrier(X2),X5)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4))
| X5 != esk18_4(X2,X1,X4,X3)
| ~ element(X5,powerset(the_carrier(X2)))
| esk10_3(X2,X1,X4) != esk11_3(X2,X1,X4) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(175,plain,
( esk19_4(X2,X1,X4,X3) = subset_complement(the_carrier(X2),X5)
| esk9_3(X2,X1,X4) = esk11_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4))
| X5 != esk18_4(X2,X1,X4,X3)
| ~ element(X5,powerset(the_carrier(X2))) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(176,plain,
( esk19_4(X2,X1,X4,X3) = subset_complement(the_carrier(X2),X5)
| esk9_3(X2,X1,X4) = esk10_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| ~ in(X3,esk16_3(X2,X1,X4))
| X5 != esk18_4(X2,X1,X4,X3)
| ~ element(X5,powerset(the_carrier(X2))) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(183,plain,
( in(X3,esk16_3(X2,X1,X4))
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3
| X7 != subset_complement(the_carrier(X2),esk20_7(X2,X1,X4,X3,X5,X6,X7))
| esk10_3(X2,X1,X4) != esk11_3(X2,X1,X4) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(184,plain,
( in(X3,esk16_3(X2,X1,X4))
| esk9_3(X2,X1,X4) = esk11_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3
| X7 != subset_complement(the_carrier(X2),esk20_7(X2,X1,X4,X3,X5,X6,X7)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(185,plain,
( in(X3,esk16_3(X2,X1,X4))
| esk9_3(X2,X1,X4) = esk10_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3
| X7 != subset_complement(the_carrier(X2),esk20_7(X2,X1,X4,X3,X5,X6,X7)) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(192,plain,
( in(X3,esk16_3(X2,X1,X4))
| esk20_7(X2,X1,X4,X3,X5,X6,X7) = X6
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3
| esk10_3(X2,X1,X4) != esk11_3(X2,X1,X4) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(193,plain,
( in(X3,esk16_3(X2,X1,X4))
| esk20_7(X2,X1,X4,X3,X5,X6,X7) = X6
| esk9_3(X2,X1,X4) = esk11_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3 ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(194,plain,
( in(X3,esk16_3(X2,X1,X4))
| esk20_7(X2,X1,X4,X3,X5,X6,X7) = X6
| esk9_3(X2,X1,X4) = esk10_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3 ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(201,plain,
( in(X3,esk16_3(X2,X1,X4))
| element(esk20_7(X2,X1,X4,X3,X5,X6,X7),powerset(the_carrier(X2)))
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3
| esk10_3(X2,X1,X4) != esk11_3(X2,X1,X4) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(202,plain,
( in(X3,esk16_3(X2,X1,X4))
| element(esk20_7(X2,X1,X4,X3,X5,X6,X7),powerset(the_carrier(X2)))
| esk9_3(X2,X1,X4) = esk11_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3 ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(203,plain,
( in(X3,esk16_3(X2,X1,X4))
| element(esk20_7(X2,X1,X4,X3,X5,X6,X7),powerset(the_carrier(X2)))
| esk9_3(X2,X1,X4) = esk10_3(X2,X1,X4)
| ~ element(X1,powerset(powerset(the_carrier(X2))))
| ~ one_sorted_str(X2)
| X5 != X3
| ~ in(X5,cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))
| ~ in(X6,complements_of_subsets(the_carrier(X2),X1))
| ordered_pair(X6,X7) != X3 ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(432,negated_conjecture,
( subset_complement(the_carrier(esk2_0),esk7_1(X1)) = esk8_1(X1)
| in(esk5_1(X1),X1)
| ~ element(esk7_1(X1),powerset(the_carrier(esk2_0))) ),
inference(er,[status(thm)],[86,theory(equality)]) ).
cnf(453,negated_conjecture,
( esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| esk17_4(esk2_0,esk3_0,X1,X2) = X2
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ one_sorted_str(esk2_0) ),
inference(spm,[status(thm)],[140,78,theory(equality)]) ).
cnf(458,negated_conjecture,
( esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| esk17_4(esk2_0,esk3_0,X1,X2) = X2
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false ),
inference(rw,[status(thm)],[453,79,theory(equality)]) ).
cnf(459,negated_conjecture,
( esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| esk17_4(esk2_0,esk3_0,X1,X2) = X2
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(cn,[status(thm)],[458,theory(equality)]) ).
cnf(461,negated_conjecture,
( esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| esk17_4(esk2_0,esk3_0,X1,X2) = X2
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ one_sorted_str(esk2_0) ),
inference(spm,[status(thm)],[139,78,theory(equality)]) ).
cnf(466,negated_conjecture,
( esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| esk17_4(esk2_0,esk3_0,X1,X2) = X2
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false ),
inference(rw,[status(thm)],[461,79,theory(equality)]) ).
cnf(467,negated_conjecture,
( esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| esk17_4(esk2_0,esk3_0,X1,X2) = X2
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(cn,[status(thm)],[466,theory(equality)]) ).
cnf(514,plain,
( in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| esk11_3(X1,X2,X3) != esk10_3(X1,X2,X3)
| ~ in(X4,esk16_3(X1,X2,X3))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(spm,[status(thm)],[147,138,theory(equality)]) ).
cnf(567,plain,
( esk19_4(X1,X2,X3,X4) = subset_complement(the_carrier(X1),esk18_4(X1,X2,X3,X4))
| esk9_3(X1,X2,X3) = esk10_3(X1,X2,X3)
| ~ in(X4,esk16_3(X1,X2,X3))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1))))
| ~ element(esk18_4(X1,X2,X3,X4),powerset(the_carrier(X1))) ),
inference(er,[status(thm)],[176,theory(equality)]) ).
cnf(577,plain,
( esk19_4(X1,X2,X3,X4) = subset_complement(the_carrier(X1),esk18_4(X1,X2,X3,X4))
| esk9_3(X1,X2,X3) = esk11_3(X1,X2,X3)
| ~ in(X4,esk16_3(X1,X2,X3))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1))))
| ~ element(esk18_4(X1,X2,X3,X4),powerset(the_carrier(X1))) ),
inference(er,[status(thm)],[175,theory(equality)]) ).
cnf(578,plain,
( esk19_4(X1,X2,X3,X4) = subset_complement(the_carrier(X1),esk18_4(X1,X2,X3,X4))
| esk11_3(X1,X2,X3) != esk10_3(X1,X2,X3)
| ~ in(X4,esk16_3(X1,X2,X3))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1))))
| ~ element(esk18_4(X1,X2,X3,X4),powerset(the_carrier(X1))) ),
inference(er,[status(thm)],[174,theory(equality)]) ).
cnf(590,plain,
( esk20_7(X1,X2,X3,X4,X4,X5,X6) = X5
| esk9_3(X1,X2,X3) = esk10_3(X1,X2,X3)
| in(X4,esk16_3(X1,X2,X3))
| ordered_pair(X5,X6) != X4
| ~ in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| ~ in(X5,complements_of_subsets(the_carrier(X1),X2))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(er,[status(thm)],[194,theory(equality)]) ).
cnf(591,plain,
( esk20_7(X1,X2,X3,X4,X4,X5,X6) = X5
| esk9_3(X1,X2,X3) = esk11_3(X1,X2,X3)
| in(X4,esk16_3(X1,X2,X3))
| ordered_pair(X5,X6) != X4
| ~ in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| ~ in(X5,complements_of_subsets(the_carrier(X1),X2))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(er,[status(thm)],[193,theory(equality)]) ).
cnf(593,plain,
( esk20_7(X1,X2,X3,X4,X4,X5,X6) = X5
| in(X4,esk16_3(X1,X2,X3))
| esk11_3(X1,X2,X3) != esk10_3(X1,X2,X3)
| ordered_pair(X5,X6) != X4
| ~ in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| ~ in(X5,complements_of_subsets(the_carrier(X1),X2))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(er,[status(thm)],[192,theory(equality)]) ).
cnf(594,plain,
( esk9_3(X1,X2,X3) = esk10_3(X1,X2,X3)
| in(X4,esk16_3(X1,X2,X3))
| element(esk20_7(X1,X2,X3,X4,X4,X5,X6),powerset(the_carrier(X1)))
| ordered_pair(X5,X6) != X4
| ~ in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| ~ in(X5,complements_of_subsets(the_carrier(X1),X2))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(er,[status(thm)],[203,theory(equality)]) ).
cnf(595,plain,
( esk9_3(X1,X2,X3) = esk11_3(X1,X2,X3)
| in(X4,esk16_3(X1,X2,X3))
| element(esk20_7(X1,X2,X3,X4,X4,X5,X6),powerset(the_carrier(X1)))
| ordered_pair(X5,X6) != X4
| ~ in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| ~ in(X5,complements_of_subsets(the_carrier(X1),X2))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(er,[status(thm)],[202,theory(equality)]) ).
cnf(596,plain,
( in(X1,esk16_3(X2,X3,X4))
| element(esk20_7(X2,X3,X4,X1,X1,X5,X6),powerset(the_carrier(X2)))
| esk11_3(X2,X3,X4) != esk10_3(X2,X3,X4)
| ordered_pair(X5,X6) != X1
| ~ in(X1,cartesian_product2(complements_of_subsets(the_carrier(X2),X3),X4))
| ~ in(X5,complements_of_subsets(the_carrier(X2),X3))
| ~ one_sorted_str(X2)
| ~ element(X3,powerset(powerset(the_carrier(X2)))) ),
inference(er,[status(thm)],[201,theory(equality)]) ).
cnf(599,plain,
( esk9_3(X1,X2,X3) = esk10_3(X1,X2,X3)
| in(X4,esk16_3(X1,X2,X3))
| subset_complement(the_carrier(X1),esk20_7(X1,X2,X3,X4,X4,X5,X6)) != X6
| ordered_pair(X5,X6) != X4
| ~ in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| ~ in(X5,complements_of_subsets(the_carrier(X1),X2))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(er,[status(thm)],[185,theory(equality)]) ).
cnf(600,plain,
( esk9_3(X1,X2,X3) = esk11_3(X1,X2,X3)
| in(X4,esk16_3(X1,X2,X3))
| subset_complement(the_carrier(X1),esk20_7(X1,X2,X3,X4,X4,X5,X6)) != X6
| ordered_pair(X5,X6) != X4
| ~ in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))
| ~ in(X5,complements_of_subsets(the_carrier(X1),X2))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(er,[status(thm)],[184,theory(equality)]) ).
cnf(602,plain,
( in(X1,esk16_3(X2,X3,X4))
| subset_complement(the_carrier(X2),esk20_7(X2,X3,X4,X1,X1,X5,X6)) != X6
| esk11_3(X2,X3,X4) != esk10_3(X2,X3,X4)
| ordered_pair(X5,X6) != X1
| ~ in(X1,cartesian_product2(complements_of_subsets(the_carrier(X2),X3),X4))
| ~ in(X5,complements_of_subsets(the_carrier(X2),X3))
| ~ one_sorted_str(X2)
| ~ element(X3,powerset(powerset(the_carrier(X2)))) ),
inference(er,[status(thm)],[183,theory(equality)]) ).
cnf(1837,negated_conjecture,
( esk6_3(X1,X2,X3) = X2
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[81,514,theory(equality)]) ).
cnf(1838,negated_conjecture,
( element(esk6_3(X1,X2,X3),powerset(the_carrier(esk2_0)))
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[82,514,theory(equality)]) ).
cnf(1840,negated_conjecture,
( esk6_3(X1,X2,X3) = X2
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[1837,79,theory(equality)]) ).
cnf(1841,negated_conjecture,
( esk6_3(X1,X2,X3) = X2
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| $false ),
inference(rw,[status(thm)],[1840,78,theory(equality)]) ).
cnf(1842,negated_conjecture,
( esk6_3(X1,X2,X3) = X2
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(cn,[status(thm)],[1841,theory(equality)]) ).
cnf(1843,negated_conjecture,
( element(esk6_3(X1,X2,X3),powerset(the_carrier(esk2_0)))
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[1838,79,theory(equality)]) ).
cnf(1844,negated_conjecture,
( element(esk6_3(X1,X2,X3),powerset(the_carrier(esk2_0)))
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| $false ),
inference(rw,[status(thm)],[1843,78,theory(equality)]) ).
cnf(1845,negated_conjecture,
( element(esk6_3(X1,X2,X3),powerset(the_carrier(esk2_0)))
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(cn,[status(thm)],[1844,theory(equality)]) ).
cnf(4780,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[590,83,theory(equality)]) ).
cnf(4856,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[4780,79,theory(equality)]) ).
cnf(4857,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[4856,78,theory(equality)]) ).
cnf(4858,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[4857,theory(equality)]) ).
cnf(5080,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[591,83,theory(equality)]) ).
cnf(5157,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[5080,79,theory(equality)]) ).
cnf(5158,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[5157,78,theory(equality)]) ).
cnf(5159,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[5158,theory(equality)]) ).
cnf(5293,negated_conjecture,
( esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[593,83,theory(equality)]) ).
cnf(5370,negated_conjecture,
( esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[5293,79,theory(equality)]) ).
cnf(5371,negated_conjecture,
( esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[5370,78,theory(equality)]) ).
cnf(5372,negated_conjecture,
( esk20_7(esk2_0,esk3_0,esk4_0,esk5_1(X1),esk5_1(X1),X2,X3) = X2
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[5371,theory(equality)]) ).
cnf(7704,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[594,4858,theory(equality)]) ).
cnf(7709,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[599,4858,theory(equality)]) ).
cnf(7716,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[7704,79,theory(equality)]) ).
cnf(7717,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[7716,78,theory(equality)]) ).
cnf(7718,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[7717,theory(equality)]) ).
cnf(7731,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[7709,79,theory(equality)]) ).
cnf(7732,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[7731,78,theory(equality)]) ).
cnf(7733,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[7732,theory(equality)]) ).
cnf(7754,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[595,5159,theory(equality)]) ).
cnf(7759,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[600,5159,theory(equality)]) ).
cnf(7768,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[7754,79,theory(equality)]) ).
cnf(7769,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[7768,78,theory(equality)]) ).
cnf(7770,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[7769,theory(equality)]) ).
cnf(7783,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[7759,79,theory(equality)]) ).
cnf(7784,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[7783,78,theory(equality)]) ).
cnf(7785,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[7784,theory(equality)]) ).
cnf(7895,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[596,5372,theory(equality)]) ).
cnf(7900,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[602,5372,theory(equality)]) ).
cnf(7911,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[7895,79,theory(equality)]) ).
cnf(7912,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[7911,78,theory(equality)]) ).
cnf(7913,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| element(X2,powerset(the_carrier(esk2_0)))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[7912,theory(equality)]) ).
cnf(7926,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[7900,79,theory(equality)]) ).
cnf(7927,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[7926,78,theory(equality)]) ).
cnf(7928,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[7927,theory(equality)]) ).
cnf(7941,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(X2,powerset(the_carrier(esk2_0)))
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[7718,83]) ).
cnf(7942,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(esk7_1(X2),powerset(the_carrier(esk2_0)))
| in(esk5_1(X2),X2)
| ordered_pair(esk7_1(X2),X3) != esk5_1(X1) ),
inference(spm,[status(thm)],[7941,84,theory(equality)]) ).
cnf(7972,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),X2)
| in(esk5_1(X1),X1)
| element(esk7_1(X2),powerset(the_carrier(esk2_0)))
| esk5_1(X2) != esk5_1(X1) ),
inference(spm,[status(thm)],[7942,85,theory(equality)]) ).
cnf(7973,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(esk7_1(X1),powerset(the_carrier(esk2_0))) ),
inference(er,[status(thm)],[7972,theory(equality)]) ).
cnf(8081,negated_conjecture,
( subset_complement(the_carrier(esk2_0),esk7_1(X1)) = esk8_1(X1)
| in(esk5_1(X1),X1)
| esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[432,7973,theory(equality)]) ).
cnf(10301,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(X2,powerset(the_carrier(esk2_0)))
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[7770,83]) ).
cnf(10302,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(esk7_1(X2),powerset(the_carrier(esk2_0)))
| in(esk5_1(X2),X2)
| ordered_pair(esk7_1(X2),X3) != esk5_1(X1) ),
inference(spm,[status(thm)],[10301,84,theory(equality)]) ).
cnf(10332,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),X2)
| in(esk5_1(X1),X1)
| element(esk7_1(X2),powerset(the_carrier(esk2_0)))
| esk5_1(X2) != esk5_1(X1) ),
inference(spm,[status(thm)],[10302,85,theory(equality)]) ).
cnf(10333,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(esk7_1(X1),powerset(the_carrier(esk2_0))) ),
inference(er,[status(thm)],[10332,theory(equality)]) ).
cnf(10438,negated_conjecture,
( subset_complement(the_carrier(esk2_0),esk7_1(X1)) = esk8_1(X1)
| in(esk5_1(X1),X1)
| esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[432,10333,theory(equality)]) ).
cnf(12837,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(X2,powerset(the_carrier(esk2_0)))
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[7913,83]) ).
cnf(12838,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(esk7_1(X2),powerset(the_carrier(esk2_0)))
| in(esk5_1(X2),X2)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(esk7_1(X2),X3) != esk5_1(X1) ),
inference(spm,[status(thm)],[12837,84,theory(equality)]) ).
cnf(12868,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),X2)
| in(esk5_1(X1),X1)
| element(esk7_1(X2),powerset(the_carrier(esk2_0)))
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| esk5_1(X2) != esk5_1(X1) ),
inference(spm,[status(thm)],[12838,85,theory(equality)]) ).
cnf(12869,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(esk7_1(X1),powerset(the_carrier(esk2_0)))
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0) ),
inference(er,[status(thm)],[12868,theory(equality)]) ).
cnf(22269,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[7733,83]) ).
cnf(22270,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,subset_complement(the_carrier(esk2_0),X2)) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(er,[status(thm)],[22269,theory(equality)]) ).
cnf(22290,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),X2)
| ordered_pair(esk7_1(X2),esk8_1(X2)) != esk5_1(X1)
| ~ in(esk7_1(X2),complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(spm,[status(thm)],[22270,8081,theory(equality)]) ).
cnf(22339,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[7785,83]) ).
cnf(22340,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,subset_complement(the_carrier(esk2_0),X2)) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(er,[status(thm)],[22339,theory(equality)]) ).
cnf(22362,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),X2)
| ordered_pair(esk7_1(X2),esk8_1(X2)) != esk5_1(X1)
| ~ in(esk7_1(X2),complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(spm,[status(thm)],[22340,10438,theory(equality)]) ).
cnf(22412,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| subset_complement(the_carrier(esk2_0),X2) != X3
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[7928,83]) ).
cnf(22413,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X2,subset_complement(the_carrier(esk2_0),X2)) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(er,[status(thm)],[22412,theory(equality)]) ).
cnf(22654,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),X2)
| ordered_pair(esk7_1(X2),esk8_1(X2)) != esk5_1(X1) ),
inference(csr,[status(thm)],[22290,84]) ).
cnf(22655,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),X2)
| esk5_1(X1) != esk5_1(X2) ),
inference(spm,[status(thm)],[22654,85,theory(equality)]) ).
cnf(22656,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1) ),
inference(er,[status(thm)],[22655,theory(equality)]) ).
cnf(22657,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(ef,[status(thm)],[22656,theory(equality)]) ).
cnf(22776,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk17_4(esk2_0,esk3_0,esk4_0,esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))) = esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[459,22657,theory(equality)]) ).
cnf(22992,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[149,22776,theory(equality)]) ).
cnf(23020,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[22992,79,theory(equality)]) ).
cnf(23021,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| $false ),
inference(rw,[status(thm)],[23020,78,theory(equality)]) ).
cnf(23022,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(cn,[status(thm)],[23021,theory(equality)]) ).
cnf(23104,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0)) ),
inference(csr,[status(thm)],[23022,83]) ).
cnf(23106,negated_conjecture,
( esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2) = X1
| esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[81,23104,theory(equality)]) ).
cnf(23107,negated_conjecture,
( element(esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[82,23104,theory(equality)]) ).
cnf(24455,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[23107,22657]) ).
cnf(25690,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),X2)
| ordered_pair(esk7_1(X2),esk8_1(X2)) != esk5_1(X1) ),
inference(csr,[status(thm)],[22362,84]) ).
cnf(25691,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),X2)
| esk5_1(X1) != esk5_1(X2) ),
inference(spm,[status(thm)],[25690,85,theory(equality)]) ).
cnf(25692,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1) ),
inference(er,[status(thm)],[25691,theory(equality)]) ).
cnf(25701,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(ef,[status(thm)],[25692,theory(equality)]) ).
cnf(25991,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk17_4(esk2_0,esk3_0,esk4_0,esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))) = esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[467,25701,theory(equality)]) ).
cnf(26033,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[148,25991,theory(equality)]) ).
cnf(26071,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[26033,79,theory(equality)]) ).
cnf(26072,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| $false ),
inference(rw,[status(thm)],[26071,78,theory(equality)]) ).
cnf(26073,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(cn,[status(thm)],[26072,theory(equality)]) ).
cnf(26124,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0)) ),
inference(csr,[status(thm)],[26073,83]) ).
cnf(26126,negated_conjecture,
( esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2) = X1
| esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[81,26124,theory(equality)]) ).
cnf(26127,negated_conjecture,
( element(esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[82,26124,theory(equality)]) ).
cnf(27393,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| element(esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[26127,25701]) ).
cnf(28345,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2) = X1
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[23106,22657]) ).
cnf(28346,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| subset_complement(the_carrier(esk2_0),X1) != X2
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[80,28345,theory(equality)]) ).
cnf(28347,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(X1,powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(spm,[status(thm)],[24455,28345,theory(equality)]) ).
cnf(28412,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[28347,158,theory(equality)]) ).
cnf(28456,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[28412,79,theory(equality)]) ).
cnf(28457,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| $false ),
inference(rw,[status(thm)],[28456,78,theory(equality)]) ).
cnf(28458,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(cn,[status(thm)],[28457,theory(equality)]) ).
cnf(29626,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[28346,22657]) ).
cnf(29627,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[29626,23104]) ).
cnf(29631,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(X1,X2,X3) = esk10_3(X1,X2,X3)
| X4 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),esk18_4(X1,X2,X3,X4)) != esk19_4(X1,X2,X3,X4)
| ~ in(esk18_4(X1,X2,X3,X4),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X4,esk16_3(X1,X2,X3))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(spm,[status(thm)],[29627,167,theory(equality)]) ).
cnf(29689,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,X1,X2) = esk10_3(esk2_0,X1,X2)
| X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| ~ one_sorted_str(esk2_0)
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(spm,[status(thm)],[29631,567,theory(equality)]) ).
cnf(29692,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,X1,X2) = esk10_3(esk2_0,X1,X2)
| X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| $false
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(rw,[status(thm)],[29689,79,theory(equality)]) ).
cnf(29693,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,X1,X2) = esk10_3(esk2_0,X1,X2)
| X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(cn,[status(thm)],[29692,theory(equality)]) ).
cnf(29698,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0))))
| ~ one_sorted_str(esk2_0) ),
inference(spm,[status(thm)],[29693,158,theory(equality)]) ).
cnf(29736,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| $false
| ~ one_sorted_str(esk2_0) ),
inference(rw,[status(thm)],[29698,78,theory(equality)]) ).
cnf(29737,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| $false
| $false ),
inference(rw,[status(thm)],[29736,79,theory(equality)]) ).
cnf(29738,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0))) ),
inference(cn,[status(thm)],[29737,theory(equality)]) ).
cnf(30318,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2) = X1
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[26126,25701]) ).
cnf(30319,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| subset_complement(the_carrier(esk2_0),X1) != X2
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[80,30318,theory(equality)]) ).
cnf(30351,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| element(X1,powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(spm,[status(thm)],[27393,30318,theory(equality)]) ).
cnf(31645,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[30319,25701]) ).
cnf(31646,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(csr,[status(thm)],[31645,26124]) ).
cnf(31651,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(X1,X2,X3) = esk11_3(X1,X2,X3)
| X4 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),esk18_4(X1,X2,X3,X4)) != esk19_4(X1,X2,X3,X4)
| ~ in(esk18_4(X1,X2,X3,X4),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X4,esk16_3(X1,X2,X3))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(spm,[status(thm)],[31646,166,theory(equality)]) ).
cnf(31887,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,X1,X2) = esk11_3(esk2_0,X1,X2)
| X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| ~ one_sorted_str(esk2_0)
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(spm,[status(thm)],[31651,577,theory(equality)]) ).
cnf(31891,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,X1,X2) = esk11_3(esk2_0,X1,X2)
| X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| $false
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(rw,[status(thm)],[31887,79,theory(equality)]) ).
cnf(31892,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,X1,X2) = esk11_3(esk2_0,X1,X2)
| X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(cn,[status(thm)],[31891,theory(equality)]) ).
cnf(31896,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0))))
| ~ one_sorted_str(esk2_0) ),
inference(spm,[status(thm)],[31892,157,theory(equality)]) ).
cnf(31936,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| $false
| ~ one_sorted_str(esk2_0) ),
inference(rw,[status(thm)],[31896,78,theory(equality)]) ).
cnf(31937,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| $false
| $false ),
inference(rw,[status(thm)],[31936,79,theory(equality)]) ).
cnf(31938,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0))) ),
inference(cn,[status(thm)],[31937,theory(equality)]) ).
cnf(39859,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[28458,167,theory(equality)]) ).
cnf(39878,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[39859,79,theory(equality)]) ).
cnf(39879,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| $false ),
inference(rw,[status(thm)],[39878,78,theory(equality)]) ).
cnf(39880,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(cn,[status(thm)],[39879,theory(equality)]) ).
cnf(39893,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(csr,[status(thm)],[39880,29738]) ).
cnf(39894,negated_conjecture,
( esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk10_3(esk2_0,esk3_0,X1)
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,X1)) ),
inference(er,[status(thm)],[39893,theory(equality)]) ).
cnf(39895,negated_conjecture,
esk9_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0),
inference(spm,[status(thm)],[39894,22657,theory(equality)]) ).
cnf(39940,negated_conjecture,
( esk10_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0))) ),
inference(rw,[status(thm)],[31938,39895,theory(equality)]) ).
cnf(40010,negated_conjecture,
( esk10_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| element(X1,powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(rw,[status(thm)],[30351,39895,theory(equality)]) ).
cnf(40247,negated_conjecture,
( esk10_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0)
| in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(rw,[status(thm)],[25701,39895,theory(equality)]) ).
cnf(41028,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[40010,157,theory(equality)]) ).
cnf(41064,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[41028,79,theory(equality)]) ).
cnf(41065,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| $false ),
inference(rw,[status(thm)],[41064,78,theory(equality)]) ).
cnf(41066,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(cn,[status(thm)],[41065,theory(equality)]) ).
cnf(45641,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[41066,166,theory(equality)]) ).
cnf(45658,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[45641,79,theory(equality)]) ).
cnf(45659,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| $false ),
inference(rw,[status(thm)],[45658,78,theory(equality)]) ).
cnf(45660,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(cn,[status(thm)],[45659,theory(equality)]) ).
cnf(45678,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(csr,[status(thm)],[45660,39940]) ).
cnf(45679,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,X1) = esk11_3(esk2_0,esk3_0,X1)
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,X1)) ),
inference(er,[status(thm)],[45678,theory(equality)]) ).
cnf(45680,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk9_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0) ),
inference(spm,[status(thm)],[45679,40247,theory(equality)]) ).
cnf(45681,negated_conjecture,
( esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0)
| esk10_3(esk2_0,esk3_0,esk4_0) = esk11_3(esk2_0,esk3_0,esk4_0) ),
inference(rw,[status(thm)],[45680,39895,theory(equality)]) ).
cnf(45682,negated_conjecture,
esk11_3(esk2_0,esk3_0,esk4_0) = esk10_3(esk2_0,esk3_0,esk4_0),
inference(cn,[status(thm)],[45681,theory(equality)]) ).
cnf(46161,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| $false
| ordered_pair(X2,subset_complement(the_carrier(esk2_0),X2)) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(rw,[status(thm)],[22413,45682,theory(equality)]) ).
cnf(46162,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| ordered_pair(X2,subset_complement(the_carrier(esk2_0),X2)) != esk5_1(X1)
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[46161,theory(equality)]) ).
cnf(46173,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(esk7_1(X1),powerset(the_carrier(esk2_0)))
| $false ),
inference(rw,[status(thm)],[12869,45682,theory(equality)]) ).
cnf(46174,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| element(esk7_1(X1),powerset(the_carrier(esk2_0))) ),
inference(cn,[status(thm)],[46173,theory(equality)]) ).
cnf(46189,negated_conjecture,
( esk6_3(X1,X2,X3) = X2
| $false
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1) ),
inference(rw,[status(thm)],[1842,45682,theory(equality)]) ).
cnf(46190,negated_conjecture,
( esk6_3(X1,X2,X3) = X2
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1) ),
inference(cn,[status(thm)],[46189,theory(equality)]) ).
cnf(46191,negated_conjecture,
( element(esk6_3(X1,X2,X3),powerset(the_carrier(esk2_0)))
| $false
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1) ),
inference(rw,[status(thm)],[1845,45682,theory(equality)]) ).
cnf(46192,negated_conjecture,
( element(esk6_3(X1,X2,X3),powerset(the_carrier(esk2_0)))
| ordered_pair(X2,X3) != esk5_1(X1)
| ~ in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(X1),X1) ),
inference(cn,[status(thm)],[46191,theory(equality)]) ).
cnf(46242,negated_conjecture,
( subset_complement(the_carrier(esk2_0),esk7_1(X1)) = esk8_1(X1)
| in(esk5_1(X1),X1)
| in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[432,46174,theory(equality)]) ).
cnf(46570,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),X2)
| ordered_pair(esk7_1(X2),esk8_1(X2)) != esk5_1(X1)
| ~ in(esk7_1(X2),complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(spm,[status(thm)],[46162,46242,theory(equality)]) ).
cnf(47325,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),X2)
| ordered_pair(esk7_1(X2),esk8_1(X2)) != esk5_1(X1) ),
inference(csr,[status(thm)],[46570,84]) ).
cnf(47326,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X2),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1)
| in(esk5_1(X2),X2)
| esk5_1(X1) != esk5_1(X2) ),
inference(spm,[status(thm)],[47325,85,theory(equality)]) ).
cnf(47333,negated_conjecture,
( in(esk5_1(X1),esk16_3(esk2_0,esk3_0,esk4_0))
| in(esk5_1(X1),X1) ),
inference(er,[status(thm)],[47326,theory(equality)]) ).
cnf(47334,negated_conjecture,
in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)),
inference(ef,[status(thm)],[47333,theory(equality)]) ).
cnf(47475,negated_conjecture,
( esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2) = X1
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[46190,47334,theory(equality)]) ).
cnf(47476,negated_conjecture,
( element(esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(spm,[status(thm)],[46192,47334,theory(equality)]) ).
cnf(47492,negated_conjecture,
( esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2) = X1
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false ),
inference(rw,[status(thm)],[47475,47334,theory(equality)]) ).
cnf(47493,negated_conjecture,
( esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2) = X1
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[47492,theory(equality)]) ).
cnf(47494,negated_conjecture,
( element(esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| $false
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(rw,[status(thm)],[47476,47334,theory(equality)]) ).
cnf(47495,negated_conjecture,
( element(esk6_3(esk16_3(esk2_0,esk3_0,esk4_0),X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[47494,theory(equality)]) ).
cnf(47537,negated_conjecture,
( subset_complement(the_carrier(esk2_0),X1) != X2
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[80,47493,theory(equality)]) ).
cnf(47538,negated_conjecture,
( subset_complement(the_carrier(esk2_0),X1) != X2
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false ),
inference(rw,[status(thm)],[47537,47334,theory(equality)]) ).
cnf(47539,negated_conjecture,
( subset_complement(the_carrier(esk2_0),X1) != X2
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),cartesian_product2(complements_of_subsets(the_carrier(esk2_0),esk3_0),esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[47538,theory(equality)]) ).
cnf(48628,negated_conjecture,
( element(X1,powerset(the_carrier(esk2_0)))
| ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(spm,[status(thm)],[47495,47493,theory(equality)]) ).
cnf(48634,negated_conjecture,
( element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[48628,156,theory(equality)]) ).
cnf(48674,negated_conjecture,
( element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[48634,79,theory(equality)]) ).
cnf(48675,negated_conjecture,
( element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| $false ),
inference(rw,[status(thm)],[48674,78,theory(equality)]) ).
cnf(48676,negated_conjecture,
( element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| ordered_pair(esk18_4(esk2_0,esk3_0,X1,X2),X3) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(cn,[status(thm)],[48675,theory(equality)]) ).
cnf(51902,negated_conjecture,
( ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0)
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[47539,514,theory(equality)]) ).
cnf(51924,negated_conjecture,
( ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,esk4_0))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[51902,45682,theory(equality)]) ).
cnf(51925,negated_conjecture,
( ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[51924,47334,theory(equality)]) ).
cnf(51926,negated_conjecture,
( ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[51925,79,theory(equality)]) ).
cnf(51927,negated_conjecture,
( ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0))
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[51926,78,theory(equality)]) ).
cnf(51928,negated_conjecture,
( ordered_pair(X1,X2) != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),X1) != X2
| ~ in(X1,complements_of_subsets(the_carrier(esk2_0),esk3_0)) ),
inference(cn,[status(thm)],[51927,theory(equality)]) ).
cnf(51952,negated_conjecture,
( X4 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| subset_complement(the_carrier(esk2_0),esk18_4(X1,X2,X3,X4)) != esk19_4(X1,X2,X3,X4)
| ~ in(esk18_4(X1,X2,X3,X4),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| esk11_3(X1,X2,X3) != esk10_3(X1,X2,X3)
| ~ in(X4,esk16_3(X1,X2,X3))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(spm,[status(thm)],[51928,165,theory(equality)]) ).
cnf(52660,negated_conjecture,
( element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ one_sorted_str(esk2_0)
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(spm,[status(thm)],[48676,165,theory(equality)]) ).
cnf(52679,negated_conjecture,
( element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0)))) ),
inference(rw,[status(thm)],[52660,79,theory(equality)]) ).
cnf(52680,negated_conjecture,
( element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| $false
| $false ),
inference(rw,[status(thm)],[52679,78,theory(equality)]) ).
cnf(52681,negated_conjecture,
( element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(cn,[status(thm)],[52680,theory(equality)]) ).
cnf(59976,negated_conjecture,
( X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,X1,X2) != esk10_3(esk2_0,X1,X2)
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| ~ one_sorted_str(esk2_0)
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(spm,[status(thm)],[51952,578,theory(equality)]) ).
cnf(59981,negated_conjecture,
( X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,X1,X2) != esk10_3(esk2_0,X1,X2)
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| $false
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(rw,[status(thm)],[59976,79,theory(equality)]) ).
cnf(59982,negated_conjecture,
( X3 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| esk11_3(esk2_0,X1,X2) != esk10_3(esk2_0,X1,X2)
| ~ in(esk18_4(esk2_0,X1,X2,X3),complements_of_subsets(the_carrier(esk2_0),esk3_0))
| ~ in(X3,esk16_3(esk2_0,X1,X2))
| ~ element(X1,powerset(powerset(the_carrier(esk2_0))))
| ~ element(esk18_4(esk2_0,X1,X2,X3),powerset(the_carrier(esk2_0))) ),
inference(cn,[status(thm)],[59981,theory(equality)]) ).
cnf(59985,negated_conjecture,
( esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| ~ element(esk3_0,powerset(powerset(the_carrier(esk2_0))))
| ~ one_sorted_str(esk2_0) ),
inference(spm,[status(thm)],[59982,156,theory(equality)]) ).
cnf(60019,negated_conjecture,
( esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| $false
| ~ one_sorted_str(esk2_0) ),
inference(rw,[status(thm)],[59985,78,theory(equality)]) ).
cnf(60020,negated_conjecture,
( esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0)))
| $false
| $false ),
inference(rw,[status(thm)],[60019,79,theory(equality)]) ).
cnf(60021,negated_conjecture,
( esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1))
| ~ element(esk18_4(esk2_0,esk3_0,X1,X2),powerset(the_carrier(esk2_0))) ),
inference(cn,[status(thm)],[60020,theory(equality)]) ).
cnf(60076,negated_conjecture,
( esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| X2 != esk5_1(esk16_3(esk2_0,esk3_0,esk4_0))
| ~ in(X2,esk16_3(esk2_0,esk3_0,X1)) ),
inference(csr,[status(thm)],[60021,52681]) ).
cnf(60077,negated_conjecture,
( esk11_3(esk2_0,esk3_0,X1) != esk10_3(esk2_0,esk3_0,X1)
| ~ in(esk5_1(esk16_3(esk2_0,esk3_0,esk4_0)),esk16_3(esk2_0,esk3_0,X1)) ),
inference(er,[status(thm)],[60076,theory(equality)]) ).
cnf(60078,negated_conjecture,
esk11_3(esk2_0,esk3_0,esk4_0) != esk10_3(esk2_0,esk3_0,esk4_0),
inference(spm,[status(thm)],[60077,47334,theory(equality)]) ).
cnf(60079,negated_conjecture,
$false,
inference(rw,[status(thm)],[60078,45682,theory(equality)]) ).
cnf(60080,negated_conjecture,
$false,
inference(cn,[status(thm)],[60079,theory(equality)]) ).
cnf(60081,negated_conjecture,
$false,
60080,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% /home/graph/tptp/Systems/SInE---0.4/Source/sine.py:10: DeprecationWarning: the sets module is deprecated
% from sets import Set
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU329+1.p
% --creating new selector for []
% -running prover on /tmp/tmpdXuoT0/sel_SEU329+1.p_1 with time limit 29
% -prover status Theorem
% Problem SEU329+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU329+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU329+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------