%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU329+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Thu Dec 30 03:34:45 EST 2010
% Result : Theorem 12.86s
% Output : Solution 12.86s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP31074/SEU329+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP31074/SEU329+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP31074/SEU329+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 31170
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.91 CPU 2.01 WC
% PrfWatch: 3.90 CPU 4.01 WC
% PrfWatch: 5.55 CPU 6.02 WC
% PrfWatch: 7.16 CPU 8.02 WC
% PrfWatch: 9.15 CPU 10.03 WC
% # Preprocessing time : 0.023 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 11.15 CPU 12.03 WC
% # SZS output start CNFRefutation.
% fof(6, 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/SRASS.s.p', s1_tarski__e4_7_1__tops_2__2)).
% fof(34, 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/SRASS.s.p', s1_xboole_0__e4_7_1__tops_2__1)).
% 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)],[34])).
% fof(56, 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)],[6])).
% fof(57, 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)],[56])).
% fof(58, plain,![X16]:![X17]:((~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))|![X18]:(((((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)&((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)&in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17)))&![X24]:(~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))))&esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18))&((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)&in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17)))&![X27]:(~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))))&~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18)))|![X29]:((~(in(X29,esk8_3(X16,X17,X18)))|((in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))&esk9_4(X16,X17,X18,X29)=X29)&((ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29&in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17)))&![X33]:(~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_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(esk12_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))&(esk12_7(X16,X17,X18,X29,X34,X35,X36)=X35&~(X36=subset_complement(the_carrier(X16),esk12_7(X16,X17,X18,X29,X34,X35,X36)))))))|in(X29,esk8_3(X16,X17,X18)))))),inference(skolemize,[status(esa)],[57])).
% fof(59, 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(esk12_7(X16,X17,X18,X29,X34,X35,X36),powerset(the_carrier(X16)))&(esk12_7(X16,X17,X18,X29,X34,X35,X36)=X35&~(X36=subset_complement(the_carrier(X16),esk12_7(X16,X17,X18,X29,X34,X35,X36))))))|(~(in(X34,cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18)))|~(X34=X29)))|in(X29,esk8_3(X16,X17,X18)))&((((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))&(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29&in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))))&(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))&esk9_4(X16,X17,X18,X29)=X29))|~(in(X29,esk8_3(X16,X17,X18)))))|((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))&(ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)&in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))))&((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))&(ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)&in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))))&esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18))&esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)))&~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))),inference(shift_quantors,[status(thm)],[58])).
% fof(60, plain,![X16]:![X17]:![X18]:![X24]:![X27]:![X29]:![X33]:![X34]:![X35]:![X36]:((((((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))|(((element(esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&(((((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))|(((esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))|(((~(X36=subset_complement(the_carrier(X16),esk12_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,esk8_3(X16,X17,X18))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))))&((((((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))|((~(element(X33,powerset(the_carrier(X16))))|(~(X33=esk10_4(X16,X17,X18,X29))|esk11_4(X16,X17,X18,X29)=subset_complement(the_carrier(X16),X33)))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&(((((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))|(ordered_pair(esk10_4(X16,X17,X18,X29),esk11_4(X16,X17,X18,X29))=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))|(in(esk10_4(X16,X17,X18,X29),complements_of_subsets(the_carrier(X16),X17))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))))&(((((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))|(in(esk9_4(X16,X17,X18,X29),cartesian_product2(complements_of_subsets(the_carrier(X16),X17),X18))|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((((((~(element(X27,powerset(the_carrier(X16))))|(~(X27=esk6_3(X16,X17,X18))|esk7_3(X16,X17,X18)=subset_complement(the_carrier(X16),X27)))|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk6_3(X16,X17,X18),esk7_3(X16,X17,X18))=esk3_3(X16,X17,X18)|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk6_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((((((~(element(X24,powerset(the_carrier(X16))))|(~(X24=esk4_3(X16,X17,X18))|esk5_3(X16,X17,X18)=subset_complement(the_carrier(X16),X24)))|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&(((ordered_pair(esk4_3(X16,X17,X18),esk5_3(X16,X17,X18))=esk2_3(X16,X17,X18)|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))&((in(esk4_3(X16,X17,X18),complements_of_subsets(the_carrier(X16),X17))|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((esk1_3(X16,X17,X18)=esk2_3(X16,X17,X18)|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))&((esk1_3(X16,X17,X18)=esk3_3(X16,X17,X18)|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16)))))))))&((~(esk2_3(X16,X17,X18)=esk3_3(X16,X17,X18))|(esk9_4(X16,X17,X18,X29)=X29|~(in(X29,esk8_3(X16,X17,X18)))))|(~(one_sorted_str(X16))|~(element(X17,powerset(powerset(the_carrier(X16))))))))))),inference(distribute,[status(thm)],[59])).
% cnf(61,plain,(esk9_4(X2,X1,X4,X3)=X3|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))|esk2_3(X2,X1,X4)!=esk3_3(X2,X1,X4)),inference(split_conjunct,[status(thm)],[60])).
% cnf(62,plain,(esk9_4(X2,X1,X4,X3)=X3|esk1_3(X2,X1,X4)=esk3_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))),inference(split_conjunct,[status(thm)],[60])).
% cnf(63,plain,(esk9_4(X2,X1,X4,X3)=X3|esk1_3(X2,X1,X4)=esk2_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))),inference(split_conjunct,[status(thm)],[60])).
% cnf(70,plain,(in(esk9_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,esk8_3(X2,X1,X4))|esk2_3(X2,X1,X4)!=esk3_3(X2,X1,X4)),inference(split_conjunct,[status(thm)],[60])).
% cnf(71,plain,(in(esk9_4(X2,X1,X4,X3),cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))|esk1_3(X2,X1,X4)=esk3_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))),inference(split_conjunct,[status(thm)],[60])).
% cnf(72,plain,(in(esk9_4(X2,X1,X4,X3),cartesian_product2(complements_of_subsets(the_carrier(X2),X1),X4))|esk1_3(X2,X1,X4)=esk2_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))),inference(split_conjunct,[status(thm)],[60])).
% cnf(79,plain,(in(esk10_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,esk8_3(X2,X1,X4))|esk2_3(X2,X1,X4)!=esk3_3(X2,X1,X4)),inference(split_conjunct,[status(thm)],[60])).
% cnf(80,plain,(in(esk10_4(X2,X1,X4,X3),complements_of_subsets(the_carrier(X2),X1))|esk1_3(X2,X1,X4)=esk3_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))),inference(split_conjunct,[status(thm)],[60])).
% cnf(81,plain,(in(esk10_4(X2,X1,X4,X3),complements_of_subsets(the_carrier(X2),X1))|esk1_3(X2,X1,X4)=esk2_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))),inference(split_conjunct,[status(thm)],[60])).
% cnf(88,plain,(ordered_pair(esk10_4(X2,X1,X4,X3),esk11_4(X2,X1,X4,X3))=X3|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))|esk2_3(X2,X1,X4)!=esk3_3(X2,X1,X4)),inference(split_conjunct,[status(thm)],[60])).
% cnf(89,plain,(ordered_pair(esk10_4(X2,X1,X4,X3),esk11_4(X2,X1,X4,X3))=X3|esk1_3(X2,X1,X4)=esk3_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))),inference(split_conjunct,[status(thm)],[60])).
% cnf(90,plain,(ordered_pair(esk10_4(X2,X1,X4,X3),esk11_4(X2,X1,X4,X3))=X3|esk1_3(X2,X1,X4)=esk2_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))),inference(split_conjunct,[status(thm)],[60])).
% cnf(97,plain,(esk11_4(X2,X1,X4,X3)=subset_complement(the_carrier(X2),X5)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))|X5!=esk10_4(X2,X1,X4,X3)|~element(X5,powerset(the_carrier(X2)))|esk2_3(X2,X1,X4)!=esk3_3(X2,X1,X4)),inference(split_conjunct,[status(thm)],[60])).
% cnf(98,plain,(esk11_4(X2,X1,X4,X3)=subset_complement(the_carrier(X2),X5)|esk1_3(X2,X1,X4)=esk3_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))|X5!=esk10_4(X2,X1,X4,X3)|~element(X5,powerset(the_carrier(X2)))),inference(split_conjunct,[status(thm)],[60])).
% cnf(99,plain,(esk11_4(X2,X1,X4,X3)=subset_complement(the_carrier(X2),X5)|esk1_3(X2,X1,X4)=esk2_3(X2,X1,X4)|~element(X1,powerset(powerset(the_carrier(X2))))|~one_sorted_str(X2)|~in(X3,esk8_3(X2,X1,X4))|X5!=esk10_4(X2,X1,X4,X3)|~element(X5,powerset(the_carrier(X2)))),inference(split_conjunct,[status(thm)],[60])).
% cnf(106,plain,(in(X3,esk8_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),esk12_7(X2,X1,X4,X3,X5,X6,X7))|esk2_3(X2,X1,X4)!=esk3_3(X2,X1,X4)),inference(split_conjunct,[status(thm)],[60])).
% cnf(107,plain,(in(X3,esk8_3(X2,X1,X4))|esk1_3(X2,X1,X4)=esk3_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),esk12_7(X2,X1,X4,X3,X5,X6,X7))),inference(split_conjunct,[status(thm)],[60])).
% cnf(108,plain,(in(X3,esk8_3(X2,X1,X4))|esk1_3(X2,X1,X4)=esk2_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),esk12_7(X2,X1,X4,X3,X5,X6,X7))),inference(split_conjunct,[status(thm)],[60])).
% cnf(115,plain,(in(X3,esk8_3(X2,X1,X4))|esk12_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|esk2_3(X2,X1,X4)!=esk3_3(X2,X1,X4)),inference(split_conjunct,[status(thm)],[60])).
% cnf(116,plain,(in(X3,esk8_3(X2,X1,X4))|esk12_7(X2,X1,X4,X3,X5,X6,X7)=X6|esk1_3(X2,X1,X4)=esk3_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)],[60])).
% cnf(117,plain,(in(X3,esk8_3(X2,X1,X4))|esk12_7(X2,X1,X4,X3,X5,X6,X7)=X6|esk1_3(X2,X1,X4)=esk2_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)],[60])).
% cnf(124,plain,(in(X3,esk8_3(X2,X1,X4))|element(esk12_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|esk2_3(X2,X1,X4)!=esk3_3(X2,X1,X4)),inference(split_conjunct,[status(thm)],[60])).
% cnf(125,plain,(in(X3,esk8_3(X2,X1,X4))|element(esk12_7(X2,X1,X4,X3,X5,X6,X7),powerset(the_carrier(X2)))|esk1_3(X2,X1,X4)=esk3_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)],[60])).
% cnf(126,plain,(in(X3,esk8_3(X2,X1,X4))|element(esk12_7(X2,X1,X4,X3,X5,X6,X7),powerset(the_carrier(X2)))|esk1_3(X2,X1,X4)=esk2_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)],[60])).
% fof(253, 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(254, 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)],[253])).
% fof(255, negated_conjecture,((one_sorted_str(esk16_0)&element(esk17_0,powerset(powerset(the_carrier(esk16_0)))))&![X12]:((~(in(esk19_1(X12),X12))|(~(in(esk19_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0)))|![X14]:![X15]:((~(ordered_pair(X14,X15)=esk19_1(X12))|~(in(X14,complements_of_subsets(the_carrier(esk16_0),esk17_0))))|(element(esk20_3(X12,X14,X15),powerset(the_carrier(esk16_0)))&(esk20_3(X12,X14,X15)=X14&~(X15=subset_complement(the_carrier(esk16_0),esk20_3(X12,X14,X15))))))))&(in(esk19_1(X12),X12)|(in(esk19_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))&((ordered_pair(esk21_1(X12),esk22_1(X12))=esk19_1(X12)&in(esk21_1(X12),complements_of_subsets(the_carrier(esk16_0),esk17_0)))&![X19]:(~(element(X19,powerset(the_carrier(esk16_0))))|(~(X19=esk21_1(X12))|esk22_1(X12)=subset_complement(the_carrier(esk16_0),X19)))))))),inference(skolemize,[status(esa)],[254])).
% fof(256, negated_conjecture,![X12]:![X14]:![X15]:![X19]:((((((~(element(X19,powerset(the_carrier(esk16_0))))|(~(X19=esk21_1(X12))|esk22_1(X12)=subset_complement(the_carrier(esk16_0),X19)))&(ordered_pair(esk21_1(X12),esk22_1(X12))=esk19_1(X12)&in(esk21_1(X12),complements_of_subsets(the_carrier(esk16_0),esk17_0))))&in(esk19_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0)))|in(esk19_1(X12),X12))&((((~(ordered_pair(X14,X15)=esk19_1(X12))|~(in(X14,complements_of_subsets(the_carrier(esk16_0),esk17_0))))|(element(esk20_3(X12,X14,X15),powerset(the_carrier(esk16_0)))&(esk20_3(X12,X14,X15)=X14&~(X15=subset_complement(the_carrier(esk16_0),esk20_3(X12,X14,X15))))))|~(in(esk19_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))))|~(in(esk19_1(X12),X12))))&(one_sorted_str(esk16_0)&element(esk17_0,powerset(powerset(the_carrier(esk16_0)))))),inference(shift_quantors,[status(thm)],[255])).
% fof(257, negated_conjecture,![X12]:![X14]:![X15]:![X19]:((((((~(element(X19,powerset(the_carrier(esk16_0))))|(~(X19=esk21_1(X12))|esk22_1(X12)=subset_complement(the_carrier(esk16_0),X19)))|in(esk19_1(X12),X12))&((ordered_pair(esk21_1(X12),esk22_1(X12))=esk19_1(X12)|in(esk19_1(X12),X12))&(in(esk21_1(X12),complements_of_subsets(the_carrier(esk16_0),esk17_0))|in(esk19_1(X12),X12))))&(in(esk19_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|in(esk19_1(X12),X12)))&((((element(esk20_3(X12,X14,X15),powerset(the_carrier(esk16_0)))|(~(ordered_pair(X14,X15)=esk19_1(X12))|~(in(X14,complements_of_subsets(the_carrier(esk16_0),esk17_0)))))|~(in(esk19_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))))|~(in(esk19_1(X12),X12)))&((((esk20_3(X12,X14,X15)=X14|(~(ordered_pair(X14,X15)=esk19_1(X12))|~(in(X14,complements_of_subsets(the_carrier(esk16_0),esk17_0)))))|~(in(esk19_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))))|~(in(esk19_1(X12),X12)))&(((~(X15=subset_complement(the_carrier(esk16_0),esk20_3(X12,X14,X15)))|(~(ordered_pair(X14,X15)=esk19_1(X12))|~(in(X14,complements_of_subsets(the_carrier(esk16_0),esk17_0)))))|~(in(esk19_1(X12),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))))|~(in(esk19_1(X12),X12))))))&(one_sorted_str(esk16_0)&element(esk17_0,powerset(powerset(the_carrier(esk16_0)))))),inference(distribute,[status(thm)],[256])).
% cnf(258,negated_conjecture,(element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(split_conjunct,[status(thm)],[257])).
% cnf(259,negated_conjecture,(one_sorted_str(esk16_0)),inference(split_conjunct,[status(thm)],[257])).
% cnf(260,negated_conjecture,(~in(esk19_1(X1),X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(X2,complements_of_subsets(the_carrier(esk16_0),esk17_0))|ordered_pair(X2,X3)!=esk19_1(X1)|X3!=subset_complement(the_carrier(esk16_0),esk20_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[257])).
% cnf(261,negated_conjecture,(esk20_3(X1,X2,X3)=X2|~in(esk19_1(X1),X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(X2,complements_of_subsets(the_carrier(esk16_0),esk17_0))|ordered_pair(X2,X3)!=esk19_1(X1)),inference(split_conjunct,[status(thm)],[257])).
% cnf(262,negated_conjecture,(element(esk20_3(X1,X2,X3),powerset(the_carrier(esk16_0)))|~in(esk19_1(X1),X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(X2,complements_of_subsets(the_carrier(esk16_0),esk17_0))|ordered_pair(X2,X3)!=esk19_1(X1)),inference(split_conjunct,[status(thm)],[257])).
% cnf(263,negated_conjecture,(in(esk19_1(X1),X1)|in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(split_conjunct,[status(thm)],[257])).
% cnf(264,negated_conjecture,(in(esk19_1(X1),X1)|in(esk21_1(X1),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(split_conjunct,[status(thm)],[257])).
% cnf(265,negated_conjecture,(in(esk19_1(X1),X1)|ordered_pair(esk21_1(X1),esk22_1(X1))=esk19_1(X1)),inference(split_conjunct,[status(thm)],[257])).
% cnf(266,negated_conjecture,(in(esk19_1(X1),X1)|esk22_1(X1)=subset_complement(the_carrier(esk16_0),X2)|X2!=esk21_1(X1)|~element(X2,powerset(the_carrier(esk16_0)))),inference(split_conjunct,[status(thm)],[257])).
% cnf(382,negated_conjecture,(esk9_4(X1,X2,X3,esk19_1(esk8_3(X1,X2,X3)))=esk19_1(esk8_3(X1,X2,X3))|in(esk19_1(esk8_3(X1,X2,X3)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|esk3_3(X1,X2,X3)!=esk2_3(X1,X2,X3)|~one_sorted_str(X1)|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[61,263,theory(equality)])).
% cnf(383,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk21_1(X1))=esk22_1(X1)|in(esk19_1(X1),X1)|~element(esk21_1(X1),powerset(the_carrier(esk16_0)))),inference(er,[status(thm)],[266,theory(equality)])).
% cnf(397,negated_conjecture,(esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|esk9_4(X1,X2,X3,esk19_1(esk8_3(X1,X2,X3)))=esk19_1(esk8_3(X1,X2,X3))|in(esk19_1(esk8_3(X1,X2,X3)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~one_sorted_str(X1)|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[63,263,theory(equality)])).
% cnf(398,negated_conjecture,(esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|esk9_4(X1,X2,X3,esk19_1(esk8_3(X1,X2,X3)))=esk19_1(esk8_3(X1,X2,X3))|in(esk19_1(esk8_3(X1,X2,X3)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~one_sorted_str(X1)|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[62,263,theory(equality)])).
% cnf(399,plain,(in(X1,esk8_3(X2,X3,X4))|subset_complement(the_carrier(X2),esk12_7(X2,X3,X4,X1,X1,X5,X6))!=X6|esk3_3(X2,X3,X4)!=esk2_3(X2,X3,X4)|ordered_pair(X5,X6)!=X1|~one_sorted_str(X2)|~in(X1,cartesian_product2(complements_of_subsets(the_carrier(X2),X3),X4))|~in(X5,complements_of_subsets(the_carrier(X2),X3))|~element(X3,powerset(powerset(the_carrier(X2))))),inference(er,[status(thm)],[106,theory(equality)])).
% cnf(400,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~one_sorted_str(esk16_0)|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(spm,[status(thm)],[81,258,theory(equality)])).
% cnf(403,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|$false|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(rw,[status(thm)],[400,259,theory(equality)])).
% cnf(404,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(cn,[status(thm)],[403,theory(equality)])).
% cnf(406,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~one_sorted_str(esk16_0)|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(spm,[status(thm)],[80,258,theory(equality)])).
% cnf(409,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|$false|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(rw,[status(thm)],[406,259,theory(equality)])).
% cnf(410,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(cn,[status(thm)],[409,theory(equality)])).
% cnf(412,negated_conjecture,(in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|~one_sorted_str(esk16_0)|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(spm,[status(thm)],[79,258,theory(equality)])).
% cnf(415,negated_conjecture,(in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|$false|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(rw,[status(thm)],[412,259,theory(equality)])).
% cnf(416,negated_conjecture,(in(esk10_4(esk16_0,esk17_0,X1,X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(cn,[status(thm)],[415,theory(equality)])).
% cnf(445,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~one_sorted_str(esk16_0)|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(spm,[status(thm)],[72,258,theory(equality)])).
% cnf(448,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|$false|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(rw,[status(thm)],[445,259,theory(equality)])).
% cnf(449,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(cn,[status(thm)],[448,theory(equality)])).
% cnf(451,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~one_sorted_str(esk16_0)|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(spm,[status(thm)],[71,258,theory(equality)])).
% cnf(454,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|$false|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(rw,[status(thm)],[451,259,theory(equality)])).
% cnf(455,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(cn,[status(thm)],[454,theory(equality)])).
% cnf(472,negated_conjecture,(in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|~one_sorted_str(esk16_0)|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(spm,[status(thm)],[70,258,theory(equality)])).
% cnf(475,negated_conjecture,(in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|$false|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(rw,[status(thm)],[472,259,theory(equality)])).
% cnf(476,negated_conjecture,(in(esk9_4(esk16_0,esk17_0,X1,X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|~in(X2,esk8_3(esk16_0,esk17_0,X1))),inference(cn,[status(thm)],[475,theory(equality)])).
% cnf(478,plain,(esk11_4(X1,X2,X3,X4)=subset_complement(the_carrier(X1),esk10_4(X1,X2,X3,X4))|esk3_3(X1,X2,X3)!=esk2_3(X1,X2,X3)|~one_sorted_str(X1)|~in(X4,esk8_3(X1,X2,X3))|~element(X2,powerset(powerset(the_carrier(X1))))|~element(esk10_4(X1,X2,X3,X4),powerset(the_carrier(X1)))),inference(er,[status(thm)],[97,theory(equality)])).
% cnf(479,plain,(esk12_7(X1,X2,X3,X4,X4,X5,X6)=X5|in(X4,esk8_3(X1,X2,X3))|esk3_3(X1,X2,X3)!=esk2_3(X1,X2,X3)|ordered_pair(X5,X6)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(X5,complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[115,theory(equality)])).
% cnf(480,plain,(esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|subset_complement(the_carrier(X1),esk12_7(X1,X2,X3,X4,X4,X5,X6))!=X6|ordered_pair(X5,X6)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(X5,complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[108,theory(equality)])).
% cnf(481,plain,(esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|subset_complement(the_carrier(X1),esk12_7(X1,X2,X3,X4,X4,X5,X6))!=X6|ordered_pair(X5,X6)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(X5,complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[107,theory(equality)])).
% cnf(485,plain,(esk11_4(X1,X2,X3,X4)=subset_complement(the_carrier(X1),esk10_4(X1,X2,X3,X4))|esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|~one_sorted_str(X1)|~in(X4,esk8_3(X1,X2,X3))|~element(X2,powerset(powerset(the_carrier(X1))))|~element(esk10_4(X1,X2,X3,X4),powerset(the_carrier(X1)))),inference(er,[status(thm)],[99,theory(equality)])).
% cnf(513,plain,(esk12_7(X1,X2,X3,X4,X4,X5,X6)=X5|esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|ordered_pair(X5,X6)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(X5,complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[117,theory(equality)])).
% cnf(514,plain,(esk12_7(X1,X2,X3,X4,X4,X5,X6)=X5|esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|ordered_pair(X5,X6)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(X5,complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[116,theory(equality)])).
% cnf(518,plain,(esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|element(esk12_7(X1,X2,X3,X4,X4,X5,X6),powerset(the_carrier(X1)))|ordered_pair(X5,X6)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(X5,complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[126,theory(equality)])).
% cnf(519,plain,(esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|element(esk12_7(X1,X2,X3,X4,X4,X5,X6),powerset(the_carrier(X1)))|ordered_pair(X5,X6)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(X5,complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[125,theory(equality)])).
% cnf(520,plain,(esk11_4(X1,X2,X3,X4)=subset_complement(the_carrier(X1),esk10_4(X1,X2,X3,X4))|esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|~one_sorted_str(X1)|~in(X4,esk8_3(X1,X2,X3))|~element(X2,powerset(powerset(the_carrier(X1))))|~element(esk10_4(X1,X2,X3,X4),powerset(the_carrier(X1)))),inference(er,[status(thm)],[98,theory(equality)])).
% cnf(524,plain,(in(X1,esk8_3(X2,X3,X4))|element(esk12_7(X2,X3,X4,X1,X1,X5,X6),powerset(the_carrier(X2)))|esk3_3(X2,X3,X4)!=esk2_3(X2,X3,X4)|ordered_pair(X5,X6)!=X1|~one_sorted_str(X2)|~in(X1,cartesian_product2(complements_of_subsets(the_carrier(X2),X3),X4))|~in(X5,complements_of_subsets(the_carrier(X2),X3))|~element(X3,powerset(powerset(the_carrier(X2))))),inference(er,[status(thm)],[124,theory(equality)])).
% cnf(1357,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|~one_sorted_str(esk16_0)),inference(spm,[status(thm)],[382,258,theory(equality)])).
% cnf(1369,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|$false),inference(rw,[status(thm)],[1357,259,theory(equality)])).
% cnf(1370,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)),inference(cn,[status(thm)],[1369,theory(equality)])).
% cnf(1537,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~one_sorted_str(esk16_0)),inference(spm,[status(thm)],[397,258,theory(equality)])).
% cnf(1549,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|$false),inference(rw,[status(thm)],[1537,259,theory(equality)])).
% cnf(1550,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(cn,[status(thm)],[1549,theory(equality)])).
% cnf(1588,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~one_sorted_str(esk16_0)),inference(spm,[status(thm)],[398,258,theory(equality)])).
% cnf(1600,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|$false),inference(rw,[status(thm)],[1588,259,theory(equality)])).
% cnf(1601,negated_conjecture,(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1)))=esk19_1(esk8_3(esk16_0,esk17_0,X1))|esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(cn,[status(thm)],[1600,theory(equality)])).
% cnf(1618,negated_conjecture,(in(X1,esk8_3(X2,X3,X4))|in(esk19_1(X5),X5)|subset_complement(the_carrier(X2),esk12_7(X2,X3,X4,X1,X1,esk21_1(X5),esk22_1(X5)))!=esk22_1(X5)|esk3_3(X2,X3,X4)!=esk2_3(X2,X3,X4)|esk19_1(X5)!=X1|~one_sorted_str(X2)|~in(X1,cartesian_product2(complements_of_subsets(the_carrier(X2),X3),X4))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X2),X3))|~element(X3,powerset(powerset(the_carrier(X2))))),inference(spm,[status(thm)],[399,265,theory(equality)])).
% cnf(2710,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1))),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[449,263,theory(equality)])).
% cnf(3117,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1))),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[455,263,theory(equality)])).
% cnf(3685,negated_conjecture,(in(esk9_4(esk16_0,esk17_0,X1,esk19_1(esk8_3(esk16_0,esk17_0,X1))),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)),inference(spm,[status(thm)],[476,263,theory(equality)])).
% cnf(4013,negated_conjecture,(esk12_7(X1,X2,X3,X4,X4,esk21_1(X5),esk22_1(X5))=esk21_1(X5)|in(X4,esk8_3(X1,X2,X3))|in(esk19_1(X5),X5)|esk3_3(X1,X2,X3)!=esk2_3(X1,X2,X3)|esk19_1(X5)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[479,265,theory(equality)])).
% cnf(4040,negated_conjecture,(esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|in(esk19_1(X5),X5)|subset_complement(the_carrier(X1),esk12_7(X1,X2,X3,X4,X4,esk21_1(X5),esk22_1(X5)))!=esk22_1(X5)|esk19_1(X5)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[480,265,theory(equality)])).
% cnf(4070,negated_conjecture,(esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|in(esk19_1(X5),X5)|subset_complement(the_carrier(X1),esk12_7(X1,X2,X3,X4,X4,esk21_1(X5),esk22_1(X5)))!=esk22_1(X5)|esk19_1(X5)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[481,265,theory(equality)])).
% cnf(5280,negated_conjecture,(esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|esk12_7(X1,X2,X3,X4,X4,esk21_1(X5),esk22_1(X5))=esk21_1(X5)|in(X4,esk8_3(X1,X2,X3))|in(esk19_1(X5),X5)|esk19_1(X5)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[513,265,theory(equality)])).
% cnf(5289,negated_conjecture,(esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|esk12_7(X1,X2,X3,X4,X4,esk21_1(X5),esk22_1(X5))=esk21_1(X5)|in(X4,esk8_3(X1,X2,X3))|in(esk19_1(X5),X5)|esk19_1(X5)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[514,265,theory(equality)])).
% cnf(5487,negated_conjecture,(in(esk19_1(X1),esk8_3(X2,X3,X4))|in(esk19_1(X1),X1)|subset_complement(the_carrier(X2),esk12_7(X2,X3,X4,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)))!=esk22_1(X1)|esk3_3(X2,X3,X4)!=esk2_3(X2,X3,X4)|~one_sorted_str(X2)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(X2),X3),X4))|~in(esk21_1(X1),complements_of_subsets(the_carrier(X2),X3))|~element(X3,powerset(powerset(the_carrier(X2))))),inference(er,[status(thm)],[1618,theory(equality)])).
% cnf(6244,negated_conjecture,(esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|element(esk12_7(X1,X2,X3,X4,X4,esk21_1(X5),esk22_1(X5)),powerset(the_carrier(X1)))|in(esk19_1(X5),X5)|esk19_1(X5)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[518,265,theory(equality)])).
% cnf(6549,negated_conjecture,(esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(X4,esk8_3(X1,X2,X3))|element(esk12_7(X1,X2,X3,X4,X4,esk21_1(X5),esk22_1(X5)),powerset(the_carrier(X1)))|in(esk19_1(X5),X5)|esk19_1(X5)!=X4|~one_sorted_str(X1)|~in(X4,cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(spm,[status(thm)],[519,265,theory(equality)])).
% cnf(6557,negated_conjecture,(in(X1,esk8_3(X2,X3,X4))|element(esk12_7(X2,X3,X4,X1,X1,esk21_1(X5),esk22_1(X5)),powerset(the_carrier(X2)))|in(esk19_1(X5),X5)|esk3_3(X2,X3,X4)!=esk2_3(X2,X3,X4)|esk19_1(X5)!=X1|~one_sorted_str(X2)|~in(X1,cartesian_product2(complements_of_subsets(the_carrier(X2),X3),X4))|~in(esk21_1(X5),complements_of_subsets(the_carrier(X2),X3))|~element(X3,powerset(powerset(the_carrier(X2))))),inference(spm,[status(thm)],[524,265,theory(equality)])).
% cnf(6572,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,X2))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X2,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)))!=esk22_1(X1)|esk3_3(esk16_0,esk17_0,X2)!=esk2_3(esk16_0,esk17_0,X2)|~one_sorted_str(esk16_0)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X2))|~in(esk21_1(X1),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[5487,258,theory(equality)])).
% cnf(6608,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,X2))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X2,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)))!=esk22_1(X1)|esk3_3(esk16_0,esk17_0,X2)!=esk2_3(esk16_0,esk17_0,X2)|$false|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X2))|~in(esk21_1(X1),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[6572,259,theory(equality)])).
% cnf(6609,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,X2))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X2,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)))!=esk22_1(X1)|esk3_3(esk16_0,esk17_0,X2)!=esk2_3(esk16_0,esk17_0,X2)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X2))|~in(esk21_1(X1),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[6608,theory(equality)])).
% cnf(6693,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,X2))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X2,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)))!=esk22_1(X1)|esk3_3(esk16_0,esk17_0,X2)!=esk2_3(esk16_0,esk17_0,X2)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X2))),inference(csr,[status(thm)],[6609,264])).
% cnf(7045,negated_conjecture,(esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|in(esk19_1(X4),esk8_3(X1,X2,X3))|in(esk19_1(X4),X4)|subset_complement(the_carrier(X1),esk12_7(X1,X2,X3,esk19_1(X4),esk19_1(X4),esk21_1(X4),esk22_1(X4)))!=esk22_1(X4)|~one_sorted_str(X1)|~in(esk19_1(X4),cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X4),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[4040,theory(equality)])).
% cnf(7046,negated_conjecture,(esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(esk19_1(X4),esk8_3(X1,X2,X3))|in(esk19_1(X4),X4)|subset_complement(the_carrier(X1),esk12_7(X1,X2,X3,esk19_1(X4),esk19_1(X4),esk21_1(X4),esk22_1(X4)))!=esk22_1(X4)|~one_sorted_str(X1)|~in(esk19_1(X4),cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X4),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[4070,theory(equality)])).
% cnf(8141,negated_conjecture,(esk12_7(X1,X2,X3,esk19_1(X4),esk19_1(X4),esk21_1(X4),esk22_1(X4))=esk21_1(X4)|in(esk19_1(X4),esk8_3(X1,X2,X3))|in(esk19_1(X4),X4)|esk3_3(X1,X2,X3)!=esk2_3(X1,X2,X3)|~one_sorted_str(X1)|~in(esk19_1(X4),cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X4),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[4013,theory(equality)])).
% cnf(8142,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)))!=esk22_1(X2)|~one_sorted_str(esk16_0)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[7045,258,theory(equality)])).
% cnf(8184,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)))!=esk22_1(X2)|$false|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[8142,259,theory(equality)])).
% cnf(8185,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)))!=esk22_1(X2)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[8184,theory(equality)])).
% cnf(8279,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)))!=esk22_1(X2)|~one_sorted_str(esk16_0)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[7046,258,theory(equality)])).
% cnf(8321,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)))!=esk22_1(X2)|$false|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[8279,259,theory(equality)])).
% cnf(8322,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)))!=esk22_1(X2)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[8321,theory(equality)])).
% cnf(8475,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)))!=esk22_1(X2)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))),inference(csr,[status(thm)],[8185,264])).
% cnf(8480,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)))!=esk22_1(X2)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))),inference(csr,[status(thm)],[8322,264])).
% cnf(8483,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)))!=esk22_1(X1)),inference(spm,[status(thm)],[8480,263,theory(equality)])).
% cnf(11050,negated_conjecture,(in(esk19_1(X1),esk8_3(X2,X3,X4))|in(esk19_1(X1),X1)|element(esk12_7(X2,X3,X4,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(X2)))|esk3_3(X2,X3,X4)!=esk2_3(X2,X3,X4)|~one_sorted_str(X2)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(X2),X3),X4))|~in(esk21_1(X1),complements_of_subsets(the_carrier(X2),X3))|~element(X3,powerset(powerset(the_carrier(X2))))),inference(er,[status(thm)],[6557,theory(equality)])).
% cnf(11403,negated_conjecture,(esk12_7(X1,X2,X3,esk19_1(X4),esk19_1(X4),esk21_1(X4),esk22_1(X4))=esk21_1(X4)|esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|in(esk19_1(X4),esk8_3(X1,X2,X3))|in(esk19_1(X4),X4)|~one_sorted_str(X1)|~in(esk19_1(X4),cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X4),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[5280,theory(equality)])).
% cnf(11404,negated_conjecture,(esk12_7(X1,X2,X3,esk19_1(X4),esk19_1(X4),esk21_1(X4),esk22_1(X4))=esk21_1(X4)|esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(esk19_1(X4),esk8_3(X1,X2,X3))|in(esk19_1(X4),X4)|~one_sorted_str(X1)|~in(esk19_1(X4),cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X4),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[5289,theory(equality)])).
% cnf(11419,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|~one_sorted_str(esk16_0)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[8141,258,theory(equality)])).
% cnf(11468,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|$false|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[11419,259,theory(equality)])).
% cnf(11469,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[11468,theory(equality)])).
% cnf(11582,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|esk3_3(esk16_0,esk17_0,X1)!=esk2_3(esk16_0,esk17_0,X1)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))),inference(csr,[status(thm)],[11469,264])).
% cnf(14691,negated_conjecture,(esk1_3(X1,X2,X3)=esk2_3(X1,X2,X3)|in(esk19_1(X4),esk8_3(X1,X2,X3))|in(esk19_1(X4),X4)|element(esk12_7(X1,X2,X3,esk19_1(X4),esk19_1(X4),esk21_1(X4),esk22_1(X4)),powerset(the_carrier(X1)))|~one_sorted_str(X1)|~in(esk19_1(X4),cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X4),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[6244,theory(equality)])).
% cnf(15160,negated_conjecture,(esk1_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(esk19_1(X4),esk8_3(X1,X2,X3))|in(esk19_1(X4),X4)|element(esk12_7(X1,X2,X3,esk19_1(X4),esk19_1(X4),esk21_1(X4),esk22_1(X4)),powerset(the_carrier(X1)))|~one_sorted_str(X1)|~in(esk19_1(X4),cartesian_product2(complements_of_subsets(the_carrier(X1),X2),X3))|~in(esk21_1(X4),complements_of_subsets(the_carrier(X1),X2))|~element(X2,powerset(powerset(the_carrier(X1))))),inference(er,[status(thm)],[6549,theory(equality)])).
% cnf(15547,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,X2))|in(esk19_1(X1),X1)|element(esk12_7(esk16_0,esk17_0,X2,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(esk16_0)))|esk3_3(esk16_0,esk17_0,X2)!=esk2_3(esk16_0,esk17_0,X2)|~one_sorted_str(esk16_0)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X2))|~in(esk21_1(X1),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[11050,258,theory(equality)])).
% cnf(15604,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,X2))|in(esk19_1(X1),X1)|element(esk12_7(esk16_0,esk17_0,X2,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(esk16_0)))|esk3_3(esk16_0,esk17_0,X2)!=esk2_3(esk16_0,esk17_0,X2)|$false|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X2))|~in(esk21_1(X1),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[15547,259,theory(equality)])).
% cnf(15605,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,X2))|in(esk19_1(X1),X1)|element(esk12_7(esk16_0,esk17_0,X2,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(esk16_0)))|esk3_3(esk16_0,esk17_0,X2)!=esk2_3(esk16_0,esk17_0,X2)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X2))|~in(esk21_1(X1),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[15604,theory(equality)])).
% cnf(15840,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|~one_sorted_str(esk16_0)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[11403,258,theory(equality)])).
% cnf(15897,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|$false|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[15840,259,theory(equality)])).
% cnf(15898,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[15897,theory(equality)])).
% cnf(16033,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|~one_sorted_str(esk16_0)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[11404,258,theory(equality)])).
% cnf(16090,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|$false|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[16033,259,theory(equality)])).
% cnf(16091,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[16090,theory(equality)])).
% cnf(17126,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,X2))|in(esk19_1(X1),X1)|element(esk12_7(esk16_0,esk17_0,X2,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(esk16_0)))|esk3_3(esk16_0,esk17_0,X2)!=esk2_3(esk16_0,esk17_0,X2)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X2))),inference(csr,[status(thm)],[15605,264])).
% cnf(17671,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[2710,1550,theory(equality)])).
% cnf(17675,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(ef,[status(thm)],[17671,theory(equality)])).
% cnf(17692,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk21_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk22_1(esk8_3(esk16_0,esk17_0,esk18_0))))!=esk22_1(esk8_3(esk16_0,esk17_0,esk18_0))),inference(spm,[status(thm)],[8475,17675,theory(equality)])).
% cnf(17723,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|in(esk19_1(esk8_3(esk16_0,esk17_0,X1)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[3117,1601,theory(equality)])).
% cnf(17725,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(ef,[status(thm)],[17723,theory(equality)])).
% cnf(19839,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))),inference(csr,[status(thm)],[15898,264])).
% cnf(19843,negated_conjecture,(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk21_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk22_1(esk8_3(esk16_0,esk17_0,esk18_0)))=esk21_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(spm,[status(thm)],[19839,17675,theory(equality)])).
% cnf(19848,negated_conjecture,(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1))=esk21_1(X1)|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)),inference(spm,[status(thm)],[19839,263,theory(equality)])).
% cnf(19850,negated_conjecture,(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2))=esk21_1(X2)|esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))),inference(csr,[status(thm)],[16091,264])).
% cnf(19859,negated_conjecture,(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1))=esk21_1(X1)|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)),inference(spm,[status(thm)],[19850,263,theory(equality)])).
% cnf(19872,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk21_1(X1))!=esk22_1(X1)),inference(spm,[status(thm)],[8483,19859,theory(equality)])).
% cnf(19934,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))|subset_complement(the_carrier(esk16_0),esk21_1(esk8_3(esk16_0,esk17_0,esk18_0)))!=esk22_1(esk8_3(esk16_0,esk17_0,esk18_0))),inference(spm,[status(thm)],[17692,19848,theory(equality)])).
% cnf(20667,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|element(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)),powerset(the_carrier(esk16_0)))|~one_sorted_str(esk16_0)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[14691,258,theory(equality)])).
% cnf(20731,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|element(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)),powerset(the_carrier(esk16_0)))|$false|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[20667,259,theory(equality)])).
% cnf(20732,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|element(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)),powerset(the_carrier(esk16_0)))|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[20731,theory(equality)])).
% cnf(20884,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|element(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)),powerset(the_carrier(esk16_0)))|~one_sorted_str(esk16_0)|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[15160,258,theory(equality)])).
% cnf(20948,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|element(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)),powerset(the_carrier(esk16_0)))|$false|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[20884,259,theory(equality)])).
% cnf(20949,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|element(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)),powerset(the_carrier(esk16_0)))|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))|~in(esk21_1(X2),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[20948,theory(equality)])).
% cnf(24904,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk2_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|element(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)),powerset(the_carrier(esk16_0)))|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))),inference(csr,[status(thm)],[20732,264])).
% cnf(24925,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|element(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(esk16_0)))),inference(spm,[status(thm)],[24904,263,theory(equality)])).
% cnf(24927,negated_conjecture,(esk1_3(esk16_0,esk17_0,X1)=esk3_3(esk16_0,esk17_0,X1)|in(esk19_1(X2),esk8_3(esk16_0,esk17_0,X1))|in(esk19_1(X2),X2)|element(esk12_7(esk16_0,esk17_0,X1,esk19_1(X2),esk19_1(X2),esk21_1(X2),esk22_1(X2)),powerset(the_carrier(esk16_0)))|~in(esk19_1(X2),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),X1))),inference(csr,[status(thm)],[20949,264])).
% cnf(24948,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|element(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(esk16_0)))),inference(spm,[status(thm)],[24927,263,theory(equality)])).
% cnf(24992,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))|element(esk21_1(esk8_3(esk16_0,esk17_0,esk18_0)),powerset(the_carrier(esk16_0)))),inference(spm,[status(thm)],[24925,19843,theory(equality)])).
% cnf(25026,negated_conjecture,(esk22_1(esk8_3(esk16_0,esk17_0,esk18_0))=subset_complement(the_carrier(esk16_0),esk21_1(esk8_3(esk16_0,esk17_0,esk18_0)))|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)),inference(spm,[status(thm)],[383,24992,theory(equality)])).
% cnf(25027,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(csr,[status(thm)],[25026,19934])).
% cnf(25034,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|~one_sorted_str(esk16_0)|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(spm,[status(thm)],[90,25027,theory(equality)])).
% cnf(25042,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|~one_sorted_str(esk16_0)|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(spm,[status(thm)],[485,25027,theory(equality)])).
% cnf(25052,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[404,25027,theory(equality)])).
% cnf(25089,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|$false|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(rw,[status(thm)],[25034,259,theory(equality)])).
% cnf(25090,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|$false|$false),inference(rw,[status(thm)],[25089,258,theory(equality)])).
% cnf(25091,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)),inference(cn,[status(thm)],[25090,theory(equality)])).
% cnf(25113,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|$false|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(rw,[status(thm)],[25042,259,theory(equality)])).
% cnf(25114,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|$false|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|$false),inference(rw,[status(thm)],[25113,258,theory(equality)])).
% cnf(25115,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))),inference(cn,[status(thm)],[25114,theory(equality)])).
% cnf(25712,negated_conjecture,(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[261,25091,theory(equality)])).
% cnf(25713,negated_conjecture,(element(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[262,25091,theory(equality)])).
% cnf(25714,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[260,25091,theory(equality)])).
% cnf(25784,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(csr,[status(thm)],[25714,25052])).
% cnf(25785,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[25784,theory(equality)])).
% cnf(25786,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(csr,[status(thm)],[25785,25027])).
% cnf(25787,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),inference(csr,[status(thm)],[25786,17675])).
% cnf(26433,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|element(esk21_1(X1),powerset(the_carrier(esk16_0)))),inference(spm,[status(thm)],[24948,19859,theory(equality)])).
% cnf(26469,negated_conjecture,(esk22_1(X1)=subset_complement(the_carrier(esk16_0),esk21_1(X1))|in(esk19_1(X1),X1)|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))),inference(spm,[status(thm)],[383,26433,theory(equality)])).
% cnf(26470,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)),inference(csr,[status(thm)],[26469,19872])).
% cnf(26471,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(ef,[status(thm)],[26470,theory(equality)])).
% cnf(26853,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|~one_sorted_str(esk16_0)|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(spm,[status(thm)],[89,26471,theory(equality)])).
% cnf(26861,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|~one_sorted_str(esk16_0)|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(spm,[status(thm)],[520,26471,theory(equality)])).
% cnf(26871,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(spm,[status(thm)],[410,26471,theory(equality)])).
% cnf(26910,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|$false|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(rw,[status(thm)],[26853,259,theory(equality)])).
% cnf(26911,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|$false|$false),inference(rw,[status(thm)],[26910,258,theory(equality)])).
% cnf(26912,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)),inference(cn,[status(thm)],[26911,theory(equality)])).
% cnf(26934,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|$false|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(rw,[status(thm)],[26861,259,theory(equality)])).
% cnf(26935,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|$false|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|$false),inference(rw,[status(thm)],[26934,258,theory(equality)])).
% cnf(26936,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))),inference(cn,[status(thm)],[26935,theory(equality)])).
% cnf(27361,negated_conjecture,(element(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[262,26912,theory(equality)])).
% cnf(27362,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[260,26912,theory(equality)])).
% cnf(27401,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(csr,[status(thm)],[27362,26871])).
% cnf(27402,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[27401,theory(equality)])).
% cnf(27403,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(csr,[status(thm)],[27402,26471])).
% cnf(27404,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),inference(csr,[status(thm)],[27403,17725])).
% cnf(98425,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(csr,[status(thm)],[25713,25052])).
% cnf(98426,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[98425,theory(equality)])).
% cnf(98427,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(csr,[status(thm)],[98426,25027])).
% cnf(98428,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))),inference(csr,[status(thm)],[98427,17675])).
% cnf(98523,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(csr,[status(thm)],[27361,26871])).
% cnf(98524,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[98523,theory(equality)])).
% cnf(98525,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(csr,[status(thm)],[98524,26471])).
% cnf(98526,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))),inference(csr,[status(thm)],[98525,17725])).
% cnf(106872,negated_conjecture,(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(csr,[status(thm)],[25712,25052])).
% cnf(106873,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[106872,theory(equality)])).
% cnf(106874,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(csr,[status(thm)],[106873,25027])).
% cnf(106875,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)),inference(csr,[status(thm)],[106874,17675])).
% cnf(106876,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),inference(spm,[status(thm)],[25787,106875,theory(equality)])).
% cnf(106884,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))),inference(spm,[status(thm)],[98428,106875,theory(equality)])).
% cnf(106951,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)),inference(spm,[status(thm)],[25115,106884,theory(equality)])).
% cnf(106963,negated_conjecture,(esk1_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)),inference(csr,[status(thm)],[106951,106876])).
% cnf(107290,negated_conjecture,(esk2_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))),inference(rw,[status(thm)],[98526,106963,theory(equality)])).
% cnf(107579,negated_conjecture,(esk2_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),inference(rw,[status(thm)],[27404,106963,theory(equality)])).
% cnf(107582,negated_conjecture,(esk2_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(rw,[status(thm)],[26871,106963,theory(equality)])).
% cnf(107583,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk2_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))),inference(rw,[status(thm)],[26936,106963,theory(equality)])).
% cnf(107586,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk2_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)),inference(rw,[status(thm)],[26912,106963,theory(equality)])).
% cnf(107661,negated_conjecture,(esk2_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(rw,[status(thm)],[26471,106963,theory(equality)])).
% cnf(107807,negated_conjecture,(esk2_3(esk16_0,esk17_0,esk18_0)=esk3_3(esk16_0,esk17_0,esk18_0)|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(rw,[status(thm)],[17725,106963,theory(equality)])).
% cnf(109338,negated_conjecture,(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[261,107586,theory(equality)])).
% cnf(126469,negated_conjecture,(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(csr,[status(thm)],[109338,107582])).
% cnf(126470,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[126469,theory(equality)])).
% cnf(126471,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(csr,[status(thm)],[126470,107661])).
% cnf(126472,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)),inference(csr,[status(thm)],[126471,107807])).
% cnf(126473,negated_conjecture,(esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),inference(spm,[status(thm)],[107579,126472,theory(equality)])).
% cnf(126478,negated_conjecture,(esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)|element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))),inference(spm,[status(thm)],[107290,126472,theory(equality)])).
% cnf(126531,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)),inference(spm,[status(thm)],[107583,126478,theory(equality)])).
% cnf(126547,negated_conjecture,(esk3_3(esk16_0,esk17_0,esk18_0)=esk2_3(esk16_0,esk17_0,esk18_0)),inference(csr,[status(thm)],[126531,126473])).
% cnf(126548,negated_conjecture,(esk9_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[1370,126547,theory(equality)])).
% cnf(126551,negated_conjecture,(in(esk9_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[3685,126547,theory(equality)])).
% cnf(126553,negated_conjecture,(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1))=esk21_1(X1)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[11582,126547,theory(equality)])).
% cnf(126578,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)))!=esk22_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[6693,126547,theory(equality)])).
% cnf(126579,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|element(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(esk16_0)))|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[17126,126547,theory(equality)])).
% cnf(128345,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)))!=esk22_1(X1)),inference(csr,[status(thm)],[126578,263])).
% cnf(128750,negated_conjecture,(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1))=esk21_1(X1)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)),inference(csr,[status(thm)],[126553,263])).
% cnf(128751,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|subset_complement(the_carrier(esk16_0),esk21_1(X1))!=esk22_1(X1)),inference(spm,[status(thm)],[128345,128750,theory(equality)])).
% cnf(128850,negated_conjecture,(in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))),inference(spm,[status(thm)],[126551,126548,theory(equality)])).
% cnf(128983,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|element(esk12_7(esk16_0,esk17_0,esk18_0,esk19_1(X1),esk19_1(X1),esk21_1(X1),esk22_1(X1)),powerset(the_carrier(esk16_0)))),inference(csr,[status(thm)],[126579,263])).
% cnf(129016,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)|element(esk21_1(X1),powerset(the_carrier(esk16_0)))),inference(spm,[status(thm)],[128983,128750,theory(equality)])).
% cnf(129049,negated_conjecture,(esk22_1(X1)=subset_complement(the_carrier(esk16_0),esk21_1(X1))|in(esk19_1(X1),X1)|in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))),inference(spm,[status(thm)],[383,129016,theory(equality)])).
% cnf(129056,negated_conjecture,(in(esk19_1(X1),esk8_3(esk16_0,esk17_0,esk18_0))|in(esk19_1(X1),X1)),inference(csr,[status(thm)],[129049,128751])).
% cnf(129057,negated_conjecture,(in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(ef,[status(thm)],[129056,theory(equality)])).
% cnf(129767,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|esk3_3(esk16_0,esk17_0,esk18_0)!=esk2_3(esk16_0,esk17_0,esk18_0)|~one_sorted_str(esk16_0)|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(spm,[status(thm)],[88,129057,theory(equality)])).
% cnf(129771,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|esk3_3(esk16_0,esk17_0,esk18_0)!=esk2_3(esk16_0,esk17_0,esk18_0)|~one_sorted_str(esk16_0)|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(spm,[status(thm)],[478,129057,theory(equality)])).
% cnf(129785,negated_conjecture,(in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|esk3_3(esk16_0,esk17_0,esk18_0)!=esk2_3(esk16_0,esk17_0,esk18_0)),inference(spm,[status(thm)],[416,129057,theory(equality)])).
% cnf(129834,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|$false|~one_sorted_str(esk16_0)|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(rw,[status(thm)],[129767,126547,theory(equality)])).
% cnf(129835,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|$false|$false|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(rw,[status(thm)],[129834,259,theory(equality)])).
% cnf(129836,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))|$false|$false|$false),inference(rw,[status(thm)],[129835,258,theory(equality)])).
% cnf(129837,negated_conjecture,(ordered_pair(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),inference(cn,[status(thm)],[129836,theory(equality)])).
% cnf(129848,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|$false|~one_sorted_str(esk16_0)|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(rw,[status(thm)],[129771,126547,theory(equality)])).
% cnf(129849,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|$false|$false|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|~element(esk17_0,powerset(powerset(the_carrier(esk16_0))))),inference(rw,[status(thm)],[129848,259,theory(equality)])).
% cnf(129850,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|$false|$false|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))|$false),inference(rw,[status(thm)],[129849,258,theory(equality)])).
% cnf(129851,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|~element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))),inference(cn,[status(thm)],[129850,theory(equality)])).
% cnf(129886,negated_conjecture,(in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|$false),inference(rw,[status(thm)],[129785,126547,theory(equality)])).
% cnf(129887,negated_conjecture,(in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))),inference(cn,[status(thm)],[129886,theory(equality)])).
% cnf(131101,negated_conjecture,(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[261,129837,theory(equality)])).
% cnf(131102,negated_conjecture,(element(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[262,129837,theory(equality)])).
% cnf(131103,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),complements_of_subsets(the_carrier(esk16_0),esk17_0))|~in(esk19_1(X1),X1)),inference(spm,[status(thm)],[260,129837,theory(equality)])).
% cnf(131131,negated_conjecture,(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|$false|~in(esk19_1(X1),X1)),inference(rw,[status(thm)],[131101,129887,theory(equality)])).
% cnf(131132,negated_conjecture,(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(cn,[status(thm)],[131131,theory(equality)])).
% cnf(131133,negated_conjecture,(element(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|$false|~in(esk19_1(X1),X1)),inference(rw,[status(thm)],[131102,129887,theory(equality)])).
% cnf(131134,negated_conjecture,(element(esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(cn,[status(thm)],[131133,theory(equality)])).
% cnf(131135,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|$false|~in(esk19_1(X1),X1)),inference(rw,[status(thm)],[131103,129887,theory(equality)])).
% cnf(131136,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk20_3(X1,esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))!=esk19_1(X1)|~in(esk19_1(X1),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(X1),X1)),inference(cn,[status(thm)],[131135,theory(equality)])).
% cnf(131143,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[131136,theory(equality)])).
% cnf(131144,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|$false|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(rw,[status(thm)],[131143,128850,theory(equality)])).
% cnf(131145,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|$false|$false),inference(rw,[status(thm)],[131144,129057,theory(equality)])).
% cnf(131146,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),inference(cn,[status(thm)],[131145,theory(equality)])).
% cnf(136549,negated_conjecture,(element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[131134,theory(equality)])).
% cnf(136550,negated_conjecture,(element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|$false|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(rw,[status(thm)],[136549,128850,theory(equality)])).
% cnf(136551,negated_conjecture,(element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))|$false|$false),inference(rw,[status(thm)],[136550,129057,theory(equality)])).
% cnf(136552,negated_conjecture,(element(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),powerset(the_carrier(esk16_0)))),inference(cn,[status(thm)],[136551,theory(equality)])).
% cnf(137950,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),cartesian_product2(complements_of_subsets(the_carrier(esk16_0),esk17_0),esk18_0))|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(er,[status(thm)],[131132,theory(equality)])).
% cnf(137951,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|$false|~in(esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)),esk8_3(esk16_0,esk17_0,esk18_0))),inference(rw,[status(thm)],[137950,128850,theory(equality)])).
% cnf(137952,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))|$false|$false),inference(rw,[status(thm)],[137951,129057,theory(equality)])).
% cnf(137953,negated_conjecture,(esk20_3(esk8_3(esk16_0,esk17_0,esk18_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))=esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),inference(cn,[status(thm)],[137952,theory(equality)])).
% cnf(138001,negated_conjecture,(element(esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))),powerset(the_carrier(esk16_0)))),inference(rw,[status(thm)],[136552,137953,theory(equality)])).
% cnf(138016,negated_conjecture,(subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))!=esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))),inference(rw,[status(thm)],[131146,137953,theory(equality)])).
% cnf(138084,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))|$false),inference(rw,[status(thm)],[129851,138001,theory(equality)])).
% cnf(138085,negated_conjecture,(esk11_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0)))=subset_complement(the_carrier(esk16_0),esk10_4(esk16_0,esk17_0,esk18_0,esk19_1(esk8_3(esk16_0,esk17_0,esk18_0))))),inference(cn,[status(thm)],[138084,theory(equality)])).
% cnf(138086,negated_conjecture,($false),inference(sr,[status(thm)],[138085,138016,theory(equality)])).
% cnf(138087,negated_conjecture,($false),138086,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 16921
% # ...of these trivial : 82
% # ...subsumed : 10584
% # ...remaining for further processing: 6255
% # Other redundant clauses eliminated : 27
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 489
% # Backward-rewritten : 1510
% # Generated clauses : 65088
% # ...of the previous two non-trivial : 64789
% # Contextual simplify-reflections : 9084
% # Paramodulations : 64701
% # Factorizations : 32
% # Equation resolutions : 355
% # Current number of processed clauses: 4229
% # Positive orientable unit clauses: 160
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 7
% # Non-unit-clauses : 4062
% # Current number of unprocessed clauses: 14571
% # ...number of literals in the above : 89367
% # Clause-clause subsumption calls (NU) : 1013718
% # Rec. Clause-clause subsumption calls : 660995
% # Unit Clause-clause subsumption calls : 1622
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1579
% # Indexed BW rewrite successes : 9
% # Backwards rewriting index: 744 leaves, 3.51+/-5.152 terms/leaf
% # Paramod-from index: 111 leaves, 3.04+/-4.992 terms/leaf
% # Paramod-into index: 333 leaves, 2.34+/-3.413 terms/leaf
% # -------------------------------------------------
% # User time : 9.332 s
% # System time : 0.138 s
% # Total time : 9.470 s
% # Maximum resident set size: 0 pages
% PrfWatch: 11.97 CPU 12.87 WC
% FINAL PrfWatch: 11.97 CPU 12.87 WC
% SZS output end Solution for /tmp/SystemOnTPTP31074/SEU329+1.tptp
%
%------------------------------------------------------------------------------