%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU297+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 : art02.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:11:27 EST 2010
% Result : Theorem 1.33s
% Output : Solution 1.33s
% 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/SystemOnTPTP16073/SEU297+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP16073/SEU297+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP16073/SEU297+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 16169
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:![X2]:![X3]:(((element(X2,powerset(powerset(X1)))&relation(X3))&function(X3))=>(![X4]:![X5]:![X6]:((((X4=X5&in(relation_image(X3,X5),X2))&X4=X6)&in(relation_image(X3,X6),X2))=>X5=X6)=>?[X4]:![X5]:(in(X5,X4)<=>?[X6]:((in(X6,powerset(relation_dom(X3)))&X6=X5)&in(relation_image(X3,X5),X2))))),file('/tmp/SRASS.s.p', s1_tarski__e6_27__finset_1__1)).
% fof(37, conjecture,![X1]:![X2]:![X3]:(((element(X2,powerset(powerset(X1)))&relation(X3))&function(X3))=>?[X4]:![X5]:(in(X5,X4)<=>(in(X5,powerset(relation_dom(X3)))&in(relation_image(X3,X5),X2)))),file('/tmp/SRASS.s.p', s1_xboole_0__e6_27__finset_1)).
% fof(38, negated_conjecture,~(![X1]:![X2]:![X3]:(((element(X2,powerset(powerset(X1)))&relation(X3))&function(X3))=>?[X4]:![X5]:(in(X5,X4)<=>(in(X5,powerset(relation_dom(X3)))&in(relation_image(X3,X5),X2))))),inference(assume_negation,[status(cth)],[37])).
% fof(56, plain,![X1]:![X2]:![X3]:(((~(element(X2,powerset(powerset(X1))))|~(relation(X3)))|~(function(X3)))|(?[X4]:?[X5]:?[X6]:((((X4=X5&in(relation_image(X3,X5),X2))&X4=X6)&in(relation_image(X3,X6),X2))&~(X5=X6))|?[X4]:![X5]:((~(in(X5,X4))|?[X6]:((in(X6,powerset(relation_dom(X3)))&X6=X5)&in(relation_image(X3,X5),X2)))&(![X6]:((~(in(X6,powerset(relation_dom(X3))))|~(X6=X5))|~(in(relation_image(X3,X5),X2)))|in(X5,X4))))),inference(fof_nnf,[status(thm)],[3])).
% fof(57, plain,![X7]:![X8]:![X9]:(((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))|(?[X10]:?[X11]:?[X12]:((((X10=X11&in(relation_image(X9,X11),X8))&X10=X12)&in(relation_image(X9,X12),X8))&~(X11=X12))|?[X13]:![X14]:((~(in(X14,X13))|?[X15]:((in(X15,powerset(relation_dom(X9)))&X15=X14)&in(relation_image(X9,X14),X8)))&(![X16]:((~(in(X16,powerset(relation_dom(X9))))|~(X16=X14))|~(in(relation_image(X9,X14),X8)))|in(X14,X13))))),inference(variable_rename,[status(thm)],[56])).
% fof(58, plain,![X7]:![X8]:![X9]:(((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))|(((((esk2_3(X7,X8,X9)=esk3_3(X7,X8,X9)&in(relation_image(X9,esk3_3(X7,X8,X9)),X8))&esk2_3(X7,X8,X9)=esk4_3(X7,X8,X9))&in(relation_image(X9,esk4_3(X7,X8,X9)),X8))&~(esk3_3(X7,X8,X9)=esk4_3(X7,X8,X9)))|![X14]:((~(in(X14,esk5_3(X7,X8,X9)))|((in(esk6_4(X7,X8,X9,X14),powerset(relation_dom(X9)))&esk6_4(X7,X8,X9,X14)=X14)&in(relation_image(X9,X14),X8)))&(![X16]:((~(in(X16,powerset(relation_dom(X9))))|~(X16=X14))|~(in(relation_image(X9,X14),X8)))|in(X14,esk5_3(X7,X8,X9)))))),inference(skolemize,[status(esa)],[57])).
% fof(59, plain,![X7]:![X8]:![X9]:![X14]:![X16]:((((((~(in(X16,powerset(relation_dom(X9))))|~(X16=X14))|~(in(relation_image(X9,X14),X8)))|in(X14,esk5_3(X7,X8,X9)))&(~(in(X14,esk5_3(X7,X8,X9)))|((in(esk6_4(X7,X8,X9,X14),powerset(relation_dom(X9)))&esk6_4(X7,X8,X9,X14)=X14)&in(relation_image(X9,X14),X8))))|((((esk2_3(X7,X8,X9)=esk3_3(X7,X8,X9)&in(relation_image(X9,esk3_3(X7,X8,X9)),X8))&esk2_3(X7,X8,X9)=esk4_3(X7,X8,X9))&in(relation_image(X9,esk4_3(X7,X8,X9)),X8))&~(esk3_3(X7,X8,X9)=esk4_3(X7,X8,X9))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))),inference(shift_quantors,[status(thm)],[58])).
% fof(60, plain,![X7]:![X8]:![X9]:![X14]:![X16]:(((((((esk2_3(X7,X8,X9)=esk3_3(X7,X8,X9)|(((~(in(X16,powerset(relation_dom(X9))))|~(X16=X14))|~(in(relation_image(X9,X14),X8)))|in(X14,esk5_3(X7,X8,X9))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9))))&((in(relation_image(X9,esk3_3(X7,X8,X9)),X8)|(((~(in(X16,powerset(relation_dom(X9))))|~(X16=X14))|~(in(relation_image(X9,X14),X8)))|in(X14,esk5_3(X7,X8,X9))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((esk2_3(X7,X8,X9)=esk4_3(X7,X8,X9)|(((~(in(X16,powerset(relation_dom(X9))))|~(X16=X14))|~(in(relation_image(X9,X14),X8)))|in(X14,esk5_3(X7,X8,X9))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((in(relation_image(X9,esk4_3(X7,X8,X9)),X8)|(((~(in(X16,powerset(relation_dom(X9))))|~(X16=X14))|~(in(relation_image(X9,X14),X8)))|in(X14,esk5_3(X7,X8,X9))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((~(esk3_3(X7,X8,X9)=esk4_3(X7,X8,X9))|(((~(in(X16,powerset(relation_dom(X9))))|~(X16=X14))|~(in(relation_image(X9,X14),X8)))|in(X14,esk5_3(X7,X8,X9))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((((((((esk2_3(X7,X8,X9)=esk3_3(X7,X8,X9)|(in(esk6_4(X7,X8,X9,X14),powerset(relation_dom(X9)))|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9))))&((in(relation_image(X9,esk3_3(X7,X8,X9)),X8)|(in(esk6_4(X7,X8,X9,X14),powerset(relation_dom(X9)))|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((esk2_3(X7,X8,X9)=esk4_3(X7,X8,X9)|(in(esk6_4(X7,X8,X9,X14),powerset(relation_dom(X9)))|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((in(relation_image(X9,esk4_3(X7,X8,X9)),X8)|(in(esk6_4(X7,X8,X9,X14),powerset(relation_dom(X9)))|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((~(esk3_3(X7,X8,X9)=esk4_3(X7,X8,X9))|(in(esk6_4(X7,X8,X9,X14),powerset(relation_dom(X9)))|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((((((esk2_3(X7,X8,X9)=esk3_3(X7,X8,X9)|(esk6_4(X7,X8,X9,X14)=X14|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9))))&((in(relation_image(X9,esk3_3(X7,X8,X9)),X8)|(esk6_4(X7,X8,X9,X14)=X14|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((esk2_3(X7,X8,X9)=esk4_3(X7,X8,X9)|(esk6_4(X7,X8,X9,X14)=X14|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((in(relation_image(X9,esk4_3(X7,X8,X9)),X8)|(esk6_4(X7,X8,X9,X14)=X14|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((~(esk3_3(X7,X8,X9)=esk4_3(X7,X8,X9))|(esk6_4(X7,X8,X9,X14)=X14|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9))))))&((((((esk2_3(X7,X8,X9)=esk3_3(X7,X8,X9)|(in(relation_image(X9,X14),X8)|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9))))&((in(relation_image(X9,esk3_3(X7,X8,X9)),X8)|(in(relation_image(X9,X14),X8)|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((esk2_3(X7,X8,X9)=esk4_3(X7,X8,X9)|(in(relation_image(X9,X14),X8)|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((in(relation_image(X9,esk4_3(X7,X8,X9)),X8)|(in(relation_image(X9,X14),X8)|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9)))))&((~(esk3_3(X7,X8,X9)=esk4_3(X7,X8,X9))|(in(relation_image(X9,X14),X8)|~(in(X14,esk5_3(X7,X8,X9)))))|((~(element(X8,powerset(powerset(X7))))|~(relation(X9)))|~(function(X9))))))),inference(distribute,[status(thm)],[59])).
% cnf(61,plain,(in(relation_image(X1,X4),X2)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))|esk3_3(X3,X2,X1)!=esk4_3(X3,X2,X1)),inference(split_conjunct,[status(thm)],[60])).
% cnf(63,plain,(in(relation_image(X1,X4),X2)|esk2_3(X3,X2,X1)=esk4_3(X3,X2,X1)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))),inference(split_conjunct,[status(thm)],[60])).
% cnf(65,plain,(in(relation_image(X1,X4),X2)|esk2_3(X3,X2,X1)=esk3_3(X3,X2,X1)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))),inference(split_conjunct,[status(thm)],[60])).
% cnf(66,plain,(esk6_4(X3,X2,X1,X4)=X4|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))|esk3_3(X3,X2,X1)!=esk4_3(X3,X2,X1)),inference(split_conjunct,[status(thm)],[60])).
% cnf(68,plain,(esk6_4(X3,X2,X1,X4)=X4|esk2_3(X3,X2,X1)=esk4_3(X3,X2,X1)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))),inference(split_conjunct,[status(thm)],[60])).
% cnf(70,plain,(esk6_4(X3,X2,X1,X4)=X4|esk2_3(X3,X2,X1)=esk3_3(X3,X2,X1)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))),inference(split_conjunct,[status(thm)],[60])).
% cnf(71,plain,(in(esk6_4(X3,X2,X1,X4),powerset(relation_dom(X1)))|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))|esk3_3(X3,X2,X1)!=esk4_3(X3,X2,X1)),inference(split_conjunct,[status(thm)],[60])).
% cnf(73,plain,(in(esk6_4(X3,X2,X1,X4),powerset(relation_dom(X1)))|esk2_3(X3,X2,X1)=esk4_3(X3,X2,X1)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))),inference(split_conjunct,[status(thm)],[60])).
% cnf(75,plain,(in(esk6_4(X3,X2,X1,X4),powerset(relation_dom(X1)))|esk2_3(X3,X2,X1)=esk3_3(X3,X2,X1)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(X4,esk5_3(X3,X2,X1))),inference(split_conjunct,[status(thm)],[60])).
% cnf(76,plain,(in(X4,esk5_3(X3,X2,X1))|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(relation_image(X1,X4),X2)|X5!=X4|~in(X5,powerset(relation_dom(X1)))|esk3_3(X3,X2,X1)!=esk4_3(X3,X2,X1)),inference(split_conjunct,[status(thm)],[60])).
% cnf(78,plain,(in(X4,esk5_3(X3,X2,X1))|esk2_3(X3,X2,X1)=esk4_3(X3,X2,X1)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(relation_image(X1,X4),X2)|X5!=X4|~in(X5,powerset(relation_dom(X1)))),inference(split_conjunct,[status(thm)],[60])).
% cnf(80,plain,(in(X4,esk5_3(X3,X2,X1))|esk2_3(X3,X2,X1)=esk3_3(X3,X2,X1)|~function(X1)|~relation(X1)|~element(X2,powerset(powerset(X3)))|~in(relation_image(X1,X4),X2)|X5!=X4|~in(X5,powerset(relation_dom(X1)))),inference(split_conjunct,[status(thm)],[60])).
% fof(229, negated_conjecture,?[X1]:?[X2]:?[X3]:(((element(X2,powerset(powerset(X1)))&relation(X3))&function(X3))&![X4]:?[X5]:((~(in(X5,X4))|(~(in(X5,powerset(relation_dom(X3))))|~(in(relation_image(X3,X5),X2))))&(in(X5,X4)|(in(X5,powerset(relation_dom(X3)))&in(relation_image(X3,X5),X2))))),inference(fof_nnf,[status(thm)],[38])).
% fof(230, negated_conjecture,?[X6]:?[X7]:?[X8]:(((element(X7,powerset(powerset(X6)))&relation(X8))&function(X8))&![X9]:?[X10]:((~(in(X10,X9))|(~(in(X10,powerset(relation_dom(X8))))|~(in(relation_image(X8,X10),X7))))&(in(X10,X9)|(in(X10,powerset(relation_dom(X8)))&in(relation_image(X8,X10),X7))))),inference(variable_rename,[status(thm)],[229])).
% fof(231, negated_conjecture,(((element(esk23_0,powerset(powerset(esk22_0)))&relation(esk24_0))&function(esk24_0))&![X9]:((~(in(esk25_1(X9),X9))|(~(in(esk25_1(X9),powerset(relation_dom(esk24_0))))|~(in(relation_image(esk24_0,esk25_1(X9)),esk23_0))))&(in(esk25_1(X9),X9)|(in(esk25_1(X9),powerset(relation_dom(esk24_0)))&in(relation_image(esk24_0,esk25_1(X9)),esk23_0))))),inference(skolemize,[status(esa)],[230])).
% fof(232, negated_conjecture,![X9]:(((~(in(esk25_1(X9),X9))|(~(in(esk25_1(X9),powerset(relation_dom(esk24_0))))|~(in(relation_image(esk24_0,esk25_1(X9)),esk23_0))))&(in(esk25_1(X9),X9)|(in(esk25_1(X9),powerset(relation_dom(esk24_0)))&in(relation_image(esk24_0,esk25_1(X9)),esk23_0))))&((element(esk23_0,powerset(powerset(esk22_0)))&relation(esk24_0))&function(esk24_0))),inference(shift_quantors,[status(thm)],[231])).
% fof(233, negated_conjecture,![X9]:(((~(in(esk25_1(X9),X9))|(~(in(esk25_1(X9),powerset(relation_dom(esk24_0))))|~(in(relation_image(esk24_0,esk25_1(X9)),esk23_0))))&((in(esk25_1(X9),powerset(relation_dom(esk24_0)))|in(esk25_1(X9),X9))&(in(relation_image(esk24_0,esk25_1(X9)),esk23_0)|in(esk25_1(X9),X9))))&((element(esk23_0,powerset(powerset(esk22_0)))&relation(esk24_0))&function(esk24_0))),inference(distribute,[status(thm)],[232])).
% cnf(234,negated_conjecture,(function(esk24_0)),inference(split_conjunct,[status(thm)],[233])).
% cnf(235,negated_conjecture,(relation(esk24_0)),inference(split_conjunct,[status(thm)],[233])).
% cnf(236,negated_conjecture,(element(esk23_0,powerset(powerset(esk22_0)))),inference(split_conjunct,[status(thm)],[233])).
% cnf(237,negated_conjecture,(in(esk25_1(X1),X1)|in(relation_image(esk24_0,esk25_1(X1)),esk23_0)),inference(split_conjunct,[status(thm)],[233])).
% cnf(238,negated_conjecture,(in(esk25_1(X1),X1)|in(esk25_1(X1),powerset(relation_dom(esk24_0)))),inference(split_conjunct,[status(thm)],[233])).
% cnf(239,negated_conjecture,(~in(relation_image(esk24_0,esk25_1(X1)),esk23_0)|~in(esk25_1(X1),powerset(relation_dom(esk24_0)))|~in(esk25_1(X1),X1)),inference(split_conjunct,[status(thm)],[233])).
% cnf(245,plain,(esk2_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(X4,esk5_3(X1,X2,X3))|~element(X2,powerset(powerset(X1)))|~function(X3)|~relation(X3)|~in(X4,powerset(relation_dom(X3)))|~in(relation_image(X3,X4),X2)),inference(er,[status(thm)],[80,theory(equality)])).
% cnf(246,plain,(in(X1,esk5_3(X2,X3,X4))|esk4_3(X2,X3,X4)!=esk3_3(X2,X3,X4)|~element(X3,powerset(powerset(X2)))|~function(X4)|~relation(X4)|~in(X1,powerset(relation_dom(X4)))|~in(relation_image(X4,X1),X3)),inference(er,[status(thm)],[76,theory(equality)])).
% cnf(249,plain,(esk2_3(X1,X2,X3)=esk4_3(X1,X2,X3)|in(X4,esk5_3(X1,X2,X3))|~element(X2,powerset(powerset(X1)))|~function(X3)|~relation(X3)|~in(X4,powerset(relation_dom(X3)))|~in(relation_image(X3,X4),X2)),inference(er,[status(thm)],[78,theory(equality)])).
% cnf(306,negated_conjecture,(in(relation_image(X1,esk25_1(esk5_3(X2,X3,X1))),X3)|in(relation_image(esk24_0,esk25_1(esk5_3(X2,X3,X1))),esk23_0)|esk4_3(X2,X3,X1)!=esk3_3(X2,X3,X1)|~element(X3,powerset(powerset(X2)))|~function(X1)|~relation(X1)),inference(spm,[status(thm)],[61,237,theory(equality)])).
% cnf(310,plain,(in(X4,powerset(relation_dom(X3)))|esk4_3(X1,X2,X3)!=esk3_3(X1,X2,X3)|~element(X2,powerset(powerset(X1)))|~function(X3)|~relation(X3)|~in(X4,esk5_3(X1,X2,X3))),inference(spm,[status(thm)],[71,66,theory(equality)])).
% cnf(314,negated_conjecture,(esk2_3(X1,X2,X3)=esk3_3(X1,X2,X3)|in(relation_image(X3,esk25_1(esk5_3(X1,X2,X3))),X2)|in(relation_image(esk24_0,esk25_1(esk5_3(X1,X2,X3))),esk23_0)|~element(X2,powerset(powerset(X1)))|~function(X3)|~relation(X3)),inference(spm,[status(thm)],[65,237,theory(equality)])).
% cnf(316,negated_conjecture,(esk2_3(X1,X2,X3)=esk4_3(X1,X2,X3)|in(relation_image(X3,esk25_1(esk5_3(X1,X2,X3))),X2)|in(relation_image(esk24_0,esk25_1(esk5_3(X1,X2,X3))),esk23_0)|~element(X2,powerset(powerset(X1)))|~function(X3)|~relation(X3)),inference(spm,[status(thm)],[63,237,theory(equality)])).
% cnf(319,negated_conjecture,(in(esk25_1(X1),esk5_3(X2,X3,esk24_0))|in(esk25_1(X1),X1)|esk4_3(X2,X3,esk24_0)!=esk3_3(X2,X3,esk24_0)|~element(X3,powerset(powerset(X2)))|~function(esk24_0)|~relation(esk24_0)|~in(relation_image(esk24_0,esk25_1(X1)),X3)),inference(spm,[status(thm)],[246,238,theory(equality)])).
% cnf(321,negated_conjecture,(in(esk25_1(X1),esk5_3(X2,X3,esk24_0))|in(esk25_1(X1),X1)|esk4_3(X2,X3,esk24_0)!=esk3_3(X2,X3,esk24_0)|~element(X3,powerset(powerset(X2)))|$false|~relation(esk24_0)|~in(relation_image(esk24_0,esk25_1(X1)),X3)),inference(rw,[status(thm)],[319,234,theory(equality)])).
% cnf(322,negated_conjecture,(in(esk25_1(X1),esk5_3(X2,X3,esk24_0))|in(esk25_1(X1),X1)|esk4_3(X2,X3,esk24_0)!=esk3_3(X2,X3,esk24_0)|~element(X3,powerset(powerset(X2)))|$false|$false|~in(relation_image(esk24_0,esk25_1(X1)),X3)),inference(rw,[status(thm)],[321,235,theory(equality)])).
% cnf(323,negated_conjecture,(in(esk25_1(X1),esk5_3(X2,X3,esk24_0))|in(esk25_1(X1),X1)|esk4_3(X2,X3,esk24_0)!=esk3_3(X2,X3,esk24_0)|~element(X3,powerset(powerset(X2)))|~in(relation_image(esk24_0,esk25_1(X1)),X3)),inference(cn,[status(thm)],[322,theory(equality)])).
% cnf(369,negated_conjecture,(esk2_3(esk22_0,esk23_0,X1)=esk3_3(esk22_0,esk23_0,X1)|esk6_4(esk22_0,esk23_0,X1,X2)=X2|~function(X1)|~relation(X1)|~in(X2,esk5_3(esk22_0,esk23_0,X1))),inference(spm,[status(thm)],[70,236,theory(equality)])).
% cnf(376,negated_conjecture,(esk2_3(esk22_0,esk23_0,X1)=esk4_3(esk22_0,esk23_0,X1)|esk6_4(esk22_0,esk23_0,X1,X2)=X2|~function(X1)|~relation(X1)|~in(X2,esk5_3(esk22_0,esk23_0,X1))),inference(spm,[status(thm)],[68,236,theory(equality)])).
% cnf(385,negated_conjecture,(esk2_3(X1,X2,esk24_0)=esk3_3(X1,X2,esk24_0)|in(esk25_1(X3),esk5_3(X1,X2,esk24_0))|in(esk25_1(X3),X3)|~element(X2,powerset(powerset(X1)))|~function(esk24_0)|~relation(esk24_0)|~in(relation_image(esk24_0,esk25_1(X3)),X2)),inference(spm,[status(thm)],[245,238,theory(equality)])).
% cnf(389,negated_conjecture,(esk2_3(X1,X2,esk24_0)=esk3_3(X1,X2,esk24_0)|in(esk25_1(X3),esk5_3(X1,X2,esk24_0))|in(esk25_1(X3),X3)|~element(X2,powerset(powerset(X1)))|$false|~relation(esk24_0)|~in(relation_image(esk24_0,esk25_1(X3)),X2)),inference(rw,[status(thm)],[385,234,theory(equality)])).
% cnf(390,negated_conjecture,(esk2_3(X1,X2,esk24_0)=esk3_3(X1,X2,esk24_0)|in(esk25_1(X3),esk5_3(X1,X2,esk24_0))|in(esk25_1(X3),X3)|~element(X2,powerset(powerset(X1)))|$false|$false|~in(relation_image(esk24_0,esk25_1(X3)),X2)),inference(rw,[status(thm)],[389,235,theory(equality)])).
% cnf(391,negated_conjecture,(esk2_3(X1,X2,esk24_0)=esk3_3(X1,X2,esk24_0)|in(esk25_1(X3),esk5_3(X1,X2,esk24_0))|in(esk25_1(X3),X3)|~element(X2,powerset(powerset(X1)))|~in(relation_image(esk24_0,esk25_1(X3)),X2)),inference(cn,[status(thm)],[390,theory(equality)])).
% cnf(394,negated_conjecture,(esk2_3(X1,X2,esk24_0)=esk4_3(X1,X2,esk24_0)|in(esk25_1(X3),esk5_3(X1,X2,esk24_0))|in(esk25_1(X3),X3)|~element(X2,powerset(powerset(X1)))|~function(esk24_0)|~relation(esk24_0)|~in(relation_image(esk24_0,esk25_1(X3)),X2)),inference(spm,[status(thm)],[249,238,theory(equality)])).
% cnf(398,negated_conjecture,(esk2_3(X1,X2,esk24_0)=esk4_3(X1,X2,esk24_0)|in(esk25_1(X3),esk5_3(X1,X2,esk24_0))|in(esk25_1(X3),X3)|~element(X2,powerset(powerset(X1)))|$false|~relation(esk24_0)|~in(relation_image(esk24_0,esk25_1(X3)),X2)),inference(rw,[status(thm)],[394,234,theory(equality)])).
% cnf(399,negated_conjecture,(esk2_3(X1,X2,esk24_0)=esk4_3(X1,X2,esk24_0)|in(esk25_1(X3),esk5_3(X1,X2,esk24_0))|in(esk25_1(X3),X3)|~element(X2,powerset(powerset(X1)))|$false|$false|~in(relation_image(esk24_0,esk25_1(X3)),X2)),inference(rw,[status(thm)],[398,235,theory(equality)])).
% cnf(400,negated_conjecture,(esk2_3(X1,X2,esk24_0)=esk4_3(X1,X2,esk24_0)|in(esk25_1(X3),esk5_3(X1,X2,esk24_0))|in(esk25_1(X3),X3)|~element(X2,powerset(powerset(X1)))|~in(relation_image(esk24_0,esk25_1(X3)),X2)),inference(cn,[status(thm)],[399,theory(equality)])).
% cnf(622,negated_conjecture,(in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,X1))),esk23_0)|in(relation_image(X1,esk25_1(esk5_3(esk22_0,esk23_0,X1))),esk23_0)|esk4_3(esk22_0,esk23_0,X1)!=esk3_3(esk22_0,esk23_0,X1)|~function(X1)|~relation(X1)),inference(spm,[status(thm)],[306,236,theory(equality)])).
% cnf(655,negated_conjecture,(in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)|~relation(esk24_0)),inference(spm,[status(thm)],[622,234,theory(equality)])).
% cnf(662,negated_conjecture,(in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)|$false),inference(rw,[status(thm)],[655,235,theory(equality)])).
% cnf(663,negated_conjecture,(in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)),inference(cn,[status(thm)],[662,theory(equality)])).
% cnf(1008,negated_conjecture,(esk2_3(esk22_0,esk23_0,X1)=esk3_3(esk22_0,esk23_0,X1)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,X1))),esk23_0)|in(relation_image(X1,esk25_1(esk5_3(esk22_0,esk23_0,X1))),esk23_0)|~function(X1)|~relation(X1)),inference(spm,[status(thm)],[314,236,theory(equality)])).
% cnf(1159,negated_conjecture,(esk2_3(esk22_0,esk23_0,X1)=esk4_3(esk22_0,esk23_0,X1)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,X1))),esk23_0)|in(relation_image(X1,esk25_1(esk5_3(esk22_0,esk23_0,X1))),esk23_0)|~function(X1)|~relation(X1)),inference(spm,[status(thm)],[316,236,theory(equality)])).
% cnf(1312,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|~relation(esk24_0)),inference(spm,[status(thm)],[1008,234,theory(equality)])).
% cnf(1319,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|$false),inference(rw,[status(thm)],[1312,235,theory(equality)])).
% cnf(1320,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)),inference(cn,[status(thm)],[1319,theory(equality)])).
% cnf(1333,negated_conjecture,(in(esk25_1(X1),esk5_3(X2,esk23_0,esk24_0))|in(esk25_1(X1),X1)|esk4_3(X2,esk23_0,esk24_0)!=esk3_3(X2,esk23_0,esk24_0)|~element(esk23_0,powerset(powerset(X2)))),inference(spm,[status(thm)],[323,237,theory(equality)])).
% cnf(1371,negated_conjecture,(in(esk25_1(X1),esk5_3(esk22_0,esk23_0,esk24_0))|in(esk25_1(X1),X1)|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)),inference(spm,[status(thm)],[1333,236,theory(equality)])).
% cnf(1517,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|~relation(esk24_0)),inference(spm,[status(thm)],[1159,234,theory(equality)])).
% cnf(1524,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|$false),inference(rw,[status(thm)],[1517,235,theory(equality)])).
% cnf(1525,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)),inference(cn,[status(thm)],[1524,theory(equality)])).
% cnf(5363,negated_conjecture,(esk2_3(X1,esk23_0,esk24_0)=esk3_3(X1,esk23_0,esk24_0)|in(esk25_1(X2),esk5_3(X1,esk23_0,esk24_0))|in(esk25_1(X2),X2)|~element(esk23_0,powerset(powerset(X1)))),inference(spm,[status(thm)],[391,237,theory(equality)])).
% cnf(5397,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(X1),esk5_3(esk22_0,esk23_0,esk24_0))|in(esk25_1(X1),X1)),inference(spm,[status(thm)],[5363,236,theory(equality)])).
% cnf(5398,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(ef,[status(thm)],[5397,theory(equality)])).
% cnf(5536,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))|~function(esk24_0)|~relation(esk24_0)),inference(spm,[status(thm)],[369,5398,theory(equality)])).
% cnf(5574,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))|$false|~relation(esk24_0)),inference(rw,[status(thm)],[5536,234,theory(equality)])).
% cnf(5575,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))|$false|$false),inference(rw,[status(thm)],[5574,235,theory(equality)])).
% cnf(5576,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),inference(cn,[status(thm)],[5575,theory(equality)])).
% cnf(5588,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|~element(esk23_0,powerset(powerset(esk22_0)))|~function(esk24_0)|~relation(esk24_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(spm,[status(thm)],[75,5576,theory(equality)])).
% cnf(5607,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|$false|~function(esk24_0)|~relation(esk24_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(rw,[status(thm)],[5588,236,theory(equality)])).
% cnf(5608,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|$false|$false|~relation(esk24_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(rw,[status(thm)],[5607,234,theory(equality)])).
% cnf(5609,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|$false|$false|$false|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(rw,[status(thm)],[5608,235,theory(equality)])).
% cnf(5610,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(cn,[status(thm)],[5609,theory(equality)])).
% cnf(5836,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))),inference(csr,[status(thm)],[5610,238])).
% cnf(5843,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|~in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(spm,[status(thm)],[239,5836,theory(equality)])).
% cnf(5859,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)|~in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)),inference(csr,[status(thm)],[5843,5398])).
% cnf(5860,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk3_3(esk22_0,esk23_0,esk24_0)),inference(csr,[status(thm)],[5859,1320])).
% cnf(5867,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)),inference(rw,[status(thm)],[1525,5860,theory(equality)])).
% cnf(5872,negated_conjecture,(in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)),inference(csr,[status(thm)],[5867,663])).
% cnf(6566,negated_conjecture,(esk2_3(X1,esk23_0,esk24_0)=esk4_3(X1,esk23_0,esk24_0)|in(esk25_1(X2),esk5_3(X1,esk23_0,esk24_0))|in(esk25_1(X2),X2)|~element(esk23_0,powerset(powerset(X1)))),inference(spm,[status(thm)],[400,237,theory(equality)])).
% cnf(6598,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(X1),esk5_3(esk22_0,esk23_0,esk24_0))|in(esk25_1(X1),X1)),inference(spm,[status(thm)],[6566,236,theory(equality)])).
% cnf(6599,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(X1),esk5_3(esk22_0,esk23_0,esk24_0))|in(esk25_1(X1),X1)),inference(rw,[status(thm)],[6598,5860,theory(equality)])).
% cnf(6600,negated_conjecture,(in(esk25_1(X1),esk5_3(esk22_0,esk23_0,esk24_0))|in(esk25_1(X1),X1)),inference(csr,[status(thm)],[6599,1371])).
% cnf(6601,negated_conjecture,(in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(ef,[status(thm)],[6600,theory(equality)])).
% cnf(6740,negated_conjecture,(in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)|~element(esk23_0,powerset(powerset(esk22_0)))|~function(esk24_0)|~relation(esk24_0)),inference(spm,[status(thm)],[310,6601,theory(equality)])).
% cnf(6744,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))|~function(esk24_0)|~relation(esk24_0)),inference(spm,[status(thm)],[376,6601,theory(equality)])).
% cnf(6776,negated_conjecture,(in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)|$false|~function(esk24_0)|~relation(esk24_0)),inference(rw,[status(thm)],[6740,236,theory(equality)])).
% cnf(6777,negated_conjecture,(in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)|$false|$false|~relation(esk24_0)),inference(rw,[status(thm)],[6776,234,theory(equality)])).
% cnf(6778,negated_conjecture,(in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)|$false|$false|$false),inference(rw,[status(thm)],[6777,235,theory(equality)])).
% cnf(6779,negated_conjecture,(in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)),inference(cn,[status(thm)],[6778,theory(equality)])).
% cnf(6792,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))|~function(esk24_0)|~relation(esk24_0)),inference(rw,[status(thm)],[6744,5860,theory(equality)])).
% cnf(6793,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))|$false|~relation(esk24_0)),inference(rw,[status(thm)],[6792,234,theory(equality)])).
% cnf(6794,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))|$false|$false),inference(rw,[status(thm)],[6793,235,theory(equality)])).
% cnf(6795,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),inference(cn,[status(thm)],[6794,theory(equality)])).
% cnf(6810,negated_conjecture,(~in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)),inference(spm,[status(thm)],[239,6779,theory(equality)])).
% cnf(6826,negated_conjecture,($false|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)),inference(rw,[status(thm)],[6810,5872,theory(equality)])).
% cnf(6827,negated_conjecture,($false|$false|esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)),inference(rw,[status(thm)],[6826,6601,theory(equality)])).
% cnf(6828,negated_conjecture,(esk4_3(esk22_0,esk23_0,esk24_0)!=esk3_3(esk22_0,esk23_0,esk24_0)),inference(cn,[status(thm)],[6827,theory(equality)])).
% cnf(6830,negated_conjecture,(esk6_4(esk22_0,esk23_0,esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)))=esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),inference(sr,[status(thm)],[6795,6828,theory(equality)])).
% cnf(6832,negated_conjecture,(esk2_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|~element(esk23_0,powerset(powerset(esk22_0)))|~function(esk24_0)|~relation(esk24_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(spm,[status(thm)],[73,6830,theory(equality)])).
% cnf(6859,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|~element(esk23_0,powerset(powerset(esk22_0)))|~function(esk24_0)|~relation(esk24_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(rw,[status(thm)],[6832,5860,theory(equality)])).
% cnf(6860,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|$false|~function(esk24_0)|~relation(esk24_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(rw,[status(thm)],[6859,236,theory(equality)])).
% cnf(6861,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|$false|$false|~relation(esk24_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(rw,[status(thm)],[6860,234,theory(equality)])).
% cnf(6862,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|$false|$false|$false|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(rw,[status(thm)],[6861,235,theory(equality)])).
% cnf(6863,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))|$false|$false|$false|$false),inference(rw,[status(thm)],[6862,6601,theory(equality)])).
% cnf(6864,negated_conjecture,(esk3_3(esk22_0,esk23_0,esk24_0)=esk4_3(esk22_0,esk23_0,esk24_0)|in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))),inference(cn,[status(thm)],[6863,theory(equality)])).
% cnf(6865,negated_conjecture,(in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),powerset(relation_dom(esk24_0)))),inference(sr,[status(thm)],[6864,6828,theory(equality)])).
% cnf(7116,negated_conjecture,(~in(relation_image(esk24_0,esk25_1(esk5_3(esk22_0,esk23_0,esk24_0))),esk23_0)|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(spm,[status(thm)],[239,6865,theory(equality)])).
% cnf(7132,negated_conjecture,($false|~in(esk25_1(esk5_3(esk22_0,esk23_0,esk24_0)),esk5_3(esk22_0,esk23_0,esk24_0))),inference(rw,[status(thm)],[7116,5872,theory(equality)])).
% cnf(7133,negated_conjecture,($false|$false),inference(rw,[status(thm)],[7132,6601,theory(equality)])).
% cnf(7134,negated_conjecture,($false),inference(cn,[status(thm)],[7133,theory(equality)])).
% cnf(7135,negated_conjecture,($false),7134,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 937
% # ...of these trivial : 2
% # ...subsumed : 146
% # ...remaining for further processing: 789
% # Other redundant clauses eliminated : 5
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 80
% # Backward-rewritten : 26
% # Generated clauses : 2747
% # ...of the previous two non-trivial : 2551
% # Contextual simplify-reflections : 234
% # Paramodulations : 2732
% # Factorizations : 10
% # Equation resolutions : 5
% # Current number of processed clauses: 579
% # Positive orientable unit clauses: 53
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 14
% # Non-unit-clauses : 512
% # Current number of unprocessed clauses: 1308
% # ...number of literals in the above : 9376
% # Clause-clause subsumption calls (NU) : 11035
% # Rec. Clause-clause subsumption calls : 5873
% # Unit Clause-clause subsumption calls : 1115
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 62
% # Indexed BW rewrite successes : 5
% # Backwards rewriting index: 325 leaves, 1.87+/-2.405 terms/leaf
% # Paramod-from index: 99 leaves, 1.29+/-1.765 terms/leaf
% # Paramod-into index: 221 leaves, 1.56+/-2.010 terms/leaf
% # -------------------------------------------------
% # User time : 0.285 s
% # System time : 0.011 s
% # Total time : 0.296 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.48 CPU 0.58 WC
% FINAL PrfWatch: 0.48 CPU 0.58 WC
% SZS output end Solution for /tmp/SystemOnTPTP16073/SEU297+1.tptp
%
%------------------------------------------------------------------------------