%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU293+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:22:14 PM UTC 2026
% Result : Theorem 0.13s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU293+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 06:06:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.41 fof(f2,axiom,(
% 0.13/0.41 (! [A] :( empty(A)=> function(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f3,axiom,(
% 0.13/0.41 (! [A] :( empty(A)=> relation(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f4,axiom,(
% 0.13/0.41 (! [A,B,C] :( element(C,powerset(cartesian_product2(A,B)))=> relation(C) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f5,axiom,(
% 0.13/0.41 (! [A] :( ( relation(A)& empty(A)& function(A) )=> ( relation(A)& function(A)& one_to_one(A) ) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f6,axiom,(
% 0.13/0.41 (! [A] :( ( relation(A)& function(A) )=> (! [B,C] :( C = relation_inverse_image(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,relation_dom(A))& in(apply(A,D),B) ) ) )) )) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f7,axiom,(
% 0.13/0.41 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> ( ( ( B = empty_set=> A = empty_set )=> ( quasi_total(C,A,B)<=> A = relation_dom_as_subset(A,B,C) ) )& ( B = empty_set=> ( A = empty_set| ( quasi_total(C,A,B)<=> C = empty_set ) ) ) ) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f17,axiom,(
% 0.13/0.41 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> element(C,powerset(cartesian_product2(A,B))) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f21,axiom,(
% 0.13/0.41 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f27,axiom,(
% 0.13/0.41 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f28,axiom,(
% 0.13/0.41 (? [A] :( relation(A)& function(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f30,axiom,(
% 0.13/0.41 (? [A] :( relation(A)& function(A)& one_to_one(A)& empty(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f31,axiom,(
% 0.13/0.41 (? [A] :( empty(A)& relation(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f34,axiom,(
% 0.13/0.41 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f39,axiom,(
% 0.13/0.41 (? [A] :( relation(A)& function(A)& one_to_one(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f41,axiom,(
% 0.13/0.41 (? [A] :( relation(A)& relation_empty_yielding(A)& function(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f42,axiom,(
% 0.13/0.41 (! [A,B,C] :( relation_of2(C,A,B)=> relation_dom_as_subset(A,B,C) = relation_dom(C) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f43,axiom,(
% 0.13/0.41 (! [A,B,C] :( relation_of2_as_subset(C,A,B)<=> relation_of2(C,A,B) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f48,conjecture,(
% 0.13/0.41 (! [A,B,C,D] :( ( function(D)& quasi_total(D,A,B)& relation_of2_as_subset(D,A,B) )=> ( B != empty_set=> (! [E] :( in(E,relation_inverse_image(D,C))<=> ( in(E,A)& in(apply(D,E),C) ) ) )) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f49,negated_conjecture,(
% 0.13/0.41 ~((! [A,B,C,D] :( ( function(D)& quasi_total(D,A,B)& relation_of2_as_subset(D,A,B) )=> ( B != empty_set=> (! [E] :( in(E,relation_inverse_image(D,C))<=> ( in(E,A)& in(apply(D,E),C) ) ) )) ) ))),
% 0.13/0.41 inference(negated_conjecture,[status(cth)],[f48])).
% 0.13/0.41 fof(f52,axiom,(
% 0.13/0.41 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f53,axiom,(
% 0.13/0.41 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f57,plain,(
% 0.13/0.41 ![A]: (~empty(A)|function(A))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.13/0.41 fof(f58,plain,(
% 0.13/0.41 ![X0]: (~empty(X0)|function(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f57])).
% 0.13/0.41 fof(f59,plain,(
% 0.13/0.41 ![A]: (~empty(A)|relation(A))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.13/0.41 fof(f60,plain,(
% 0.13/0.41 ![X0]: (~empty(X0)|relation(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.13/0.41 fof(f61,plain,(
% 0.13/0.41 ![A,B,C]: (~element(C,powerset(cartesian_product2(A,B)))|relation(C))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.13/0.41 fof(f62,plain,(
% 0.13/0.41 ![C]: ((![A,B]: ~element(C,powerset(cartesian_product2(A,B))))|relation(C))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f61])).
% 0.13/0.41 fof(f63,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~element(X0,powerset(cartesian_product2(X1,X2)))|relation(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/0.41 fof(f64,plain,(
% 0.13/0.41 ![A]: (((~relation(A)|~empty(A))|~function(A))|((relation(A)&function(A))&one_to_one(A)))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.13/0.41 fof(f67,plain,(
% 0.13/0.41 ![X0]: (~relation(X0)|~empty(X0)|~function(X0)|one_to_one(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f64])).
% 0.13/0.41 fof(f68,plain,(
% 0.13/0.41 ![A]: ((~relation(A)|~function(A))|(![B,C]: (C=relation_inverse_image(A,B)<=>(![D]: (in(D,C)<=>(in(D,relation_dom(A))&in(apply(A,D),B)))))))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.13/0.41 fof(f69,plain,(
% 0.13/0.41 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~C=relation_inverse_image(A,B)|(![D]: ((~in(D,C)|(in(D,relation_dom(A))&in(apply(A,D),B)))&(in(D,C)|(~in(D,relation_dom(A))|~in(apply(A,D),B))))))&(C=relation_inverse_image(A,B)|(?[D]: ((~in(D,C)|(~in(D,relation_dom(A))|~in(apply(A,D),B)))&(in(D,C)|(in(D,relation_dom(A))&in(apply(A,D),B)))))))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f68])).
% 0.13/0.41 fof(f70,plain,(
% 0.13/0.41 ![A]: ((~relation(A)|~function(A))|((![B,C]: (~C=relation_inverse_image(A,B)|((![D]: (~in(D,C)|(in(D,relation_dom(A))&in(apply(A,D),B))))&(![D]: (in(D,C)|(~in(D,relation_dom(A))|~in(apply(A,D),B)))))))&(![B,C]: (C=relation_inverse_image(A,B)|(?[D]: ((~in(D,C)|(~in(D,relation_dom(A))|~in(apply(A,D),B)))&(in(D,C)|(in(D,relation_dom(A))&in(apply(A,D),B)))))))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f69])).
% 0.13/0.41 fof(f71,plain,(
% 0.13/0.41 ![A]: ((~relation(A)|~function(A))|((![B,C]: (~C=relation_inverse_image(A,B)|((![D]: (~in(D,C)|(in(D,relation_dom(A))&in(apply(A,D),B))))&(![D]: (in(D,C)|(~in(D,relation_dom(A))|~in(apply(A,D),B)))))))&(![B,C]: (C=relation_inverse_image(A,B)|((~in(sK0_skl(C,B,A),C)|(~in(sK0_skl(C,B,A),relation_dom(A))|~in(apply(A,sK0_skl(C,B,A)),B)))&(in(sK0_skl(C,B,A),C)|(in(sK0_skl(C,B,A),relation_dom(A))&in(apply(A,sK0_skl(C,B,A)),B))))))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(D,sK0_skl(C,B,A))],[f70])).
% 0.13/0.41 fof(f72,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~X1=relation_inverse_image(X0,X2)|~in(X3,X1)|in(X3,relation_dom(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.13/0.41 fof(f73,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~X1=relation_inverse_image(X0,X2)|~in(X3,X1)|in(apply(X0,X3),X2))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.13/0.41 fof(f74,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~X1=relation_inverse_image(X0,X2)|in(X3,X1)|~in(X3,relation_dom(X0))|~in(apply(X0,X3),X2))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.13/0.41 fof(f75,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation(X0)|~function(X0)|X1=relation_inverse_image(X0,X2)|~in(sK0_skl(X1,X2,X0),X1)|~in(sK0_skl(X1,X2,X0),relation_dom(X0))|~in(apply(X0,sK0_skl(X1,X2,X0)),X2))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.13/0.41 fof(f76,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation(X0)|~function(X0)|X1=relation_inverse_image(X0,X2)|in(sK0_skl(X1,X2,X0),X1)|in(sK0_skl(X1,X2,X0),relation_dom(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.13/0.41 fof(f77,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation(X0)|~function(X0)|X1=relation_inverse_image(X0,X2)|in(sK0_skl(X1,X2,X0),X1)|in(apply(X0,sK0_skl(X1,X2,X0)),X2))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.13/0.41 fof(f78,plain,(
% 0.13/0.41 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|(((B=empty_set&~A=empty_set)|(quasi_total(C,A,B)<=>A=relation_dom_as_subset(A,B,C)))&(~B=empty_set|(A=empty_set|(quasi_total(C,A,B)<=>C=empty_set)))))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.13/0.41 fof(f79,definition,(
% 0.13/0.41 ![A,B]: (sP0_prd(B,A)<=>(B=empty_set&~A=empty_set))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.41 fof(f80,plain,(
% 0.13/0.41 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|((sP0_prd(B,A)|(quasi_total(C,A,B)<=>A=relation_dom_as_subset(A,B,C)))&(~B=empty_set|(A=empty_set|(quasi_total(C,A,B)<=>C=empty_set)))))),
% 0.13/0.41 inference(formula_renaming,[status(thm)],[f78,f79])).
% 0.13/0.41 fof(f81,plain,(
% 0.13/0.41 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|((sP0_prd(B,A)|((~quasi_total(C,A,B)|A=relation_dom_as_subset(A,B,C))&(quasi_total(C,A,B)|~A=relation_dom_as_subset(A,B,C))))&(~B=empty_set|(A=empty_set|((~quasi_total(C,A,B)|C=empty_set)&(quasi_total(C,A,B)|~C=empty_set))))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f80])).
% 0.13/0.41 fof(f82,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|sP0_prd(X2,X1)|~quasi_total(X0,X1,X2)|X1=relation_dom_as_subset(X1,X2,X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f81])).
% 0.13/0.41 fof(f83,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|sP0_prd(X2,X1)|quasi_total(X0,X1,X2)|~X1=relation_dom_as_subset(X1,X2,X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f81])).
% 0.13/0.41 fof(f88,plain,(
% 0.13/0.41 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|element(C,powerset(cartesian_product2(A,B))))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.13/0.41 fof(f89,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|element(X0,powerset(cartesian_product2(X1,X2))))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f88])).
% 0.13/0.41 fof(f96,plain,(
% 0.13/0.41 empty(empty_set)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f21])).
% 0.13/0.41 fof(f97,plain,(
% 0.13/0.41 relation(empty_set)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f21])).
% 0.13/0.41 fof(f107,plain,(
% 0.13/0.41 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.13/0.41 fof(f108,plain,(
% 0.13/0.41 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.41 fof(f110,plain,(
% 0.13/0.41 (relation(sK4_skl)&function(sK4_skl))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f28])).
% 0.13/0.41 fof(f111,plain,(
% 0.13/0.41 relation(sK4_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f110])).
% 0.13/0.41 fof(f112,plain,(
% 0.13/0.41 function(sK4_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f110])).
% 0.13/0.41 fof(f118,plain,(
% 0.13/0.41 (((relation(sK6_skl)&function(sK6_skl))&one_to_one(sK6_skl))&empty(sK6_skl))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f30])).
% 0.13/0.41 fof(f119,plain,(
% 0.13/0.41 relation(sK6_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f118])).
% 0.13/0.41 fof(f120,plain,(
% 0.13/0.41 function(sK6_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f118])).
% 0.13/0.41 fof(f122,plain,(
% 0.13/0.41 empty(sK6_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f118])).
% 0.13/0.41 fof(f123,plain,(
% 0.13/0.41 (empty(sK7_skl)&relation(sK7_skl))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f31])).
% 0.13/0.41 fof(f124,plain,(
% 0.13/0.41 empty(sK7_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f123])).
% 0.13/0.41 fof(f125,plain,(
% 0.13/0.41 relation(sK7_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f123])).
% 0.13/0.41 fof(f132,plain,(
% 0.13/0.41 ((relation(sK10_skl)&empty(sK10_skl))&function(sK10_skl))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f34])).
% 0.13/0.41 fof(f133,plain,(
% 0.13/0.41 relation(sK10_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f132])).
% 0.13/0.41 fof(f135,plain,(
% 0.13/0.41 function(sK10_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f132])).
% 0.13/0.41 fof(f148,plain,(
% 0.13/0.41 ((relation(sK15_skl)&function(sK15_skl))&one_to_one(sK15_skl))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f39])).
% 0.13/0.41 fof(f149,plain,(
% 0.13/0.41 relation(sK15_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f148])).
% 0.13/0.41 fof(f150,plain,(
% 0.13/0.41 function(sK15_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f148])).
% 0.13/0.41 fof(f155,plain,(
% 0.13/0.41 ((relation(sK17_skl)&relation_empty_yielding(sK17_skl))&function(sK17_skl))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f41])).
% 0.13/0.41 fof(f156,plain,(
% 0.13/0.41 relation(sK17_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f155])).
% 0.13/0.41 fof(f158,plain,(
% 0.13/0.41 function(sK17_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f155])).
% 0.13/0.41 fof(f159,plain,(
% 0.13/0.41 ![A,B,C]: (~relation_of2(C,A,B)|relation_dom_as_subset(A,B,C)=relation_dom(C))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.13/0.41 fof(f160,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation_of2(X0,X1,X2)|relation_dom_as_subset(X1,X2,X0)=relation_dom(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f159])).
% 0.13/0.41 fof(f161,plain,(
% 0.13/0.41 ![A,B,C]: ((~relation_of2_as_subset(C,A,B)|relation_of2(C,A,B))&(relation_of2_as_subset(C,A,B)|~relation_of2(C,A,B)))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f43])).
% 0.13/0.41 fof(f162,plain,(
% 0.13/0.41 (![A,B,C]: (~relation_of2_as_subset(C,A,B)|relation_of2(C,A,B)))&(![A,B,C]: (relation_of2_as_subset(C,A,B)|~relation_of2(C,A,B)))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f161])).
% 0.13/0.41 fof(f163,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|relation_of2(X0,X1,X2))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f162])).
% 0.13/0.41 fof(f175,plain,(
% 0.13/0.41 (?[A,B,C,D]: (((function(D)&quasi_total(D,A,B))&relation_of2_as_subset(D,A,B))&(~B=empty_set&(?[E]: (in(E,relation_inverse_image(D,C))<~>(in(E,A)&in(apply(D,E),C)))))))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.13/0.41 fof(f176,plain,(
% 0.13/0.41 ?[A,B,C,D]: (((function(D)&quasi_total(D,A,B))&relation_of2_as_subset(D,A,B))&(~B=empty_set&(?[E]: ((in(E,relation_inverse_image(D,C))|(in(E,A)&in(apply(D,E),C)))&(~in(E,relation_inverse_image(D,C))|(~in(E,A)|~in(apply(D,E),C)))))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f175])).
% 0.13/0.41 fof(f177,plain,(
% 0.13/0.41 ?[A,B,D]: (((function(D)&quasi_total(D,A,B))&relation_of2_as_subset(D,A,B))&(~B=empty_set&(?[C,E]: ((in(E,relation_inverse_image(D,C))|(in(E,A)&in(apply(D,E),C)))&(~in(E,relation_inverse_image(D,C))|(~in(E,A)|~in(apply(D,E),C)))))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f176])).
% 0.13/0.41 fof(f178,plain,(
% 0.13/0.41 (((function(sK20_skl)&quasi_total(sK20_skl,sK18_skl,sK19_skl))&relation_of2_as_subset(sK20_skl,sK18_skl,sK19_skl))&(~sK19_skl=empty_set&((in(sK22_skl,relation_inverse_image(sK20_skl,sK21_skl))|(in(sK22_skl,sK18_skl)&in(apply(sK20_skl,sK22_skl),sK21_skl)))&(~in(sK22_skl,relation_inverse_image(sK20_skl,sK21_skl))|(~in(sK22_skl,sK18_skl)|~in(apply(sK20_skl,sK22_skl),sK21_skl))))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl]),skolemize(A,sK18_skl),skolemize(B,sK19_skl),skolemize(D,sK20_skl),skolemize(C,sK21_skl),skolemize(E,sK22_skl)],[f177])).
% 0.13/0.41 fof(f179,plain,(
% 0.13/0.41 function(sK20_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.41 fof(f180,plain,(
% 0.13/0.41 quasi_total(sK20_skl,sK18_skl,sK19_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.41 fof(f181,plain,(
% 0.13/0.41 relation_of2_as_subset(sK20_skl,sK18_skl,sK19_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.41 fof(f182,plain,(
% 0.13/0.41 ~sK19_skl=empty_set),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.41 fof(f183,plain,(
% 0.13/0.41 in(sK22_skl,relation_inverse_image(sK20_skl,sK21_skl))|in(sK22_skl,sK18_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.41 fof(f184,plain,(
% 0.13/0.41 in(sK22_skl,relation_inverse_image(sK20_skl,sK21_skl))|in(apply(sK20_skl,sK22_skl),sK21_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.41 fof(f185,plain,(
% 0.13/0.41 ~in(sK22_skl,relation_inverse_image(sK20_skl,sK21_skl))|~in(sK22_skl,sK18_skl)|~in(apply(sK20_skl,sK22_skl),sK21_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.41 fof(f192,plain,(
% 0.13/0.41 ![A]: (~empty(A)|A=empty_set)),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 0.13/0.41 fof(f193,plain,(
% 0.13/0.41 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f192])).
% 0.13/0.41 fof(f194,plain,(
% 0.13/0.41 ![A,B]: (~in(A,B)|~empty(B))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.13/0.41 fof(f195,plain,(
% 0.13/0.41 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f194])).
% 0.13/0.41 fof(f196,plain,(
% 0.13/0.41 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f195])).
% 0.13/0.41 fof(f200,plain,(
% 0.13/0.41 ![A,B]: ((~sP0_prd(B,A)|(B=empty_set&~A=empty_set))&(sP0_prd(B,A)|(~B=empty_set|A=empty_set)))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f79])).
% 0.13/0.41 fof(f201,plain,(
% 0.13/0.41 (![A,B]: (~sP0_prd(B,A)|(B=empty_set&~A=empty_set)))&(![A,B]: (sP0_prd(B,A)|(~B=empty_set|A=empty_set)))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f200])).
% 0.13/0.41 fof(f202,plain,(
% 0.13/0.41 ![X0,X1]: (~sP0_prd(X0,X1)|X0=empty_set)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f201])).
% 0.13/0.41 fof(f205,definition,(
% 0.13/0.41 sQ0_spl <=> (in(sK22_skl,relation_inverse_image(sK20_skl,sK21_skl)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f206,plain,(
% 0.13/0.41 in(sK22_skl,relation_inverse_image(sK20_skl,sK21_skl))|~sQ0_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f205])).
% 0.13/0.41 fof(f208,definition,(
% 0.13/0.41 sQ1_spl <=> (in(sK22_skl,sK18_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f209,plain,(
% 0.13/0.41 in(sK22_skl,sK18_skl)|~sQ1_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f208])).
% 0.13/0.41 fof(f211,plain,(
% 0.13/0.41 sQ0_spl|sQ1_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f183,f205,f208])).
% 0.13/0.41 fof(f212,definition,(
% 0.13/0.41 sQ2_spl <=> (in(apply(sK20_skl,sK22_skl),sK21_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f213,plain,(
% 0.13/0.41 in(apply(sK20_skl,sK22_skl),sK21_skl)|~sQ2_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f212])).
% 0.13/0.41 fof(f215,plain,(
% 0.13/0.41 sQ0_spl|sQ2_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f184,f205,f212])).
% 0.13/0.41 fof(f216,plain,(
% 0.13/0.41 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f185,f205,f208,f212])).
% 0.13/0.41 fof(f217,plain,(
% 0.13/0.41 ![X0]: (~empty(X0)|~function(X0)|one_to_one(X0))),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f67,f60])).
% 0.13/0.41 fof(f218,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~in(X1,relation_inverse_image(X0,X2))|in(X1,relation_dom(X0)))),
% 0.13/0.41 inference(destructive_equality_resolution,[status(thm)],[f72])).
% 0.13/0.41 fof(f219,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~in(X1,relation_inverse_image(X0,X2))|in(apply(X0,X1),X2))),
% 0.13/0.41 inference(destructive_equality_resolution,[status(thm)],[f73])).
% 0.13/0.41 fof(f220,plain,(
% 0.13/0.41 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_inverse_image(X0,X2))|~in(X1,relation_dom(X0))|~in(apply(X0,X1),X2))),
% 0.13/0.41 inference(destructive_equality_resolution,[status(thm)],[f74])).
% 0.13/0.41 fof(f225,plain,(
% 0.13/0.41 function(empty_set)),
% 0.13/0.41 inference(resolution,[status(thm)],[f58,f96])).
% 0.13/0.41 fof(f243,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK4_skl)|X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|in(sK0_skl(X0,X1,sK4_skl),relation_dom(sK4_skl)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f76,f111])).
% 0.13/0.41 fof(f244,plain,(
% 0.13/0.41 ![X0,X1]: (~function(empty_set)|X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|in(sK0_skl(X0,X1,empty_set),relation_dom(empty_set)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f76,f97])).
% 0.13/0.41 fof(f245,definition,(
% 0.13/0.41 sQ7_spl <=> (function(sK4_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f247,plain,(
% 0.13/0.41 ~function(sK4_skl)|sQ7_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f245])).
% 0.13/0.41 fof(f248,definition,(
% 0.13/0.41 ![X0,X1]: (sQ8_spl <=> (X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|in(sK0_skl(X0,X1,sK4_skl),relation_dom(sK4_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f251,plain,(
% 0.13/0.41 ~sQ7_spl|sQ8_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f243,f245,f248])).
% 0.13/0.41 fof(f252,definition,(
% 0.13/0.41 sQ9_spl <=> (function(empty_set))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f254,plain,(
% 0.13/0.41 ~function(empty_set)|sQ9_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f252])).
% 0.13/0.41 fof(f255,definition,(
% 0.13/0.41 ![X0,X1]: (sQ10_spl <=> (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|in(sK0_skl(X0,X1,empty_set),relation_dom(empty_set))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f256,plain,(
% 0.13/0.41 ![X0,X1]: (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|in(sK0_skl(X0,X1,empty_set),relation_dom(empty_set))|~sQ10_spl)),
% 0.13/0.41 inference(component_clause,[status(thm)],[f255])).
% 0.13/0.41 fof(f258,plain,(
% 0.13/0.41 ~sQ9_spl|sQ10_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f244,f252,f255])).
% 0.13/0.41 fof(f259,plain,(
% 0.13/0.41 $false|sQ9_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f254,f225])).
% 0.13/0.41 fof(f260,plain,(
% 0.13/0.41 sQ9_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f259])).
% 0.13/0.41 fof(f261,plain,(
% 0.13/0.41 $false|sQ7_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f247,f112])).
% 0.13/0.41 fof(f262,plain,(
% 0.13/0.41 sQ7_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f261])).
% 0.13/0.41 fof(f263,plain,(
% 0.13/0.41 ~relation(sK20_skl)|~function(sK20_skl)|in(sK22_skl,relation_dom(sK20_skl))|~sQ0_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f206,f218])).
% 0.13/0.41 fof(f264,plain,(
% 0.13/0.41 ~relation(sK20_skl)|~function(sK20_skl)|in(apply(sK20_skl,sK22_skl),sK21_skl)|~sQ0_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f206,f219])).
% 0.13/0.41 fof(f266,definition,(
% 0.13/0.41 sQ11_spl <=> (relation(sK20_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f268,plain,(
% 0.13/0.41 ~relation(sK20_skl)|sQ11_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f266])).
% 0.13/0.41 fof(f269,definition,(
% 0.13/0.41 sQ12_spl <=> (function(sK20_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f271,plain,(
% 0.13/0.41 ~function(sK20_skl)|sQ12_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f269])).
% 0.13/0.41 fof(f272,definition,(
% 0.13/0.41 sQ13_spl <=> (in(sK22_skl,relation_dom(sK20_skl)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f273,plain,(
% 0.13/0.41 in(sK22_skl,relation_dom(sK20_skl))|~sQ13_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f272])).
% 0.13/0.41 fof(f274,plain,(
% 0.13/0.41 ~in(sK22_skl,relation_dom(sK20_skl))|sQ13_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f272])).
% 0.13/0.41 fof(f275,plain,(
% 0.13/0.41 ~sQ11_spl|~sQ12_spl|sQ13_spl|~sQ0_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f263,f266,f269,f272,f205])).
% 0.13/0.41 fof(f276,plain,(
% 0.13/0.41 ~sQ11_spl|~sQ12_spl|sQ2_spl|~sQ0_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f264,f266,f269,f212,f205])).
% 0.13/0.41 fof(f277,plain,(
% 0.13/0.41 ~empty(empty_set)|one_to_one(empty_set)),
% 0.13/0.41 inference(resolution,[status(thm)],[f225,f217])).
% 0.13/0.41 fof(f278,definition,(
% 0.13/0.41 sQ14_spl <=> (empty(empty_set))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f280,plain,(
% 0.13/0.41 ~empty(empty_set)|sQ14_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f278])).
% 0.13/0.41 fof(f281,definition,(
% 0.13/0.41 sQ15_spl <=> (one_to_one(empty_set))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f284,plain,(
% 0.13/0.41 ~sQ14_spl|sQ15_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f277,f278,f281])).
% 0.13/0.41 fof(f285,plain,(
% 0.13/0.41 $false|sQ14_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f280,f96])).
% 0.13/0.41 fof(f286,plain,(
% 0.13/0.41 sQ14_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f285])).
% 0.13/0.41 fof(f287,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK4_skl)|X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|in(apply(sK4_skl,sK0_skl(X0,X1,sK4_skl)),X1))),
% 0.13/0.41 inference(resolution,[status(thm)],[f77,f111])).
% 0.13/0.41 fof(f288,plain,(
% 0.13/0.41 ![X0,X1]: (~function(empty_set)|X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|in(apply(empty_set,sK0_skl(X0,X1,empty_set)),X1))),
% 0.13/0.41 inference(resolution,[status(thm)],[f77,f97])).
% 0.13/0.41 fof(f289,definition,(
% 0.13/0.41 ![X0,X1]: (sQ16_spl <=> (X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|in(apply(sK4_skl,sK0_skl(X0,X1,sK4_skl)),X1)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f290,plain,(
% 0.13/0.41 ![X0,X1]: (X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|in(apply(sK4_skl,sK0_skl(X0,X1,sK4_skl)),X1)|~sQ16_spl)),
% 0.13/0.41 inference(component_clause,[status(thm)],[f289])).
% 0.13/0.41 fof(f292,plain,(
% 0.13/0.41 ~sQ7_spl|sQ16_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f287,f245,f289])).
% 0.13/0.41 fof(f293,definition,(
% 0.13/0.41 ![X0,X1]: (sQ17_spl <=> (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|in(apply(empty_set,sK0_skl(X0,X1,empty_set)),X1)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f294,plain,(
% 0.13/0.41 ![X0,X1]: (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|in(apply(empty_set,sK0_skl(X0,X1,empty_set)),X1)|~sQ17_spl)),
% 0.13/0.41 inference(component_clause,[status(thm)],[f293])).
% 0.13/0.41 fof(f296,plain,(
% 0.13/0.41 ~sQ9_spl|sQ17_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f288,f252,f293])).
% 0.13/0.41 fof(f298,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK6_skl)|X0=relation_inverse_image(sK6_skl,X1)|in(sK0_skl(X0,X1,sK6_skl),X0)|in(apply(sK6_skl,sK0_skl(X0,X1,sK6_skl)),X1))),
% 0.13/0.41 inference(resolution,[status(thm)],[f119,f77])).
% 0.13/0.41 fof(f299,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK6_skl)|X0=relation_inverse_image(sK6_skl,X1)|in(sK0_skl(X0,X1,sK6_skl),X0)|in(sK0_skl(X0,X1,sK6_skl),relation_dom(sK6_skl)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f119,f76])).
% 0.13/0.41 fof(f300,definition,(
% 0.13/0.41 sQ18_spl <=> (function(sK6_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f302,plain,(
% 0.13/0.41 ~function(sK6_skl)|sQ18_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f300])).
% 0.13/0.41 fof(f303,definition,(
% 0.13/0.41 ![X0,X1]: (sQ19_spl <=> (X0=relation_inverse_image(sK6_skl,X1)|in(sK0_skl(X0,X1,sK6_skl),X0)|in(apply(sK6_skl,sK0_skl(X0,X1,sK6_skl)),X1)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f306,plain,(
% 0.13/0.41 ~sQ18_spl|sQ19_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f298,f300,f303])).
% 0.13/0.41 fof(f307,definition,(
% 0.13/0.41 ![X0,X1]: (sQ20_spl <=> (X0=relation_inverse_image(sK6_skl,X1)|in(sK0_skl(X0,X1,sK6_skl),X0)|in(sK0_skl(X0,X1,sK6_skl),relation_dom(sK6_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f310,plain,(
% 0.13/0.41 ~sQ18_spl|sQ20_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f299,f300,f307])).
% 0.13/0.41 fof(f311,plain,(
% 0.13/0.41 $false|sQ18_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f302,f120])).
% 0.13/0.41 fof(f312,plain,(
% 0.13/0.41 sQ18_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f311])).
% 0.13/0.41 fof(f313,plain,(
% 0.13/0.41 ~empty(sK6_skl)|one_to_one(sK6_skl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f120,f217])).
% 0.13/0.41 fof(f314,definition,(
% 0.13/0.41 sQ21_spl <=> (empty(sK6_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f316,plain,(
% 0.13/0.41 ~empty(sK6_skl)|sQ21_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f314])).
% 0.13/0.41 fof(f317,definition,(
% 0.13/0.41 sQ22_spl <=> (one_to_one(sK6_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f320,plain,(
% 0.13/0.41 ~sQ21_spl|sQ22_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f313,f314,f317])).
% 0.13/0.41 fof(f321,plain,(
% 0.13/0.41 $false|sQ21_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f316,f122])).
% 0.13/0.41 fof(f322,plain,(
% 0.13/0.41 sQ21_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f321])).
% 0.13/0.41 fof(f323,plain,(
% 0.13/0.41 ~relation_of2_as_subset(sK20_skl,sK18_skl,sK19_skl)|sP0_prd(sK19_skl,sK18_skl)|sK18_skl=relation_dom_as_subset(sK18_skl,sK19_skl,sK20_skl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f82,f180])).
% 0.13/0.41 fof(f324,definition,(
% 0.13/0.41 sQ23_spl <=> (relation_of2_as_subset(sK20_skl,sK18_skl,sK19_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f326,plain,(
% 0.13/0.41 ~relation_of2_as_subset(sK20_skl,sK18_skl,sK19_skl)|sQ23_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f324])).
% 0.13/0.41 fof(f327,definition,(
% 0.13/0.41 sQ24_spl <=> (sP0_prd(sK19_skl,sK18_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f328,plain,(
% 0.13/0.41 sP0_prd(sK19_skl,sK18_skl)|~sQ24_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f327])).
% 0.13/0.41 fof(f330,definition,(
% 0.13/0.41 sQ25_spl <=> (sK18_skl=relation_dom_as_subset(sK18_skl,sK19_skl,sK20_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f331,plain,(
% 0.13/0.41 sK18_skl=relation_dom_as_subset(sK18_skl,sK19_skl,sK20_skl)|~sQ25_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f330])).
% 0.13/0.41 fof(f333,plain,(
% 0.13/0.41 ~sQ23_spl|sQ24_spl|sQ25_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f323,f324,f327,f330])).
% 0.13/0.41 fof(f334,plain,(
% 0.13/0.41 $false|sQ12_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f271,f179])).
% 0.13/0.41 fof(f335,plain,(
% 0.13/0.41 sQ12_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f334])).
% 0.13/0.41 fof(f336,plain,(
% 0.13/0.41 element(sK20_skl,powerset(cartesian_product2(sK18_skl,sK19_skl)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f89,f181])).
% 0.13/0.41 fof(f339,plain,(
% 0.13/0.41 ~relation_of2_as_subset(sK20_skl,sK18_skl,sK19_skl)|sP0_prd(sK19_skl,sK18_skl)|quasi_total(sK20_skl,sK18_skl,sK19_skl)|~sQ25_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f331,f83])).
% 0.13/0.41 fof(f341,definition,(
% 0.13/0.41 sQ26_spl <=> (quasi_total(sK20_skl,sK18_skl,sK19_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f344,plain,(
% 0.13/0.41 ~sQ23_spl|sQ24_spl|sQ26_spl|~sQ25_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f339,f324,f327,f341,f330])).
% 0.13/0.41 fof(f352,plain,(
% 0.13/0.41 ![X0]: (relation_dom(empty_set)=relation_inverse_image(empty_set,X0)|~empty(relation_dom(empty_set))|~sQ10_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f256,f196])).
% 0.13/0.41 fof(f356,plain,(
% 0.13/0.41 ![X0,X1]: (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|~empty(relation_dom(empty_set))|~sQ10_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f256,f196])).
% 0.13/0.41 fof(f359,definition,(
% 0.13/0.41 ![X0]: (sQ28_spl <=> (relation_dom(empty_set)=relation_inverse_image(empty_set,X0)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f362,definition,(
% 0.13/0.41 sQ29_spl <=> (empty(relation_dom(empty_set)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f364,plain,(
% 0.13/0.41 ~empty(relation_dom(empty_set))|sQ29_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f362])).
% 0.13/0.41 fof(f365,plain,(
% 0.13/0.41 sQ28_spl|~sQ29_spl|~sQ10_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f352,f359,f362,f255])).
% 0.13/0.41 fof(f366,definition,(
% 0.13/0.41 ![X0,X1]: (sQ30_spl <=> (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f369,plain,(
% 0.13/0.41 sQ30_spl|~sQ29_spl|~sQ10_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f356,f366,f362,f255])).
% 0.13/0.41 fof(f374,plain,(
% 0.13/0.41 ![X0,X1]: (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|~relation(empty_set)|~function(empty_set)|X0=relation_inverse_image(empty_set,X1)|~in(sK0_skl(X0,X1,empty_set),X0)|~in(sK0_skl(X0,X1,empty_set),relation_dom(empty_set))|~sQ17_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f294,f75])).
% 0.13/0.41 fof(f375,plain,(
% 0.13/0.41 ![X0,X1]: (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|~relation(empty_set)|~function(empty_set)|in(sK0_skl(X0,X1,empty_set),relation_inverse_image(empty_set,X1))|~in(sK0_skl(X0,X1,empty_set),relation_dom(empty_set))|~sQ17_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f294,f220])).
% 0.13/0.41 fof(f380,definition,(
% 0.13/0.41 ![X0,X1]: (sQ31_spl <=> (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|X0=relation_inverse_image(empty_set,X1)|~in(sK0_skl(X0,X1,empty_set),X0)|~in(sK0_skl(X0,X1,empty_set),relation_dom(empty_set))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f383,definition,(
% 0.13/0.41 sQ32_spl <=> (relation(empty_set))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f385,plain,(
% 0.13/0.41 ~relation(empty_set)|sQ32_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f383])).
% 0.13/0.41 fof(f386,plain,(
% 0.13/0.41 sQ31_spl|~sQ32_spl|~sQ9_spl|~sQ17_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f374,f380,f383,f252,f293])).
% 0.13/0.41 fof(f387,definition,(
% 0.13/0.41 ![X0,X1]: (sQ33_spl <=> (X0=relation_inverse_image(empty_set,X1)|in(sK0_skl(X0,X1,empty_set),X0)|in(sK0_skl(X0,X1,empty_set),relation_inverse_image(empty_set,X1))|~in(sK0_skl(X0,X1,empty_set),relation_dom(empty_set))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f390,plain,(
% 0.13/0.41 sQ33_spl|~sQ32_spl|~sQ9_spl|~sQ17_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f375,f387,f383,f252,f293])).
% 0.13/0.41 fof(f391,plain,(
% 0.13/0.41 $false|sQ32_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f385,f97])).
% 0.13/0.41 fof(f392,plain,(
% 0.13/0.41 sQ32_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f391])).
% 0.13/0.41 fof(f398,plain,(
% 0.13/0.41 ![X0,X1]: (X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|~relation(sK4_skl)|~function(sK4_skl)|X0=relation_inverse_image(sK4_skl,X1)|~in(sK0_skl(X0,X1,sK4_skl),X0)|~in(sK0_skl(X0,X1,sK4_skl),relation_dom(sK4_skl))|~sQ16_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f290,f75])).
% 0.13/0.41 fof(f399,plain,(
% 0.13/0.41 ![X0,X1]: (X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|~relation(sK4_skl)|~function(sK4_skl)|in(sK0_skl(X0,X1,sK4_skl),relation_inverse_image(sK4_skl,X1))|~in(sK0_skl(X0,X1,sK4_skl),relation_dom(sK4_skl))|~sQ16_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f290,f220])).
% 0.13/0.41 fof(f404,definition,(
% 0.13/0.41 ![X0,X1]: (sQ34_spl <=> (X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|X0=relation_inverse_image(sK4_skl,X1)|~in(sK0_skl(X0,X1,sK4_skl),X0)|~in(sK0_skl(X0,X1,sK4_skl),relation_dom(sK4_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f407,definition,(
% 0.13/0.41 sQ35_spl <=> (relation(sK4_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f409,plain,(
% 0.13/0.41 ~relation(sK4_skl)|sQ35_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f407])).
% 0.13/0.41 fof(f410,plain,(
% 0.13/0.41 sQ34_spl|~sQ35_spl|~sQ7_spl|~sQ16_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f398,f404,f407,f245,f289])).
% 0.13/0.41 fof(f411,definition,(
% 0.13/0.41 ![X0,X1]: (sQ36_spl <=> (X0=relation_inverse_image(sK4_skl,X1)|in(sK0_skl(X0,X1,sK4_skl),X0)|in(sK0_skl(X0,X1,sK4_skl),relation_inverse_image(sK4_skl,X1))|~in(sK0_skl(X0,X1,sK4_skl),relation_dom(sK4_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f414,plain,(
% 0.13/0.41 sQ36_spl|~sQ35_spl|~sQ7_spl|~sQ16_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f399,f411,f407,f245,f289])).
% 0.13/0.41 fof(f415,plain,(
% 0.13/0.41 $false|sQ35_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f409,f111])).
% 0.13/0.41 fof(f416,plain,(
% 0.13/0.41 sQ35_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f415])).
% 0.13/0.41 fof(f418,plain,(
% 0.13/0.41 sK6_skl=empty_set),
% 0.13/0.41 inference(resolution,[status(thm)],[f122,f193])).
% 0.13/0.41 fof(f428,plain,(
% 0.13/0.41 ~sK19_skl=sK6_skl),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f418,f182])).
% 0.13/0.41 fof(f441,plain,(
% 0.13/0.41 ~empty(relation_dom(sK6_skl))|sQ29_spl),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f418,f364])).
% 0.13/0.41 fof(f451,plain,(
% 0.13/0.41 ![X0,X1]: (~sP0_prd(X0,X1)|X0=sK6_skl)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f418,f202])).
% 0.13/0.41 fof(f513,plain,(
% 0.13/0.41 function(sK7_skl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f124,f58])).
% 0.13/0.41 fof(f514,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK7_skl)|X0=relation_inverse_image(sK7_skl,X1)|in(sK0_skl(X0,X1,sK7_skl),X0)|in(apply(sK7_skl,sK0_skl(X0,X1,sK7_skl)),X1))),
% 0.13/0.41 inference(resolution,[status(thm)],[f125,f77])).
% 0.13/0.41 fof(f515,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK7_skl)|X0=relation_inverse_image(sK7_skl,X1)|in(sK0_skl(X0,X1,sK7_skl),X0)|in(sK0_skl(X0,X1,sK7_skl),relation_dom(sK7_skl)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f125,f76])).
% 0.13/0.41 fof(f516,definition,(
% 0.13/0.41 sQ37_spl <=> (function(sK7_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f518,plain,(
% 0.13/0.41 ~function(sK7_skl)|sQ37_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f516])).
% 0.13/0.41 fof(f519,definition,(
% 0.13/0.41 ![X0,X1]: (sQ38_spl <=> (X0=relation_inverse_image(sK7_skl,X1)|in(sK0_skl(X0,X1,sK7_skl),X0)|in(apply(sK7_skl,sK0_skl(X0,X1,sK7_skl)),X1)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f522,plain,(
% 0.13/0.41 ~sQ37_spl|sQ38_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f514,f516,f519])).
% 0.13/0.41 fof(f523,definition,(
% 0.13/0.41 ![X0,X1]: (sQ39_spl <=> (X0=relation_inverse_image(sK7_skl,X1)|in(sK0_skl(X0,X1,sK7_skl),X0)|in(sK0_skl(X0,X1,sK7_skl),relation_dom(sK7_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f526,plain,(
% 0.13/0.41 ~sQ37_spl|sQ39_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f515,f516,f523])).
% 0.13/0.41 fof(f527,plain,(
% 0.13/0.41 $false|sQ37_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f518,f513])).
% 0.13/0.41 fof(f528,plain,(
% 0.13/0.41 sQ37_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f527])).
% 0.13/0.41 fof(f531,plain,(
% 0.13/0.41 empty(relation_dom(sK6_skl))),
% 0.13/0.41 inference(resolution,[status(thm)],[f108,f122])).
% 0.13/0.41 fof(f532,plain,(
% 0.13/0.41 $false|sQ29_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f531,f441])).
% 0.13/0.41 fof(f533,plain,(
% 0.13/0.41 sQ29_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f532])).
% 0.13/0.41 fof(f572,plain,(
% 0.13/0.41 relation(sK20_skl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f336,f63])).
% 0.13/0.41 fof(f573,plain,(
% 0.13/0.41 $false|sQ11_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f572,f268])).
% 0.13/0.41 fof(f574,plain,(
% 0.13/0.41 sQ11_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f573])).
% 0.13/0.41 fof(f575,plain,(
% 0.13/0.41 ~relation(sK20_skl)|~function(sK20_skl)|in(sK22_skl,relation_inverse_image(sK20_skl,sK21_skl))|~in(sK22_skl,relation_dom(sK20_skl))|~sQ2_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f213,f220])).
% 0.13/0.41 fof(f578,plain,(
% 0.13/0.41 ~sQ11_spl|~sQ12_spl|sQ0_spl|~sQ13_spl|~sQ2_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f575,f266,f269,f205,f272,f212])).
% 0.13/0.41 fof(f606,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK10_skl)|X0=relation_inverse_image(sK10_skl,X1)|in(sK0_skl(X0,X1,sK10_skl),X0)|in(apply(sK10_skl,sK0_skl(X0,X1,sK10_skl)),X1))),
% 0.13/0.41 inference(resolution,[status(thm)],[f133,f77])).
% 0.13/0.41 fof(f607,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK10_skl)|X0=relation_inverse_image(sK10_skl,X1)|in(sK0_skl(X0,X1,sK10_skl),X0)|in(sK0_skl(X0,X1,sK10_skl),relation_dom(sK10_skl)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f133,f76])).
% 0.13/0.41 fof(f608,definition,(
% 0.13/0.41 sQ43_spl <=> (function(sK10_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f610,plain,(
% 0.13/0.41 ~function(sK10_skl)|sQ43_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f608])).
% 0.13/0.41 fof(f611,definition,(
% 0.13/0.41 ![X0,X1]: (sQ44_spl <=> (X0=relation_inverse_image(sK10_skl,X1)|in(sK0_skl(X0,X1,sK10_skl),X0)|in(apply(sK10_skl,sK0_skl(X0,X1,sK10_skl)),X1)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f614,plain,(
% 0.13/0.41 ~sQ43_spl|sQ44_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f606,f608,f611])).
% 0.13/0.41 fof(f615,definition,(
% 0.13/0.41 ![X0,X1]: (sQ45_spl <=> (X0=relation_inverse_image(sK10_skl,X1)|in(sK0_skl(X0,X1,sK10_skl),X0)|in(sK0_skl(X0,X1,sK10_skl),relation_dom(sK10_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f618,plain,(
% 0.13/0.41 ~sQ43_spl|sQ45_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f607,f608,f615])).
% 0.13/0.41 fof(f619,plain,(
% 0.13/0.41 $false|sQ43_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f610,f135])).
% 0.13/0.41 fof(f620,plain,(
% 0.13/0.41 sQ43_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f619])).
% 0.13/0.41 fof(f652,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK20_skl)|X0=relation_inverse_image(sK20_skl,X1)|in(sK0_skl(X0,X1,sK20_skl),X0)|in(apply(sK20_skl,sK0_skl(X0,X1,sK20_skl)),X1))),
% 0.13/0.41 inference(resolution,[status(thm)],[f572,f77])).
% 0.13/0.41 fof(f653,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK20_skl)|X0=relation_inverse_image(sK20_skl,X1)|in(sK0_skl(X0,X1,sK20_skl),X0)|in(sK0_skl(X0,X1,sK20_skl),relation_dom(sK20_skl)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f572,f76])).
% 0.13/0.41 fof(f654,definition,(
% 0.13/0.41 ![X0,X1]: (sQ46_spl <=> (X0=relation_inverse_image(sK20_skl,X1)|in(sK0_skl(X0,X1,sK20_skl),X0)|in(apply(sK20_skl,sK0_skl(X0,X1,sK20_skl)),X1)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f657,plain,(
% 0.13/0.41 ~sQ12_spl|sQ46_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f652,f269,f654])).
% 0.13/0.41 fof(f658,definition,(
% 0.13/0.41 ![X0,X1]: (sQ47_spl <=> (X0=relation_inverse_image(sK20_skl,X1)|in(sK0_skl(X0,X1,sK20_skl),X0)|in(sK0_skl(X0,X1,sK20_skl),relation_dom(sK20_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f661,plain,(
% 0.13/0.41 ~sQ12_spl|sQ47_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f653,f269,f658])).
% 0.13/0.41 fof(f670,plain,(
% 0.13/0.41 sK19_skl=sK6_skl|~sQ24_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f451,f328])).
% 0.13/0.41 fof(f678,plain,(
% 0.13/0.41 $false|~sQ24_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f670,f428])).
% 0.13/0.41 fof(f679,plain,(
% 0.13/0.41 ~sQ24_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f678])).
% 0.13/0.41 fof(f680,plain,(
% 0.13/0.41 $false|sQ23_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f326,f181])).
% 0.13/0.41 fof(f681,plain,(
% 0.13/0.41 sQ23_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f680])).
% 0.13/0.41 fof(f716,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK15_skl)|X0=relation_inverse_image(sK15_skl,X1)|in(sK0_skl(X0,X1,sK15_skl),X0)|in(apply(sK15_skl,sK0_skl(X0,X1,sK15_skl)),X1))),
% 0.13/0.41 inference(resolution,[status(thm)],[f149,f77])).
% 0.13/0.41 fof(f717,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK15_skl)|X0=relation_inverse_image(sK15_skl,X1)|in(sK0_skl(X0,X1,sK15_skl),X0)|in(sK0_skl(X0,X1,sK15_skl),relation_dom(sK15_skl)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f149,f76])).
% 0.13/0.41 fof(f718,definition,(
% 0.13/0.41 sQ53_spl <=> (function(sK15_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f720,plain,(
% 0.13/0.41 ~function(sK15_skl)|sQ53_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f718])).
% 0.13/0.41 fof(f721,definition,(
% 0.13/0.41 ![X0,X1]: (sQ54_spl <=> (X0=relation_inverse_image(sK15_skl,X1)|in(sK0_skl(X0,X1,sK15_skl),X0)|in(apply(sK15_skl,sK0_skl(X0,X1,sK15_skl)),X1)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f724,plain,(
% 0.13/0.41 ~sQ53_spl|sQ54_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f716,f718,f721])).
% 0.13/0.41 fof(f725,definition,(
% 0.13/0.41 ![X0,X1]: (sQ55_spl <=> (X0=relation_inverse_image(sK15_skl,X1)|in(sK0_skl(X0,X1,sK15_skl),X0)|in(sK0_skl(X0,X1,sK15_skl),relation_dom(sK15_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f728,plain,(
% 0.13/0.41 ~sQ53_spl|sQ55_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f717,f718,f725])).
% 0.13/0.41 fof(f729,plain,(
% 0.13/0.41 $false|sQ53_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f720,f150])).
% 0.13/0.41 fof(f730,plain,(
% 0.13/0.41 sQ53_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f729])).
% 0.13/0.41 fof(f768,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK17_skl)|X0=relation_inverse_image(sK17_skl,X1)|in(sK0_skl(X0,X1,sK17_skl),X0)|in(apply(sK17_skl,sK0_skl(X0,X1,sK17_skl)),X1))),
% 0.13/0.41 inference(resolution,[status(thm)],[f156,f77])).
% 0.13/0.41 fof(f769,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK17_skl)|X0=relation_inverse_image(sK17_skl,X1)|in(sK0_skl(X0,X1,sK17_skl),X0)|in(sK0_skl(X0,X1,sK17_skl),relation_dom(sK17_skl)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f156,f76])).
% 0.13/0.41 fof(f770,definition,(
% 0.13/0.41 sQ61_spl <=> (function(sK17_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f772,plain,(
% 0.13/0.41 ~function(sK17_skl)|sQ61_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f770])).
% 0.13/0.41 fof(f773,definition,(
% 0.13/0.41 ![X0,X1]: (sQ62_spl <=> (X0=relation_inverse_image(sK17_skl,X1)|in(sK0_skl(X0,X1,sK17_skl),X0)|in(apply(sK17_skl,sK0_skl(X0,X1,sK17_skl)),X1)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f776,plain,(
% 0.13/0.41 ~sQ61_spl|sQ62_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f768,f770,f773])).
% 0.13/0.41 fof(f777,definition,(
% 0.13/0.41 ![X0,X1]: (sQ63_spl <=> (X0=relation_inverse_image(sK17_skl,X1)|in(sK0_skl(X0,X1,sK17_skl),X0)|in(sK0_skl(X0,X1,sK17_skl),relation_dom(sK17_skl))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f780,plain,(
% 0.13/0.41 ~sQ61_spl|sQ63_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f769,f770,f777])).
% 0.13/0.41 fof(f781,plain,(
% 0.13/0.41 $false|sQ61_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f772,f158])).
% 0.13/0.41 fof(f782,plain,(
% 0.13/0.41 sQ61_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f781])).
% 0.13/0.41 fof(f799,plain,(
% 0.13/0.41 relation_of2(sK20_skl,sK18_skl,sK19_skl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f163,f181])).
% 0.13/0.41 fof(f800,plain,(
% 0.13/0.41 relation_dom_as_subset(sK18_skl,sK19_skl,sK20_skl)=relation_dom(sK20_skl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f799,f160])).
% 0.13/0.41 fof(f803,plain,(
% 0.13/0.41 in(sK22_skl,sK18_skl)|~sQ25_spl|~sQ13_spl),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f806,f273])).
% 0.13/0.41 fof(f806,plain,(
% 0.13/0.41 sK18_skl=relation_dom(sK20_skl)|~sQ25_spl),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f331,f800])).
% 0.13/0.41 fof(f808,plain,(
% 0.13/0.41 sQ1_spl|~sQ25_spl|~sQ13_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f803,f208,f330,f272])).
% 0.13/0.41 fof(f809,plain,(
% 0.13/0.41 ~in(sK22_skl,sK18_skl)|~sQ25_spl|sQ13_spl),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f806,f274])).
% 0.13/0.41 fof(f810,plain,(
% 0.13/0.41 $false|~sQ1_spl|~sQ25_spl|sQ13_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f809,f209])).
% 0.13/0.41 fof(f811,plain,(
% 0.13/0.41 ~sQ1_spl|~sQ25_spl|sQ13_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f810])).
% 0.13/0.41 fof(f812,plain,(
% 0.13/0.41 $false),
% 0.13/0.42 inference(sat_refutation,[status(thm)],[f211,f215,f216,f251,f258,f260,f262,f275,f276,f284,f286,f292,f296,f306,f310,f312,f320,f322,f333,f335,f344,f365,f369,f386,f390,f392,f410,f414,f416,f522,f526,f528,f533,f574,f578,f614,f618,f620,f657,f661,f679,f681,f724,f728,f730,f776,f780,f782,f808,f811])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.45 % Elapsed time: 0.072739 seconds
% 0.13/0.45 % CPU time: 0.198483 seconds
% 0.13/0.45 % Total memory used: 84.446 MB
% 0.13/0.45 % Net memory used: 84.342 MB
%------------------------------------------------------------------------------