%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU078+1 : TPTP v5.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art06.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 00:58:19 EST 2010
% Result : Theorem 31.81s
% Output : Solution 31.81s
% 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/SystemOnTPTP3449/SEU078+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP3449/SEU078+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP3449/SEU078+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 3545
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.93 CPU 2.02 WC
% PrfWatch: 3.92 CPU 4.03 WC
% PrfWatch: 5.92 CPU 6.03 WC
% PrfWatch: 7.82 CPU 8.09 WC
% PrfWatch: 9.41 CPU 10.10 WC
% PrfWatch: 11.19 CPU 12.11 WC
% PrfWatch: 13.18 CPU 14.11 WC
% PrfWatch: 15.16 CPU 16.12 WC
% PrfWatch: 17.15 CPU 18.12 WC
% # Preprocessing time : 0.016 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 19.13 CPU 20.13 WC
% PrfWatch: 21.12 CPU 22.13 WC
% PrfWatch: 23.11 CPU 24.14 WC
% PrfWatch: 25.10 CPU 26.14 WC
% PrfWatch: 27.10 CPU 28.15 WC
% PrfWatch: 29.09 CPU 30.15 WC
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:![X2]:subset(X1,X1),file('/tmp/SRASS.s.p', reflexivity_r1_tarski)).
% fof(6, axiom,![X1]:~(empty(singleton(X1))),file('/tmp/SRASS.s.p', fc2_subset_1)).
% fof(8, axiom,![X1]:((relation(X1)&function(X1))=>(![X2]:~((in(X2,relation_rng(X1))&![X3]:~(relation_inverse_image(X1,singleton(X2))=singleton(X3))))<=>one_to_one(X1))),file('/tmp/SRASS.s.p', t144_funct_1)).
% fof(12, axiom,![X1]:subset(empty_set,X1),file('/tmp/SRASS.s.p', t2_xboole_1)).
% fof(13, axiom,![X1]:![X2]:(subset(X1,singleton(X2))<=>(X1=empty_set|X1=singleton(X2))),file('/tmp/SRASS.s.p', t39_zfmisc_1)).
% fof(15, axiom,![X1]:![X2]:(X2=singleton(X1)<=>![X3]:(in(X3,X2)<=>X3=X1)),file('/tmp/SRASS.s.p', d1_tarski)).
% fof(18, axiom,![X1]:(empty(X1)=>X1=empty_set),file('/tmp/SRASS.s.p', t6_boole)).
% fof(23, axiom,![X1]:((relation(X1)&function(X1))=>![X2]:![X3]:(X3=relation_inverse_image(X1,X2)<=>![X4]:(in(X4,X3)<=>(in(X4,relation_dom(X1))&in(apply(X1,X4),X2))))),file('/tmp/SRASS.s.p', d13_funct_1)).
% fof(24, axiom,![X1]:((relation(X1)&function(X1))=>![X2]:(X2=relation_rng(X1)<=>![X3]:(in(X3,X2)<=>?[X4]:(in(X4,relation_dom(X1))&X3=apply(X1,X4))))),file('/tmp/SRASS.s.p', d5_funct_1)).
% fof(25, axiom,![X1]:?[X2]:element(X2,X1),file('/tmp/SRASS.s.p', existence_m1_subset_1)).
% fof(27, axiom,empty(empty_set),file('/tmp/SRASS.s.p', fc1_xboole_0)).
% fof(28, axiom,![X1]:![X2]:(disjoint(X1,X2)=>disjoint(X2,X1)),file('/tmp/SRASS.s.p', symmetry_r1_xboole_0)).
% fof(30, axiom,![X1]:![X2]:(relation(X2)=>(relation_inverse_image(X2,X1)=empty_set<=>disjoint(relation_rng(X2),X1))),file('/tmp/SRASS.s.p', t173_relat_1)).
% fof(31, axiom,![X1]:![X2]:(~(in(X1,X2))=>disjoint(singleton(X1),X2)),file('/tmp/SRASS.s.p', t56_zfmisc_1)).
% fof(32, axiom,![X1]:![X2]:~((in(X1,X2)&empty(X2))),file('/tmp/SRASS.s.p', t7_boole)).
% fof(38, axiom,![X1]:![X2]:![X3]:((in(X1,X2)&element(X2,powerset(X3)))=>element(X1,X3)),file('/tmp/SRASS.s.p', t4_subset)).
% fof(39, axiom,![X1]:![X2]:(element(X1,X2)=>(empty(X2)|in(X1,X2))),file('/tmp/SRASS.s.p', t2_subset)).
% fof(40, axiom,![X1]:![X2]:![X3]:~(((in(X1,X2)&element(X2,powerset(X3)))&empty(X3))),file('/tmp/SRASS.s.p', t5_subset)).
% fof(41, axiom,![X1]:(~(empty(X1))=>?[X2]:(element(X2,powerset(X1))&~(empty(X2)))),file('/tmp/SRASS.s.p', rc1_subset_1)).
% fof(42, axiom,![X1]:?[X2]:(element(X2,powerset(X1))&empty(X2)),file('/tmp/SRASS.s.p', rc2_subset_1)).
% fof(43, conjecture,![X1]:((relation(X1)&function(X1))=>(one_to_one(X1)<=>![X2]:?[X3]:subset(relation_inverse_image(X1,singleton(X2)),singleton(X3)))),file('/tmp/SRASS.s.p', t159_funct_1)).
% fof(44, negated_conjecture,~(![X1]:((relation(X1)&function(X1))=>(one_to_one(X1)<=>![X2]:?[X3]:subset(relation_inverse_image(X1,singleton(X2)),singleton(X3))))),inference(assume_negation,[status(cth)],[43])).
% fof(45, plain,![X1]:~(empty(singleton(X1))),inference(fof_simplification,[status(thm)],[6,theory(equality)])).
% fof(51, plain,![X1]:![X2]:(~(in(X1,X2))=>disjoint(singleton(X1),X2)),inference(fof_simplification,[status(thm)],[31,theory(equality)])).
% fof(53, plain,![X1]:(~(empty(X1))=>?[X2]:(element(X2,powerset(X1))&~(empty(X2)))),inference(fof_simplification,[status(thm)],[41,theory(equality)])).
% fof(63, plain,![X3]:![X4]:subset(X3,X3),inference(variable_rename,[status(thm)],[3])).
% cnf(64,plain,(subset(X1,X1)),inference(split_conjunct,[status(thm)],[63])).
% fof(76, plain,![X2]:~(empty(singleton(X2))),inference(variable_rename,[status(thm)],[45])).
% cnf(77,plain,(~empty(singleton(X1))),inference(split_conjunct,[status(thm)],[76])).
% fof(81, plain,![X1]:((~(relation(X1))|~(function(X1)))|((?[X2]:(in(X2,relation_rng(X1))&![X3]:~(relation_inverse_image(X1,singleton(X2))=singleton(X3)))|one_to_one(X1))&(~(one_to_one(X1))|![X2]:(~(in(X2,relation_rng(X1)))|?[X3]:relation_inverse_image(X1,singleton(X2))=singleton(X3))))),inference(fof_nnf,[status(thm)],[8])).
% fof(82, plain,![X4]:((~(relation(X4))|~(function(X4)))|((?[X5]:(in(X5,relation_rng(X4))&![X6]:~(relation_inverse_image(X4,singleton(X5))=singleton(X6)))|one_to_one(X4))&(~(one_to_one(X4))|![X7]:(~(in(X7,relation_rng(X4)))|?[X8]:relation_inverse_image(X4,singleton(X7))=singleton(X8))))),inference(variable_rename,[status(thm)],[81])).
% fof(83, plain,![X4]:((~(relation(X4))|~(function(X4)))|(((in(esk4_1(X4),relation_rng(X4))&![X6]:~(relation_inverse_image(X4,singleton(esk4_1(X4)))=singleton(X6)))|one_to_one(X4))&(~(one_to_one(X4))|![X7]:(~(in(X7,relation_rng(X4)))|relation_inverse_image(X4,singleton(X7))=singleton(esk5_2(X4,X7)))))),inference(skolemize,[status(esa)],[82])).
% fof(84, plain,![X4]:![X6]:![X7]:((((~(in(X7,relation_rng(X4)))|relation_inverse_image(X4,singleton(X7))=singleton(esk5_2(X4,X7)))|~(one_to_one(X4)))&((~(relation_inverse_image(X4,singleton(esk4_1(X4)))=singleton(X6))&in(esk4_1(X4),relation_rng(X4)))|one_to_one(X4)))|(~(relation(X4))|~(function(X4)))),inference(shift_quantors,[status(thm)],[83])).
% fof(85, plain,![X4]:![X6]:![X7]:((((~(in(X7,relation_rng(X4)))|relation_inverse_image(X4,singleton(X7))=singleton(esk5_2(X4,X7)))|~(one_to_one(X4)))|(~(relation(X4))|~(function(X4))))&(((~(relation_inverse_image(X4,singleton(esk4_1(X4)))=singleton(X6))|one_to_one(X4))|(~(relation(X4))|~(function(X4))))&((in(esk4_1(X4),relation_rng(X4))|one_to_one(X4))|(~(relation(X4))|~(function(X4)))))),inference(distribute,[status(thm)],[84])).
% cnf(86,plain,(one_to_one(X1)|in(esk4_1(X1),relation_rng(X1))|~function(X1)|~relation(X1)),inference(split_conjunct,[status(thm)],[85])).
% cnf(87,plain,(one_to_one(X1)|~function(X1)|~relation(X1)|relation_inverse_image(X1,singleton(esk4_1(X1)))!=singleton(X2)),inference(split_conjunct,[status(thm)],[85])).
% cnf(88,plain,(relation_inverse_image(X1,singleton(X2))=singleton(esk5_2(X1,X2))|~function(X1)|~relation(X1)|~one_to_one(X1)|~in(X2,relation_rng(X1))),inference(split_conjunct,[status(thm)],[85])).
% fof(100, plain,![X2]:subset(empty_set,X2),inference(variable_rename,[status(thm)],[12])).
% cnf(101,plain,(subset(empty_set,X1)),inference(split_conjunct,[status(thm)],[100])).
% fof(102, plain,![X1]:![X2]:((~(subset(X1,singleton(X2)))|(X1=empty_set|X1=singleton(X2)))&((~(X1=empty_set)&~(X1=singleton(X2)))|subset(X1,singleton(X2)))),inference(fof_nnf,[status(thm)],[13])).
% fof(103, plain,![X3]:![X4]:((~(subset(X3,singleton(X4)))|(X3=empty_set|X3=singleton(X4)))&((~(X3=empty_set)&~(X3=singleton(X4)))|subset(X3,singleton(X4)))),inference(variable_rename,[status(thm)],[102])).
% fof(104, plain,![X3]:![X4]:((~(subset(X3,singleton(X4)))|(X3=empty_set|X3=singleton(X4)))&((~(X3=empty_set)|subset(X3,singleton(X4)))&(~(X3=singleton(X4))|subset(X3,singleton(X4))))),inference(distribute,[status(thm)],[103])).
% cnf(107,plain,(X1=singleton(X2)|X1=empty_set|~subset(X1,singleton(X2))),inference(split_conjunct,[status(thm)],[104])).
% fof(111, plain,![X1]:![X2]:((~(X2=singleton(X1))|![X3]:((~(in(X3,X2))|X3=X1)&(~(X3=X1)|in(X3,X2))))&(?[X3]:((~(in(X3,X2))|~(X3=X1))&(in(X3,X2)|X3=X1))|X2=singleton(X1))),inference(fof_nnf,[status(thm)],[15])).
% fof(112, plain,![X4]:![X5]:((~(X5=singleton(X4))|![X6]:((~(in(X6,X5))|X6=X4)&(~(X6=X4)|in(X6,X5))))&(?[X7]:((~(in(X7,X5))|~(X7=X4))&(in(X7,X5)|X7=X4))|X5=singleton(X4))),inference(variable_rename,[status(thm)],[111])).
% fof(113, plain,![X4]:![X5]:((~(X5=singleton(X4))|![X6]:((~(in(X6,X5))|X6=X4)&(~(X6=X4)|in(X6,X5))))&(((~(in(esk8_2(X4,X5),X5))|~(esk8_2(X4,X5)=X4))&(in(esk8_2(X4,X5),X5)|esk8_2(X4,X5)=X4))|X5=singleton(X4))),inference(skolemize,[status(esa)],[112])).
% fof(114, plain,![X4]:![X5]:![X6]:((((~(in(X6,X5))|X6=X4)&(~(X6=X4)|in(X6,X5)))|~(X5=singleton(X4)))&(((~(in(esk8_2(X4,X5),X5))|~(esk8_2(X4,X5)=X4))&(in(esk8_2(X4,X5),X5)|esk8_2(X4,X5)=X4))|X5=singleton(X4))),inference(shift_quantors,[status(thm)],[113])).
% fof(115, plain,![X4]:![X5]:![X6]:((((~(in(X6,X5))|X6=X4)|~(X5=singleton(X4)))&((~(X6=X4)|in(X6,X5))|~(X5=singleton(X4))))&(((~(in(esk8_2(X4,X5),X5))|~(esk8_2(X4,X5)=X4))|X5=singleton(X4))&((in(esk8_2(X4,X5),X5)|esk8_2(X4,X5)=X4)|X5=singleton(X4)))),inference(distribute,[status(thm)],[114])).
% cnf(118,plain,(in(X3,X1)|X1!=singleton(X2)|X3!=X2),inference(split_conjunct,[status(thm)],[115])).
% cnf(119,plain,(X3=X2|X1!=singleton(X2)|~in(X3,X1)),inference(split_conjunct,[status(thm)],[115])).
% fof(126, plain,![X1]:(~(empty(X1))|X1=empty_set),inference(fof_nnf,[status(thm)],[18])).
% fof(127, plain,![X2]:(~(empty(X2))|X2=empty_set),inference(variable_rename,[status(thm)],[126])).
% cnf(128,plain,(X1=empty_set|~empty(X1)),inference(split_conjunct,[status(thm)],[127])).
% fof(145, plain,![X1]:((~(relation(X1))|~(function(X1)))|![X2]:![X3]:((~(X3=relation_inverse_image(X1,X2))|![X4]:((~(in(X4,X3))|(in(X4,relation_dom(X1))&in(apply(X1,X4),X2)))&((~(in(X4,relation_dom(X1)))|~(in(apply(X1,X4),X2)))|in(X4,X3))))&(?[X4]:((~(in(X4,X3))|(~(in(X4,relation_dom(X1)))|~(in(apply(X1,X4),X2))))&(in(X4,X3)|(in(X4,relation_dom(X1))&in(apply(X1,X4),X2))))|X3=relation_inverse_image(X1,X2)))),inference(fof_nnf,[status(thm)],[23])).
% fof(146, plain,![X5]:((~(relation(X5))|~(function(X5)))|![X6]:![X7]:((~(X7=relation_inverse_image(X5,X6))|![X8]:((~(in(X8,X7))|(in(X8,relation_dom(X5))&in(apply(X5,X8),X6)))&((~(in(X8,relation_dom(X5)))|~(in(apply(X5,X8),X6)))|in(X8,X7))))&(?[X9]:((~(in(X9,X7))|(~(in(X9,relation_dom(X5)))|~(in(apply(X5,X9),X6))))&(in(X9,X7)|(in(X9,relation_dom(X5))&in(apply(X5,X9),X6))))|X7=relation_inverse_image(X5,X6)))),inference(variable_rename,[status(thm)],[145])).
% fof(147, plain,![X5]:((~(relation(X5))|~(function(X5)))|![X6]:![X7]:((~(X7=relation_inverse_image(X5,X6))|![X8]:((~(in(X8,X7))|(in(X8,relation_dom(X5))&in(apply(X5,X8),X6)))&((~(in(X8,relation_dom(X5)))|~(in(apply(X5,X8),X6)))|in(X8,X7))))&(((~(in(esk12_3(X5,X6,X7),X7))|(~(in(esk12_3(X5,X6,X7),relation_dom(X5)))|~(in(apply(X5,esk12_3(X5,X6,X7)),X6))))&(in(esk12_3(X5,X6,X7),X7)|(in(esk12_3(X5,X6,X7),relation_dom(X5))&in(apply(X5,esk12_3(X5,X6,X7)),X6))))|X7=relation_inverse_image(X5,X6)))),inference(skolemize,[status(esa)],[146])).
% fof(148, plain,![X5]:![X6]:![X7]:![X8]:(((((~(in(X8,X7))|(in(X8,relation_dom(X5))&in(apply(X5,X8),X6)))&((~(in(X8,relation_dom(X5)))|~(in(apply(X5,X8),X6)))|in(X8,X7)))|~(X7=relation_inverse_image(X5,X6)))&(((~(in(esk12_3(X5,X6,X7),X7))|(~(in(esk12_3(X5,X6,X7),relation_dom(X5)))|~(in(apply(X5,esk12_3(X5,X6,X7)),X6))))&(in(esk12_3(X5,X6,X7),X7)|(in(esk12_3(X5,X6,X7),relation_dom(X5))&in(apply(X5,esk12_3(X5,X6,X7)),X6))))|X7=relation_inverse_image(X5,X6)))|(~(relation(X5))|~(function(X5)))),inference(shift_quantors,[status(thm)],[147])).
% fof(149, plain,![X5]:![X6]:![X7]:![X8]:((((((in(X8,relation_dom(X5))|~(in(X8,X7)))|~(X7=relation_inverse_image(X5,X6)))|(~(relation(X5))|~(function(X5))))&(((in(apply(X5,X8),X6)|~(in(X8,X7)))|~(X7=relation_inverse_image(X5,X6)))|(~(relation(X5))|~(function(X5)))))&((((~(in(X8,relation_dom(X5)))|~(in(apply(X5,X8),X6)))|in(X8,X7))|~(X7=relation_inverse_image(X5,X6)))|(~(relation(X5))|~(function(X5)))))&((((~(in(esk12_3(X5,X6,X7),X7))|(~(in(esk12_3(X5,X6,X7),relation_dom(X5)))|~(in(apply(X5,esk12_3(X5,X6,X7)),X6))))|X7=relation_inverse_image(X5,X6))|(~(relation(X5))|~(function(X5))))&((((in(esk12_3(X5,X6,X7),relation_dom(X5))|in(esk12_3(X5,X6,X7),X7))|X7=relation_inverse_image(X5,X6))|(~(relation(X5))|~(function(X5))))&(((in(apply(X5,esk12_3(X5,X6,X7)),X6)|in(esk12_3(X5,X6,X7),X7))|X7=relation_inverse_image(X5,X6))|(~(relation(X5))|~(function(X5))))))),inference(distribute,[status(thm)],[148])).
% cnf(153,plain,(in(X4,X2)|~function(X1)|~relation(X1)|X2!=relation_inverse_image(X1,X3)|~in(apply(X1,X4),X3)|~in(X4,relation_dom(X1))),inference(split_conjunct,[status(thm)],[149])).
% fof(156, plain,![X1]:((~(relation(X1))|~(function(X1)))|![X2]:((~(X2=relation_rng(X1))|![X3]:((~(in(X3,X2))|?[X4]:(in(X4,relation_dom(X1))&X3=apply(X1,X4)))&(![X4]:(~(in(X4,relation_dom(X1)))|~(X3=apply(X1,X4)))|in(X3,X2))))&(?[X3]:((~(in(X3,X2))|![X4]:(~(in(X4,relation_dom(X1)))|~(X3=apply(X1,X4))))&(in(X3,X2)|?[X4]:(in(X4,relation_dom(X1))&X3=apply(X1,X4))))|X2=relation_rng(X1)))),inference(fof_nnf,[status(thm)],[24])).
% fof(157, plain,![X5]:((~(relation(X5))|~(function(X5)))|![X6]:((~(X6=relation_rng(X5))|![X7]:((~(in(X7,X6))|?[X8]:(in(X8,relation_dom(X5))&X7=apply(X5,X8)))&(![X9]:(~(in(X9,relation_dom(X5)))|~(X7=apply(X5,X9)))|in(X7,X6))))&(?[X10]:((~(in(X10,X6))|![X11]:(~(in(X11,relation_dom(X5)))|~(X10=apply(X5,X11))))&(in(X10,X6)|?[X12]:(in(X12,relation_dom(X5))&X10=apply(X5,X12))))|X6=relation_rng(X5)))),inference(variable_rename,[status(thm)],[156])).
% fof(158, plain,![X5]:((~(relation(X5))|~(function(X5)))|![X6]:((~(X6=relation_rng(X5))|![X7]:((~(in(X7,X6))|(in(esk13_3(X5,X6,X7),relation_dom(X5))&X7=apply(X5,esk13_3(X5,X6,X7))))&(![X9]:(~(in(X9,relation_dom(X5)))|~(X7=apply(X5,X9)))|in(X7,X6))))&(((~(in(esk14_2(X5,X6),X6))|![X11]:(~(in(X11,relation_dom(X5)))|~(esk14_2(X5,X6)=apply(X5,X11))))&(in(esk14_2(X5,X6),X6)|(in(esk15_2(X5,X6),relation_dom(X5))&esk14_2(X5,X6)=apply(X5,esk15_2(X5,X6)))))|X6=relation_rng(X5)))),inference(skolemize,[status(esa)],[157])).
% fof(159, plain,![X5]:![X6]:![X7]:![X9]:![X11]:((((((~(in(X11,relation_dom(X5)))|~(esk14_2(X5,X6)=apply(X5,X11)))|~(in(esk14_2(X5,X6),X6)))&(in(esk14_2(X5,X6),X6)|(in(esk15_2(X5,X6),relation_dom(X5))&esk14_2(X5,X6)=apply(X5,esk15_2(X5,X6)))))|X6=relation_rng(X5))&((((~(in(X9,relation_dom(X5)))|~(X7=apply(X5,X9)))|in(X7,X6))&(~(in(X7,X6))|(in(esk13_3(X5,X6,X7),relation_dom(X5))&X7=apply(X5,esk13_3(X5,X6,X7)))))|~(X6=relation_rng(X5))))|(~(relation(X5))|~(function(X5)))),inference(shift_quantors,[status(thm)],[158])).
% fof(160, plain,![X5]:![X6]:![X7]:![X9]:![X11]:((((((~(in(X11,relation_dom(X5)))|~(esk14_2(X5,X6)=apply(X5,X11)))|~(in(esk14_2(X5,X6),X6)))|X6=relation_rng(X5))|(~(relation(X5))|~(function(X5))))&((((in(esk15_2(X5,X6),relation_dom(X5))|in(esk14_2(X5,X6),X6))|X6=relation_rng(X5))|(~(relation(X5))|~(function(X5))))&(((esk14_2(X5,X6)=apply(X5,esk15_2(X5,X6))|in(esk14_2(X5,X6),X6))|X6=relation_rng(X5))|(~(relation(X5))|~(function(X5))))))&(((((~(in(X9,relation_dom(X5)))|~(X7=apply(X5,X9)))|in(X7,X6))|~(X6=relation_rng(X5)))|(~(relation(X5))|~(function(X5))))&((((in(esk13_3(X5,X6,X7),relation_dom(X5))|~(in(X7,X6)))|~(X6=relation_rng(X5)))|(~(relation(X5))|~(function(X5))))&(((X7=apply(X5,esk13_3(X5,X6,X7))|~(in(X7,X6)))|~(X6=relation_rng(X5)))|(~(relation(X5))|~(function(X5))))))),inference(distribute,[status(thm)],[159])).
% cnf(161,plain,(X3=apply(X1,esk13_3(X1,X2,X3))|~function(X1)|~relation(X1)|X2!=relation_rng(X1)|~in(X3,X2)),inference(split_conjunct,[status(thm)],[160])).
% cnf(162,plain,(in(esk13_3(X1,X2,X3),relation_dom(X1))|~function(X1)|~relation(X1)|X2!=relation_rng(X1)|~in(X3,X2)),inference(split_conjunct,[status(thm)],[160])).
% fof(167, plain,![X3]:?[X4]:element(X4,X3),inference(variable_rename,[status(thm)],[25])).
% fof(168, plain,![X3]:element(esk16_1(X3),X3),inference(skolemize,[status(esa)],[167])).
% cnf(169,plain,(element(esk16_1(X1),X1)),inference(split_conjunct,[status(thm)],[168])).
% cnf(172,plain,(empty(empty_set)),inference(split_conjunct,[status(thm)],[27])).
% fof(173, plain,![X1]:![X2]:(~(disjoint(X1,X2))|disjoint(X2,X1)),inference(fof_nnf,[status(thm)],[28])).
% fof(174, plain,![X3]:![X4]:(~(disjoint(X3,X4))|disjoint(X4,X3)),inference(variable_rename,[status(thm)],[173])).
% cnf(175,plain,(disjoint(X1,X2)|~disjoint(X2,X1)),inference(split_conjunct,[status(thm)],[174])).
% fof(179, plain,![X1]:![X2]:(~(relation(X2))|((~(relation_inverse_image(X2,X1)=empty_set)|disjoint(relation_rng(X2),X1))&(~(disjoint(relation_rng(X2),X1))|relation_inverse_image(X2,X1)=empty_set))),inference(fof_nnf,[status(thm)],[30])).
% fof(180, plain,![X3]:![X4]:(~(relation(X4))|((~(relation_inverse_image(X4,X3)=empty_set)|disjoint(relation_rng(X4),X3))&(~(disjoint(relation_rng(X4),X3))|relation_inverse_image(X4,X3)=empty_set))),inference(variable_rename,[status(thm)],[179])).
% fof(181, plain,![X3]:![X4]:(((~(relation_inverse_image(X4,X3)=empty_set)|disjoint(relation_rng(X4),X3))|~(relation(X4)))&((~(disjoint(relation_rng(X4),X3))|relation_inverse_image(X4,X3)=empty_set)|~(relation(X4)))),inference(distribute,[status(thm)],[180])).
% cnf(182,plain,(relation_inverse_image(X1,X2)=empty_set|~relation(X1)|~disjoint(relation_rng(X1),X2)),inference(split_conjunct,[status(thm)],[181])).
% fof(184, plain,![X1]:![X2]:(in(X1,X2)|disjoint(singleton(X1),X2)),inference(fof_nnf,[status(thm)],[51])).
% fof(185, plain,![X3]:![X4]:(in(X3,X4)|disjoint(singleton(X3),X4)),inference(variable_rename,[status(thm)],[184])).
% cnf(186,plain,(disjoint(singleton(X1),X2)|in(X1,X2)),inference(split_conjunct,[status(thm)],[185])).
% fof(187, plain,![X1]:![X2]:(~(in(X1,X2))|~(empty(X2))),inference(fof_nnf,[status(thm)],[32])).
% fof(188, plain,![X3]:![X4]:(~(in(X3,X4))|~(empty(X4))),inference(variable_rename,[status(thm)],[187])).
% cnf(189,plain,(~empty(X1)|~in(X2,X1)),inference(split_conjunct,[status(thm)],[188])).
% fof(206, plain,![X1]:![X2]:![X3]:((~(in(X1,X2))|~(element(X2,powerset(X3))))|element(X1,X3)),inference(fof_nnf,[status(thm)],[38])).
% fof(207, plain,![X4]:![X5]:![X6]:((~(in(X4,X5))|~(element(X5,powerset(X6))))|element(X4,X6)),inference(variable_rename,[status(thm)],[206])).
% cnf(208,plain,(element(X1,X2)|~element(X3,powerset(X2))|~in(X1,X3)),inference(split_conjunct,[status(thm)],[207])).
% fof(209, plain,![X1]:![X2]:(~(element(X1,X2))|(empty(X2)|in(X1,X2))),inference(fof_nnf,[status(thm)],[39])).
% fof(210, plain,![X3]:![X4]:(~(element(X3,X4))|(empty(X4)|in(X3,X4))),inference(variable_rename,[status(thm)],[209])).
% cnf(211,plain,(in(X1,X2)|empty(X2)|~element(X1,X2)),inference(split_conjunct,[status(thm)],[210])).
% fof(212, plain,![X1]:![X2]:![X3]:((~(in(X1,X2))|~(element(X2,powerset(X3))))|~(empty(X3))),inference(fof_nnf,[status(thm)],[40])).
% fof(213, plain,![X4]:![X5]:![X6]:((~(in(X4,X5))|~(element(X5,powerset(X6))))|~(empty(X6))),inference(variable_rename,[status(thm)],[212])).
% cnf(214,plain,(~empty(X1)|~element(X2,powerset(X1))|~in(X3,X2)),inference(split_conjunct,[status(thm)],[213])).
% fof(215, plain,![X1]:(empty(X1)|?[X2]:(element(X2,powerset(X1))&~(empty(X2)))),inference(fof_nnf,[status(thm)],[53])).
% fof(216, plain,![X3]:(empty(X3)|?[X4]:(element(X4,powerset(X3))&~(empty(X4)))),inference(variable_rename,[status(thm)],[215])).
% fof(217, plain,![X3]:(empty(X3)|(element(esk17_1(X3),powerset(X3))&~(empty(esk17_1(X3))))),inference(skolemize,[status(esa)],[216])).
% fof(218, plain,![X3]:((element(esk17_1(X3),powerset(X3))|empty(X3))&(~(empty(esk17_1(X3)))|empty(X3))),inference(distribute,[status(thm)],[217])).
% cnf(219,plain,(empty(X1)|~empty(esk17_1(X1))),inference(split_conjunct,[status(thm)],[218])).
% cnf(220,plain,(empty(X1)|element(esk17_1(X1),powerset(X1))),inference(split_conjunct,[status(thm)],[218])).
% fof(221, plain,![X3]:?[X4]:(element(X4,powerset(X3))&empty(X4)),inference(variable_rename,[status(thm)],[42])).
% fof(222, plain,![X3]:(element(esk18_1(X3),powerset(X3))&empty(esk18_1(X3))),inference(skolemize,[status(esa)],[221])).
% cnf(223,plain,(empty(esk18_1(X1))),inference(split_conjunct,[status(thm)],[222])).
% cnf(224,plain,(element(esk18_1(X1),powerset(X1))),inference(split_conjunct,[status(thm)],[222])).
% fof(225, negated_conjecture,?[X1]:((relation(X1)&function(X1))&((~(one_to_one(X1))|?[X2]:![X3]:~(subset(relation_inverse_image(X1,singleton(X2)),singleton(X3))))&(one_to_one(X1)|![X2]:?[X3]:subset(relation_inverse_image(X1,singleton(X2)),singleton(X3))))),inference(fof_nnf,[status(thm)],[44])).
% fof(226, negated_conjecture,?[X4]:((relation(X4)&function(X4))&((~(one_to_one(X4))|?[X5]:![X6]:~(subset(relation_inverse_image(X4,singleton(X5)),singleton(X6))))&(one_to_one(X4)|![X7]:?[X8]:subset(relation_inverse_image(X4,singleton(X7)),singleton(X8))))),inference(variable_rename,[status(thm)],[225])).
% fof(227, negated_conjecture,((relation(esk19_0)&function(esk19_0))&((~(one_to_one(esk19_0))|![X6]:~(subset(relation_inverse_image(esk19_0,singleton(esk20_0)),singleton(X6))))&(one_to_one(esk19_0)|![X7]:subset(relation_inverse_image(esk19_0,singleton(X7)),singleton(esk21_1(X7)))))),inference(skolemize,[status(esa)],[226])).
% fof(228, negated_conjecture,![X6]:![X7]:(((subset(relation_inverse_image(esk19_0,singleton(X7)),singleton(esk21_1(X7)))|one_to_one(esk19_0))&(~(subset(relation_inverse_image(esk19_0,singleton(esk20_0)),singleton(X6)))|~(one_to_one(esk19_0))))&(relation(esk19_0)&function(esk19_0))),inference(shift_quantors,[status(thm)],[227])).
% cnf(229,negated_conjecture,(function(esk19_0)),inference(split_conjunct,[status(thm)],[228])).
% cnf(230,negated_conjecture,(relation(esk19_0)),inference(split_conjunct,[status(thm)],[228])).
% cnf(231,negated_conjecture,(~one_to_one(esk19_0)|~subset(relation_inverse_image(esk19_0,singleton(esk20_0)),singleton(X1))),inference(split_conjunct,[status(thm)],[228])).
% cnf(232,negated_conjecture,(one_to_one(esk19_0)|subset(relation_inverse_image(esk19_0,singleton(X1)),singleton(esk21_1(X1)))),inference(split_conjunct,[status(thm)],[228])).
% cnf(238,plain,(in(X1,X2)|singleton(X1)!=X2),inference(er,[status(thm)],[118,theory(equality)])).
% cnf(239,plain,(empty_set=esk18_1(X1)),inference(spm,[status(thm)],[128,223,theory(equality)])).
% cnf(249,plain,(~empty(X2)|singleton(X1)!=X2),inference(spm,[status(thm)],[189,238,theory(equality)])).
% cnf(263,plain,(disjoint(X1,singleton(X2))|in(X2,X1)),inference(spm,[status(thm)],[175,186,theory(equality)])).
% cnf(269,plain,(in(esk16_1(X1),X1)|empty(X1)),inference(spm,[status(thm)],[211,169,theory(equality)])).
% cnf(293,plain,(element(X1,X2)|empty(X2)|~in(X1,esk17_1(X2))),inference(spm,[status(thm)],[208,220,theory(equality)])).
% cnf(297,negated_conjecture,(~subset(singleton(esk5_2(esk19_0,esk20_0)),singleton(X1))|~one_to_one(esk19_0)|~in(esk20_0,relation_rng(esk19_0))|~function(esk19_0)|~relation(esk19_0)),inference(spm,[status(thm)],[231,88,theory(equality)])).
% cnf(300,negated_conjecture,(~subset(singleton(esk5_2(esk19_0,esk20_0)),singleton(X1))|~one_to_one(esk19_0)|~in(esk20_0,relation_rng(esk19_0))|$false|~relation(esk19_0)),inference(rw,[status(thm)],[297,229,theory(equality)])).
% cnf(301,negated_conjecture,(~subset(singleton(esk5_2(esk19_0,esk20_0)),singleton(X1))|~one_to_one(esk19_0)|~in(esk20_0,relation_rng(esk19_0))|$false|$false),inference(rw,[status(thm)],[300,230,theory(equality)])).
% cnf(302,negated_conjecture,(~subset(singleton(esk5_2(esk19_0,esk20_0)),singleton(X1))|~one_to_one(esk19_0)|~in(esk20_0,relation_rng(esk19_0))),inference(cn,[status(thm)],[301,theory(equality)])).
% cnf(313,plain,(in(esk13_3(X1,X2,X3),X4)|relation_inverse_image(X1,X5)!=X4|~in(X3,X5)|~in(esk13_3(X1,X2,X3),relation_dom(X1))|~function(X1)|~relation(X1)|relation_rng(X1)!=X2|~in(X3,X2)),inference(spm,[status(thm)],[153,161,theory(equality)])).
% cnf(399,plain,(element(empty_set,powerset(X1))),inference(rw,[status(thm)],[224,239,theory(equality)])).
% cnf(404,plain,(~in(X2,empty_set)|~empty(X1)),inference(spm,[status(thm)],[214,399,theory(equality)])).
% cnf(484,plain,(relation_inverse_image(X1,singleton(X2))=empty_set|in(X2,relation_rng(X1))|~relation(X1)),inference(spm,[status(thm)],[182,263,theory(equality)])).
% fof(492, plain,(~(epred1_0)<=>![X2]:~(in(X2,empty_set))),introduced(definition),['split']).
% cnf(493,plain,(epred1_0|~in(X2,empty_set)),inference(split_equiv,[status(thm)],[492])).
% fof(494, plain,(~(epred2_0)<=>![X1]:~(empty(X1))),introduced(definition),['split']).
% cnf(495,plain,(epred2_0|~empty(X1)),inference(split_equiv,[status(thm)],[494])).
% cnf(496,plain,(~epred2_0|~epred1_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[404,492,theory(equality)]),494,theory(equality)]),['split']).
% cnf(501,plain,(epred2_0),inference(spm,[status(thm)],[495,172,theory(equality)])).
% cnf(503,plain,($false|~epred1_0),inference(rw,[status(thm)],[496,501,theory(equality)])).
% cnf(504,plain,(~epred1_0),inference(cn,[status(thm)],[503,theory(equality)])).
% cnf(506,plain,(~in(X2,empty_set)),inference(sr,[status(thm)],[493,504,theory(equality)])).
% cnf(683,plain,(element(esk16_1(esk17_1(X1)),X1)|empty(X1)|empty(esk17_1(X1))),inference(spm,[status(thm)],[293,269,theory(equality)])).
% cnf(687,negated_conjecture,(in(esk20_0,relation_rng(esk19_0))|~subset(empty_set,singleton(X1))|~one_to_one(esk19_0)|~relation(esk19_0)),inference(spm,[status(thm)],[231,484,theory(equality)])).
% cnf(696,negated_conjecture,(in(esk20_0,relation_rng(esk19_0))|$false|~one_to_one(esk19_0)|~relation(esk19_0)),inference(rw,[status(thm)],[687,101,theory(equality)])).
% cnf(697,negated_conjecture,(in(esk20_0,relation_rng(esk19_0))|$false|~one_to_one(esk19_0)|$false),inference(rw,[status(thm)],[696,230,theory(equality)])).
% cnf(698,negated_conjecture,(in(esk20_0,relation_rng(esk19_0))|~one_to_one(esk19_0)),inference(cn,[status(thm)],[697,theory(equality)])).
% cnf(785,negated_conjecture,(~subset(singleton(esk5_2(esk19_0,esk20_0)),singleton(X1))|~one_to_one(esk19_0)),inference(csr,[status(thm)],[302,698])).
% cnf(786,negated_conjecture,(~one_to_one(esk19_0)),inference(spm,[status(thm)],[785,64,theory(equality)])).
% cnf(791,negated_conjecture,(subset(relation_inverse_image(esk19_0,singleton(X1)),singleton(esk21_1(X1)))),inference(sr,[status(thm)],[232,786,theory(equality)])).
% cnf(797,negated_conjecture,(singleton(esk21_1(X1))=relation_inverse_image(esk19_0,singleton(X1))|empty_set=relation_inverse_image(esk19_0,singleton(X1))),inference(spm,[status(thm)],[107,791,theory(equality)])).
% cnf(812,negated_conjecture,(one_to_one(esk19_0)|relation_inverse_image(esk19_0,singleton(esk4_1(esk19_0)))=empty_set|singleton(esk21_1(esk4_1(esk19_0)))!=singleton(X1)|~function(esk19_0)|~relation(esk19_0)),inference(spm,[status(thm)],[87,797,theory(equality)])).
% cnf(827,negated_conjecture,(one_to_one(esk19_0)|relation_inverse_image(esk19_0,singleton(esk4_1(esk19_0)))=empty_set|singleton(esk21_1(esk4_1(esk19_0)))!=singleton(X1)|$false|~relation(esk19_0)),inference(rw,[status(thm)],[812,229,theory(equality)])).
% cnf(828,negated_conjecture,(one_to_one(esk19_0)|relation_inverse_image(esk19_0,singleton(esk4_1(esk19_0)))=empty_set|singleton(esk21_1(esk4_1(esk19_0)))!=singleton(X1)|$false|$false),inference(rw,[status(thm)],[827,230,theory(equality)])).
% cnf(829,negated_conjecture,(one_to_one(esk19_0)|relation_inverse_image(esk19_0,singleton(esk4_1(esk19_0)))=empty_set|singleton(esk21_1(esk4_1(esk19_0)))!=singleton(X1)),inference(cn,[status(thm)],[828,theory(equality)])).
% cnf(830,negated_conjecture,(relation_inverse_image(esk19_0,singleton(esk4_1(esk19_0)))=empty_set|singleton(esk21_1(esk4_1(esk19_0)))!=singleton(X1)),inference(sr,[status(thm)],[829,786,theory(equality)])).
% cnf(991,plain,(in(esk13_3(X1,X2,X3),X4)|relation_inverse_image(X1,X5)!=X4|relation_rng(X1)!=X2|~in(X3,X2)|~in(X3,X5)|~function(X1)|~relation(X1)),inference(csr,[status(thm)],[313,162])).
% cnf(992,plain,(in(esk13_3(X1,X2,X3),relation_inverse_image(X1,X4))|relation_rng(X1)!=X2|~in(X3,X4)|~in(X3,X2)|~function(X1)|~relation(X1)),inference(er,[status(thm)],[991,theory(equality)])).
% cnf(4223,plain,(element(esk16_1(esk17_1(X1)),X1)|empty(X1)),inference(csr,[status(thm)],[683,219])).
% cnf(4227,plain,(in(esk16_1(esk17_1(X1)),X1)|empty(X1)),inference(spm,[status(thm)],[211,4223,theory(equality)])).
% cnf(4508,plain,(X1=esk16_1(esk17_1(X2))|empty(X2)|singleton(X1)!=X2),inference(spm,[status(thm)],[119,4227,theory(equality)])).
% cnf(5353,negated_conjecture,(relation_inverse_image(esk19_0,singleton(esk4_1(esk19_0)))=empty_set),inference(er,[status(thm)],[830,theory(equality)])).
% cnf(8873,negated_conjecture,(in(esk13_3(esk19_0,X1,X2),empty_set)|relation_rng(esk19_0)!=X1|~in(X2,singleton(esk4_1(esk19_0)))|~in(X2,X1)|~function(esk19_0)|~relation(esk19_0)),inference(spm,[status(thm)],[992,5353,theory(equality)])).
% cnf(8904,negated_conjecture,(in(esk13_3(esk19_0,X1,X2),empty_set)|relation_rng(esk19_0)!=X1|~in(X2,singleton(esk4_1(esk19_0)))|~in(X2,X1)|$false|~relation(esk19_0)),inference(rw,[status(thm)],[8873,229,theory(equality)])).
% cnf(8905,negated_conjecture,(in(esk13_3(esk19_0,X1,X2),empty_set)|relation_rng(esk19_0)!=X1|~in(X2,singleton(esk4_1(esk19_0)))|~in(X2,X1)|$false|$false),inference(rw,[status(thm)],[8904,230,theory(equality)])).
% cnf(8906,negated_conjecture,(in(esk13_3(esk19_0,X1,X2),empty_set)|relation_rng(esk19_0)!=X1|~in(X2,singleton(esk4_1(esk19_0)))|~in(X2,X1)),inference(cn,[status(thm)],[8905,theory(equality)])).
% cnf(8907,negated_conjecture,(relation_rng(esk19_0)!=X1|~in(X2,singleton(esk4_1(esk19_0)))|~in(X2,X1)),inference(sr,[status(thm)],[8906,506,theory(equality)])).
% cnf(216980,plain,(X1=esk16_1(esk17_1(X2))|singleton(X1)!=X2),inference(csr,[status(thm)],[4508,249])).
% cnf(216981,plain,(X1=esk16_1(esk17_1(singleton(X1)))),inference(er,[status(thm)],[216980,theory(equality)])).
% cnf(865700,negated_conjecture,(empty(singleton(esk4_1(esk19_0)))|relation_rng(esk19_0)!=X1|~in(esk16_1(esk17_1(singleton(esk4_1(esk19_0)))),X1)),inference(spm,[status(thm)],[8907,4227,theory(equality)])).
% cnf(865861,negated_conjecture,(empty(singleton(esk4_1(esk19_0)))|relation_rng(esk19_0)!=X1|~in(esk4_1(esk19_0),X1)),inference(rw,[status(thm)],[865700,216981,theory(equality)])).
% cnf(865862,negated_conjecture,(relation_rng(esk19_0)!=X1|~in(esk4_1(esk19_0),X1)),inference(sr,[status(thm)],[865861,77,theory(equality)])).
% cnf(865910,negated_conjecture,(one_to_one(esk19_0)|~function(esk19_0)|~relation(esk19_0)),inference(spm,[status(thm)],[865862,86,theory(equality)])).
% cnf(865911,negated_conjecture,(one_to_one(esk19_0)|$false|~relation(esk19_0)),inference(rw,[status(thm)],[865910,229,theory(equality)])).
% cnf(865912,negated_conjecture,(one_to_one(esk19_0)|$false|$false),inference(rw,[status(thm)],[865911,230,theory(equality)])).
% cnf(865913,negated_conjecture,(one_to_one(esk19_0)),inference(cn,[status(thm)],[865912,theory(equality)])).
% cnf(865914,negated_conjecture,($false),inference(sr,[status(thm)],[865913,786,theory(equality)])).
% cnf(865915,negated_conjecture,($false),865914,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 24680
% # ...of these trivial : 38
% # ...subsumed : 21381
% # ...remaining for further processing: 3261
% # Other redundant clauses eliminated : 10
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 127
% # Backward-rewritten : 119
% # Generated clauses : 370091
% # ...of the previous two non-trivial : 314334
% # Contextual simplify-reflections : 15068
% # Paramodulations : 369650
% # Factorizations : 24
% # Equation resolutions : 276
% # Current number of processed clauses: 2873
% # Positive orientable unit clauses: 111
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 76
% # Non-unit-clauses : 2686
% # Current number of unprocessed clauses: 282073
% # ...number of literals in the above : 1535808
% # Clause-clause subsumption calls (NU) : 278965
% # Rec. Clause-clause subsumption calls : 215725
% # Unit Clause-clause subsumption calls : 7528
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 136
% # Indexed BW rewrite successes : 76
% # Backwards rewriting index: 1485 leaves, 1.87+/-2.736 terms/leaf
% # Paramod-from index: 565 leaves, 1.56+/-2.126 terms/leaf
% # Paramod-into index: 1190 leaves, 1.77+/-2.375 terms/leaf
% # -------------------------------------------------
% # User time : 16.958 s
% # System time : 0.675 s
% # Total time : 17.633 s
% # Maximum resident set size: 0 pages
% PrfWatch: 30.89 CPU 31.97 WC
% FINAL PrfWatch: 30.89 CPU 31.97 WC
% SZS output end Solution for /tmp/SystemOnTPTP3449/SEU078+1.tptp
%
%------------------------------------------------------------------------------