%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU356+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 : art04.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:58:50 EST 2010
% Result : Theorem 0.91s
% Output : Solution 0.91s
% 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/SystemOnTPTP5752/SEU356+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ... found
% SZS status THM for /tmp/SystemOnTPTP5752/SEU356+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP5752/SEU356+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 5848
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.012 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:(rel_str(X1)=>![X2]:(ex_sup_of_relstr_set(X1,X2)<=>?[X3]:(((element(X3,the_carrier(X1))&relstr_set_smaller(X1,X2,X3))&![X4]:(element(X4,the_carrier(X1))=>(relstr_set_smaller(X1,X2,X4)=>related(X1,X3,X4))))&![X4]:(element(X4,the_carrier(X1))=>((relstr_set_smaller(X1,X2,X4)&![X5]:(element(X5,the_carrier(X1))=>(relstr_set_smaller(X1,X2,X5)=>related(X1,X4,X5))))=>X4=X3))))),file('/tmp/SRASS.s.p', d7_yellow_0)).
% fof(4, axiom,![X1]:((antisymmetric_relstr(X1)&rel_str(X1))=>![X2]:(element(X2,the_carrier(X1))=>![X3]:(element(X3,the_carrier(X1))=>((related(X1,X2,X3)&related(X1,X3,X2))=>X2=X3)))),file('/tmp/SRASS.s.p', t25_orders_2)).
% fof(10, conjecture,![X1]:((antisymmetric_relstr(X1)&rel_str(X1))=>![X2]:(ex_sup_of_relstr_set(X1,X2)<=>?[X3]:((element(X3,the_carrier(X1))&relstr_set_smaller(X1,X2,X3))&![X4]:(element(X4,the_carrier(X1))=>(relstr_set_smaller(X1,X2,X4)=>related(X1,X3,X4)))))),file('/tmp/SRASS.s.p', t15_yellow_0)).
% fof(11, negated_conjecture,~(![X1]:((antisymmetric_relstr(X1)&rel_str(X1))=>![X2]:(ex_sup_of_relstr_set(X1,X2)<=>?[X3]:((element(X3,the_carrier(X1))&relstr_set_smaller(X1,X2,X3))&![X4]:(element(X4,the_carrier(X1))=>(relstr_set_smaller(X1,X2,X4)=>related(X1,X3,X4))))))),inference(assume_negation,[status(cth)],[10])).
% fof(18, plain,![X1]:(~(rel_str(X1))|![X2]:((~(ex_sup_of_relstr_set(X1,X2))|?[X3]:(((element(X3,the_carrier(X1))&relstr_set_smaller(X1,X2,X3))&![X4]:(~(element(X4,the_carrier(X1)))|(~(relstr_set_smaller(X1,X2,X4))|related(X1,X3,X4))))&![X4]:(~(element(X4,the_carrier(X1)))|((~(relstr_set_smaller(X1,X2,X4))|?[X5]:(element(X5,the_carrier(X1))&(relstr_set_smaller(X1,X2,X5)&~(related(X1,X4,X5)))))|X4=X3))))&(![X3]:(((~(element(X3,the_carrier(X1)))|~(relstr_set_smaller(X1,X2,X3)))|?[X4]:(element(X4,the_carrier(X1))&(relstr_set_smaller(X1,X2,X4)&~(related(X1,X3,X4)))))|?[X4]:(element(X4,the_carrier(X1))&((relstr_set_smaller(X1,X2,X4)&![X5]:(~(element(X5,the_carrier(X1)))|(~(relstr_set_smaller(X1,X2,X5))|related(X1,X4,X5))))&~(X4=X3))))|ex_sup_of_relstr_set(X1,X2)))),inference(fof_nnf,[status(thm)],[3])).
% fof(19, plain,![X6]:(~(rel_str(X6))|![X7]:((~(ex_sup_of_relstr_set(X6,X7))|?[X8]:(((element(X8,the_carrier(X6))&relstr_set_smaller(X6,X7,X8))&![X9]:(~(element(X9,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X9))|related(X6,X8,X9))))&![X10]:(~(element(X10,the_carrier(X6)))|((~(relstr_set_smaller(X6,X7,X10))|?[X11]:(element(X11,the_carrier(X6))&(relstr_set_smaller(X6,X7,X11)&~(related(X6,X10,X11)))))|X10=X8))))&(![X12]:(((~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12)))|?[X13]:(element(X13,the_carrier(X6))&(relstr_set_smaller(X6,X7,X13)&~(related(X6,X12,X13)))))|?[X14]:(element(X14,the_carrier(X6))&((relstr_set_smaller(X6,X7,X14)&![X15]:(~(element(X15,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X15))|related(X6,X14,X15))))&~(X14=X12))))|ex_sup_of_relstr_set(X6,X7)))),inference(variable_rename,[status(thm)],[18])).
% fof(20, plain,![X6]:(~(rel_str(X6))|![X7]:((~(ex_sup_of_relstr_set(X6,X7))|(((element(esk3_2(X6,X7),the_carrier(X6))&relstr_set_smaller(X6,X7,esk3_2(X6,X7)))&![X9]:(~(element(X9,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X9))|related(X6,esk3_2(X6,X7),X9))))&![X10]:(~(element(X10,the_carrier(X6)))|((~(relstr_set_smaller(X6,X7,X10))|(element(esk4_3(X6,X7,X10),the_carrier(X6))&(relstr_set_smaller(X6,X7,esk4_3(X6,X7,X10))&~(related(X6,X10,esk4_3(X6,X7,X10))))))|X10=esk3_2(X6,X7)))))&(![X12]:(((~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12)))|(element(esk5_3(X6,X7,X12),the_carrier(X6))&(relstr_set_smaller(X6,X7,esk5_3(X6,X7,X12))&~(related(X6,X12,esk5_3(X6,X7,X12))))))|(element(esk6_3(X6,X7,X12),the_carrier(X6))&((relstr_set_smaller(X6,X7,esk6_3(X6,X7,X12))&![X15]:(~(element(X15,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X15))|related(X6,esk6_3(X6,X7,X12),X15))))&~(esk6_3(X6,X7,X12)=X12))))|ex_sup_of_relstr_set(X6,X7)))),inference(skolemize,[status(esa)],[19])).
% fof(21, plain,![X6]:![X7]:![X9]:![X10]:![X12]:![X15]:((((((((~(element(X15,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X15))|related(X6,esk6_3(X6,X7,X12),X15)))&relstr_set_smaller(X6,X7,esk6_3(X6,X7,X12)))&~(esk6_3(X6,X7,X12)=X12))&element(esk6_3(X6,X7,X12),the_carrier(X6)))|((~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12)))|(element(esk5_3(X6,X7,X12),the_carrier(X6))&(relstr_set_smaller(X6,X7,esk5_3(X6,X7,X12))&~(related(X6,X12,esk5_3(X6,X7,X12)))))))|ex_sup_of_relstr_set(X6,X7))&(((~(element(X10,the_carrier(X6)))|((~(relstr_set_smaller(X6,X7,X10))|(element(esk4_3(X6,X7,X10),the_carrier(X6))&(relstr_set_smaller(X6,X7,esk4_3(X6,X7,X10))&~(related(X6,X10,esk4_3(X6,X7,X10))))))|X10=esk3_2(X6,X7)))&((~(element(X9,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X9))|related(X6,esk3_2(X6,X7),X9)))&(element(esk3_2(X6,X7),the_carrier(X6))&relstr_set_smaller(X6,X7,esk3_2(X6,X7)))))|~(ex_sup_of_relstr_set(X6,X7))))|~(rel_str(X6))),inference(shift_quantors,[status(thm)],[20])).
% fof(22, plain,![X6]:![X7]:![X9]:![X10]:![X12]:![X15]:(((((((((element(esk5_3(X6,X7,X12),the_carrier(X6))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|(~(element(X15,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X15))|related(X6,esk6_3(X6,X7,X12),X15))))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))&(((((relstr_set_smaller(X6,X7,esk5_3(X6,X7,X12))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|(~(element(X15,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X15))|related(X6,esk6_3(X6,X7,X12),X15))))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))&((((~(related(X6,X12,esk5_3(X6,X7,X12)))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|(~(element(X15,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X15))|related(X6,esk6_3(X6,X7,X12),X15))))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))))&(((((element(esk5_3(X6,X7,X12),the_carrier(X6))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|relstr_set_smaller(X6,X7,esk6_3(X6,X7,X12)))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))&(((((relstr_set_smaller(X6,X7,esk5_3(X6,X7,X12))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|relstr_set_smaller(X6,X7,esk6_3(X6,X7,X12)))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))&((((~(related(X6,X12,esk5_3(X6,X7,X12)))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|relstr_set_smaller(X6,X7,esk6_3(X6,X7,X12)))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6))))))&(((((element(esk5_3(X6,X7,X12),the_carrier(X6))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|~(esk6_3(X6,X7,X12)=X12))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))&(((((relstr_set_smaller(X6,X7,esk5_3(X6,X7,X12))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|~(esk6_3(X6,X7,X12)=X12))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))&((((~(related(X6,X12,esk5_3(X6,X7,X12)))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|~(esk6_3(X6,X7,X12)=X12))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6))))))&(((((element(esk5_3(X6,X7,X12),the_carrier(X6))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|element(esk6_3(X6,X7,X12),the_carrier(X6)))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))&(((((relstr_set_smaller(X6,X7,esk5_3(X6,X7,X12))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|element(esk6_3(X6,X7,X12),the_carrier(X6)))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6)))&((((~(related(X6,X12,esk5_3(X6,X7,X12)))|(~(element(X12,the_carrier(X6)))|~(relstr_set_smaller(X6,X7,X12))))|element(esk6_3(X6,X7,X12),the_carrier(X6)))|ex_sup_of_relstr_set(X6,X7))|~(rel_str(X6))))))&(((((((element(esk4_3(X6,X7,X10),the_carrier(X6))|~(relstr_set_smaller(X6,X7,X10)))|X10=esk3_2(X6,X7))|~(element(X10,the_carrier(X6))))|~(ex_sup_of_relstr_set(X6,X7)))|~(rel_str(X6)))&((((((relstr_set_smaller(X6,X7,esk4_3(X6,X7,X10))|~(relstr_set_smaller(X6,X7,X10)))|X10=esk3_2(X6,X7))|~(element(X10,the_carrier(X6))))|~(ex_sup_of_relstr_set(X6,X7)))|~(rel_str(X6)))&(((((~(related(X6,X10,esk4_3(X6,X7,X10)))|~(relstr_set_smaller(X6,X7,X10)))|X10=esk3_2(X6,X7))|~(element(X10,the_carrier(X6))))|~(ex_sup_of_relstr_set(X6,X7)))|~(rel_str(X6)))))&((((~(element(X9,the_carrier(X6)))|(~(relstr_set_smaller(X6,X7,X9))|related(X6,esk3_2(X6,X7),X9)))|~(ex_sup_of_relstr_set(X6,X7)))|~(rel_str(X6)))&(((element(esk3_2(X6,X7),the_carrier(X6))|~(ex_sup_of_relstr_set(X6,X7)))|~(rel_str(X6)))&((relstr_set_smaller(X6,X7,esk3_2(X6,X7))|~(ex_sup_of_relstr_set(X6,X7)))|~(rel_str(X6))))))),inference(distribute,[status(thm)],[21])).
% cnf(23,plain,(relstr_set_smaller(X1,X2,esk3_2(X1,X2))|~rel_str(X1)|~ex_sup_of_relstr_set(X1,X2)),inference(split_conjunct,[status(thm)],[22])).
% cnf(24,plain,(element(esk3_2(X1,X2),the_carrier(X1))|~rel_str(X1)|~ex_sup_of_relstr_set(X1,X2)),inference(split_conjunct,[status(thm)],[22])).
% cnf(25,plain,(related(X1,esk3_2(X1,X2),X3)|~rel_str(X1)|~ex_sup_of_relstr_set(X1,X2)|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% cnf(29,plain,(ex_sup_of_relstr_set(X1,X2)|element(esk6_3(X1,X2,X3),the_carrier(X1))|~rel_str(X1)|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))|~related(X1,X3,esk5_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[22])).
% cnf(30,plain,(ex_sup_of_relstr_set(X1,X2)|element(esk6_3(X1,X2,X3),the_carrier(X1))|relstr_set_smaller(X1,X2,esk5_3(X1,X2,X3))|~rel_str(X1)|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% cnf(31,plain,(ex_sup_of_relstr_set(X1,X2)|element(esk6_3(X1,X2,X3),the_carrier(X1))|element(esk5_3(X1,X2,X3),the_carrier(X1))|~rel_str(X1)|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% cnf(32,plain,(ex_sup_of_relstr_set(X1,X2)|~rel_str(X1)|esk6_3(X1,X2,X3)!=X3|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))|~related(X1,X3,esk5_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[22])).
% cnf(33,plain,(ex_sup_of_relstr_set(X1,X2)|relstr_set_smaller(X1,X2,esk5_3(X1,X2,X3))|~rel_str(X1)|esk6_3(X1,X2,X3)!=X3|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% cnf(34,plain,(ex_sup_of_relstr_set(X1,X2)|element(esk5_3(X1,X2,X3),the_carrier(X1))|~rel_str(X1)|esk6_3(X1,X2,X3)!=X3|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% cnf(35,plain,(ex_sup_of_relstr_set(X1,X2)|relstr_set_smaller(X1,X2,esk6_3(X1,X2,X3))|~rel_str(X1)|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))|~related(X1,X3,esk5_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[22])).
% cnf(36,plain,(ex_sup_of_relstr_set(X1,X2)|relstr_set_smaller(X1,X2,esk6_3(X1,X2,X3))|relstr_set_smaller(X1,X2,esk5_3(X1,X2,X3))|~rel_str(X1)|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% cnf(37,plain,(ex_sup_of_relstr_set(X1,X2)|relstr_set_smaller(X1,X2,esk6_3(X1,X2,X3))|element(esk5_3(X1,X2,X3),the_carrier(X1))|~rel_str(X1)|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% cnf(38,plain,(ex_sup_of_relstr_set(X1,X2)|related(X1,esk6_3(X1,X2,X3),X4)|~rel_str(X1)|~relstr_set_smaller(X1,X2,X4)|~element(X4,the_carrier(X1))|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))|~related(X1,X3,esk5_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[22])).
% cnf(39,plain,(ex_sup_of_relstr_set(X1,X2)|related(X1,esk6_3(X1,X2,X3),X4)|relstr_set_smaller(X1,X2,esk5_3(X1,X2,X3))|~rel_str(X1)|~relstr_set_smaller(X1,X2,X4)|~element(X4,the_carrier(X1))|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% cnf(40,plain,(ex_sup_of_relstr_set(X1,X2)|related(X1,esk6_3(X1,X2,X3),X4)|element(esk5_3(X1,X2,X3),the_carrier(X1))|~rel_str(X1)|~relstr_set_smaller(X1,X2,X4)|~element(X4,the_carrier(X1))|~relstr_set_smaller(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[22])).
% fof(41, plain,![X1]:((~(antisymmetric_relstr(X1))|~(rel_str(X1)))|![X2]:(~(element(X2,the_carrier(X1)))|![X3]:(~(element(X3,the_carrier(X1)))|((~(related(X1,X2,X3))|~(related(X1,X3,X2)))|X2=X3)))),inference(fof_nnf,[status(thm)],[4])).
% fof(42, plain,![X4]:((~(antisymmetric_relstr(X4))|~(rel_str(X4)))|![X5]:(~(element(X5,the_carrier(X4)))|![X6]:(~(element(X6,the_carrier(X4)))|((~(related(X4,X5,X6))|~(related(X4,X6,X5)))|X5=X6)))),inference(variable_rename,[status(thm)],[41])).
% fof(43, plain,![X4]:![X5]:![X6]:(((~(element(X6,the_carrier(X4)))|((~(related(X4,X5,X6))|~(related(X4,X6,X5)))|X5=X6))|~(element(X5,the_carrier(X4))))|(~(antisymmetric_relstr(X4))|~(rel_str(X4)))),inference(shift_quantors,[status(thm)],[42])).
% cnf(44,plain,(X2=X3|~rel_str(X1)|~antisymmetric_relstr(X1)|~element(X2,the_carrier(X1))|~related(X1,X3,X2)|~related(X1,X2,X3)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[43])).
% fof(54, negated_conjecture,?[X1]:((antisymmetric_relstr(X1)&rel_str(X1))&?[X2]:((~(ex_sup_of_relstr_set(X1,X2))|![X3]:((~(element(X3,the_carrier(X1)))|~(relstr_set_smaller(X1,X2,X3)))|?[X4]:(element(X4,the_carrier(X1))&(relstr_set_smaller(X1,X2,X4)&~(related(X1,X3,X4))))))&(ex_sup_of_relstr_set(X1,X2)|?[X3]:((element(X3,the_carrier(X1))&relstr_set_smaller(X1,X2,X3))&![X4]:(~(element(X4,the_carrier(X1)))|(~(relstr_set_smaller(X1,X2,X4))|related(X1,X3,X4))))))),inference(fof_nnf,[status(thm)],[11])).
% fof(55, negated_conjecture,?[X5]:((antisymmetric_relstr(X5)&rel_str(X5))&?[X6]:((~(ex_sup_of_relstr_set(X5,X6))|![X7]:((~(element(X7,the_carrier(X5)))|~(relstr_set_smaller(X5,X6,X7)))|?[X8]:(element(X8,the_carrier(X5))&(relstr_set_smaller(X5,X6,X8)&~(related(X5,X7,X8))))))&(ex_sup_of_relstr_set(X5,X6)|?[X9]:((element(X9,the_carrier(X5))&relstr_set_smaller(X5,X6,X9))&![X10]:(~(element(X10,the_carrier(X5)))|(~(relstr_set_smaller(X5,X6,X10))|related(X5,X9,X10))))))),inference(variable_rename,[status(thm)],[54])).
% fof(56, negated_conjecture,((antisymmetric_relstr(esk8_0)&rel_str(esk8_0))&((~(ex_sup_of_relstr_set(esk8_0,esk9_0))|![X7]:((~(element(X7,the_carrier(esk8_0)))|~(relstr_set_smaller(esk8_0,esk9_0,X7)))|(element(esk10_1(X7),the_carrier(esk8_0))&(relstr_set_smaller(esk8_0,esk9_0,esk10_1(X7))&~(related(esk8_0,X7,esk10_1(X7)))))))&(ex_sup_of_relstr_set(esk8_0,esk9_0)|((element(esk11_0,the_carrier(esk8_0))&relstr_set_smaller(esk8_0,esk9_0,esk11_0))&![X10]:(~(element(X10,the_carrier(esk8_0)))|(~(relstr_set_smaller(esk8_0,esk9_0,X10))|related(esk8_0,esk11_0,X10))))))),inference(skolemize,[status(esa)],[55])).
% fof(57, negated_conjecture,![X7]:![X10]:(((((~(element(X10,the_carrier(esk8_0)))|(~(relstr_set_smaller(esk8_0,esk9_0,X10))|related(esk8_0,esk11_0,X10)))&(element(esk11_0,the_carrier(esk8_0))&relstr_set_smaller(esk8_0,esk9_0,esk11_0)))|ex_sup_of_relstr_set(esk8_0,esk9_0))&(((~(element(X7,the_carrier(esk8_0)))|~(relstr_set_smaller(esk8_0,esk9_0,X7)))|(element(esk10_1(X7),the_carrier(esk8_0))&(relstr_set_smaller(esk8_0,esk9_0,esk10_1(X7))&~(related(esk8_0,X7,esk10_1(X7))))))|~(ex_sup_of_relstr_set(esk8_0,esk9_0))))&(antisymmetric_relstr(esk8_0)&rel_str(esk8_0))),inference(shift_quantors,[status(thm)],[56])).
% fof(58, negated_conjecture,![X7]:![X10]:(((((~(element(X10,the_carrier(esk8_0)))|(~(relstr_set_smaller(esk8_0,esk9_0,X10))|related(esk8_0,esk11_0,X10)))|ex_sup_of_relstr_set(esk8_0,esk9_0))&((element(esk11_0,the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0))&(relstr_set_smaller(esk8_0,esk9_0,esk11_0)|ex_sup_of_relstr_set(esk8_0,esk9_0))))&(((element(esk10_1(X7),the_carrier(esk8_0))|(~(element(X7,the_carrier(esk8_0)))|~(relstr_set_smaller(esk8_0,esk9_0,X7))))|~(ex_sup_of_relstr_set(esk8_0,esk9_0)))&(((relstr_set_smaller(esk8_0,esk9_0,esk10_1(X7))|(~(element(X7,the_carrier(esk8_0)))|~(relstr_set_smaller(esk8_0,esk9_0,X7))))|~(ex_sup_of_relstr_set(esk8_0,esk9_0)))&((~(related(esk8_0,X7,esk10_1(X7)))|(~(element(X7,the_carrier(esk8_0)))|~(relstr_set_smaller(esk8_0,esk9_0,X7))))|~(ex_sup_of_relstr_set(esk8_0,esk9_0))))))&(antisymmetric_relstr(esk8_0)&rel_str(esk8_0))),inference(distribute,[status(thm)],[57])).
% cnf(59,negated_conjecture,(rel_str(esk8_0)),inference(split_conjunct,[status(thm)],[58])).
% cnf(60,negated_conjecture,(antisymmetric_relstr(esk8_0)),inference(split_conjunct,[status(thm)],[58])).
% cnf(61,negated_conjecture,(~ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))|~related(esk8_0,X1,esk10_1(X1))),inference(split_conjunct,[status(thm)],[58])).
% cnf(62,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk10_1(X1))|~ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))),inference(split_conjunct,[status(thm)],[58])).
% cnf(63,negated_conjecture,(element(esk10_1(X1),the_carrier(esk8_0))|~ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))),inference(split_conjunct,[status(thm)],[58])).
% cnf(64,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|relstr_set_smaller(esk8_0,esk9_0,esk11_0)),inference(split_conjunct,[status(thm)],[58])).
% cnf(65,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk11_0,the_carrier(esk8_0))),inference(split_conjunct,[status(thm)],[58])).
% cnf(66,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|related(esk8_0,esk11_0,X1)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))),inference(split_conjunct,[status(thm)],[58])).
% cnf(68,negated_conjecture,(X1=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|~antisymmetric_relstr(esk8_0)|~related(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)),inference(spm,[status(thm)],[44,66,theory(equality)])).
% cnf(69,negated_conjecture,(X1=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|$false|~related(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)),inference(rw,[status(thm)],[68,60,theory(equality)])).
% cnf(70,negated_conjecture,(X1=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|$false|~related(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,X1)),inference(rw,[status(thm)],[69,59,theory(equality)])).
% cnf(71,negated_conjecture,(X1=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|~related(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,X1)),inference(cn,[status(thm)],[70,theory(equality)])).
% cnf(72,negated_conjecture,(~relstr_set_smaller(esk8_0,esk9_0,esk3_2(esk8_0,X1))|~ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk3_2(esk8_0,X1),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,X1,esk10_1(esk3_2(esk8_0,X1)))|~ex_sup_of_relstr_set(esk8_0,X1)|~element(esk10_1(esk3_2(esk8_0,X1)),the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[61,25,theory(equality)])).
% cnf(74,negated_conjecture,(~relstr_set_smaller(esk8_0,esk9_0,esk3_2(esk8_0,X1))|~ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk3_2(esk8_0,X1),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,X1,esk10_1(esk3_2(esk8_0,X1)))|~ex_sup_of_relstr_set(esk8_0,X1)|~element(esk10_1(esk3_2(esk8_0,X1)),the_carrier(esk8_0))|$false),inference(rw,[status(thm)],[72,59,theory(equality)])).
% cnf(75,negated_conjecture,(~relstr_set_smaller(esk8_0,esk9_0,esk3_2(esk8_0,X1))|~ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk3_2(esk8_0,X1),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,X1,esk10_1(esk3_2(esk8_0,X1)))|~ex_sup_of_relstr_set(esk8_0,X1)|~element(esk10_1(esk3_2(esk8_0,X1)),the_carrier(esk8_0))),inference(cn,[status(thm)],[74,theory(equality)])).
% cnf(80,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,X1,esk11_0)!=esk11_0|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[32,66,theory(equality)])).
% cnf(82,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,X1,esk11_0)!=esk11_0|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[80,59,theory(equality)])).
% cnf(83,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,X1,esk11_0)!=esk11_0|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[82,theory(equality)])).
% cnf(84,negated_conjecture,(relstr_set_smaller(esk8_0,X1,esk6_3(esk8_0,X1,esk11_0))|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[35,66,theory(equality)])).
% cnf(86,negated_conjecture,(relstr_set_smaller(esk8_0,X1,esk6_3(esk8_0,X1,esk11_0))|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[84,59,theory(equality)])).
% cnf(87,negated_conjecture,(relstr_set_smaller(esk8_0,X1,esk6_3(esk8_0,X1,esk11_0))|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[86,theory(equality)])).
% cnf(88,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[29,66,theory(equality)])).
% cnf(90,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[88,59,theory(equality)])).
% cnf(91,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[90,theory(equality)])).
% cnf(92,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,esk11_0),X2)|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,X2)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(X2,the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[38,66,theory(equality)])).
% cnf(94,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,esk11_0),X2)|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,X2)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(X2,the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[92,59,theory(equality)])).
% cnf(95,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,esk11_0),X2)|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,X2)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(X2,the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[94,theory(equality)])).
% cnf(102,plain,(X1=esk6_3(X2,X3,X4)|ex_sup_of_relstr_set(X2,X3)|element(esk5_3(X2,X3,X4),the_carrier(X2))|~antisymmetric_relstr(X2)|~related(X2,X1,esk6_3(X2,X3,X4))|~element(esk6_3(X2,X3,X4),the_carrier(X2))|~element(X1,the_carrier(X2))|~rel_str(X2)|~relstr_set_smaller(X2,X3,X1)|~relstr_set_smaller(X2,X3,X4)|~element(X4,the_carrier(X2))),inference(spm,[status(thm)],[44,40,theory(equality)])).
% cnf(113,negated_conjecture,(X1=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|~related(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))),inference(csr,[status(thm)],[71,65])).
% cnf(127,negated_conjecture,(~relstr_set_smaller(esk8_0,X1,esk10_1(esk3_2(esk8_0,X1)))|~relstr_set_smaller(esk8_0,esk9_0,esk3_2(esk8_0,X1))|~ex_sup_of_relstr_set(esk8_0,esk9_0)|~ex_sup_of_relstr_set(esk8_0,X1)|~element(esk3_2(esk8_0,X1),the_carrier(esk8_0))),inference(csr,[status(thm)],[75,63])).
% cnf(128,negated_conjecture,(~relstr_set_smaller(esk8_0,esk9_0,esk3_2(esk8_0,esk9_0))|~ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk3_2(esk8_0,esk9_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[127,62,theory(equality)])).
% cnf(129,negated_conjecture,(~ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk3_2(esk8_0,esk9_0),the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[128,23,theory(equality)])).
% cnf(130,negated_conjecture,(~ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk3_2(esk8_0,esk9_0),the_carrier(esk8_0))|$false),inference(rw,[status(thm)],[129,59,theory(equality)])).
% cnf(131,negated_conjecture,(~ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk3_2(esk8_0,esk9_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[130,theory(equality)])).
% cnf(136,negated_conjecture,(~ex_sup_of_relstr_set(esk8_0,esk9_0)|~rel_str(esk8_0)),inference(spm,[status(thm)],[131,24,theory(equality)])).
% cnf(137,negated_conjecture,(~ex_sup_of_relstr_set(esk8_0,esk9_0)|$false),inference(rw,[status(thm)],[136,59,theory(equality)])).
% cnf(138,negated_conjecture,(~ex_sup_of_relstr_set(esk8_0,esk9_0)),inference(cn,[status(thm)],[137,theory(equality)])).
% cnf(139,negated_conjecture,(element(esk11_0,the_carrier(esk8_0))),inference(sr,[status(thm)],[65,138,theory(equality)])).
% cnf(140,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk11_0)),inference(sr,[status(thm)],[64,138,theory(equality)])).
% cnf(141,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,X2),esk11_0)|relstr_set_smaller(esk8_0,X1,esk5_3(esk8_0,X1,X2))|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|~element(X2,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[39,139,theory(equality)])).
% cnf(142,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,X2),esk11_0)|relstr_set_smaller(esk8_0,X1,esk5_3(esk8_0,X1,X2))|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|~element(X2,the_carrier(esk8_0))|$false),inference(rw,[status(thm)],[141,59,theory(equality)])).
% cnf(143,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,X2),esk11_0)|relstr_set_smaller(esk8_0,X1,esk5_3(esk8_0,X1,X2))|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|~element(X2,the_carrier(esk8_0))),inference(cn,[status(thm)],[142,theory(equality)])).
% cnf(157,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,X1,esk11_0)!=esk11_0|~relstr_set_smaller(esk8_0,X1,esk11_0)|$false|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[83,139,theory(equality)])).
% cnf(158,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,X1,esk11_0)!=esk11_0|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[157,theory(equality)])).
% cnf(159,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|esk6_3(esk8_0,X1,esk11_0)!=esk11_0|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[158,138,theory(equality)])).
% cnf(160,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[159,33,theory(equality)])).
% cnf(162,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(rw,[status(thm)],[160,140,theory(equality)])).
% cnf(163,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~rel_str(esk8_0)),inference(rw,[status(thm)],[162,139,theory(equality)])).
% cnf(164,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|$false),inference(rw,[status(thm)],[163,59,theory(equality)])).
% cnf(165,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[164,theory(equality)])).
% cnf(166,negated_conjecture,(esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[165,138,theory(equality)])).
% cnf(172,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[166,34,theory(equality)])).
% cnf(173,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|$false|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(rw,[status(thm)],[172,140,theory(equality)])).
% cnf(174,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|$false|$false|~rel_str(esk8_0)),inference(rw,[status(thm)],[173,139,theory(equality)])).
% cnf(175,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0|$false|$false|$false),inference(rw,[status(thm)],[174,59,theory(equality)])).
% cnf(176,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0),inference(cn,[status(thm)],[175,theory(equality)])).
% cnf(177,negated_conjecture,(esk6_3(esk8_0,esk9_0,esk11_0)!=esk11_0),inference(sr,[status(thm)],[176,138,theory(equality)])).
% cnf(183,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,esk11_0),esk11_0)|relstr_set_smaller(esk8_0,X1,esk5_3(esk8_0,X1,esk11_0))|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,X1,esk11_0)),inference(spm,[status(thm)],[143,139,theory(equality)])).
% cnf(198,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,esk9_0,esk11_0),esk11_0)|relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)),inference(spm,[status(thm)],[183,140,theory(equality)])).
% cnf(199,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,esk9_0,esk11_0),esk11_0)|relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))),inference(sr,[status(thm)],[198,138,theory(equality)])).
% cnf(201,negated_conjecture,(esk6_3(esk8_0,esk9_0,esk11_0)=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[113,199,theory(equality)])).
% cnf(207,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[201,177,theory(equality)])).
% cnf(208,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[207,138,theory(equality)])).
% cnf(211,negated_conjecture,(relstr_set_smaller(esk8_0,X1,esk6_3(esk8_0,X1,esk11_0))|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|$false|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[87,139,theory(equality)])).
% cnf(212,negated_conjecture,(relstr_set_smaller(esk8_0,X1,esk6_3(esk8_0,X1,esk11_0))|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[211,theory(equality)])).
% cnf(213,negated_conjecture,(relstr_set_smaller(esk8_0,X1,esk6_3(esk8_0,X1,esk11_0))|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[212,138,theory(equality)])).
% cnf(215,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[213,30,theory(equality)])).
% cnf(221,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(rw,[status(thm)],[215,140,theory(equality)])).
% cnf(222,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~rel_str(esk8_0)),inference(rw,[status(thm)],[221,139,theory(equality)])).
% cnf(223,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|$false),inference(rw,[status(thm)],[222,59,theory(equality)])).
% cnf(224,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[223,theory(equality)])).
% cnf(225,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[224,138,theory(equality)])).
% cnf(228,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[208,36,theory(equality)])).
% cnf(234,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(rw,[status(thm)],[228,140,theory(equality)])).
% cnf(235,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|$false|~rel_str(esk8_0)),inference(rw,[status(thm)],[234,139,theory(equality)])).
% cnf(236,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|$false|$false),inference(rw,[status(thm)],[235,59,theory(equality)])).
% cnf(237,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[236,theory(equality)])).
% cnf(238,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[237,138,theory(equality)])).
% cnf(240,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[213,238,theory(equality)])).
% cnf(244,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[240,140,theory(equality)])).
% cnf(245,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[244,theory(equality)])).
% cnf(246,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[245,138,theory(equality)])).
% cnf(252,negated_conjecture,(relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,esk9_0,esk11_0))|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(csr,[status(thm)],[225,246])).
% cnf(253,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|$false|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[91,139,theory(equality)])).
% cnf(254,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[253,theory(equality)])).
% cnf(255,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[254,138,theory(equality)])).
% cnf(257,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[255,30,theory(equality)])).
% cnf(264,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(rw,[status(thm)],[257,140,theory(equality)])).
% cnf(265,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~rel_str(esk8_0)),inference(rw,[status(thm)],[264,139,theory(equality)])).
% cnf(266,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|$false|$false),inference(rw,[status(thm)],[265,59,theory(equality)])).
% cnf(267,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[266,theory(equality)])).
% cnf(268,negated_conjecture,(element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[267,138,theory(equality)])).
% cnf(282,plain,(X1=esk6_3(X2,X3,X4)|ex_sup_of_relstr_set(X2,X3)|element(esk5_3(X2,X3,X4),the_carrier(X2))|~antisymmetric_relstr(X2)|~related(X2,X1,esk6_3(X2,X3,X4))|~relstr_set_smaller(X2,X3,X1)|~relstr_set_smaller(X2,X3,X4)|~element(X1,the_carrier(X2))|~element(X4,the_carrier(X2))|~rel_str(X2)),inference(csr,[status(thm)],[102,31])).
% cnf(283,negated_conjecture,(esk11_0=esk6_3(esk8_0,X1,X2)|ex_sup_of_relstr_set(esk8_0,X1)|element(esk5_3(esk8_0,X1,X2),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~antisymmetric_relstr(esk8_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|~element(esk11_0,the_carrier(esk8_0))|~element(X2,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,X2))|~element(esk6_3(esk8_0,X1,X2),the_carrier(esk8_0))),inference(spm,[status(thm)],[282,66,theory(equality)])).
% cnf(286,negated_conjecture,(esk11_0=esk6_3(esk8_0,X1,X2)|ex_sup_of_relstr_set(esk8_0,X1)|element(esk5_3(esk8_0,X1,X2),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|$false|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|~element(esk11_0,the_carrier(esk8_0))|~element(X2,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,X2))|~element(esk6_3(esk8_0,X1,X2),the_carrier(esk8_0))),inference(rw,[status(thm)],[283,60,theory(equality)])).
% cnf(287,negated_conjecture,(esk11_0=esk6_3(esk8_0,X1,X2)|ex_sup_of_relstr_set(esk8_0,X1)|element(esk5_3(esk8_0,X1,X2),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|$false|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|$false|~element(X2,the_carrier(esk8_0))|~rel_str(esk8_0)|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,X2))|~element(esk6_3(esk8_0,X1,X2),the_carrier(esk8_0))),inference(rw,[status(thm)],[286,139,theory(equality)])).
% cnf(288,negated_conjecture,(esk11_0=esk6_3(esk8_0,X1,X2)|ex_sup_of_relstr_set(esk8_0,X1)|element(esk5_3(esk8_0,X1,X2),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|$false|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|$false|~element(X2,the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,X2))|~element(esk6_3(esk8_0,X1,X2),the_carrier(esk8_0))),inference(rw,[status(thm)],[287,59,theory(equality)])).
% cnf(289,negated_conjecture,(esk11_0=esk6_3(esk8_0,X1,X2)|ex_sup_of_relstr_set(esk8_0,X1)|element(esk5_3(esk8_0,X1,X2),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|~element(X2,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,X2))|~element(esk6_3(esk8_0,X1,X2),the_carrier(esk8_0))),inference(cn,[status(thm)],[288,theory(equality)])).
% cnf(290,negated_conjecture,(esk6_3(esk8_0,X1,X2)=esk11_0|ex_sup_of_relstr_set(esk8_0,X1)|element(esk5_3(esk8_0,X1,X2),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,X1,esk11_0)|~relstr_set_smaller(esk8_0,X1,X2)|~element(X2,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,X2))|~element(esk6_3(esk8_0,X1,X2),the_carrier(esk8_0))),inference(sr,[status(thm)],[289,138,theory(equality)])).
% cnf(291,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(esk6_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[290,37,theory(equality)])).
% cnf(294,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(esk6_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(rw,[status(thm)],[291,140,theory(equality)])).
% cnf(295,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(esk6_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))|$false),inference(rw,[status(thm)],[294,59,theory(equality)])).
% cnf(296,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(esk6_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))),inference(cn,[status(thm)],[295,theory(equality)])).
% cnf(297,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(esk6_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~element(X1,the_carrier(esk8_0))),inference(sr,[status(thm)],[296,138,theory(equality)])).
% cnf(305,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))|~rel_str(esk8_0)),inference(spm,[status(thm)],[297,31,theory(equality)])).
% cnf(307,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))|$false),inference(rw,[status(thm)],[305,59,theory(equality)])).
% cnf(308,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))),inference(cn,[status(thm)],[307,theory(equality)])).
% cnf(309,negated_conjecture,(esk6_3(esk8_0,esk9_0,X1)=esk11_0|element(esk5_3(esk8_0,esk9_0,X1),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,X1)|~element(X1,the_carrier(esk8_0))),inference(sr,[status(thm)],[308,138,theory(equality)])).
% cnf(323,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,esk11_0),X2)|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,X2)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(X2,the_carrier(esk8_0))|$false|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[95,139,theory(equality)])).
% cnf(324,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,esk11_0),X2)|ex_sup_of_relstr_set(esk8_0,X1)|ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,X1,X2)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(X2,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[323,theory(equality)])).
% cnf(325,negated_conjecture,(related(esk8_0,esk6_3(esk8_0,X1,esk11_0),X2)|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,X1,X2)|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(X2,the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[324,138,theory(equality)])).
% cnf(335,negated_conjecture,(esk6_3(esk8_0,X1,esk11_0)=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,esk11_0))|~element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|~element(esk11_0,the_carrier(esk8_0))),inference(spm,[status(thm)],[113,325,theory(equality)])).
% cnf(355,negated_conjecture,(esk6_3(esk8_0,X1,esk11_0)=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,esk11_0))|~element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|$false),inference(rw,[status(thm)],[335,139,theory(equality)])).
% cnf(356,negated_conjecture,(esk6_3(esk8_0,X1,esk11_0)=esk11_0|ex_sup_of_relstr_set(esk8_0,esk9_0)|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,esk11_0))|~element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[355,theory(equality)])).
% cnf(357,negated_conjecture,(esk6_3(esk8_0,X1,esk11_0)=esk11_0|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,esk11_0))|~element(esk6_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[356,138,theory(equality)])).
% cnf(358,negated_conjecture,(esk6_3(esk8_0,X1,esk11_0)=esk11_0|ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,esk11_0))|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(csr,[status(thm)],[357,255])).
% cnf(359,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,X1)|~relstr_set_smaller(esk8_0,esk9_0,esk6_3(esk8_0,X1,esk11_0))|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,X1,esk11_0))|~relstr_set_smaller(esk8_0,X1,esk11_0)|~element(esk5_3(esk8_0,X1,esk11_0),the_carrier(esk8_0))),inference(csr,[status(thm)],[358,159])).
% cnf(362,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[359,252,theory(equality)])).
% cnf(371,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|$false|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(rw,[status(thm)],[362,140,theory(equality)])).
% cnf(372,negated_conjecture,(ex_sup_of_relstr_set(esk8_0,esk9_0)|~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(cn,[status(thm)],[371,theory(equality)])).
% cnf(373,negated_conjecture,(~relstr_set_smaller(esk8_0,esk9_0,esk5_3(esk8_0,esk9_0,esk11_0))|~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(sr,[status(thm)],[372,138,theory(equality)])).
% cnf(376,negated_conjecture,(~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))|~element(esk6_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(spm,[status(thm)],[373,238,theory(equality)])).
% cnf(387,negated_conjecture,(~element(esk5_3(esk8_0,esk9_0,esk11_0),the_carrier(esk8_0))),inference(csr,[status(thm)],[376,268])).
% cnf(389,negated_conjecture,(esk6_3(esk8_0,esk9_0,esk11_0)=esk11_0|~relstr_set_smaller(esk8_0,esk9_0,esk11_0)|~element(esk11_0,the_carrier(esk8_0))),inference(spm,[status(thm)],[387,309,theory(equality)])).
% cnf(395,negated_conjecture,(esk6_3(esk8_0,esk9_0,esk11_0)=esk11_0|$false|~element(esk11_0,the_carrier(esk8_0))),inference(rw,[status(thm)],[389,140,theory(equality)])).
% cnf(396,negated_conjecture,(esk6_3(esk8_0,esk9_0,esk11_0)=esk11_0|$false|$false),inference(rw,[status(thm)],[395,139,theory(equality)])).
% cnf(397,negated_conjecture,(esk6_3(esk8_0,esk9_0,esk11_0)=esk11_0),inference(cn,[status(thm)],[396,theory(equality)])).
% cnf(398,negated_conjecture,($false),inference(sr,[status(thm)],[397,177,theory(equality)])).
% cnf(399,negated_conjecture,($false),398,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 76
% # ...of these trivial : 0
% # ...subsumed : 8
% # ...remaining for further processing: 68
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 5
% # Backward-rewritten : 0
% # Generated clauses : 100
% # ...of the previous two non-trivial : 85
% # Contextual simplify-reflections : 26
% # Paramodulations : 98
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 61
% # Positive orientable unit clauses: 7
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 51
% # Current number of unprocessed clauses: 38
% # ...number of literals in the above : 354
% # Clause-clause subsumption calls (NU) : 165
% # Rec. Clause-clause subsumption calls : 43
% # Unit Clause-clause subsumption calls : 17
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 4
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 58 leaves, 2.10+/-2.171 terms/leaf
% # Paramod-from index: 21 leaves, 1.29+/-0.881 terms/leaf
% # Paramod-into index: 49 leaves, 1.57+/-1.512 terms/leaf
% # -------------------------------------------------
% # User time : 0.022 s
% # System time : 0.002 s
% # Total time : 0.024 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.11 CPU 0.21 WC
% FINAL PrfWatch: 0.11 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP5752/SEU356+1.tptp
%
%------------------------------------------------------------------------------