%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SET675+3 : TPTP v5.0.0. Released v2.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art03.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 : Wed Dec 29 23:27:26 EST 2010
% Result : Theorem 0.97s
% Output : Solution 0.97s
% 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/SystemOnTPTP11010/SET675+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP11010/SET675+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP11010/SET675+3.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 11106
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.019 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>(image4(X1,X2,X3,X1)=range(X1,X2,X3)&inverse4(X1,X2,X3,X2)=domain(X1,X2,X3))))),file('/tmp/SRASS.s.p', p3)).
% fof(3, axiom,![X1]:ilf_type(X1,set_type),file('/tmp/SRASS.s.p', p35)).
% fof(4, axiom,![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>domain(X1,X2,X3)=domain_of(X3)))),file('/tmp/SRASS.s.p', p27)).
% fof(5, axiom,![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>range(X1,X2,X3)=range_of(X3)))),file('/tmp/SRASS.s.p', p29)).
% fof(6, axiom,![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>![X4]:(ilf_type(X4,set_type)=>image4(X1,X2,X3,X4)=image(X3,X4))))),file('/tmp/SRASS.s.p', p31)).
% fof(7, axiom,![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X1,X2))=>![X4]:(ilf_type(X4,set_type)=>inverse4(X1,X2,X3,X4)=inverse2(X3,X4))))),file('/tmp/SRASS.s.p', p33)).
% fof(18, axiom,![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(![X3]:(ilf_type(X3,subset_type(cross_product(X1,X2)))=>ilf_type(X3,relation_type(X1,X2)))&![X4]:(ilf_type(X4,relation_type(X1,X2))=>ilf_type(X4,subset_type(cross_product(X1,X2))))))),file('/tmp/SRASS.s.p', p4)).
% fof(25, axiom,![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,subset_type(cross_product(X1,X2)))=>relation_like(X3)))),file('/tmp/SRASS.s.p', p23)).
% fof(26, axiom,![X1]:(ilf_type(X1,binary_relation_type)=>image(X1,domain_of(X1))=range_of(X1)),file('/tmp/SRASS.s.p', p1)).
% fof(27, axiom,![X1]:(ilf_type(X1,binary_relation_type)=>inverse2(X1,range_of(X1))=domain_of(X1)),file('/tmp/SRASS.s.p', p2)).
% fof(31, axiom,![X1]:(ilf_type(X1,set_type)=>(ilf_type(X1,binary_relation_type)<=>(relation_like(X1)&ilf_type(X1,set_type)))),file('/tmp/SRASS.s.p', p12)).
% fof(36, conjecture,![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X2,X1))=>(image4(X2,X1,X3,inverse4(X2,X1,X3,X1))=range(X2,X1,X3)&inverse4(X2,X1,X3,image4(X2,X1,X3,X2))=domain(X2,X1,X3))))),file('/tmp/SRASS.s.p', prove_relset_1_39)).
% fof(37, negated_conjecture,~(![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,relation_type(X2,X1))=>(image4(X2,X1,X3,inverse4(X2,X1,X3,X1))=range(X2,X1,X3)&inverse4(X2,X1,X3,image4(X2,X1,X3,X2))=domain(X2,X1,X3)))))),inference(assume_negation,[status(cth)],[36])).
% fof(42, plain,![X1]:(~(ilf_type(X1,set_type))|![X2]:(~(ilf_type(X2,set_type))|![X3]:(~(ilf_type(X3,relation_type(X1,X2)))|(image4(X1,X2,X3,X1)=range(X1,X2,X3)&inverse4(X1,X2,X3,X2)=domain(X1,X2,X3))))),inference(fof_nnf,[status(thm)],[1])).
% fof(43, plain,![X4]:(~(ilf_type(X4,set_type))|![X5]:(~(ilf_type(X5,set_type))|![X6]:(~(ilf_type(X6,relation_type(X4,X5)))|(image4(X4,X5,X6,X4)=range(X4,X5,X6)&inverse4(X4,X5,X6,X5)=domain(X4,X5,X6))))),inference(variable_rename,[status(thm)],[42])).
% fof(44, plain,![X4]:![X5]:![X6]:(((~(ilf_type(X6,relation_type(X4,X5)))|(image4(X4,X5,X6,X4)=range(X4,X5,X6)&inverse4(X4,X5,X6,X5)=domain(X4,X5,X6)))|~(ilf_type(X5,set_type)))|~(ilf_type(X4,set_type))),inference(shift_quantors,[status(thm)],[43])).
% fof(45, plain,![X4]:![X5]:![X6]:((((image4(X4,X5,X6,X4)=range(X4,X5,X6)|~(ilf_type(X6,relation_type(X4,X5))))|~(ilf_type(X5,set_type)))|~(ilf_type(X4,set_type)))&(((inverse4(X4,X5,X6,X5)=domain(X4,X5,X6)|~(ilf_type(X6,relation_type(X4,X5))))|~(ilf_type(X5,set_type)))|~(ilf_type(X4,set_type)))),inference(distribute,[status(thm)],[44])).
% cnf(46,plain,(inverse4(X1,X2,X3,X2)=domain(X1,X2,X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(split_conjunct,[status(thm)],[45])).
% cnf(47,plain,(image4(X1,X2,X3,X1)=range(X1,X2,X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(split_conjunct,[status(thm)],[45])).
% fof(53, plain,![X2]:ilf_type(X2,set_type),inference(variable_rename,[status(thm)],[3])).
% cnf(54,plain,(ilf_type(X1,set_type)),inference(split_conjunct,[status(thm)],[53])).
% fof(55, plain,![X1]:(~(ilf_type(X1,set_type))|![X2]:(~(ilf_type(X2,set_type))|![X3]:(~(ilf_type(X3,relation_type(X1,X2)))|domain(X1,X2,X3)=domain_of(X3)))),inference(fof_nnf,[status(thm)],[4])).
% fof(56, plain,![X4]:(~(ilf_type(X4,set_type))|![X5]:(~(ilf_type(X5,set_type))|![X6]:(~(ilf_type(X6,relation_type(X4,X5)))|domain(X4,X5,X6)=domain_of(X6)))),inference(variable_rename,[status(thm)],[55])).
% fof(57, plain,![X4]:![X5]:![X6]:(((~(ilf_type(X6,relation_type(X4,X5)))|domain(X4,X5,X6)=domain_of(X6))|~(ilf_type(X5,set_type)))|~(ilf_type(X4,set_type))),inference(shift_quantors,[status(thm)],[56])).
% cnf(58,plain,(domain(X1,X2,X3)=domain_of(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(split_conjunct,[status(thm)],[57])).
% fof(59, plain,![X1]:(~(ilf_type(X1,set_type))|![X2]:(~(ilf_type(X2,set_type))|![X3]:(~(ilf_type(X3,relation_type(X1,X2)))|range(X1,X2,X3)=range_of(X3)))),inference(fof_nnf,[status(thm)],[5])).
% fof(60, plain,![X4]:(~(ilf_type(X4,set_type))|![X5]:(~(ilf_type(X5,set_type))|![X6]:(~(ilf_type(X6,relation_type(X4,X5)))|range(X4,X5,X6)=range_of(X6)))),inference(variable_rename,[status(thm)],[59])).
% fof(61, plain,![X4]:![X5]:![X6]:(((~(ilf_type(X6,relation_type(X4,X5)))|range(X4,X5,X6)=range_of(X6))|~(ilf_type(X5,set_type)))|~(ilf_type(X4,set_type))),inference(shift_quantors,[status(thm)],[60])).
% cnf(62,plain,(range(X1,X2,X3)=range_of(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(split_conjunct,[status(thm)],[61])).
% fof(63, plain,![X1]:(~(ilf_type(X1,set_type))|![X2]:(~(ilf_type(X2,set_type))|![X3]:(~(ilf_type(X3,relation_type(X1,X2)))|![X4]:(~(ilf_type(X4,set_type))|image4(X1,X2,X3,X4)=image(X3,X4))))),inference(fof_nnf,[status(thm)],[6])).
% fof(64, plain,![X5]:(~(ilf_type(X5,set_type))|![X6]:(~(ilf_type(X6,set_type))|![X7]:(~(ilf_type(X7,relation_type(X5,X6)))|![X8]:(~(ilf_type(X8,set_type))|image4(X5,X6,X7,X8)=image(X7,X8))))),inference(variable_rename,[status(thm)],[63])).
% fof(65, plain,![X5]:![X6]:![X7]:![X8]:((((~(ilf_type(X8,set_type))|image4(X5,X6,X7,X8)=image(X7,X8))|~(ilf_type(X7,relation_type(X5,X6))))|~(ilf_type(X6,set_type)))|~(ilf_type(X5,set_type))),inference(shift_quantors,[status(thm)],[64])).
% cnf(66,plain,(image4(X1,X2,X3,X4)=image(X3,X4)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))|~ilf_type(X4,set_type)),inference(split_conjunct,[status(thm)],[65])).
% fof(67, plain,![X1]:(~(ilf_type(X1,set_type))|![X2]:(~(ilf_type(X2,set_type))|![X3]:(~(ilf_type(X3,relation_type(X1,X2)))|![X4]:(~(ilf_type(X4,set_type))|inverse4(X1,X2,X3,X4)=inverse2(X3,X4))))),inference(fof_nnf,[status(thm)],[7])).
% fof(68, plain,![X5]:(~(ilf_type(X5,set_type))|![X6]:(~(ilf_type(X6,set_type))|![X7]:(~(ilf_type(X7,relation_type(X5,X6)))|![X8]:(~(ilf_type(X8,set_type))|inverse4(X5,X6,X7,X8)=inverse2(X7,X8))))),inference(variable_rename,[status(thm)],[67])).
% fof(69, plain,![X5]:![X6]:![X7]:![X8]:((((~(ilf_type(X8,set_type))|inverse4(X5,X6,X7,X8)=inverse2(X7,X8))|~(ilf_type(X7,relation_type(X5,X6))))|~(ilf_type(X6,set_type)))|~(ilf_type(X5,set_type))),inference(shift_quantors,[status(thm)],[68])).
% cnf(70,plain,(inverse4(X1,X2,X3,X4)=inverse2(X3,X4)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))|~ilf_type(X4,set_type)),inference(split_conjunct,[status(thm)],[69])).
% fof(112, plain,![X1]:(~(ilf_type(X1,set_type))|![X2]:(~(ilf_type(X2,set_type))|(![X3]:(~(ilf_type(X3,subset_type(cross_product(X1,X2))))|ilf_type(X3,relation_type(X1,X2)))&![X4]:(~(ilf_type(X4,relation_type(X1,X2)))|ilf_type(X4,subset_type(cross_product(X1,X2))))))),inference(fof_nnf,[status(thm)],[18])).
% fof(113, plain,![X5]:(~(ilf_type(X5,set_type))|![X6]:(~(ilf_type(X6,set_type))|(![X7]:(~(ilf_type(X7,subset_type(cross_product(X5,X6))))|ilf_type(X7,relation_type(X5,X6)))&![X8]:(~(ilf_type(X8,relation_type(X5,X6)))|ilf_type(X8,subset_type(cross_product(X5,X6))))))),inference(variable_rename,[status(thm)],[112])).
% fof(114, plain,![X5]:![X6]:![X7]:![X8]:((((~(ilf_type(X8,relation_type(X5,X6)))|ilf_type(X8,subset_type(cross_product(X5,X6))))&(~(ilf_type(X7,subset_type(cross_product(X5,X6))))|ilf_type(X7,relation_type(X5,X6))))|~(ilf_type(X6,set_type)))|~(ilf_type(X5,set_type))),inference(shift_quantors,[status(thm)],[113])).
% fof(115, plain,![X5]:![X6]:![X7]:![X8]:((((~(ilf_type(X8,relation_type(X5,X6)))|ilf_type(X8,subset_type(cross_product(X5,X6))))|~(ilf_type(X6,set_type)))|~(ilf_type(X5,set_type)))&(((~(ilf_type(X7,subset_type(cross_product(X5,X6))))|ilf_type(X7,relation_type(X5,X6)))|~(ilf_type(X6,set_type)))|~(ilf_type(X5,set_type)))),inference(distribute,[status(thm)],[114])).
% cnf(117,plain,(ilf_type(X3,subset_type(cross_product(X1,X2)))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(split_conjunct,[status(thm)],[115])).
% fof(152, plain,![X1]:(~(ilf_type(X1,set_type))|![X2]:(~(ilf_type(X2,set_type))|![X3]:(~(ilf_type(X3,subset_type(cross_product(X1,X2))))|relation_like(X3)))),inference(fof_nnf,[status(thm)],[25])).
% fof(153, plain,![X4]:(~(ilf_type(X4,set_type))|![X5]:(~(ilf_type(X5,set_type))|![X6]:(~(ilf_type(X6,subset_type(cross_product(X4,X5))))|relation_like(X6)))),inference(variable_rename,[status(thm)],[152])).
% fof(154, plain,![X4]:![X5]:![X6]:(((~(ilf_type(X6,subset_type(cross_product(X4,X5))))|relation_like(X6))|~(ilf_type(X5,set_type)))|~(ilf_type(X4,set_type))),inference(shift_quantors,[status(thm)],[153])).
% cnf(155,plain,(relation_like(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,subset_type(cross_product(X1,X2)))),inference(split_conjunct,[status(thm)],[154])).
% fof(156, plain,![X1]:(~(ilf_type(X1,binary_relation_type))|image(X1,domain_of(X1))=range_of(X1)),inference(fof_nnf,[status(thm)],[26])).
% fof(157, plain,![X2]:(~(ilf_type(X2,binary_relation_type))|image(X2,domain_of(X2))=range_of(X2)),inference(variable_rename,[status(thm)],[156])).
% cnf(158,plain,(image(X1,domain_of(X1))=range_of(X1)|~ilf_type(X1,binary_relation_type)),inference(split_conjunct,[status(thm)],[157])).
% fof(159, plain,![X1]:(~(ilf_type(X1,binary_relation_type))|inverse2(X1,range_of(X1))=domain_of(X1)),inference(fof_nnf,[status(thm)],[27])).
% fof(160, plain,![X2]:(~(ilf_type(X2,binary_relation_type))|inverse2(X2,range_of(X2))=domain_of(X2)),inference(variable_rename,[status(thm)],[159])).
% cnf(161,plain,(inverse2(X1,range_of(X1))=domain_of(X1)|~ilf_type(X1,binary_relation_type)),inference(split_conjunct,[status(thm)],[160])).
% fof(185, plain,![X1]:(~(ilf_type(X1,set_type))|((~(ilf_type(X1,binary_relation_type))|(relation_like(X1)&ilf_type(X1,set_type)))&((~(relation_like(X1))|~(ilf_type(X1,set_type)))|ilf_type(X1,binary_relation_type)))),inference(fof_nnf,[status(thm)],[31])).
% fof(186, plain,![X2]:(~(ilf_type(X2,set_type))|((~(ilf_type(X2,binary_relation_type))|(relation_like(X2)&ilf_type(X2,set_type)))&((~(relation_like(X2))|~(ilf_type(X2,set_type)))|ilf_type(X2,binary_relation_type)))),inference(variable_rename,[status(thm)],[185])).
% fof(187, plain,![X2]:((((relation_like(X2)|~(ilf_type(X2,binary_relation_type)))|~(ilf_type(X2,set_type)))&((ilf_type(X2,set_type)|~(ilf_type(X2,binary_relation_type)))|~(ilf_type(X2,set_type))))&(((~(relation_like(X2))|~(ilf_type(X2,set_type)))|ilf_type(X2,binary_relation_type))|~(ilf_type(X2,set_type)))),inference(distribute,[status(thm)],[186])).
% cnf(188,plain,(ilf_type(X1,binary_relation_type)|~ilf_type(X1,set_type)|~ilf_type(X1,set_type)|~relation_like(X1)),inference(split_conjunct,[status(thm)],[187])).
% fof(209, negated_conjecture,?[X1]:(ilf_type(X1,set_type)&?[X2]:(ilf_type(X2,set_type)&?[X3]:(ilf_type(X3,relation_type(X2,X1))&(~(image4(X2,X1,X3,inverse4(X2,X1,X3,X1))=range(X2,X1,X3))|~(inverse4(X2,X1,X3,image4(X2,X1,X3,X2))=domain(X2,X1,X3)))))),inference(fof_nnf,[status(thm)],[37])).
% fof(210, negated_conjecture,?[X4]:(ilf_type(X4,set_type)&?[X5]:(ilf_type(X5,set_type)&?[X6]:(ilf_type(X6,relation_type(X5,X4))&(~(image4(X5,X4,X6,inverse4(X5,X4,X6,X4))=range(X5,X4,X6))|~(inverse4(X5,X4,X6,image4(X5,X4,X6,X5))=domain(X5,X4,X6)))))),inference(variable_rename,[status(thm)],[209])).
% fof(211, negated_conjecture,(ilf_type(esk11_0,set_type)&(ilf_type(esk12_0,set_type)&(ilf_type(esk13_0,relation_type(esk12_0,esk11_0))&(~(image4(esk12_0,esk11_0,esk13_0,inverse4(esk12_0,esk11_0,esk13_0,esk11_0))=range(esk12_0,esk11_0,esk13_0))|~(inverse4(esk12_0,esk11_0,esk13_0,image4(esk12_0,esk11_0,esk13_0,esk12_0))=domain(esk12_0,esk11_0,esk13_0)))))),inference(skolemize,[status(esa)],[210])).
% cnf(212,negated_conjecture,(inverse4(esk12_0,esk11_0,esk13_0,image4(esk12_0,esk11_0,esk13_0,esk12_0))!=domain(esk12_0,esk11_0,esk13_0)|image4(esk12_0,esk11_0,esk13_0,inverse4(esk12_0,esk11_0,esk13_0,esk11_0))!=range(esk12_0,esk11_0,esk13_0)),inference(split_conjunct,[status(thm)],[211])).
% cnf(213,negated_conjecture,(ilf_type(esk13_0,relation_type(esk12_0,esk11_0))),inference(split_conjunct,[status(thm)],[211])).
% cnf(231,plain,(ilf_type(X1,binary_relation_type)|~relation_like(X1)|$false),inference(rw,[status(thm)],[188,54,theory(equality)])).
% cnf(232,plain,(ilf_type(X1,binary_relation_type)|~relation_like(X1)),inference(cn,[status(thm)],[231,theory(equality)])).
% cnf(284,plain,(range(X1,X2,X3)=range_of(X3)|$false|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[62,54,theory(equality)])).
% cnf(285,plain,(range(X1,X2,X3)=range_of(X3)|$false|$false|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[284,54,theory(equality)])).
% cnf(286,plain,(range(X1,X2,X3)=range_of(X3)|~ilf_type(X3,relation_type(X1,X2))),inference(cn,[status(thm)],[285,theory(equality)])).
% cnf(287,plain,(domain(X1,X2,X3)=domain_of(X3)|$false|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[58,54,theory(equality)])).
% cnf(288,plain,(domain(X1,X2,X3)=domain_of(X3)|$false|$false|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[287,54,theory(equality)])).
% cnf(289,plain,(domain(X1,X2,X3)=domain_of(X3)|~ilf_type(X3,relation_type(X1,X2))),inference(cn,[status(thm)],[288,theory(equality)])).
% cnf(290,plain,(relation_like(X3)|$false|~ilf_type(X1,set_type)|~ilf_type(X3,subset_type(cross_product(X1,X2)))),inference(rw,[status(thm)],[155,54,theory(equality)])).
% cnf(291,plain,(relation_like(X3)|$false|$false|~ilf_type(X3,subset_type(cross_product(X1,X2)))),inference(rw,[status(thm)],[290,54,theory(equality)])).
% cnf(292,plain,(relation_like(X3)|~ilf_type(X3,subset_type(cross_product(X1,X2)))),inference(cn,[status(thm)],[291,theory(equality)])).
% cnf(319,plain,(ilf_type(X3,subset_type(cross_product(X1,X2)))|$false|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[117,54,theory(equality)])).
% cnf(320,plain,(ilf_type(X3,subset_type(cross_product(X1,X2)))|$false|$false|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[319,54,theory(equality)])).
% cnf(321,plain,(ilf_type(X3,subset_type(cross_product(X1,X2)))|~ilf_type(X3,relation_type(X1,X2))),inference(cn,[status(thm)],[320,theory(equality)])).
% cnf(332,plain,(image4(X1,X2,X3,X1)=range(X1,X2,X3)|$false|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[47,54,theory(equality)])).
% cnf(333,plain,(image4(X1,X2,X3,X1)=range(X1,X2,X3)|$false|$false|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[332,54,theory(equality)])).
% cnf(334,plain,(image4(X1,X2,X3,X1)=range(X1,X2,X3)|~ilf_type(X3,relation_type(X1,X2))),inference(cn,[status(thm)],[333,theory(equality)])).
% cnf(335,plain,(inverse4(X1,X2,X3,X2)=domain(X1,X2,X3)|$false|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[46,54,theory(equality)])).
% cnf(336,plain,(inverse4(X1,X2,X3,X2)=domain(X1,X2,X3)|$false|$false|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[335,54,theory(equality)])).
% cnf(337,plain,(inverse4(X1,X2,X3,X2)=domain(X1,X2,X3)|~ilf_type(X3,relation_type(X1,X2))),inference(cn,[status(thm)],[336,theory(equality)])).
% cnf(360,plain,(image4(X1,X2,X3,X4)=image(X3,X4)|$false|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[66,54,theory(equality)])).
% cnf(361,plain,(image4(X1,X2,X3,X4)=image(X3,X4)|$false|$false|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[360,54,theory(equality)])).
% cnf(362,plain,(image4(X1,X2,X3,X4)=image(X3,X4)|$false|$false|$false|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[361,54,theory(equality)])).
% cnf(363,plain,(image4(X1,X2,X3,X4)=image(X3,X4)|~ilf_type(X3,relation_type(X1,X2))),inference(cn,[status(thm)],[362,theory(equality)])).
% cnf(364,plain,(inverse4(X1,X2,X3,X4)=inverse2(X3,X4)|$false|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[70,54,theory(equality)])).
% cnf(365,plain,(inverse4(X1,X2,X3,X4)=inverse2(X3,X4)|$false|$false|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[364,54,theory(equality)])).
% cnf(366,plain,(inverse4(X1,X2,X3,X4)=inverse2(X3,X4)|$false|$false|$false|~ilf_type(X3,relation_type(X1,X2))),inference(rw,[status(thm)],[365,54,theory(equality)])).
% cnf(367,plain,(inverse4(X1,X2,X3,X4)=inverse2(X3,X4)|~ilf_type(X3,relation_type(X1,X2))),inference(cn,[status(thm)],[366,theory(equality)])).
% cnf(380,plain,(image(X1,domain_of(X1))=range_of(X1)|~relation_like(X1)),inference(spm,[status(thm)],[158,232,theory(equality)])).
% cnf(384,plain,(inverse2(X1,range_of(X1))=domain_of(X1)|~relation_like(X1)),inference(spm,[status(thm)],[161,232,theory(equality)])).
% cnf(386,negated_conjecture,(range(esk12_0,esk11_0,esk13_0)=range_of(esk13_0)),inference(spm,[status(thm)],[286,213,theory(equality)])).
% cnf(388,negated_conjecture,(domain(esk12_0,esk11_0,esk13_0)=domain_of(esk13_0)),inference(spm,[status(thm)],[289,213,theory(equality)])).
% cnf(394,negated_conjecture,(ilf_type(esk13_0,subset_type(cross_product(esk12_0,esk11_0)))),inference(spm,[status(thm)],[321,213,theory(equality)])).
% cnf(414,negated_conjecture,(image4(esk12_0,esk11_0,esk13_0,X1)=image(esk13_0,X1)),inference(spm,[status(thm)],[363,213,theory(equality)])).
% cnf(418,negated_conjecture,(image4(esk12_0,esk11_0,esk13_0,esk12_0)=range(esk12_0,esk11_0,esk13_0)),inference(spm,[status(thm)],[334,213,theory(equality)])).
% cnf(421,negated_conjecture,(inverse4(esk12_0,esk11_0,esk13_0,X1)=inverse2(esk13_0,X1)),inference(spm,[status(thm)],[367,213,theory(equality)])).
% cnf(424,negated_conjecture,(inverse4(esk12_0,esk11_0,esk13_0,esk11_0)=domain(esk12_0,esk11_0,esk13_0)),inference(spm,[status(thm)],[337,213,theory(equality)])).
% cnf(434,negated_conjecture,(image4(esk12_0,esk11_0,esk13_0,inverse4(esk12_0,esk11_0,esk13_0,esk11_0))!=range_of(esk13_0)|inverse4(esk12_0,esk11_0,esk13_0,image4(esk12_0,esk11_0,esk13_0,esk12_0))!=domain(esk12_0,esk11_0,esk13_0)),inference(rw,[status(thm)],[212,386,theory(equality)])).
% cnf(440,negated_conjecture,(image4(esk12_0,esk11_0,esk13_0,inverse4(esk12_0,esk11_0,esk13_0,esk11_0))!=range_of(esk13_0)|inverse4(esk12_0,esk11_0,esk13_0,image4(esk12_0,esk11_0,esk13_0,esk12_0))!=domain_of(esk13_0)),inference(rw,[status(thm)],[434,388,theory(equality)])).
% cnf(442,negated_conjecture,(range_of(esk13_0)=image4(esk12_0,esk11_0,esk13_0,esk12_0)),inference(rw,[status(thm)],[418,386,theory(equality)])).
% cnf(444,negated_conjecture,(image4(esk12_0,esk11_0,esk13_0,inverse4(esk12_0,esk11_0,esk13_0,esk11_0))!=range_of(esk13_0)|inverse4(esk12_0,esk11_0,esk13_0,range_of(esk13_0))!=domain_of(esk13_0)),inference(rw,[status(thm)],[440,442,theory(equality)])).
% cnf(447,negated_conjecture,(domain_of(esk13_0)=inverse4(esk12_0,esk11_0,esk13_0,esk11_0)),inference(rw,[status(thm)],[424,388,theory(equality)])).
% cnf(455,negated_conjecture,(image(esk13_0,domain_of(esk13_0))!=range_of(esk13_0)|inverse4(esk12_0,esk11_0,esk13_0,range_of(esk13_0))!=domain_of(esk13_0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[444,447,theory(equality)]),414,theory(equality)])).
% cnf(469,negated_conjecture,(inverse2(esk13_0,range_of(esk13_0))!=domain_of(esk13_0)|image(esk13_0,domain_of(esk13_0))!=range_of(esk13_0)),inference(rw,[status(thm)],[455,421,theory(equality)])).
% cnf(474,negated_conjecture,(relation_like(esk13_0)),inference(spm,[status(thm)],[292,394,theory(equality)])).
% cnf(492,negated_conjecture,(image(esk13_0,domain_of(esk13_0))!=range_of(esk13_0)|~relation_like(esk13_0)),inference(spm,[status(thm)],[469,384,theory(equality)])).
% cnf(493,negated_conjecture,(image(esk13_0,domain_of(esk13_0))!=range_of(esk13_0)|$false),inference(rw,[status(thm)],[492,474,theory(equality)])).
% cnf(494,negated_conjecture,(image(esk13_0,domain_of(esk13_0))!=range_of(esk13_0)),inference(cn,[status(thm)],[493,theory(equality)])).
% cnf(495,negated_conjecture,(~relation_like(esk13_0)),inference(spm,[status(thm)],[494,380,theory(equality)])).
% cnf(496,negated_conjecture,($false),inference(rw,[status(thm)],[495,474,theory(equality)])).
% cnf(497,negated_conjecture,($false),inference(cn,[status(thm)],[496,theory(equality)])).
% cnf(498,negated_conjecture,($false),497,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 145
% # ...of these trivial : 13
% # ...subsumed : 8
% # ...remaining for further processing: 124
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 7
% # Generated clauses : 92
% # ...of the previous two non-trivial : 86
% # Contextual simplify-reflections : 1
% # Paramodulations : 90
% # Factorizations : 0
% # Equation resolutions : 2
% # Current number of processed clauses: 72
% # Positive orientable unit clauses: 27
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 43
% # Current number of unprocessed clauses: 42
% # ...number of literals in the above : 80
% # Clause-clause subsumption calls (NU) : 24
% # Rec. Clause-clause subsumption calls : 18
% # Unit Clause-clause subsumption calls : 21
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 13
% # Indexed BW rewrite successes : 7
% # Backwards rewriting index: 105 leaves, 1.20+/-0.524 terms/leaf
% # Paramod-from index: 44 leaves, 1.02+/-0.149 terms/leaf
% # Paramod-into index: 97 leaves, 1.14+/-0.431 terms/leaf
% # -------------------------------------------------
% # User time : 0.023 s
% # System time : 0.006 s
% # Total time : 0.029 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.12 CPU 0.21 WC
% FINAL PrfWatch: 0.12 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP11010/SET675+3.tptp
%
%------------------------------------------------------------------------------