%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU028+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:21:36 PM UTC 2026
% Result : Theorem 54.82s 7.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU028+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n011.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 05:47:25 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 54.82/7.54 % Refutation found
% 54.82/7.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 54.82/7.54 % SZS output start CNFRefutation for theBenchmark
% 54.82/7.54 fof(f1,axiom,(
% 54.82/7.54 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f2,axiom,(
% 54.82/7.54 (! [A] :( empty(A)=> function(A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f3,axiom,(
% 54.82/7.54 (! [A] :( empty(A)=> relation(A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f4,axiom,(
% 54.82/7.54 (! [A] :( ( relation(A)& empty(A)& function(A) )=> ( relation(A)& function(A)& one_to_one(A) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f5,axiom,(
% 54.82/7.54 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f6,axiom,(
% 54.82/7.54 (! [A,B] :( ( relation(A)& relation(B) )=> relation(relation_composition(A,B)) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f7,axiom,(
% 54.82/7.54 (! [A] : relation(identity_relation(A)) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f8,axiom,(
% 54.82/7.54 (! [A] :(? [B] : element(B,A) ))),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f9,axiom,(
% 54.82/7.54 (! [A,B] :( ( empty(A)& relation(B) )=> ( empty(relation_composition(B,A))& relation(relation_composition(B,A)) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f10,axiom,(
% 54.82/7.54 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f11,axiom,(
% 54.82/7.54 (! [A,B] :( ( relation(A)& function(A)& relation(B)& function(B) )=> ( relation(relation_composition(A,B))& function(relation_composition(A,B)) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f14,axiom,(
% 54.82/7.54 (! [A] :( relation(identity_relation(A))& function(identity_relation(A)) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f17,axiom,(
% 54.82/7.54 (! [A] :( ( ~ empty(A)& relation(A) )=> ~ empty(relation_rng(A)) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f18,axiom,(
% 54.82/7.54 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f19,axiom,(
% 54.82/7.54 (! [A] :( empty(A)=> ( empty(relation_rng(A))& relation(relation_rng(A)) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f20,axiom,(
% 54.82/7.54 (! [A,B] :( ( empty(A)& relation(B) )=> ( empty(relation_composition(A,B))& relation(relation_composition(A,B)) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f21,axiom,(
% 54.82/7.54 (? [A] :( relation(A)& function(A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f22,axiom,(
% 54.82/7.54 (? [A] :( empty(A)& relation(A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f24,axiom,(
% 54.82/7.54 (? [A] : empty(A) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f25,axiom,(
% 54.82/7.54 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f26,axiom,(
% 54.82/7.54 (? [A] :( ~ empty(A)& relation(A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f27,axiom,(
% 54.82/7.54 (! [A] :(? [B] :( element(B,powerset(A))& empty(B) ) ))),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f29,axiom,(
% 54.82/7.54 (? [A] :( relation(A)& function(A)& one_to_one(A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f30,axiom,(
% 54.82/7.54 (? [A] :( relation(A)& relation_empty_yielding(A) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f31,axiom,(
% 54.82/7.54 (! [A,B] : subset(A,A) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f33,axiom,(
% 54.82/7.54 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f34,axiom,(
% 54.82/7.54 (! [A,B] :( ( relation(B)& function(B) )=> ( B = identity_relation(A)<=> ( relation_dom(B) = A& (! [C] :( in(C,A)=> apply(B,C) = C ) )) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f35,axiom,(
% 54.82/7.54 (! [A,B] :( element(A,powerset(B))<=> subset(A,B) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f36,axiom,(
% 54.82/7.54 (! [A,B,C] :( ( in(A,B)& element(B,powerset(C)) )=> element(A,C) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f37,axiom,(
% 54.82/7.54 (! [A,B] :( ( relation(B)& function(B) )=> ( ( one_to_one(B)& in(A,relation_dom(B)) )=> ( A = apply(function_inverse(B),apply(B,A))& A = apply(relation_composition(B,function_inverse(B)),A) ) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f38,axiom,(
% 54.82/7.54 (! [A,B] :( ( relation(B)& function(B) )=> ( ( one_to_one(B)& in(A,relation_rng(B)) )=> ( A = apply(B,apply(function_inverse(B),A))& A = apply(relation_composition(function_inverse(B),B),A) ) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f39,axiom,(
% 54.82/7.54 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_dom(relation_composition(A,function_inverse(A))) = relation_dom(A)& relation_rng(relation_composition(A,function_inverse(A))) = relation_dom(A) ) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f40,axiom,(
% 54.82/7.54 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_dom(relation_composition(function_inverse(A),A)) = relation_rng(A)& relation_rng(relation_composition(function_inverse(A),A)) = relation_rng(A) ) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f41,axiom,(
% 54.82/7.54 (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f42,conjecture,(
% 54.82/7.54 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_composition(A,function_inverse(A)) = identity_relation(relation_dom(A))& relation_composition(function_inverse(A),A) = identity_relation(relation_rng(A)) ) ) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f43,negated_conjecture,(
% 54.82/7.54 ~((! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_composition(A,function_inverse(A)) = identity_relation(relation_dom(A))& relation_composition(function_inverse(A),A) = identity_relation(relation_rng(A)) ) ) ) ))),
% 54.82/7.54 inference(negated_conjecture,[status(cth)],[f42])).
% 54.82/7.54 fof(f44,axiom,(
% 54.82/7.54 (! [A] :( empty(A)=> A = empty_set ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f45,axiom,(
% 54.82/7.54 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f46,axiom,(
% 54.82/7.54 (! [A,B] :~ ( empty(A)& A != B& empty(B) ) )),
% 54.82/7.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.82/7.54 fof(f47,plain,(
% 54.82/7.54 ![A,B]: (~in(A,B)|~in(B,A))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 54.82/7.54 fof(f48,plain,(
% 54.82/7.54 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f47])).
% 54.82/7.54 fof(f49,plain,(
% 54.82/7.54 ![A]: (~empty(A)|function(A))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 54.82/7.54 fof(f50,plain,(
% 54.82/7.54 ![X0]: (~empty(X0)|function(X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f49])).
% 54.82/7.54 fof(f51,plain,(
% 54.82/7.54 ![A]: (~empty(A)|relation(A))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 54.82/7.54 fof(f52,plain,(
% 54.82/7.54 ![X0]: (~empty(X0)|relation(X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f51])).
% 54.82/7.54 fof(f53,plain,(
% 54.82/7.54 ![A]: (((~relation(A)|~empty(A))|~function(A))|((relation(A)&function(A))&one_to_one(A)))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 54.82/7.54 fof(f56,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~empty(X0)|~function(X0)|one_to_one(X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f53])).
% 54.82/7.54 fof(f57,plain,(
% 54.82/7.54 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 54.82/7.54 fof(f58,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f57])).
% 54.82/7.54 fof(f59,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f57])).
% 54.82/7.54 fof(f60,plain,(
% 54.82/7.54 ![A,B]: ((~relation(A)|~relation(B))|relation(relation_composition(A,B)))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 54.82/7.54 fof(f61,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~relation(X1)|relation(relation_composition(X0,X1)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f60])).
% 54.82/7.54 fof(f62,plain,(
% 54.82/7.54 ![X0]: (relation(identity_relation(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f7])).
% 54.82/7.54 fof(f63,plain,(
% 54.82/7.54 ![A]: element(sK0_skl(A),A)),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f8])).
% 54.82/7.54 fof(f64,plain,(
% 54.82/7.54 ![X0]: (element(sK0_skl(X0),X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f63])).
% 54.82/7.54 fof(f65,plain,(
% 54.82/7.54 ![A,B]: ((~empty(A)|~relation(B))|(empty(relation_composition(B,A))&relation(relation_composition(B,A))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 54.82/7.54 fof(f66,plain,(
% 54.82/7.54 ![X0,X1]: (~empty(X0)|~relation(X1)|empty(relation_composition(X1,X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f65])).
% 54.82/7.54 fof(f68,plain,(
% 54.82/7.54 empty(empty_set)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f10])).
% 54.82/7.54 fof(f69,plain,(
% 54.82/7.54 relation(empty_set)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f10])).
% 54.82/7.54 fof(f71,plain,(
% 54.82/7.54 ![A,B]: ((((~relation(A)|~function(A))|~relation(B))|~function(B))|(relation(relation_composition(A,B))&function(relation_composition(A,B))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 54.82/7.54 fof(f73,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|function(relation_composition(X0,X1)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f71])).
% 54.82/7.54 fof(f76,plain,(
% 54.82/7.54 (![A]: relation(identity_relation(A)))&(![A]: function(identity_relation(A)))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f14])).
% 54.82/7.54 fof(f78,plain,(
% 54.82/7.54 ![X0]: (function(identity_relation(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f76])).
% 54.82/7.54 fof(f83,plain,(
% 54.82/7.54 ![A]: ((empty(A)|~relation(A))|~empty(relation_rng(A)))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 54.82/7.54 fof(f84,plain,(
% 54.82/7.54 ![X0]: (empty(X0)|~relation(X0)|~empty(relation_rng(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f83])).
% 54.82/7.54 fof(f85,plain,(
% 54.82/7.54 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 54.82/7.54 fof(f86,plain,(
% 54.82/7.54 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f85])).
% 54.82/7.54 fof(f88,plain,(
% 54.82/7.54 ![A]: (~empty(A)|(empty(relation_rng(A))&relation(relation_rng(A))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 54.82/7.54 fof(f89,plain,(
% 54.82/7.54 ![X0]: (~empty(X0)|empty(relation_rng(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f88])).
% 54.82/7.54 fof(f91,plain,(
% 54.82/7.54 ![A,B]: ((~empty(A)|~relation(B))|(empty(relation_composition(A,B))&relation(relation_composition(A,B))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 54.82/7.54 fof(f92,plain,(
% 54.82/7.54 ![X0,X1]: (~empty(X0)|~relation(X1)|empty(relation_composition(X0,X1)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f91])).
% 54.82/7.54 fof(f94,plain,(
% 54.82/7.54 (relation(sK1_skl)&function(sK1_skl))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f21])).
% 54.82/7.54 fof(f95,plain,(
% 54.82/7.54 relation(sK1_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f94])).
% 54.82/7.54 fof(f96,plain,(
% 54.82/7.54 function(sK1_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f94])).
% 54.82/7.54 fof(f97,plain,(
% 54.82/7.54 (empty(sK2_skl)&relation(sK2_skl))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f22])).
% 54.82/7.54 fof(f98,plain,(
% 54.82/7.54 empty(sK2_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f97])).
% 54.82/7.54 fof(f104,plain,(
% 54.82/7.54 empty(sK4_skl)),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f24])).
% 54.82/7.54 fof(f105,plain,(
% 54.82/7.54 empty(sK4_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f104])).
% 54.82/7.54 fof(f106,plain,(
% 54.82/7.54 ((relation(sK5_skl)&empty(sK5_skl))&function(sK5_skl))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f25])).
% 54.82/7.54 fof(f107,plain,(
% 54.82/7.54 relation(sK5_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f106])).
% 54.82/7.54 fof(f108,plain,(
% 54.82/7.54 empty(sK5_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f106])).
% 54.82/7.54 fof(f109,plain,(
% 54.82/7.54 function(sK5_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f106])).
% 54.82/7.54 fof(f110,plain,(
% 54.82/7.54 (~empty(sK6_skl)&relation(sK6_skl))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f26])).
% 54.82/7.54 fof(f112,plain,(
% 54.82/7.54 relation(sK6_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f110])).
% 54.82/7.54 fof(f113,plain,(
% 54.82/7.54 ![A]: (element(sK7_skl(A),powerset(A))&empty(sK7_skl(A)))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f27])).
% 54.82/7.54 fof(f114,plain,(
% 54.82/7.54 ![X0]: (element(sK7_skl(X0),powerset(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f113])).
% 54.82/7.54 fof(f115,plain,(
% 54.82/7.54 ![X0]: (empty(sK7_skl(X0)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f113])).
% 54.82/7.54 fof(f118,plain,(
% 54.82/7.54 ((relation(sK9_skl)&function(sK9_skl))&one_to_one(sK9_skl))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f29])).
% 54.82/7.54 fof(f119,plain,(
% 54.82/7.54 relation(sK9_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f118])).
% 54.82/7.54 fof(f120,plain,(
% 54.82/7.54 function(sK9_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f118])).
% 54.82/7.54 fof(f121,plain,(
% 54.82/7.54 one_to_one(sK9_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f118])).
% 54.82/7.54 fof(f122,plain,(
% 54.82/7.54 (relation(sK10_skl)&relation_empty_yielding(sK10_skl))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f30])).
% 54.82/7.54 fof(f123,plain,(
% 54.82/7.54 relation(sK10_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f122])).
% 54.82/7.54 fof(f125,plain,(
% 54.82/7.54 ![A]: subset(A,A)),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f31])).
% 54.82/7.54 fof(f126,plain,(
% 54.82/7.54 ![X0]: (subset(X0,X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f125])).
% 54.82/7.54 fof(f129,plain,(
% 54.82/7.54 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 54.82/7.54 fof(f130,plain,(
% 54.82/7.54 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f129])).
% 54.82/7.54 fof(f131,plain,(
% 54.82/7.54 ![A,B]: ((~relation(B)|~function(B))|(B=identity_relation(A)<=>(relation_dom(B)=A&(![C]: (~in(C,A)|apply(B,C)=C)))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 54.82/7.54 fof(f132,plain,(
% 54.82/7.54 ![A,B]: ((~relation(B)|~function(B))|((~B=identity_relation(A)|(relation_dom(B)=A&(![C]: (~in(C,A)|apply(B,C)=C))))&(B=identity_relation(A)|(~relation_dom(B)=A|(?[C]: (in(C,A)&~apply(B,C)=C))))))),
% 54.82/7.54 inference(NNF_transformation,[status(thm)],[f131])).
% 54.82/7.54 fof(f133,plain,(
% 54.82/7.54 ![B]: ((~relation(B)|~function(B))|((![A]: (~B=identity_relation(A)|(relation_dom(B)=A&(![C]: (~in(C,A)|apply(B,C)=C)))))&(![A]: (B=identity_relation(A)|(~relation_dom(B)=A|(?[C]: (in(C,A)&~apply(B,C)=C)))))))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f132])).
% 54.82/7.54 fof(f134,plain,(
% 54.82/7.54 ![B]: ((~relation(B)|~function(B))|((![A]: (~B=identity_relation(A)|(relation_dom(B)=A&(![C]: (~in(C,A)|apply(B,C)=C)))))&(![A]: (B=identity_relation(A)|(~relation_dom(B)=A|(in(sK11_skl(A,B),A)&~apply(B,sK11_skl(A,B))=sK11_skl(A,B)))))))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(C,sK11_skl(A,B))],[f133])).
% 54.82/7.54 fof(f135,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~function(X0)|~X0=identity_relation(X1)|relation_dom(X0)=X1)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f134])).
% 54.82/7.54 fof(f136,plain,(
% 54.82/7.54 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~X0=identity_relation(X1)|~in(X2,X1)|apply(X0,X2)=X2)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f134])).
% 54.82/7.54 fof(f137,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~function(X0)|X0=identity_relation(X1)|~relation_dom(X0)=X1|in(sK11_skl(X1,X0),X1))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f134])).
% 54.82/7.54 fof(f138,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~function(X0)|X0=identity_relation(X1)|~relation_dom(X0)=X1|~apply(X0,sK11_skl(X1,X0))=sK11_skl(X1,X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f134])).
% 54.82/7.54 fof(f139,plain,(
% 54.82/7.54 ![A,B]: ((~element(A,powerset(B))|subset(A,B))&(element(A,powerset(B))|~subset(A,B)))),
% 54.82/7.54 inference(NNF_transformation,[status(thm)],[f35])).
% 54.82/7.54 fof(f140,plain,(
% 54.82/7.54 (![A,B]: (~element(A,powerset(B))|subset(A,B)))&(![A,B]: (element(A,powerset(B))|~subset(A,B)))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f139])).
% 54.82/7.54 fof(f142,plain,(
% 54.82/7.54 ![X0,X1]: (element(X0,powerset(X1))|~subset(X0,X1))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f140])).
% 54.82/7.54 fof(f143,plain,(
% 54.82/7.54 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|element(A,C))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 54.82/7.54 fof(f144,plain,(
% 54.82/7.54 ![A,C]: ((![B]: (~in(A,B)|~element(B,powerset(C))))|element(A,C))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f143])).
% 54.82/7.54 fof(f145,plain,(
% 54.82/7.54 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|element(X0,X2))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f144])).
% 54.82/7.54 fof(f146,plain,(
% 54.82/7.54 ![A,B]: ((~relation(B)|~function(B))|((~one_to_one(B)|~in(A,relation_dom(B)))|(A=apply(function_inverse(B),apply(B,A))&A=apply(relation_composition(B,function_inverse(B)),A))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 54.82/7.54 fof(f147,plain,(
% 54.82/7.54 ![B]: ((~relation(B)|~function(B))|(![A]: ((~one_to_one(B)|~in(A,relation_dom(B)))|(A=apply(function_inverse(B),apply(B,A))&A=apply(relation_composition(B,function_inverse(B)),A)))))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f146])).
% 54.82/7.54 fof(f148,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~in(X1,relation_dom(X0))|X1=apply(function_inverse(X0),apply(X0,X1)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f147])).
% 54.82/7.54 fof(f149,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~in(X1,relation_dom(X0))|X1=apply(relation_composition(X0,function_inverse(X0)),X1))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f147])).
% 54.82/7.54 fof(f150,plain,(
% 54.82/7.54 ![A,B]: ((~relation(B)|~function(B))|((~one_to_one(B)|~in(A,relation_rng(B)))|(A=apply(B,apply(function_inverse(B),A))&A=apply(relation_composition(function_inverse(B),B),A))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 54.82/7.54 fof(f151,plain,(
% 54.82/7.54 ![B]: ((~relation(B)|~function(B))|(![A]: ((~one_to_one(B)|~in(A,relation_rng(B)))|(A=apply(B,apply(function_inverse(B),A))&A=apply(relation_composition(function_inverse(B),B),A)))))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f150])).
% 54.82/7.54 fof(f152,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~in(X1,relation_rng(X0))|X1=apply(X0,apply(function_inverse(X0),X1)))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f151])).
% 54.82/7.54 fof(f153,plain,(
% 54.82/7.54 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~in(X1,relation_rng(X0))|X1=apply(relation_composition(function_inverse(X0),X0),X1))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f151])).
% 54.82/7.54 fof(f154,plain,(
% 54.82/7.54 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(relation_dom(relation_composition(A,function_inverse(A)))=relation_dom(A)&relation_rng(relation_composition(A,function_inverse(A)))=relation_dom(A))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 54.82/7.54 fof(f155,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(relation_composition(X0,function_inverse(X0)))=relation_dom(X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f154])).
% 54.82/7.54 fof(f156,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_rng(relation_composition(X0,function_inverse(X0)))=relation_dom(X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f154])).
% 54.82/7.54 fof(f157,plain,(
% 54.82/7.54 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(relation_dom(relation_composition(function_inverse(A),A))=relation_rng(A)&relation_rng(relation_composition(function_inverse(A),A))=relation_rng(A))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 54.82/7.54 fof(f158,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(relation_composition(function_inverse(X0),X0))=relation_rng(X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f157])).
% 54.82/7.54 fof(f159,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_rng(relation_composition(function_inverse(X0),X0))=relation_rng(X0))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f157])).
% 54.82/7.54 fof(f160,plain,(
% 54.82/7.54 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 54.82/7.54 fof(f161,plain,(
% 54.82/7.54 ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f160])).
% 54.82/7.54 fof(f162,plain,(
% 54.82/7.54 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f161])).
% 54.82/7.54 fof(f163,plain,(
% 54.82/7.54 (?[A]: ((relation(A)&function(A))&(one_to_one(A)&(~relation_composition(A,function_inverse(A))=identity_relation(relation_dom(A))|~relation_composition(function_inverse(A),A)=identity_relation(relation_rng(A))))))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 54.82/7.54 fof(f164,plain,(
% 54.82/7.54 ((relation(sK12_skl)&function(sK12_skl))&(one_to_one(sK12_skl)&(~relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(sK12_skl))|~relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_rng(sK12_skl)))))),
% 54.82/7.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f163])).
% 54.82/7.54 fof(f165,plain,(
% 54.82/7.54 relation(sK12_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f164])).
% 54.82/7.54 fof(f166,plain,(
% 54.82/7.54 function(sK12_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f164])).
% 54.82/7.54 fof(f167,plain,(
% 54.82/7.54 one_to_one(sK12_skl)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f164])).
% 54.82/7.54 fof(f168,plain,(
% 54.82/7.54 ~relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(sK12_skl))|~relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_rng(sK12_skl))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f164])).
% 54.82/7.54 fof(f169,plain,(
% 54.82/7.54 ![A]: (~empty(A)|A=empty_set)),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 54.82/7.54 fof(f170,plain,(
% 54.82/7.54 ![X0]: (~empty(X0)|X0=empty_set)),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f169])).
% 54.82/7.54 fof(f171,plain,(
% 54.82/7.54 ![A,B]: (~in(A,B)|~empty(B))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 54.82/7.54 fof(f172,plain,(
% 54.82/7.54 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f171])).
% 54.82/7.54 fof(f173,plain,(
% 54.82/7.54 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f172])).
% 54.82/7.54 fof(f174,plain,(
% 54.82/7.54 ![A,B]: ((~empty(A)|A=B)|~empty(B))),
% 54.82/7.54 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 54.82/7.54 fof(f175,plain,(
% 54.82/7.54 ![B]: ((![A]: (~empty(A)|A=B))|~empty(B))),
% 54.82/7.54 inference(miniscoping,[status(thm)],[f174])).
% 54.82/7.54 fof(f176,plain,(
% 54.82/7.54 ![X0,X1]: (~empty(X0)|X0=X1|~empty(X1))),
% 54.82/7.54 inference(cnf_transformation,[status(thm)],[f175])).
% 54.82/7.54 fof(f177,definition,(
% 54.82/7.54 sQ0_spl <=> (relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(sK12_skl)))),
% 54.82/7.54 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 54.82/7.54 fof(f179,plain,(
% 54.82/7.54 ~relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(sK12_skl))|sQ0_spl),
% 54.82/7.54 inference(component_clause,[status(thm)],[f177])).
% 54.82/7.54 fof(f180,definition,(
% 54.82/7.54 sQ1_spl <=> (relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_rng(sK12_skl)))),
% 54.82/7.54 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 54.82/7.54 fof(f182,plain,(
% 54.82/7.54 ~relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_rng(sK12_skl))|sQ1_spl),
% 54.82/7.54 inference(component_clause,[status(thm)],[f180])).
% 54.82/7.54 fof(f183,plain,(
% 54.82/7.54 ~sQ0_spl|~sQ1_spl),
% 54.82/7.54 inference(split_clause,[status(thm)],[f168,f177,f180])).
% 54.82/7.54 fof(f184,plain,(
% 54.82/7.54 ![X0]: (~empty(X0)|~function(X0)|one_to_one(X0))),
% 54.82/7.54 inference(forward_subsumption_resolution,[status(thm)],[f56,f52])).
% 54.82/7.54 fof(f185,plain,(
% 54.82/7.54 ![X1]: (~relation(identity_relation(X1))|~function(identity_relation(X1))|relation_dom(identity_relation(X1))=X1)),
% 54.82/7.54 inference(destructive_equality_resolution,[status(thm)],[f135])).
% 54.82/7.54 fof(f186,plain,(
% 54.82/7.54 ![X0]: (~function(identity_relation(X0))|relation_dom(identity_relation(X0))=X0)),
% 54.82/7.54 inference(forward_subsumption_resolution,[status(thm)],[f185,f62])).
% 54.82/7.54 fof(f187,plain,(
% 54.82/7.54 ![X1,X2]: (~relation(identity_relation(X1))|~function(identity_relation(X1))|~in(X2,X1)|apply(identity_relation(X1),X2)=X2)),
% 54.82/7.54 inference(destructive_equality_resolution,[status(thm)],[f136])).
% 54.82/7.54 fof(f188,plain,(
% 54.82/7.54 ![X0,X1]: (~function(identity_relation(X0))|~in(X1,X0)|apply(identity_relation(X0),X1)=X1)),
% 54.82/7.54 inference(forward_subsumption_resolution,[status(thm)],[f187,f62])).
% 54.82/7.54 fof(f189,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0))|in(sK11_skl(relation_dom(X0),X0),relation_dom(X0)))),
% 54.82/7.54 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 54.82/7.54 fof(f190,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0))|~apply(X0,sK11_skl(relation_dom(X0),X0))=sK11_skl(relation_dom(X0),X0))),
% 54.82/7.54 inference(destructive_equality_resolution,[status(thm)],[f138])).
% 54.82/7.54 fof(f191,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|empty(relation_composition(empty_set,X0)))),
% 54.82/7.54 inference(resolution,[status(thm)],[f68,f92])).
% 54.82/7.54 fof(f192,plain,(
% 54.82/7.54 empty(relation_rng(empty_set))),
% 54.82/7.54 inference(resolution,[status(thm)],[f68,f89])).
% 54.82/7.54 fof(f194,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|empty(relation_composition(X0,empty_set)))),
% 54.82/7.54 inference(resolution,[status(thm)],[f68,f66])).
% 54.82/7.54 fof(f197,plain,(
% 54.82/7.54 empty(relation_rng(sK2_skl))),
% 54.82/7.54 inference(resolution,[status(thm)],[f98,f89])).
% 54.82/7.54 fof(f201,plain,(
% 54.82/7.54 empty(sK2_skl)|~relation(sK2_skl)),
% 54.82/7.54 inference(resolution,[status(thm)],[f197,f84])).
% 54.82/7.54 fof(f207,definition,(
% 54.82/7.54 sQ2_spl <=> (empty(sK2_skl))),
% 54.82/7.54 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 54.82/7.54 fof(f210,definition,(
% 54.82/7.54 sQ3_spl <=> (relation(sK2_skl))),
% 54.82/7.54 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 54.82/7.54 fof(f212,plain,(
% 54.82/7.54 ~relation(sK2_skl)|sQ3_spl),
% 54.82/7.54 inference(component_clause,[status(thm)],[f210])).
% 54.82/7.54 fof(f213,plain,(
% 54.82/7.54 sQ2_spl|~sQ3_spl),
% 54.82/7.54 inference(split_clause,[status(thm)],[f201,f207,f210])).
% 54.82/7.54 fof(f214,plain,(
% 54.82/7.54 ![X0]: (relation_dom(identity_relation(X0))=X0)),
% 54.82/7.54 inference(resolution,[status(thm)],[f186,f78])).
% 54.82/7.54 fof(f224,plain,(
% 54.82/7.54 ~relation(sK12_skl)|~function(sK12_skl)|relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl)))=relation_dom(sK12_skl)),
% 54.82/7.54 inference(resolution,[status(thm)],[f155,f167])).
% 54.82/7.54 fof(f225,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|relation_dom(relation_composition(X0,function_inverse(X0)))=relation_dom(X0)|~empty(X0)|~function(X0))),
% 54.82/7.54 inference(resolution,[status(thm)],[f155,f184])).
% 54.82/7.54 fof(f226,definition,(
% 54.82/7.54 sQ4_spl <=> (relation(sK12_skl))),
% 54.82/7.54 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 54.82/7.54 fof(f228,plain,(
% 54.82/7.54 ~relation(sK12_skl)|sQ4_spl),
% 54.82/7.54 inference(component_clause,[status(thm)],[f226])).
% 54.82/7.54 fof(f229,definition,(
% 54.82/7.54 sQ5_spl <=> (function(sK12_skl))),
% 54.82/7.54 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 54.82/7.54 fof(f231,plain,(
% 54.82/7.54 ~function(sK12_skl)|sQ5_spl),
% 54.82/7.54 inference(component_clause,[status(thm)],[f229])).
% 54.82/7.54 fof(f232,definition,(
% 54.82/7.54 sQ6_spl <=> (relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl)))=relation_dom(sK12_skl))),
% 54.82/7.54 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 54.82/7.54 fof(f233,plain,(
% 54.82/7.54 relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl)))=relation_dom(sK12_skl)|~sQ6_spl),
% 54.82/7.54 inference(component_clause,[status(thm)],[f232])).
% 54.82/7.54 fof(f235,plain,(
% 54.82/7.54 ~sQ4_spl|~sQ5_spl|sQ6_spl),
% 54.82/7.54 inference(split_clause,[status(thm)],[f224,f226,f229,f232])).
% 54.82/7.54 fof(f236,plain,(
% 54.82/7.54 ![X0]: (~relation(X0)|~function(X0)|relation_dom(relation_composition(X0,function_inverse(X0)))=relation_dom(X0)|~empty(X0))),
% 54.82/7.55 inference(duplicate_literals_removal,[status(thm)],[f225])).
% 54.82/7.55 fof(f237,plain,(
% 54.82/7.55 ![X0]: (~function(X0)|relation_dom(relation_composition(X0,function_inverse(X0)))=relation_dom(X0)|~empty(X0))),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f236,f52])).
% 54.82/7.55 fof(f238,plain,(
% 54.82/7.55 ~relation(sK12_skl)|~function(sK12_skl)|relation_rng(relation_composition(sK12_skl,function_inverse(sK12_skl)))=relation_dom(sK12_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f156,f167])).
% 54.82/7.55 fof(f239,plain,(
% 54.82/7.55 ![X0]: (~relation(X0)|~function(X0)|relation_rng(relation_composition(X0,function_inverse(X0)))=relation_dom(X0)|~empty(X0)|~function(X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f156,f184])).
% 54.82/7.55 fof(f240,definition,(
% 54.82/7.55 sQ7_spl <=> (relation_rng(relation_composition(sK12_skl,function_inverse(sK12_skl)))=relation_dom(sK12_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f243,plain,(
% 54.82/7.55 ~sQ4_spl|~sQ5_spl|sQ7_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f238,f226,f229,f240])).
% 54.82/7.55 fof(f244,plain,(
% 54.82/7.55 ![X0]: (~relation(X0)|~function(X0)|relation_rng(relation_composition(X0,function_inverse(X0)))=relation_dom(X0)|~empty(X0))),
% 54.82/7.55 inference(duplicate_literals_removal,[status(thm)],[f239])).
% 54.82/7.55 fof(f245,plain,(
% 54.82/7.55 ![X0]: (~function(X0)|relation_rng(relation_composition(X0,function_inverse(X0)))=relation_dom(X0)|~empty(X0))),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f244,f52])).
% 54.82/7.55 fof(f246,plain,(
% 54.82/7.55 $false|sQ5_spl),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f231,f166])).
% 54.82/7.55 fof(f247,plain,(
% 54.82/7.55 sQ5_spl),
% 54.82/7.55 inference(contradiction_clause,[status(thm)],[f246])).
% 54.82/7.55 fof(f248,plain,(
% 54.82/7.55 $false|sQ4_spl),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f228,f165])).
% 54.82/7.55 fof(f249,plain,(
% 54.82/7.55 sQ4_spl),
% 54.82/7.55 inference(contradiction_clause,[status(thm)],[f248])).
% 54.82/7.55 fof(f250,plain,(
% 54.82/7.55 ~relation(sK12_skl)|~function(sK12_skl)|relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl))=relation_rng(sK12_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f158,f167])).
% 54.82/7.55 fof(f251,plain,(
% 54.82/7.55 ![X0]: (~relation(X0)|~function(X0)|relation_dom(relation_composition(function_inverse(X0),X0))=relation_rng(X0)|~empty(X0)|~function(X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f158,f184])).
% 54.82/7.55 fof(f252,definition,(
% 54.82/7.55 sQ8_spl <=> (relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl))=relation_rng(sK12_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f253,plain,(
% 54.82/7.55 relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl))=relation_rng(sK12_skl)|~sQ8_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f252])).
% 54.82/7.55 fof(f255,plain,(
% 54.82/7.55 ~sQ4_spl|~sQ5_spl|sQ8_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f250,f226,f229,f252])).
% 54.82/7.55 fof(f256,plain,(
% 54.82/7.55 ![X0]: (~relation(X0)|~function(X0)|relation_dom(relation_composition(function_inverse(X0),X0))=relation_rng(X0)|~empty(X0))),
% 54.82/7.55 inference(duplicate_literals_removal,[status(thm)],[f251])).
% 54.82/7.55 fof(f257,plain,(
% 54.82/7.55 ![X0]: (~function(X0)|relation_dom(relation_composition(function_inverse(X0),X0))=relation_rng(X0)|~empty(X0))),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f256,f52])).
% 54.82/7.55 fof(f258,plain,(
% 54.82/7.55 ~relation(sK12_skl)|~function(sK12_skl)|relation_rng(relation_composition(function_inverse(sK12_skl),sK12_skl))=relation_rng(sK12_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f159,f167])).
% 54.82/7.55 fof(f259,plain,(
% 54.82/7.55 ![X0]: (~relation(X0)|~function(X0)|relation_rng(relation_composition(function_inverse(X0),X0))=relation_rng(X0)|~empty(X0)|~function(X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f159,f184])).
% 54.82/7.55 fof(f260,definition,(
% 54.82/7.55 sQ9_spl <=> (relation_rng(relation_composition(function_inverse(sK12_skl),sK12_skl))=relation_rng(sK12_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f263,plain,(
% 54.82/7.55 ~sQ4_spl|~sQ5_spl|sQ9_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f258,f226,f229,f260])).
% 54.82/7.55 fof(f264,plain,(
% 54.82/7.55 ![X0]: (~relation(X0)|~function(X0)|relation_rng(relation_composition(function_inverse(X0),X0))=relation_rng(X0)|~empty(X0))),
% 54.82/7.55 inference(duplicate_literals_removal,[status(thm)],[f259])).
% 54.82/7.55 fof(f265,plain,(
% 54.82/7.55 ![X0]: (~function(X0)|relation_rng(relation_composition(function_inverse(X0),X0))=relation_rng(X0)|~empty(X0))),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f264,f52])).
% 54.82/7.55 fof(f266,plain,(
% 54.82/7.55 ~relation(sK9_skl)|~function(sK9_skl)|relation_rng(relation_composition(function_inverse(sK9_skl),sK9_skl))=relation_rng(sK9_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f121,f159])).
% 54.82/7.55 fof(f267,plain,(
% 54.82/7.55 ~relation(sK9_skl)|~function(sK9_skl)|relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl))=relation_rng(sK9_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f121,f158])).
% 54.82/7.55 fof(f268,plain,(
% 54.82/7.55 ~relation(sK9_skl)|~function(sK9_skl)|relation_rng(relation_composition(sK9_skl,function_inverse(sK9_skl)))=relation_dom(sK9_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f121,f156])).
% 54.82/7.55 fof(f269,plain,(
% 54.82/7.55 ~relation(sK9_skl)|~function(sK9_skl)|relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl)))=relation_dom(sK9_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f121,f155])).
% 54.82/7.55 fof(f270,definition,(
% 54.82/7.55 sQ10_spl <=> (relation(sK9_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f272,plain,(
% 54.82/7.55 ~relation(sK9_skl)|sQ10_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f270])).
% 54.82/7.55 fof(f273,definition,(
% 54.82/7.55 sQ11_spl <=> (function(sK9_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f275,plain,(
% 54.82/7.55 ~function(sK9_skl)|sQ11_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f273])).
% 54.82/7.55 fof(f276,definition,(
% 54.82/7.55 sQ12_spl <=> (relation_rng(relation_composition(function_inverse(sK9_skl),sK9_skl))=relation_rng(sK9_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f279,plain,(
% 54.82/7.55 ~sQ10_spl|~sQ11_spl|sQ12_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f266,f270,f273,f276])).
% 54.82/7.55 fof(f280,definition,(
% 54.82/7.55 sQ13_spl <=> (relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl))=relation_rng(sK9_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f283,plain,(
% 54.82/7.55 ~sQ10_spl|~sQ11_spl|sQ13_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f267,f270,f273,f280])).
% 54.82/7.55 fof(f284,definition,(
% 54.82/7.55 sQ14_spl <=> (relation_rng(relation_composition(sK9_skl,function_inverse(sK9_skl)))=relation_dom(sK9_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f287,plain,(
% 54.82/7.55 ~sQ10_spl|~sQ11_spl|sQ14_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f268,f270,f273,f284])).
% 54.82/7.55 fof(f288,definition,(
% 54.82/7.55 sQ15_spl <=> (relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl)))=relation_dom(sK9_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f291,plain,(
% 54.82/7.55 ~sQ10_spl|~sQ11_spl|sQ15_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f269,f270,f273,f288])).
% 54.82/7.55 fof(f292,plain,(
% 54.82/7.55 $false|sQ11_spl),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f275,f120])).
% 54.82/7.55 fof(f293,plain,(
% 54.82/7.55 sQ11_spl),
% 54.82/7.55 inference(contradiction_clause,[status(thm)],[f292])).
% 54.82/7.55 fof(f294,plain,(
% 54.82/7.55 $false|sQ10_spl),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f272,f119])).
% 54.82/7.55 fof(f295,plain,(
% 54.82/7.55 sQ10_spl),
% 54.82/7.55 inference(contradiction_clause,[status(thm)],[f294])).
% 54.82/7.55 fof(f297,plain,(
% 54.82/7.55 empty(relation_rng(sK4_skl))),
% 54.82/7.55 inference(resolution,[status(thm)],[f105,f89])).
% 54.82/7.55 fof(f300,plain,(
% 54.82/7.55 relation(sK4_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f105,f52])).
% 54.82/7.55 fof(f302,plain,(
% 54.82/7.55 empty(relation_rng(sK5_skl))),
% 54.82/7.55 inference(resolution,[status(thm)],[f108,f89])).
% 54.82/7.55 fof(f303,plain,(
% 54.82/7.55 empty(relation_dom(sK5_skl))),
% 54.82/7.55 inference(resolution,[status(thm)],[f108,f86])).
% 54.82/7.55 fof(f315,definition,(
% 54.82/7.55 sQ18_spl <=> (relation(relation_composition(sK12_skl,function_inverse(sK12_skl))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f317,plain,(
% 54.82/7.55 ~relation(relation_composition(sK12_skl,function_inverse(sK12_skl)))|sQ18_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f315])).
% 54.82/7.55 fof(f335,definition,(
% 54.82/7.55 sQ22_spl <=> (relation(relation_composition(function_inverse(sK12_skl),sK12_skl)))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f337,plain,(
% 54.82/7.55 ~relation(relation_composition(function_inverse(sK12_skl),sK12_skl))|sQ22_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f335])).
% 54.82/7.55 fof(f338,definition,(
% 54.82/7.55 sQ23_spl <=> (empty(relation_rng(sK12_skl)))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f342,plain,(
% 54.82/7.55 empty(sK4_skl)|~relation(sK4_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f297,f84])).
% 54.82/7.55 fof(f348,definition,(
% 54.82/7.55 sQ24_spl <=> (empty(sK4_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f351,definition,(
% 54.82/7.55 sQ25_spl <=> (relation(sK4_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f353,plain,(
% 54.82/7.55 ~relation(sK4_skl)|sQ25_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f351])).
% 54.82/7.55 fof(f354,plain,(
% 54.82/7.55 sQ24_spl|~sQ25_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f342,f348,f351])).
% 54.82/7.55 fof(f355,plain,(
% 54.82/7.55 $false|sQ25_spl),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f353,f300])).
% 54.82/7.55 fof(f356,plain,(
% 54.82/7.55 sQ25_spl),
% 54.82/7.55 inference(contradiction_clause,[status(thm)],[f355])).
% 54.82/7.55 fof(f362,plain,(
% 54.82/7.55 empty(empty_set)|~relation(empty_set)),
% 54.82/7.55 inference(resolution,[status(thm)],[f192,f84])).
% 54.82/7.55 fof(f368,definition,(
% 54.82/7.55 sQ26_spl <=> (empty(empty_set))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f371,definition,(
% 54.82/7.55 sQ27_spl <=> (relation(empty_set))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f373,plain,(
% 54.82/7.55 ~relation(empty_set)|sQ27_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f371])).
% 54.82/7.55 fof(f374,plain,(
% 54.82/7.55 sQ26_spl|~sQ27_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f362,f368,f371])).
% 54.82/7.55 fof(f375,plain,(
% 54.82/7.55 $false|sQ27_spl),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f373,f69])).
% 54.82/7.55 fof(f376,plain,(
% 54.82/7.55 sQ27_spl),
% 54.82/7.55 inference(contradiction_clause,[status(thm)],[f375])).
% 54.82/7.55 fof(f396,plain,(
% 54.82/7.55 ![X0]: (empty(X0)|in(sK0_skl(X0),X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f130,f64])).
% 54.82/7.55 fof(f400,plain,(
% 54.82/7.55 ![X0]: (~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0))|~function(identity_relation(relation_dom(X0)))|apply(identity_relation(relation_dom(X0)),sK11_skl(relation_dom(X0),X0))=sK11_skl(relation_dom(X0),X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f189,f188])).
% 54.82/7.55 fof(f402,plain,(
% 54.82/7.55 ~relation(relation_composition(function_inverse(sK12_skl),sK12_skl))|~function(relation_composition(function_inverse(sK12_skl),sK12_skl))|relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)))|in(sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)))|~sQ8_spl),
% 54.82/7.55 inference(paramodulation,[status(thm)],[f253,f189])).
% 54.82/7.55 fof(f403,plain,(
% 54.82/7.55 ~relation(relation_composition(sK12_skl,function_inverse(sK12_skl)))|~function(relation_composition(sK12_skl,function_inverse(sK12_skl)))|relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))))|in(sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))))|~sQ6_spl),
% 54.82/7.55 inference(paramodulation,[status(thm)],[f233,f189])).
% 54.82/7.55 fof(f406,plain,(
% 54.82/7.55 ![X0]: (~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0))|apply(identity_relation(relation_dom(X0)),sK11_skl(relation_dom(X0),X0))=sK11_skl(relation_dom(X0),X0))),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f400,f78])).
% 54.82/7.55 fof(f407,definition,(
% 54.82/7.55 sQ28_spl <=> (function(relation_composition(function_inverse(sK12_skl),sK12_skl)))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f409,plain,(
% 54.82/7.55 ~function(relation_composition(function_inverse(sK12_skl),sK12_skl))|sQ28_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f407])).
% 54.82/7.55 fof(f410,definition,(
% 54.82/7.55 sQ29_spl <=> (relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f411,plain,(
% 54.82/7.55 relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)))|~sQ29_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f410])).
% 54.82/7.55 fof(f413,definition,(
% 54.82/7.55 sQ30_spl <=> (in(sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f414,plain,(
% 54.82/7.55 in(sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)))|~sQ30_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f413])).
% 54.82/7.55 fof(f416,plain,(
% 54.82/7.55 ~sQ22_spl|~sQ28_spl|sQ29_spl|sQ30_spl|~sQ8_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f402,f335,f407,f410,f413,f252])).
% 54.82/7.55 fof(f417,definition,(
% 54.82/7.55 sQ31_spl <=> (function(relation_composition(sK12_skl,function_inverse(sK12_skl))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f419,plain,(
% 54.82/7.55 ~function(relation_composition(sK12_skl,function_inverse(sK12_skl)))|sQ31_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f417])).
% 54.82/7.55 fof(f420,definition,(
% 54.82/7.55 sQ32_spl <=> (relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl)))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f421,plain,(
% 54.82/7.55 relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))))|~sQ32_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f420])).
% 54.82/7.55 fof(f423,definition,(
% 54.82/7.55 sQ33_spl <=> (in(sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl)))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f424,plain,(
% 54.82/7.55 in(sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))))|~sQ33_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f423])).
% 54.82/7.55 fof(f426,plain,(
% 54.82/7.55 ~sQ18_spl|~sQ31_spl|sQ32_spl|sQ33_spl|~sQ6_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f403,f315,f417,f420,f423,f232])).
% 54.82/7.55 fof(f441,plain,(
% 54.82/7.55 ~relation(sK12_skl)|~relation(function_inverse(sK12_skl))|sQ18_spl),
% 54.82/7.55 inference(resolution,[status(thm)],[f317,f61])).
% 54.82/7.55 fof(f445,definition,(
% 54.82/7.55 sQ37_spl <=> (relation(function_inverse(sK12_skl)))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f447,plain,(
% 54.82/7.55 ~relation(function_inverse(sK12_skl))|sQ37_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f445])).
% 54.82/7.55 fof(f453,plain,(
% 54.82/7.55 ~sQ4_spl|~sQ37_spl|sQ18_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f441,f226,f445,f315])).
% 54.82/7.55 fof(f454,plain,(
% 54.82/7.55 relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(sK12_skl))|~sQ6_spl|~sQ32_spl),
% 54.82/7.55 inference(forward_demodulation,[status(thm)],[f233,f421])).
% 54.82/7.55 fof(f455,plain,(
% 54.82/7.55 $false|sQ0_spl|~sQ6_spl|~sQ32_spl),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f454,f179])).
% 54.82/7.55 fof(f456,plain,(
% 54.82/7.55 sQ0_spl|~sQ6_spl|~sQ32_spl),
% 54.82/7.55 inference(contradiction_clause,[status(thm)],[f455])).
% 54.82/7.55 fof(f460,plain,(
% 54.82/7.55 relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_rng(sK12_skl))|~sQ8_spl|~sQ29_spl),
% 54.82/7.55 inference(forward_demodulation,[status(thm)],[f253,f411])).
% 54.82/7.55 fof(f473,plain,(
% 54.82/7.55 empty(sK5_skl)|~relation(sK5_skl)),
% 54.82/7.55 inference(resolution,[status(thm)],[f302,f84])).
% 54.82/7.55 fof(f479,definition,(
% 54.82/7.55 sQ39_spl <=> (empty(sK5_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f482,definition,(
% 54.82/7.55 sQ40_spl <=> (relation(sK5_skl))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f484,plain,(
% 54.82/7.55 ~relation(sK5_skl)|sQ40_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f482])).
% 54.82/7.55 fof(f485,plain,(
% 54.82/7.55 sQ39_spl|~sQ40_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f473,f479,f482])).
% 54.82/7.55 fof(f509,plain,(
% 54.82/7.55 ~relation(relation_composition(sK12_skl,function_inverse(sK12_skl)))|~function(relation_composition(sK12_skl,function_inverse(sK12_skl)))|relation_composition(sK12_skl,function_inverse(sK12_skl))=identity_relation(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))))|~apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))))=sK11_skl(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_composition(sK12_skl,function_inverse(sK12_skl)))|~sQ6_spl),
% 54.82/7.55 inference(paramodulation,[status(thm)],[f233,f190])).
% 54.82/7.55 fof(f510,definition,(
% 54.82/7.55 sQ41_spl <=> (apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))))=sK11_skl(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_composition(sK12_skl,function_inverse(sK12_skl))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f512,plain,(
% 54.82/7.55 ~apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))))=sK11_skl(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_composition(sK12_skl,function_inverse(sK12_skl)))|sQ41_spl),
% 54.82/7.55 inference(component_clause,[status(thm)],[f510])).
% 54.82/7.55 fof(f513,plain,(
% 54.82/7.55 ~sQ18_spl|~sQ31_spl|sQ32_spl|~sQ41_spl|~sQ6_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f509,f315,f417,f420,f510,f232])).
% 54.82/7.55 fof(f518,plain,(
% 54.82/7.55 ![X0]: (element(X0,powerset(X0)))),
% 54.82/7.55 inference(resolution,[status(thm)],[f142,f126])).
% 54.82/7.55 fof(f519,plain,(
% 54.82/7.55 ![X0,X1]: (~element(relation_dom(X0),powerset(X1))|element(sK11_skl(relation_dom(X0),X0),X1)|~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0)))),
% 54.82/7.55 inference(resolution,[status(thm)],[f145,f189])).
% 54.82/7.55 fof(f520,plain,(
% 54.82/7.55 ![X0]: (~relation(sK9_skl)|~function(sK9_skl)|~in(X0,relation_dom(sK9_skl))|X0=apply(function_inverse(sK9_skl),apply(sK9_skl,X0)))),
% 54.82/7.55 inference(resolution,[status(thm)],[f148,f121])).
% 54.82/7.55 fof(f521,plain,(
% 54.82/7.55 ![X0]: (~relation(sK12_skl)|~function(sK12_skl)|~in(X0,relation_dom(sK12_skl))|X0=apply(function_inverse(sK12_skl),apply(sK12_skl,X0)))),
% 54.82/7.55 inference(resolution,[status(thm)],[f148,f167])).
% 54.82/7.55 fof(f522,plain,(
% 54.82/7.55 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(X0))|X1=apply(function_inverse(X0),apply(X0,X1))|~empty(X0)|~function(X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f148,f184])).
% 54.82/7.55 fof(f523,definition,(
% 54.82/7.55 ![X0]: (sQ42_spl <=> (~in(X0,relation_dom(sK9_skl))|X0=apply(function_inverse(sK9_skl),apply(sK9_skl,X0))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f526,plain,(
% 54.82/7.55 ~sQ10_spl|~sQ11_spl|sQ42_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f520,f270,f273,f523])).
% 54.82/7.55 fof(f527,definition,(
% 54.82/7.55 ![X0]: (sQ43_spl <=> (~in(X0,relation_dom(sK12_skl))|X0=apply(function_inverse(sK12_skl),apply(sK12_skl,X0))))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 54.82/7.55 fof(f530,plain,(
% 54.82/7.55 ~sQ4_spl|~sQ5_spl|sQ43_spl),
% 54.82/7.55 inference(split_clause,[status(thm)],[f521,f226,f229,f527])).
% 54.82/7.55 fof(f531,plain,(
% 54.82/7.55 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(X0))|X1=apply(function_inverse(X0),apply(X0,X1))|~empty(X0))),
% 54.82/7.55 inference(duplicate_literals_removal,[status(thm)],[f522])).
% 54.82/7.55 fof(f532,plain,(
% 54.82/7.55 ![X0,X1]: (~function(X0)|~in(X1,relation_dom(X0))|X1=apply(function_inverse(X0),apply(X0,X1))|~empty(X0))),
% 54.82/7.55 inference(forward_subsumption_resolution,[status(thm)],[f531,f52])).
% 54.82/7.55 fof(f533,plain,(
% 54.82/7.55 ![X0]: (~relation(sK9_skl)|~function(sK9_skl)|~in(X0,relation_dom(sK9_skl))|X0=apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f149,f121])).
% 54.82/7.55 fof(f534,plain,(
% 54.82/7.55 ![X0]: (~relation(sK12_skl)|~function(sK12_skl)|~in(X0,relation_dom(sK12_skl))|X0=apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f149,f167])).
% 54.82/7.55 fof(f535,plain,(
% 54.82/7.55 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(X0))|X1=apply(relation_composition(X0,function_inverse(X0)),X1)|~empty(X0)|~function(X0))),
% 54.82/7.55 inference(resolution,[status(thm)],[f149,f184])).
% 54.82/7.55 fof(f536,definition,(
% 54.82/7.55 ![X0]: (sQ44_spl <=> (~in(X0,relation_dom(sK9_skl))|X0=apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),X0)))),
% 54.82/7.55 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 54.82/7.56 fof(f539,plain,(
% 54.82/7.56 ~sQ10_spl|~sQ11_spl|sQ44_spl),
% 54.82/7.56 inference(split_clause,[status(thm)],[f533,f270,f273,f536])).
% 54.82/7.56 fof(f540,definition,(
% 54.82/7.56 ![X0]: (sQ45_spl <=> (~in(X0,relation_dom(sK12_skl))|X0=apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),X0)))),
% 54.82/7.56 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 54.82/7.56 fof(f541,plain,(
% 54.82/7.56 ![X0]: (~in(X0,relation_dom(sK12_skl))|X0=apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),X0)|~sQ45_spl)),
% 54.82/7.56 inference(component_clause,[status(thm)],[f540])).
% 54.82/7.56 fof(f543,plain,(
% 54.82/7.56 ~sQ4_spl|~sQ5_spl|sQ45_spl),
% 54.82/7.56 inference(split_clause,[status(thm)],[f534,f226,f229,f540])).
% 54.82/7.56 fof(f544,plain,(
% 54.82/7.56 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(X0))|X1=apply(relation_composition(X0,function_inverse(X0)),X1)|~empty(X0))),
% 54.82/7.56 inference(duplicate_literals_removal,[status(thm)],[f535])).
% 54.82/7.56 fof(f545,plain,(
% 54.82/7.56 ![X0,X1]: (~function(X0)|~in(X1,relation_dom(X0))|X1=apply(relation_composition(X0,function_inverse(X0)),X1)|~empty(X0))),
% 54.82/7.56 inference(forward_subsumption_resolution,[status(thm)],[f544,f52])).
% 54.82/7.56 fof(f550,plain,(
% 54.82/7.56 ~relation(relation_composition(function_inverse(sK12_skl),sK12_skl))|~function(relation_composition(function_inverse(sK12_skl),sK12_skl))|relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)))|~apply(relation_composition(function_inverse(sK12_skl),sK12_skl),sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)))=sK11_skl(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_composition(function_inverse(sK12_skl),sK12_skl))|~sQ8_spl),
% 54.82/7.56 inference(paramodulation,[status(thm)],[f253,f190])).
% 54.82/7.56 fof(f555,definition,(
% 54.82/7.56 sQ46_spl <=> (apply(relation_composition(function_inverse(sK12_skl),sK12_skl),sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)))=sK11_skl(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_composition(function_inverse(sK12_skl),sK12_skl)))),
% 54.82/7.56 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 54.82/7.56 fof(f557,plain,(
% 54.82/7.56 ~apply(relation_composition(function_inverse(sK12_skl),sK12_skl),sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)))=sK11_skl(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_composition(function_inverse(sK12_skl),sK12_skl))|sQ46_spl),
% 54.82/7.56 inference(component_clause,[status(thm)],[f555])).
% 54.82/7.56 fof(f558,plain,(
% 54.82/7.56 ~sQ22_spl|~sQ28_spl|sQ29_spl|~sQ46_spl|~sQ8_spl),
% 54.82/7.56 inference(split_clause,[status(thm)],[f550,f335,f407,f410,f555,f252])).
% 54.82/7.56 fof(f564,plain,(
% 54.82/7.56 relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl)))=relation_dom(sK5_skl)|~empty(sK5_skl)),
% 54.82/7.56 inference(resolution,[status(thm)],[f237,f109])).
% 54.82/7.56 fof(f568,plain,(
% 54.82/7.56 ![X0]: (relation_dom(relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))))=relation_dom(identity_relation(X0))|~empty(identity_relation(X0)))),
% 54.82/7.56 inference(resolution,[status(thm)],[f237,f78])).
% 54.82/7.56 fof(f575,definition,(
% 54.82/7.56 sQ48_spl <=> (relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl)))=relation_dom(sK5_skl))),
% 54.82/7.56 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 54.82/7.56 fof(f576,plain,(
% 54.82/7.56 relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl)))=relation_dom(sK5_skl)|~sQ48_spl),
% 54.82/7.56 inference(component_clause,[status(thm)],[f575])).
% 54.82/7.56 fof(f578,plain,(
% 54.82/7.56 sQ48_spl|~sQ39_spl),
% 54.82/7.56 inference(split_clause,[status(thm)],[f564,f575,f479])).
% 54.82/7.56 fof(f586,plain,(
% 54.82/7.56 ![X0]: (relation_dom(relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))))=X0|~empty(identity_relation(X0)))),
% 54.82/7.56 inference(forward_demodulation,[status(thm)],[f214,f568])).
% 54.82/7.56 fof(f589,plain,(
% 54.82/7.56 $false|sQ40_spl),
% 54.82/7.56 inference(forward_subsumption_resolution,[status(thm)],[f484,f107])).
% 54.82/7.56 fof(f590,plain,(
% 54.82/7.56 sQ40_spl),
% 54.82/7.56 inference(contradiction_clause,[status(thm)],[f589])).
% 54.82/7.56 fof(f592,plain,(
% 54.82/7.56 relation_rng(relation_composition(sK5_skl,function_inverse(sK5_skl)))=relation_dom(sK5_skl)|~empty(sK5_skl)),
% 54.82/7.56 inference(resolution,[status(thm)],[f245,f109])).
% 54.82/7.56 fof(f596,plain,(
% 54.82/7.56 ![X0]: (relation_rng(relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))))=relation_dom(identity_relation(X0))|~empty(identity_relation(X0)))),
% 54.82/7.56 inference(resolution,[status(thm)],[f245,f78])).
% 54.82/7.56 fof(f600,definition,(
% 54.82/7.56 sQ51_spl <=> (relation_rng(relation_composition(sK5_skl,function_inverse(sK5_skl)))=relation_dom(sK5_skl))),
% 54.82/7.56 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 54.82/7.56 fof(f603,plain,(
% 54.82/7.56 sQ51_spl|~sQ39_spl),
% 54.82/7.56 inference(split_clause,[status(thm)],[f592,f600,f479])).
% 54.82/7.56 fof(f608,plain,(
% 54.82/7.56 ![X0]: (relation_rng(relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))))=X0|~empty(identity_relation(X0)))),
% 54.82/7.56 inference(forward_demodulation,[status(thm)],[f214,f596])).
% 54.82/7.56 fof(f612,plain,(
% 54.82/7.56 relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl))=relation_rng(sK5_skl)|~empty(sK5_skl)),
% 54.82/7.56 inference(resolution,[status(thm)],[f257,f109])).
% 54.82/7.56 fof(f620,definition,(
% 54.82/7.56 sQ53_spl <=> (relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl))=relation_rng(sK5_skl))),
% 54.82/7.56 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 54.82/7.56 fof(f621,plain,(
% 54.82/7.56 relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl))=relation_rng(sK5_skl)|~sQ53_spl),
% 54.82/7.56 inference(component_clause,[status(thm)],[f620])).
% 54.82/7.56 fof(f623,plain,(
% 54.82/7.56 sQ53_spl|~sQ39_spl),
% 54.82/7.56 inference(split_clause,[status(thm)],[f612,f620,f479])).
% 54.82/7.56 fof(f631,plain,(
% 54.82/7.56 relation_rng(relation_composition(function_inverse(sK5_skl),sK5_skl))=relation_rng(sK5_skl)|~empty(sK5_skl)),
% 54.82/7.56 inference(resolution,[status(thm)],[f265,f109])).
% 54.82/7.56 fof(f639,definition,(
% 54.82/7.56 sQ55_spl <=> (relation_rng(relation_composition(function_inverse(sK5_skl),sK5_skl))=relation_rng(sK5_skl))),
% 54.82/7.56 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 54.82/7.56 fof(f642,plain,(
% 54.82/7.56 sQ55_spl|~sQ39_spl),
% 54.82/7.56 inference(split_clause,[status(thm)],[f631,f639,f479])).
% 54.82/7.56 fof(f650,plain,(
% 54.82/7.56 ![X0]: (~empty(relation_dom(X0))|~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0)))),
% 54.82/7.56 inference(resolution,[status(thm)],[f173,f189])).
% 54.82/7.56 fof(f677,plain,(
% 54.82/7.56 ![X0,X1]: (~element(relation_dom(X0),powerset(X1))|~empty(X1)|~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0)))),
% 54.82/7.56 inference(resolution,[status(thm)],[f162,f189])).
% 54.82/7.56 fof(f678,plain,(
% 54.82/7.56 ![X0]: (sK7_skl(X0)=empty_set)),
% 54.82/7.56 inference(resolution,[status(thm)],[f170,f115])).
% 54.82/7.56 fof(f680,plain,(
% 54.82/7.56 ![X0]: (relation_composition(empty_set,X0)=empty_set|~relation(X0))),
% 54.82/7.56 inference(resolution,[status(thm)],[f170,f191])).
% 54.82/7.56 fof(f682,plain,(
% 54.82/7.56 ![X0]: (relation_composition(X0,empty_set)=empty_set|~relation(X0))),
% 54.82/7.56 inference(resolution,[status(thm)],[f170,f194])).
% 54.82/7.56 fof(f683,plain,(
% 54.82/7.56 sK5_skl=empty_set),
% 54.82/7.56 inference(resolution,[status(thm)],[f170,f108])).
% 54.82/7.56 fof(f685,plain,(
% 54.82/7.56 relation_dom(sK5_skl)=empty_set),
% 54.82/7.56 inference(resolution,[status(thm)],[f170,f303])).
% 54.82/7.56 fof(f689,plain,(
% 54.82/7.56 relation_rng(sK5_skl)=empty_set),
% 54.82/7.56 inference(resolution,[status(thm)],[f170,f302])).
% 54.82/7.56 fof(f693,plain,(
% 54.82/7.56 sK2_skl=empty_set),
% 54.82/7.56 inference(resolution,[status(thm)],[f170,f98])).
% 54.82/7.56 fof(f697,plain,(
% 54.82/7.56 ![X0]: (element(empty_set,powerset(X0)))),
% 54.82/7.56 inference(backward_demodulation,[status(thm)],[f678,f114])).
% 54.82/7.56 fof(f709,plain,(
% 54.82/7.56 function(empty_set)),
% 54.82/7.56 inference(backward_demodulation,[status(thm)],[f683,f109])).
% 54.82/7.56 fof(f712,plain,(
% 54.82/7.56 relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl))=relation_rng(empty_set)|~sQ53_spl),
% 54.82/7.56 inference(backward_demodulation,[status(thm)],[f683,f621])).
% 54.82/7.56 fof(f714,plain,(
% 54.82/7.56 relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl)))=relation_dom(empty_set)|~sQ48_spl),
% 54.82/7.56 inference(backward_demodulation,[status(thm)],[f683,f576])).
% 54.82/7.56 fof(f747,plain,(
% 54.82/7.56 relation_dom(empty_set)=empty_set),
% 54.82/7.56 inference(forward_demodulation,[status(thm)],[f683,f685])).
% 54.82/7.56 fof(f761,plain,(
% 54.82/7.56 relation_rng(empty_set)=empty_set),
% 54.82/7.56 inference(forward_demodulation,[status(thm)],[f683,f689])).
% 55.79/7.57 fof(f796,plain,(
% 55.79/7.57 relation_dom(relation_composition(function_inverse(empty_set),sK5_skl))=relation_rng(empty_set)|~sQ53_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f683,f712])).
% 55.79/7.57 fof(f797,plain,(
% 55.79/7.57 relation_dom(relation_composition(function_inverse(empty_set),empty_set))=relation_rng(empty_set)|~sQ53_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f683,f796])).
% 55.79/7.57 fof(f798,plain,(
% 55.79/7.57 relation_dom(relation_composition(function_inverse(empty_set),empty_set))=empty_set|~sQ53_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f761,f797])).
% 55.79/7.57 fof(f802,plain,(
% 55.79/7.57 relation_dom(relation_composition(empty_set,function_inverse(sK5_skl)))=relation_dom(empty_set)|~sQ48_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f683,f714])).
% 55.79/7.57 fof(f803,plain,(
% 55.79/7.57 relation_dom(relation_composition(empty_set,function_inverse(empty_set)))=relation_dom(empty_set)|~sQ48_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f683,f802])).
% 55.79/7.57 fof(f804,plain,(
% 55.79/7.57 relation_dom(relation_composition(empty_set,function_inverse(empty_set)))=empty_set|~sQ48_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f747,f803])).
% 55.79/7.57 fof(f841,plain,(
% 55.79/7.57 ![X0,X1]: (~empty(X0)|X0=relation_composition(empty_set,X1)|~relation(X1))),
% 55.79/7.57 inference(resolution,[status(thm)],[f176,f191])).
% 55.79/7.57 fof(f846,plain,(
% 55.79/7.57 ~relation(sK12_skl)|~function(sK12_skl)|~relation(function_inverse(sK12_skl))|~function(function_inverse(sK12_skl))|sQ31_spl),
% 55.79/7.57 inference(resolution,[status(thm)],[f419,f73])).
% 55.79/7.57 fof(f848,definition,(
% 55.79/7.57 sQ63_spl <=> (function(function_inverse(sK12_skl)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f850,plain,(
% 55.79/7.57 ~function(function_inverse(sK12_skl))|sQ63_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f848])).
% 55.79/7.57 fof(f851,plain,(
% 55.79/7.57 ~sQ4_spl|~sQ5_spl|~sQ37_spl|~sQ63_spl|sQ31_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f846,f226,f229,f445,f848,f417])).
% 55.79/7.57 fof(f979,plain,(
% 55.79/7.57 ![X0]: (empty(relation_rng(X0))|~relation(X0)|~function(X0)|~one_to_one(X0)|sK0_skl(relation_rng(X0))=apply(relation_composition(function_inverse(X0),X0),sK0_skl(relation_rng(X0))))),
% 55.79/7.57 inference(resolution,[status(thm)],[f396,f153])).
% 55.79/7.57 fof(f980,plain,(
% 55.79/7.57 ![X0]: (empty(relation_rng(X0))|~relation(X0)|~function(X0)|~one_to_one(X0)|sK0_skl(relation_rng(X0))=apply(X0,apply(function_inverse(X0),sK0_skl(relation_rng(X0)))))),
% 55.79/7.57 inference(resolution,[status(thm)],[f396,f152])).
% 55.79/7.57 fof(f997,plain,(
% 55.79/7.57 in(sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_dom(sK12_skl))|~sQ6_spl|~sQ33_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f233,f424])).
% 55.79/7.57 fof(f999,plain,(
% 55.79/7.57 ~apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))))=sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl)))|~sQ6_spl|sQ41_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f233,f512])).
% 55.79/7.57 fof(f1008,plain,(
% 55.79/7.57 ![X0,X1]: (~relation(relation_composition(X0,X1))|relation_composition(X0,X1)=identity_relation(relation_dom(relation_composition(X0,X1)))|apply(identity_relation(relation_dom(relation_composition(X0,X1))),sK11_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)))=sK11_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1))|~relation(X0)|~function(X0)|~relation(X1)|~function(X1))),
% 55.79/7.57 inference(resolution,[status(thm)],[f406,f73])).
% 55.79/7.57 fof(f1010,plain,(
% 55.79/7.57 ![X0]: (~relation(function_inverse(X0))|function_inverse(X0)=identity_relation(relation_dom(function_inverse(X0)))|apply(identity_relation(relation_dom(function_inverse(X0))),sK11_skl(relation_dom(function_inverse(X0)),function_inverse(X0)))=sK11_skl(relation_dom(function_inverse(X0)),function_inverse(X0))|~relation(X0)|~function(X0))),
% 55.79/7.57 inference(resolution,[status(thm)],[f406,f59])).
% 55.79/7.57 fof(f1014,definition,(
% 55.79/7.57 sQ93_spl <=> (empty_set=identity_relation(relation_dom(empty_set)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f1015,plain,(
% 55.79/7.57 empty_set=identity_relation(relation_dom(empty_set))|~sQ93_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f1014])).
% 55.79/7.57 fof(f1028,plain,(
% 55.79/7.57 ![X0,X1]: (relation_composition(X0,X1)=identity_relation(relation_dom(relation_composition(X0,X1)))|apply(identity_relation(relation_dom(relation_composition(X0,X1))),sK11_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)))=sK11_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1))|~relation(X0)|~function(X0)|~relation(X1)|~function(X1))),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f1008,f61])).
% 55.79/7.57 fof(f1029,definition,(
% 55.79/7.57 sQ97_spl <=> (relation(sK1_skl))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f1031,plain,(
% 55.79/7.57 ~relation(sK1_skl)|sQ97_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f1029])).
% 55.79/7.57 fof(f1039,plain,(
% 55.79/7.57 ![X0]: (function_inverse(X0)=identity_relation(relation_dom(function_inverse(X0)))|apply(identity_relation(relation_dom(function_inverse(X0))),sK11_skl(relation_dom(function_inverse(X0)),function_inverse(X0)))=sK11_skl(relation_dom(function_inverse(X0)),function_inverse(X0))|~relation(X0)|~function(X0))),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f1010,f58])).
% 55.79/7.57 fof(f1061,plain,(
% 55.79/7.57 empty_set=identity_relation(empty_set)|~sQ93_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f747,f1015])).
% 55.79/7.57 fof(f1074,plain,(
% 55.79/7.57 $false|sQ97_spl),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f1031,f95])).
% 55.79/7.57 fof(f1075,plain,(
% 55.79/7.57 sQ97_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f1074])).
% 55.79/7.57 fof(f1081,plain,(
% 55.79/7.57 ~apply(relation_composition(function_inverse(sK12_skl),sK12_skl),sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)))=sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl))|~sQ8_spl|sQ46_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f253,f557])).
% 55.79/7.57 fof(f1083,plain,(
% 55.79/7.57 in(sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_rng(sK12_skl))|~sQ8_spl|~sQ30_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f253,f414])).
% 55.79/7.57 fof(f1084,plain,(
% 55.79/7.57 ~relation(empty_set)|sQ3_spl),
% 55.79/7.57 inference(forward_demodulation,[status(thm)],[f693,f212])).
% 55.79/7.57 fof(f1085,plain,(
% 55.79/7.57 $false|sQ3_spl),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f1084,f69])).
% 55.79/7.57 fof(f1086,plain,(
% 55.79/7.57 sQ3_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f1085])).
% 55.79/7.57 fof(f1123,plain,(
% 55.79/7.57 $false|sQ1_spl|~sQ8_spl|~sQ29_spl),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f460,f182])).
% 55.79/7.57 fof(f1124,plain,(
% 55.79/7.57 sQ1_spl|~sQ8_spl|~sQ29_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f1123])).
% 55.79/7.57 fof(f1146,definition,(
% 55.79/7.57 sQ105_spl <=> (relation(identity_relation(relation_rng(sK12_skl))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f1148,plain,(
% 55.79/7.57 ~relation(identity_relation(relation_rng(sK12_skl)))|sQ105_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f1146])).
% 55.79/7.57 fof(f1149,definition,(
% 55.79/7.57 sQ106_spl <=> (function(identity_relation(relation_rng(sK12_skl))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f1151,plain,(
% 55.79/7.57 ~function(identity_relation(relation_rng(sK12_skl)))|sQ106_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f1149])).
% 55.79/7.57 fof(f1168,plain,(
% 55.79/7.57 $false|sQ105_spl),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f1148,f62])).
% 55.79/7.57 fof(f1169,plain,(
% 55.79/7.57 sQ105_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f1168])).
% 55.79/7.57 fof(f1170,plain,(
% 55.79/7.57 $false|sQ106_spl),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f1151,f78])).
% 55.79/7.57 fof(f1171,plain,(
% 55.79/7.57 sQ106_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f1170])).
% 55.79/7.57 fof(f1172,plain,(
% 55.79/7.57 ![X0,X1]: (~function(relation_composition(empty_set,X0))|~in(X1,relation_dom(relation_composition(empty_set,X0)))|X1=apply(function_inverse(relation_composition(empty_set,X0)),apply(relation_composition(empty_set,X0),X1))|~relation(X0))),
% 55.79/7.57 inference(resolution,[status(thm)],[f532,f191])).
% 55.79/7.57 fof(f1173,plain,(
% 55.79/7.57 ![X0,X1]: (~function(relation_composition(X0,empty_set))|~in(X1,relation_dom(relation_composition(X0,empty_set)))|X1=apply(function_inverse(relation_composition(X0,empty_set)),apply(relation_composition(X0,empty_set),X1))|~relation(X0))),
% 55.79/7.57 inference(resolution,[status(thm)],[f532,f194])).
% 55.79/7.57 fof(f1174,plain,(
% 55.79/7.57 ![X0]: (~function(empty_set)|~in(X0,relation_dom(empty_set))|X0=apply(function_inverse(empty_set),apply(empty_set,X0)))),
% 55.79/7.57 inference(resolution,[status(thm)],[f532,f68])).
% 55.79/7.57 fof(f1175,definition,(
% 55.79/7.57 sQ111_spl <=> (function(empty_set))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f1177,plain,(
% 55.79/7.57 ~function(empty_set)|sQ111_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f1175])).
% 55.79/7.57 fof(f1178,definition,(
% 55.79/7.57 ![X0]: (sQ112_spl <=> (~in(X0,relation_dom(empty_set))|X0=apply(function_inverse(empty_set),apply(empty_set,X0))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f1181,plain,(
% 55.79/7.57 ~sQ111_spl|sQ112_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f1174,f1175,f1178])).
% 55.79/7.57 fof(f1182,plain,(
% 55.79/7.57 $false|sQ111_spl),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f1177,f709])).
% 55.79/7.57 fof(f1183,plain,(
% 55.79/7.57 sQ111_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f1182])).
% 55.79/7.57 fof(f1185,plain,(
% 55.79/7.57 ![X0,X1]: (~function(relation_composition(empty_set,X0))|~in(X1,relation_dom(relation_composition(empty_set,X0)))|X1=apply(relation_composition(relation_composition(empty_set,X0),function_inverse(relation_composition(empty_set,X0))),X1)|~relation(X0))),
% 55.79/7.57 inference(resolution,[status(thm)],[f545,f191])).
% 55.79/7.57 fof(f1186,plain,(
% 55.79/7.57 ![X0,X1]: (~function(relation_composition(X0,empty_set))|~in(X1,relation_dom(relation_composition(X0,empty_set)))|X1=apply(relation_composition(relation_composition(X0,empty_set),function_inverse(relation_composition(X0,empty_set))),X1)|~relation(X0))),
% 55.79/7.57 inference(resolution,[status(thm)],[f545,f194])).
% 55.79/7.57 fof(f1187,plain,(
% 55.79/7.57 ![X0]: (~function(empty_set)|~in(X0,relation_dom(empty_set))|X0=apply(relation_composition(empty_set,function_inverse(empty_set)),X0))),
% 55.79/7.57 inference(resolution,[status(thm)],[f545,f68])).
% 55.79/7.57 fof(f1188,definition,(
% 55.79/7.57 ![X0]: (sQ113_spl <=> (~in(X0,relation_dom(empty_set))|X0=apply(relation_composition(empty_set,function_inverse(empty_set)),X0)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f1191,plain,(
% 55.79/7.57 ~sQ111_spl|sQ113_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f1187,f1175,f1188])).
% 55.79/7.57 fof(f1223,plain,(
% 55.79/7.57 ![X0,X1]: (relation_composition(empty_set,X0)=relation_composition(empty_set,X1)|~relation(X1)|~relation(X0))),
% 55.79/7.57 inference(resolution,[status(thm)],[f841,f191])).
% 55.79/7.57 fof(f1231,plain,(
% 55.79/7.57 ![X0]: (element(sK11_skl(relation_dom(X0),X0),relation_dom(X0))|~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0)))),
% 55.79/7.57 inference(resolution,[status(thm)],[f519,f518])).
% 55.79/7.57 fof(f1262,plain,(
% 55.79/7.57 ![X0,X1]: (~element(relation_dom(X0),powerset(relation_composition(empty_set,X1)))|~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0))|~relation(X1))),
% 55.79/7.57 inference(resolution,[status(thm)],[f677,f191])).
% 55.79/7.57 fof(f1517,plain,(
% 55.79/7.57 ~empty(relation_rng(sK12_skl))|~relation(relation_composition(function_inverse(sK12_skl),sK12_skl))|~function(relation_composition(function_inverse(sK12_skl),sK12_skl))|relation_composition(function_inverse(sK12_skl),sK12_skl)=identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)))|~sQ8_spl),
% 55.79/7.57 inference(paramodulation,[status(thm)],[f253,f650])).
% 55.79/7.57 fof(f1526,plain,(
% 55.79/7.57 ~sQ23_spl|~sQ22_spl|~sQ28_spl|sQ29_spl|~sQ8_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f1517,f338,f335,f407,f410,f252])).
% 55.79/7.57 fof(f1610,plain,(
% 55.79/7.57 ![X0,X1,X2]: (relation_composition(empty_set,X0)=relation_composition(empty_set,relation_composition(X1,X2))|~relation(X0)|~relation(X1)|~relation(X2))),
% 55.79/7.57 inference(resolution,[status(thm)],[f1223,f61])).
% 55.79/7.57 fof(f2274,plain,(
% 55.79/7.57 ![X0]: (relation_composition(empty_set,identity_relation(X0))=empty_set)),
% 55.79/7.57 inference(resolution,[status(thm)],[f680,f62])).
% 55.79/7.57 fof(f2275,plain,(
% 55.79/7.57 relation_composition(empty_set,sK12_skl)=empty_set),
% 55.79/7.57 inference(resolution,[status(thm)],[f680,f165])).
% 55.79/7.57 fof(f2421,plain,(
% 55.79/7.57 ~empty(empty_set)|~relation(empty_set)|~function(empty_set)|empty_set=identity_relation(relation_dom(empty_set))),
% 55.79/7.57 inference(paramodulation,[status(thm)],[f747,f650])).
% 55.79/7.57 fof(f2430,plain,(
% 55.79/7.57 ~sQ26_spl|~sQ27_spl|~sQ111_spl|sQ93_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f2421,f368,f371,f1175,f1014])).
% 55.79/7.57 fof(f2656,definition,(
% 55.79/7.57 sQ160_spl <=> (empty(relation_composition(function_inverse(empty_set),empty_set)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2692,definition,(
% 55.79/7.57 sQ166_spl <=> (in(sK11_skl(relation_dom(relation_composition(function_inverse(empty_set),empty_set)),relation_composition(function_inverse(empty_set),empty_set)),empty_set))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2693,plain,(
% 55.79/7.57 in(sK11_skl(relation_dom(relation_composition(function_inverse(empty_set),empty_set)),relation_composition(function_inverse(empty_set),empty_set)),empty_set)|~sQ166_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f2692])).
% 55.79/7.57 fof(f2696,definition,(
% 55.79/7.57 sQ167_spl <=> (in(sK11_skl(empty_set,relation_composition(function_inverse(empty_set),empty_set)),relation_dom(relation_composition(function_inverse(empty_set),empty_set))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2697,plain,(
% 55.79/7.57 in(sK11_skl(empty_set,relation_composition(function_inverse(empty_set),empty_set)),relation_dom(relation_composition(function_inverse(empty_set),empty_set)))|~sQ167_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f2696])).
% 55.79/7.57 fof(f2725,definition,(
% 55.79/7.57 sQ173_spl <=> (empty(relation_composition(empty_set,function_inverse(empty_set))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2761,definition,(
% 55.79/7.57 sQ179_spl <=> (in(sK11_skl(relation_dom(relation_composition(empty_set,function_inverse(empty_set))),relation_composition(empty_set,function_inverse(empty_set))),empty_set))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2762,plain,(
% 55.79/7.57 in(sK11_skl(relation_dom(relation_composition(empty_set,function_inverse(empty_set))),relation_composition(empty_set,function_inverse(empty_set))),empty_set)|~sQ179_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f2761])).
% 55.79/7.57 fof(f2765,definition,(
% 55.79/7.57 sQ180_spl <=> (in(sK11_skl(empty_set,relation_composition(empty_set,function_inverse(empty_set))),relation_dom(relation_composition(empty_set,function_inverse(empty_set)))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2766,plain,(
% 55.79/7.57 in(sK11_skl(empty_set,relation_composition(empty_set,function_inverse(empty_set))),relation_dom(relation_composition(empty_set,function_inverse(empty_set))))|~sQ180_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f2765])).
% 55.79/7.57 fof(f2772,plain,(
% 55.79/7.57 empty(relation_rng(sK12_skl))|~relation(sK12_skl)|~function(sK12_skl)|sK0_skl(relation_rng(sK12_skl))=apply(relation_composition(function_inverse(sK12_skl),sK12_skl),sK0_skl(relation_rng(sK12_skl)))),
% 55.79/7.57 inference(resolution,[status(thm)],[f979,f167])).
% 55.79/7.57 fof(f2781,definition,(
% 55.79/7.57 sQ183_spl <=> (sK0_skl(relation_rng(sK12_skl))=apply(relation_composition(function_inverse(sK12_skl),sK12_skl),sK0_skl(relation_rng(sK12_skl))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2784,plain,(
% 55.79/7.57 sQ23_spl|~sQ4_spl|~sQ5_spl|sQ183_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f2772,f338,f226,f229,f2781])).
% 55.79/7.57 fof(f2789,plain,(
% 55.79/7.57 empty(relation_rng(sK12_skl))|~relation(sK12_skl)|~function(sK12_skl)|sK0_skl(relation_rng(sK12_skl))=apply(sK12_skl,apply(function_inverse(sK12_skl),sK0_skl(relation_rng(sK12_skl))))),
% 55.79/7.57 inference(resolution,[status(thm)],[f980,f167])).
% 55.79/7.57 fof(f2795,definition,(
% 55.79/7.57 sQ185_spl <=> (sK0_skl(relation_rng(sK12_skl))=apply(sK12_skl,apply(function_inverse(sK12_skl),sK0_skl(relation_rng(sK12_skl)))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2798,plain,(
% 55.79/7.57 sQ23_spl|~sQ4_spl|~sQ5_spl|sQ185_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f2789,f338,f226,f229,f2795])).
% 55.79/7.57 fof(f2967,plain,(
% 55.79/7.57 ![X0]: (relation_composition(X0,empty_set)=identity_relation(relation_dom(relation_composition(X0,empty_set)))|apply(identity_relation(relation_dom(relation_composition(X0,empty_set))),sK11_skl(relation_dom(relation_composition(X0,empty_set)),relation_composition(X0,empty_set)))=sK11_skl(relation_dom(relation_composition(X0,empty_set)),relation_composition(X0,empty_set))|~relation(X0)|~function(X0)|~relation(empty_set))),
% 55.79/7.57 inference(resolution,[status(thm)],[f1028,f709])).
% 55.79/7.57 fof(f2969,plain,(
% 55.79/7.57 ![X0]: (relation_composition(X0,sK1_skl)=identity_relation(relation_dom(relation_composition(X0,sK1_skl)))|apply(identity_relation(relation_dom(relation_composition(X0,sK1_skl))),sK11_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl)))=sK11_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl))|~relation(X0)|~function(X0)|~relation(sK1_skl))),
% 55.79/7.57 inference(resolution,[status(thm)],[f1028,f96])).
% 55.79/7.57 fof(f2972,plain,(
% 55.79/7.57 ![X0]: (relation_composition(X0,sK12_skl)=identity_relation(relation_dom(relation_composition(X0,sK12_skl)))|apply(identity_relation(relation_dom(relation_composition(X0,sK12_skl))),sK11_skl(relation_dom(relation_composition(X0,sK12_skl)),relation_composition(X0,sK12_skl)))=sK11_skl(relation_dom(relation_composition(X0,sK12_skl)),relation_composition(X0,sK12_skl))|~relation(X0)|~function(X0)|~relation(sK12_skl))),
% 55.79/7.57 inference(resolution,[status(thm)],[f1028,f166])).
% 55.79/7.57 fof(f2974,definition,(
% 55.79/7.57 ![X0]: (sQ187_spl <=> (relation_composition(X0,empty_set)=identity_relation(relation_dom(relation_composition(X0,empty_set)))|apply(identity_relation(relation_dom(relation_composition(X0,empty_set))),sK11_skl(relation_dom(relation_composition(X0,empty_set)),relation_composition(X0,empty_set)))=sK11_skl(relation_dom(relation_composition(X0,empty_set)),relation_composition(X0,empty_set))|~relation(X0)|~function(X0)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2977,plain,(
% 55.79/7.57 sQ187_spl|~sQ27_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f2967,f2974,f371])).
% 55.79/7.57 fof(f2979,definition,(
% 55.79/7.57 ![X0]: (sQ188_spl <=> (relation_composition(X0,sK1_skl)=identity_relation(relation_dom(relation_composition(X0,sK1_skl)))|apply(identity_relation(relation_dom(relation_composition(X0,sK1_skl))),sK11_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl)))=sK11_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl))|~relation(X0)|~function(X0)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2982,plain,(
% 55.79/7.57 sQ188_spl|~sQ97_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f2969,f2979,f1029])).
% 55.79/7.57 fof(f2985,definition,(
% 55.79/7.57 ![X0]: (sQ189_spl <=> (relation_composition(X0,sK12_skl)=identity_relation(relation_dom(relation_composition(X0,sK12_skl)))|apply(identity_relation(relation_dom(relation_composition(X0,sK12_skl))),sK11_skl(relation_dom(relation_composition(X0,sK12_skl)),relation_composition(X0,sK12_skl)))=sK11_skl(relation_dom(relation_composition(X0,sK12_skl)),relation_composition(X0,sK12_skl))|~relation(X0)|~function(X0)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f2988,plain,(
% 55.79/7.57 sQ189_spl|~sQ4_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f2972,f2985,f226])).
% 55.79/7.57 fof(f3201,plain,(
% 55.79/7.57 ![X0,X1]: (~in(X0,relation_dom(relation_composition(empty_set,X1)))|X0=apply(function_inverse(relation_composition(empty_set,X1)),apply(relation_composition(empty_set,X1),X0))|~relation(X1)|~relation(empty_set)|~function(empty_set)|~relation(X1)|~function(X1))),
% 55.79/7.57 inference(resolution,[status(thm)],[f1172,f73])).
% 55.79/7.57 fof(f3203,definition,(
% 55.79/7.57 ![X0,X1]: (sQ211_spl <=> (~in(X0,relation_dom(relation_composition(empty_set,X1)))|X0=apply(function_inverse(relation_composition(empty_set,X1)),apply(relation_composition(empty_set,X1),X0))|~relation(X1)|~relation(X1)|~function(X1)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f3206,plain,(
% 55.79/7.57 sQ211_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f3201,f3203,f371,f1175])).
% 55.79/7.57 fof(f3209,plain,(
% 55.79/7.57 ![X0,X1]: (~in(X0,relation_dom(relation_composition(X1,empty_set)))|X0=apply(function_inverse(relation_composition(X1,empty_set)),apply(relation_composition(X1,empty_set),X0))|~relation(X1)|~relation(X1)|~function(X1)|~relation(empty_set)|~function(empty_set))),
% 55.79/7.57 inference(resolution,[status(thm)],[f1173,f73])).
% 55.79/7.57 fof(f3211,definition,(
% 55.79/7.57 ![X0,X1]: (sQ212_spl <=> (~in(X0,relation_dom(relation_composition(X1,empty_set)))|X0=apply(function_inverse(relation_composition(X1,empty_set)),apply(relation_composition(X1,empty_set),X0))|~relation(X1)|~relation(X1)|~function(X1)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f3214,plain,(
% 55.79/7.57 sQ212_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f3209,f3211,f371,f1175])).
% 55.79/7.57 fof(f3300,plain,(
% 55.79/7.57 ![X0,X1]: (~in(X0,relation_dom(relation_composition(empty_set,X1)))|X0=apply(relation_composition(relation_composition(empty_set,X1),function_inverse(relation_composition(empty_set,X1))),X0)|~relation(X1)|~relation(empty_set)|~function(empty_set)|~relation(X1)|~function(X1))),
% 55.79/7.57 inference(resolution,[status(thm)],[f1185,f73])).
% 55.79/7.57 fof(f3302,definition,(
% 55.79/7.57 ![X0,X1]: (sQ214_spl <=> (~in(X0,relation_dom(relation_composition(empty_set,X1)))|X0=apply(relation_composition(relation_composition(empty_set,X1),function_inverse(relation_composition(empty_set,X1))),X0)|~relation(X1)|~relation(X1)|~function(X1)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f3305,plain,(
% 55.79/7.57 sQ214_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f3300,f3302,f371,f1175])).
% 55.79/7.57 fof(f3308,plain,(
% 55.79/7.57 ![X0,X1]: (~in(X0,relation_dom(relation_composition(X1,empty_set)))|X0=apply(relation_composition(relation_composition(X1,empty_set),function_inverse(relation_composition(X1,empty_set))),X0)|~relation(X1)|~relation(X1)|~function(X1)|~relation(empty_set)|~function(empty_set))),
% 55.79/7.57 inference(resolution,[status(thm)],[f1186,f73])).
% 55.79/7.57 fof(f3310,definition,(
% 55.79/7.57 ![X0,X1]: (sQ215_spl <=> (~in(X0,relation_dom(relation_composition(X1,empty_set)))|X0=apply(relation_composition(relation_composition(X1,empty_set),function_inverse(relation_composition(X1,empty_set))),X0)|~relation(X1)|~relation(X1)|~function(X1)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f3313,plain,(
% 55.79/7.57 sQ215_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f3308,f3310,f371,f1175])).
% 55.79/7.57 fof(f3380,plain,(
% 55.79/7.57 ~relation(sK12_skl)|~function(sK12_skl)|sQ37_spl),
% 55.79/7.57 inference(resolution,[status(thm)],[f447,f58])).
% 55.79/7.57 fof(f3381,plain,(
% 55.79/7.57 ~sQ4_spl|~sQ5_spl|sQ37_spl),
% 55.79/7.57 inference(split_clause,[status(thm)],[f3380,f226,f229,f445])).
% 55.79/7.57 fof(f3467,definition,(
% 55.79/7.57 sQ226_spl <=> (relation(identity_relation(relation_dom(sK12_skl))))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f3469,plain,(
% 55.79/7.57 ~relation(identity_relation(relation_dom(sK12_skl)))|sQ226_spl),
% 55.79/7.57 inference(component_clause,[status(thm)],[f3467])).
% 55.79/7.57 fof(f3512,plain,(
% 55.79/7.57 $false|sQ226_spl),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f3469,f62])).
% 55.79/7.57 fof(f3513,plain,(
% 55.79/7.57 sQ226_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f3512])).
% 55.79/7.57 fof(f3540,definition,(
% 55.79/7.57 ![X0]: (sQ233_spl <=> (~element(empty_set,powerset(relation_composition(empty_set,X0)))|~relation(X0)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f3541,plain,(
% 55.79/7.57 ![X0]: (~element(empty_set,powerset(relation_composition(empty_set,X0)))|~relation(X0)|~sQ233_spl)),
% 55.79/7.57 inference(component_clause,[status(thm)],[f3540])).
% 55.79/7.57 fof(f3552,definition,(
% 55.79/7.57 ![X0]: (sQ235_spl <=> (~element(empty_set,powerset(relation_composition(X0,empty_set)))|~relation(X0)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition])).
% 55.79/7.57 fof(f3553,plain,(
% 55.79/7.57 ![X0]: (~element(empty_set,powerset(relation_composition(X0,empty_set)))|~relation(X0)|~sQ235_spl)),
% 55.79/7.57 inference(component_clause,[status(thm)],[f3552])).
% 55.79/7.57 fof(f3780,plain,(
% 55.79/7.57 $false|~sQ233_spl),
% 55.79/7.57 inference(backward_subsumption_resolution,[status(thm)],[f123,f3795])).
% 55.79/7.57 fof(f3795,plain,(
% 55.79/7.57 ![X0]: (~relation(X0)|~sQ233_spl)),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f3541,f697])).
% 55.79/7.57 fof(f3821,plain,(
% 55.79/7.57 ~sQ233_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f3780])).
% 55.79/7.57 fof(f3822,plain,(
% 55.79/7.57 ![X0]: (~empty(X0)|one_to_one(X0))),
% 55.79/7.57 inference(backward_subsumption_resolution,[status(thm)],[f184,f50])).
% 55.79/7.57 fof(f3825,plain,(
% 55.79/7.57 $false|~sQ235_spl),
% 55.79/7.57 inference(backward_subsumption_resolution,[status(thm)],[f165,f3842])).
% 55.79/7.57 fof(f3842,plain,(
% 55.79/7.57 ![X0]: (~relation(X0)|~sQ235_spl)),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f3553,f697])).
% 55.79/7.57 fof(f3843,plain,(
% 55.79/7.57 ~sQ235_spl),
% 55.79/7.57 inference(contradiction_clause,[status(thm)],[f3825])).
% 55.79/7.57 fof(f3869,plain,(
% 55.79/7.57 ![X0]: (~in(X0,empty_set))),
% 55.79/7.57 inference(resolution,[status(thm)],[f68,f173])).
% 55.79/7.57 fof(f3914,plain,(
% 55.79/7.57 ![X0,X1]: (~relation(relation_composition(X0,X1))|relation_composition(X0,X1)=identity_relation(relation_dom(relation_composition(X0,X1)))|in(sK11_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)),relation_dom(relation_composition(X0,X1)))|~relation(X0)|~function(X0)|~relation(X1)|~function(X1))),
% 55.79/7.57 inference(resolution,[status(thm)],[f189,f73])).
% 55.79/7.57 fof(f3922,plain,(
% 55.79/7.57 ![X0,X1]: (relation_composition(X0,X1)=identity_relation(relation_dom(relation_composition(X0,X1)))|in(sK11_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)),relation_dom(relation_composition(X0,X1)))|~relation(X0)|~function(X0)|~relation(X1)|~function(X1))),
% 55.79/7.57 inference(forward_subsumption_resolution,[status(thm)],[f3914,f61])).
% 55.79/7.57 fof(f3923,definition,(
% 55.79/7.57 sQ255_spl <=> (in(sK11_skl(relation_dom(empty_set),empty_set),relation_dom(empty_set)))),
% 55.79/7.57 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f3924,plain,(
% 55.79/7.59 in(sK11_skl(relation_dom(empty_set),empty_set),relation_dom(empty_set))|~sQ255_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f3923])).
% 55.79/7.59 fof(f3993,plain,(
% 55.79/7.59 ![X0,X1]: (empty(relation_composition(empty_set,relation_composition(X0,X1)))|~relation(X0)|~relation(X1))),
% 55.79/7.59 inference(resolution,[status(thm)],[f191,f61])).
% 55.79/7.59 fof(f3999,plain,(
% 55.79/7.59 ![X0]: (empty(relation_composition(empty_set,function_inverse(X0)))|~relation(X0)|~function(X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f191,f58])).
% 55.79/7.59 fof(f4019,plain,(
% 55.79/7.59 ![X0]: (empty(relation_composition(function_inverse(X0),empty_set))|~relation(X0)|~function(X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f194,f58])).
% 55.79/7.59 fof(f4061,plain,(
% 55.79/7.59 ![X0]: (~relation(sK12_skl)|~function(sK12_skl)|~in(X0,relation_rng(sK12_skl))|X0=apply(relation_composition(function_inverse(sK12_skl),sK12_skl),X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f153,f167])).
% 55.79/7.59 fof(f4062,plain,(
% 55.79/7.59 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_rng(X0))|X1=apply(relation_composition(function_inverse(X0),X0),X1)|~empty(X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f153,f3822])).
% 55.79/7.59 fof(f4063,definition,(
% 55.79/7.59 ![X0]: (sQ259_spl <=> (~in(X0,relation_rng(empty_set))|X0=apply(relation_composition(function_inverse(empty_set),empty_set),X0)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f4067,definition,(
% 55.79/7.59 ![X0]: (sQ260_spl <=> (~in(X0,relation_rng(sK12_skl))|X0=apply(relation_composition(function_inverse(sK12_skl),sK12_skl),X0)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f4068,plain,(
% 55.79/7.59 ![X0]: (~in(X0,relation_rng(sK12_skl))|X0=apply(relation_composition(function_inverse(sK12_skl),sK12_skl),X0)|~sQ260_spl)),
% 55.79/7.59 inference(component_clause,[status(thm)],[f4067])).
% 55.79/7.59 fof(f4070,plain,(
% 55.79/7.59 ~sQ4_spl|~sQ5_spl|sQ260_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f4061,f226,f229,f4067])).
% 55.79/7.59 fof(f4071,plain,(
% 55.79/7.59 ![X0,X1]: (~function(X0)|~in(X1,relation_rng(X0))|X1=apply(relation_composition(function_inverse(X0),X0),X1)|~empty(X0))),
% 55.79/7.59 inference(forward_subsumption_resolution,[status(thm)],[f4062,f52])).
% 55.79/7.59 fof(f4209,plain,(
% 55.79/7.59 ![X0,X1,X2]: (relation_composition(X0,X1)=identity_relation(relation_dom(relation_composition(X0,X1)))|~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~element(relation_dom(relation_composition(X0,X1)),powerset(X2))|element(sK11_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)),X2))),
% 55.79/7.59 inference(resolution,[status(thm)],[f3922,f145])).
% 55.79/7.59 fof(f4211,plain,(
% 55.79/7.59 ![X0,X1]: (relation_composition(X0,X1)=identity_relation(relation_dom(relation_composition(X0,X1)))|~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~in(relation_dom(relation_composition(X0,X1)),sK11_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1))))),
% 55.79/7.59 inference(resolution,[status(thm)],[f3922,f48])).
% 55.79/7.59 fof(f4235,plain,(
% 55.79/7.59 in(sK11_skl(empty_set,empty_set),relation_dom(empty_set))|~sQ255_spl),
% 55.79/7.59 inference(forward_demodulation,[status(thm)],[f747,f3924])).
% 55.79/7.59 fof(f4236,plain,(
% 55.79/7.59 in(sK11_skl(empty_set,empty_set),empty_set)|~sQ255_spl),
% 55.79/7.59 inference(forward_demodulation,[status(thm)],[f747,f4235])).
% 55.79/7.59 fof(f4237,plain,(
% 55.79/7.59 $false|~sQ255_spl),
% 55.79/7.59 inference(forward_subsumption_resolution,[status(thm)],[f4236,f3869])).
% 55.79/7.59 fof(f4238,plain,(
% 55.79/7.59 ~sQ255_spl),
% 55.79/7.59 inference(contradiction_clause,[status(thm)],[f4237])).
% 55.79/7.59 fof(f4241,plain,(
% 55.79/7.59 ![X0]: (~function(empty_set)|~in(X0,relation_rng(empty_set))|X0=apply(relation_composition(function_inverse(empty_set),empty_set),X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f4071,f68])).
% 55.79/7.59 fof(f4242,plain,(
% 55.79/7.59 ~sQ111_spl|sQ259_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f4241,f1175,f4063])).
% 55.79/7.59 fof(f4663,plain,(
% 55.79/7.59 in(sK11_skl(empty_set,relation_composition(empty_set,function_inverse(empty_set))),empty_set)|~sQ48_spl|~sQ180_spl),
% 55.79/7.59 inference(forward_demodulation,[status(thm)],[f804,f2766])).
% 55.79/7.59 fof(f4664,plain,(
% 55.79/7.59 $false|~sQ48_spl|~sQ180_spl),
% 55.79/7.59 inference(forward_subsumption_resolution,[status(thm)],[f4663,f3869])).
% 55.79/7.59 fof(f4665,plain,(
% 55.79/7.59 ~sQ48_spl|~sQ180_spl),
% 55.79/7.59 inference(contradiction_clause,[status(thm)],[f4664])).
% 55.79/7.59 fof(f4666,plain,(
% 55.79/7.59 in(sK11_skl(empty_set,relation_composition(empty_set,function_inverse(empty_set))),empty_set)|~sQ48_spl|~sQ179_spl),
% 55.79/7.59 inference(forward_demodulation,[status(thm)],[f804,f2762])).
% 55.79/7.59 fof(f4667,plain,(
% 55.79/7.59 $false|~sQ48_spl|~sQ179_spl),
% 55.79/7.59 inference(forward_subsumption_resolution,[status(thm)],[f4666,f3869])).
% 55.79/7.59 fof(f4668,plain,(
% 55.79/7.59 ~sQ48_spl|~sQ179_spl),
% 55.79/7.59 inference(contradiction_clause,[status(thm)],[f4667])).
% 55.79/7.59 fof(f4748,plain,(
% 55.79/7.59 in(sK11_skl(empty_set,relation_composition(function_inverse(empty_set),empty_set)),empty_set)|~sQ53_spl|~sQ167_spl),
% 55.79/7.59 inference(forward_demodulation,[status(thm)],[f798,f2697])).
% 55.79/7.59 fof(f4749,plain,(
% 55.79/7.59 $false|~sQ53_spl|~sQ167_spl),
% 55.79/7.59 inference(forward_subsumption_resolution,[status(thm)],[f4748,f3869])).
% 55.79/7.59 fof(f4750,plain,(
% 55.79/7.59 ~sQ53_spl|~sQ167_spl),
% 55.79/7.59 inference(contradiction_clause,[status(thm)],[f4749])).
% 55.79/7.59 fof(f4751,plain,(
% 55.79/7.59 in(sK11_skl(empty_set,relation_composition(function_inverse(empty_set),empty_set)),empty_set)|~sQ53_spl|~sQ166_spl),
% 55.79/7.59 inference(forward_demodulation,[status(thm)],[f798,f2693])).
% 55.79/7.59 fof(f4752,plain,(
% 55.79/7.59 $false|~sQ53_spl|~sQ166_spl),
% 55.79/7.59 inference(forward_subsumption_resolution,[status(thm)],[f4751,f3869])).
% 55.79/7.59 fof(f4753,plain,(
% 55.79/7.59 ~sQ53_spl|~sQ166_spl),
% 55.79/7.59 inference(contradiction_clause,[status(thm)],[f4752])).
% 55.79/7.59 fof(f4762,plain,(
% 55.79/7.59 relation_rng(relation_composition(identity_relation(empty_set),function_inverse(identity_relation(empty_set))))=empty_set|~empty(empty_set)|~sQ93_spl),
% 55.79/7.59 inference(paramodulation,[status(thm)],[f1061,f608])).
% 55.79/7.59 fof(f4764,definition,(
% 55.79/7.59 sQ273_spl <=> (relation_rng(relation_composition(identity_relation(empty_set),function_inverse(identity_relation(empty_set))))=empty_set)),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f4767,plain,(
% 55.79/7.59 sQ273_spl|~sQ26_spl|~sQ93_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f4762,f4764,f368,f1014])).
% 55.79/7.59 fof(f4771,plain,(
% 55.79/7.59 relation_dom(relation_composition(identity_relation(empty_set),function_inverse(identity_relation(empty_set))))=empty_set|~empty(empty_set)|~sQ93_spl),
% 55.79/7.59 inference(paramodulation,[status(thm)],[f1061,f586])).
% 55.79/7.59 fof(f4773,definition,(
% 55.79/7.59 sQ274_spl <=> (relation_dom(relation_composition(identity_relation(empty_set),function_inverse(identity_relation(empty_set))))=empty_set)),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f4776,plain,(
% 55.79/7.59 sQ274_spl|~sQ26_spl|~sQ93_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f4771,f4773,f368,f1014])).
% 55.79/7.59 fof(f4969,plain,(
% 55.79/7.59 sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl))=apply(relation_composition(function_inverse(sK12_skl),sK12_skl),sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)))|~sQ8_spl|~sQ30_spl|~sQ260_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f1083,f4068])).
% 55.79/7.59 fof(f4974,plain,(
% 55.79/7.59 $false|sQ46_spl|~sQ8_spl|~sQ30_spl|~sQ260_spl),
% 55.79/7.59 inference(forward_subsumption_resolution,[status(thm)],[f4969,f1081])).
% 55.79/7.59 fof(f4975,plain,(
% 55.79/7.59 sQ46_spl|~sQ8_spl|~sQ30_spl|~sQ260_spl),
% 55.79/7.59 inference(contradiction_clause,[status(thm)],[f4974])).
% 55.79/7.59 fof(f5105,plain,(
% 55.79/7.59 ![X0]: (relation_composition(empty_set,X0)=relation_composition(empty_set,relation_composition(sK12_skl,sK12_skl))|~relation(X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f1610,f165])).
% 55.79/7.59 fof(f5115,plain,(
% 55.79/7.59 ![X0]: (relation_composition(empty_set,X0)=relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))|~relation(X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f1610,f123])).
% 55.79/7.59 fof(f5157,plain,(
% 55.79/7.59 ![X0]: (relation_composition(empty_set,identity_relation(X0))=relation_composition(empty_set,relation_composition(sK12_skl,sK12_skl)))),
% 55.79/7.59 inference(resolution,[status(thm)],[f5105,f62])).
% 55.79/7.59 fof(f5171,plain,(
% 55.79/7.59 empty_set=relation_composition(empty_set,relation_composition(sK12_skl,sK12_skl))),
% 55.79/7.59 inference(forward_demodulation,[status(thm)],[f2274,f5157])).
% 55.79/7.59 fof(f5366,definition,(
% 55.79/7.59 sQ281_spl <=> (relation(relation_composition(sK12_skl,sK12_skl)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5368,plain,(
% 55.79/7.59 ~relation(relation_composition(sK12_skl,sK12_skl))|sQ281_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f5366])).
% 55.79/7.59 fof(f5369,definition,(
% 55.79/7.59 sQ282_spl <=> (function(relation_composition(sK12_skl,sK12_skl)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5370,plain,(
% 55.79/7.59 function(relation_composition(sK12_skl,sK12_skl))|~sQ282_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f5369])).
% 55.79/7.59 fof(f5371,plain,(
% 55.79/7.59 ~function(relation_composition(sK12_skl,sK12_skl))|sQ282_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f5369])).
% 55.79/7.59 fof(f5553,plain,(
% 55.79/7.59 ~relation(sK12_skl)|~function(sK12_skl)|~relation(sK12_skl)|~function(sK12_skl)|sQ282_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5371,f73])).
% 55.79/7.59 fof(f5555,plain,(
% 55.79/7.59 ~sQ4_spl|~sQ5_spl|sQ282_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f5553,f226,f229,f5369])).
% 55.79/7.59 fof(f5567,plain,(
% 55.79/7.59 ~relation(sK12_skl)|~relation(sK12_skl)|sQ281_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5368,f61])).
% 55.79/7.59 fof(f5570,plain,(
% 55.79/7.59 ~sQ4_spl|sQ281_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f5567,f226,f5366])).
% 55.79/7.59 fof(f5818,plain,(
% 55.79/7.59 ![X0]: (relation_composition(X0,relation_composition(sK12_skl,sK12_skl))=identity_relation(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))))|apply(identity_relation(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl)))),sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))),relation_composition(X0,relation_composition(sK12_skl,sK12_skl))))=sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))),relation_composition(X0,relation_composition(sK12_skl,sK12_skl)))|~relation(X0)|~function(X0)|~relation(relation_composition(sK12_skl,sK12_skl))|~sQ282_spl)),
% 55.79/7.59 inference(resolution,[status(thm)],[f1028,f5370])).
% 55.79/7.59 fof(f5827,definition,(
% 55.79/7.59 ![X0]: (sQ296_spl <=> (relation_composition(X0,relation_composition(sK12_skl,sK12_skl))=identity_relation(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))))|apply(identity_relation(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl)))),sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))),relation_composition(X0,relation_composition(sK12_skl,sK12_skl))))=sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))),relation_composition(X0,relation_composition(sK12_skl,sK12_skl)))|~relation(X0)|~function(X0)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5830,plain,(
% 55.79/7.59 sQ296_spl|~sQ281_spl|~sQ282_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f5818,f5827,f5366,f5369])).
% 55.79/7.59 fof(f5911,plain,(
% 55.79/7.59 relation_composition(empty_set,sK12_skl)=relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),
% 55.79/7.59 inference(resolution,[status(thm)],[f5115,f165])).
% 55.79/7.59 fof(f5925,plain,(
% 55.79/7.59 empty_set=relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),
% 55.79/7.59 inference(forward_demodulation,[status(thm)],[f2275,f5911])).
% 55.79/7.59 fof(f5938,plain,(
% 55.79/7.59 relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))))|in(sK11_skl(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),relation_dom(empty_set))|~relation(empty_set)|~function(empty_set)|~relation(relation_composition(sK10_skl,sK10_skl))|~function(relation_composition(sK10_skl,sK10_skl))),
% 55.79/7.59 inference(paramodulation,[status(thm)],[f5925,f3922])).
% 55.79/7.59 fof(f5939,plain,(
% 55.79/7.59 relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))))|in(sK11_skl(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),empty_set),relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))))|~relation(empty_set)|~function(empty_set)|~relation(relation_composition(sK10_skl,sK10_skl))|~function(relation_composition(sK10_skl,sK10_skl))),
% 55.79/7.59 inference(paramodulation,[status(thm)],[f5925,f3922])).
% 55.79/7.59 fof(f5940,plain,(
% 55.79/7.59 relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))))|in(sK11_skl(relation_dom(empty_set),relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))))|~relation(empty_set)|~function(empty_set)|~relation(relation_composition(sK10_skl,sK10_skl))|~function(relation_composition(sK10_skl,sK10_skl))),
% 55.79/7.59 inference(paramodulation,[status(thm)],[f5925,f3922])).
% 55.79/7.59 fof(f5945,definition,(
% 55.79/7.59 sQ301_spl <=> (relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl)))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5948,definition,(
% 55.79/7.59 sQ302_spl <=> (in(sK11_skl(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),relation_dom(empty_set)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5951,definition,(
% 55.79/7.59 sQ303_spl <=> (relation(relation_composition(sK10_skl,sK10_skl)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5952,plain,(
% 55.79/7.59 relation(relation_composition(sK10_skl,sK10_skl))|~sQ303_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f5951])).
% 55.79/7.59 fof(f5953,plain,(
% 55.79/7.59 ~relation(relation_composition(sK10_skl,sK10_skl))|sQ303_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f5951])).
% 55.79/7.59 fof(f5954,definition,(
% 55.79/7.59 sQ304_spl <=> (function(relation_composition(sK10_skl,sK10_skl)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5955,plain,(
% 55.79/7.59 function(relation_composition(sK10_skl,sK10_skl))|~sQ304_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f5954])).
% 55.79/7.59 fof(f5956,plain,(
% 55.79/7.59 ~function(relation_composition(sK10_skl,sK10_skl))|sQ304_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f5954])).
% 55.79/7.59 fof(f5957,plain,(
% 55.79/7.59 sQ301_spl|sQ302_spl|~sQ27_spl|~sQ111_spl|~sQ303_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f5938,f5945,f5948,f371,f1175,f5951,f5954])).
% 55.79/7.59 fof(f5958,definition,(
% 55.79/7.59 sQ305_spl <=> (in(sK11_skl(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),empty_set),relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl)))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5961,plain,(
% 55.79/7.59 sQ301_spl|sQ305_spl|~sQ27_spl|~sQ111_spl|~sQ303_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f5939,f5945,f5958,f371,f1175,f5951,f5954])).
% 55.79/7.59 fof(f5962,definition,(
% 55.79/7.59 sQ306_spl <=> (in(sK11_skl(relation_dom(empty_set),relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl)))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5965,plain,(
% 55.79/7.59 sQ301_spl|sQ306_spl|~sQ27_spl|~sQ111_spl|~sQ303_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f5940,f5945,f5962,f371,f1175,f5951,f5954])).
% 55.79/7.59 fof(f5981,plain,(
% 55.79/7.59 ![X0]: (~element(relation_dom(X0),powerset(empty_set))|~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0))|~relation(relation_composition(sK12_skl,sK12_skl)))),
% 55.79/7.59 inference(paramodulation,[status(thm)],[f5171,f1262])).
% 55.79/7.59 fof(f5990,definition,(
% 55.79/7.59 ![X0]: (sQ309_spl <=> (~element(relation_dom(X0),powerset(empty_set))|~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f5994,plain,(
% 55.79/7.59 sQ309_spl|~sQ281_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f5981,f5990,f5366])).
% 55.79/7.59 fof(f6025,plain,(
% 55.79/7.59 ~relation(sK10_skl)|~relation(sK10_skl)|sQ303_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5953,f61])).
% 55.79/7.59 fof(f6029,definition,(
% 55.79/7.59 sQ312_spl <=> (relation(sK10_skl))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6031,plain,(
% 55.79/7.59 ~relation(sK10_skl)|sQ312_spl),
% 55.79/7.59 inference(component_clause,[status(thm)],[f6029])).
% 55.79/7.59 fof(f6034,plain,(
% 55.79/7.59 ~sQ312_spl|sQ303_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6025,f6029,f5951])).
% 55.79/7.59 fof(f6035,plain,(
% 55.79/7.59 $false|sQ312_spl),
% 55.79/7.59 inference(forward_subsumption_resolution,[status(thm)],[f6031,f123])).
% 55.79/7.59 fof(f6036,plain,(
% 55.79/7.59 sQ312_spl),
% 55.79/7.59 inference(contradiction_clause,[status(thm)],[f6035])).
% 55.79/7.59 fof(f6113,plain,(
% 55.79/7.59 ![X0]: (empty(relation_composition(empty_set,relation_composition(X0,sK12_skl)))|~relation(X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f3993,f165])).
% 55.79/7.59 fof(f6119,plain,(
% 55.79/7.59 ![X0]: (empty(relation_composition(empty_set,relation_composition(X0,sK10_skl)))|~relation(X0))),
% 55.79/7.59 inference(resolution,[status(thm)],[f3993,f123])).
% 55.79/7.59 fof(f6126,plain,(
% 55.79/7.59 empty(relation_composition(empty_set,function_inverse(sK12_skl)))|~relation(sK12_skl)),
% 55.79/7.59 inference(resolution,[status(thm)],[f3999,f166])).
% 55.79/7.59 fof(f6127,plain,(
% 55.79/7.59 empty(relation_composition(empty_set,function_inverse(relation_composition(sK12_skl,sK12_skl))))|~relation(relation_composition(sK12_skl,sK12_skl))|~sQ282_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f3999,f5370])).
% 55.79/7.59 fof(f6129,plain,(
% 55.79/7.59 empty(relation_composition(empty_set,function_inverse(empty_set)))|~relation(empty_set)),
% 55.79/7.59 inference(resolution,[status(thm)],[f3999,f709])).
% 55.79/7.59 fof(f6130,plain,(
% 55.79/7.59 empty(relation_composition(empty_set,function_inverse(sK1_skl)))|~relation(sK1_skl)),
% 55.79/7.59 inference(resolution,[status(thm)],[f3999,f96])).
% 55.79/7.59 fof(f6135,definition,(
% 55.79/7.59 sQ313_spl <=> (empty(relation_composition(empty_set,function_inverse(sK12_skl))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6138,plain,(
% 55.79/7.59 sQ313_spl|~sQ4_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6126,f6135,f226])).
% 55.79/7.59 fof(f6139,definition,(
% 55.79/7.59 sQ314_spl <=> (empty(relation_composition(empty_set,function_inverse(relation_composition(sK12_skl,sK12_skl)))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6142,plain,(
% 55.79/7.59 sQ314_spl|~sQ281_spl|~sQ282_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6127,f6139,f5366,f5369])).
% 55.79/7.59 fof(f6144,plain,(
% 55.79/7.59 sQ173_spl|~sQ27_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6129,f2725,f371])).
% 55.79/7.59 fof(f6145,definition,(
% 55.79/7.59 sQ315_spl <=> (empty(relation_composition(empty_set,function_inverse(sK1_skl))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6148,plain,(
% 55.79/7.59 sQ315_spl|~sQ97_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6130,f6145,f1029])).
% 55.79/7.59 fof(f6168,plain,(
% 55.79/7.59 ~relation(sK10_skl)|~function(sK10_skl)|~relation(sK10_skl)|~function(sK10_skl)|sQ304_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5956,f73])).
% 55.79/7.59 fof(f6170,definition,(
% 55.79/7.59 sQ317_spl <=> (function(sK10_skl))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6173,plain,(
% 55.79/7.59 ~sQ312_spl|~sQ317_spl|sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6168,f6029,f6170,f5954])).
% 55.79/7.59 fof(f6179,plain,(
% 55.79/7.59 ~relation(function_inverse(sK12_skl))|~relation(sK12_skl)|sQ22_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f337,f61])).
% 55.79/7.59 fof(f6182,plain,(
% 55.79/7.59 ~sQ37_spl|~sQ4_spl|sQ22_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6179,f445,f226,f335])).
% 55.79/7.59 fof(f6195,plain,(
% 55.79/7.59 relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)=empty_set|~sQ303_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5952,f682])).
% 55.79/7.59 fof(f6243,plain,(
% 55.79/7.59 empty(relation_composition(empty_set,function_inverse(relation_composition(sK10_skl,sK10_skl))))|~relation(relation_composition(sK10_skl,sK10_skl))|~sQ304_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5955,f3999])).
% 55.79/7.59 fof(f6244,plain,(
% 55.79/7.59 element(sK11_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)),relation_dom(relation_composition(sK10_skl,sK10_skl)))|~relation(relation_composition(sK10_skl,sK10_skl))|relation_composition(sK10_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK10_skl,sK10_skl)))|~sQ304_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5955,f1231])).
% 55.79/7.59 fof(f6245,plain,(
% 55.79/7.59 function_inverse(relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(function_inverse(relation_composition(sK10_skl,sK10_skl))))|apply(identity_relation(relation_dom(function_inverse(relation_composition(sK10_skl,sK10_skl)))),sK11_skl(relation_dom(function_inverse(relation_composition(sK10_skl,sK10_skl))),function_inverse(relation_composition(sK10_skl,sK10_skl))))=sK11_skl(relation_dom(function_inverse(relation_composition(sK10_skl,sK10_skl))),function_inverse(relation_composition(sK10_skl,sK10_skl)))|~relation(relation_composition(sK10_skl,sK10_skl))|~sQ304_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5955,f1039])).
% 55.79/7.59 fof(f6246,plain,(
% 55.79/7.59 ![X0]: (relation_composition(X0,relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(relation_composition(X0,relation_composition(sK10_skl,sK10_skl))))|apply(identity_relation(relation_dom(relation_composition(X0,relation_composition(sK10_skl,sK10_skl)))),sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK10_skl,sK10_skl))),relation_composition(X0,relation_composition(sK10_skl,sK10_skl))))=sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK10_skl,sK10_skl))),relation_composition(X0,relation_composition(sK10_skl,sK10_skl)))|~relation(X0)|~function(X0)|~relation(relation_composition(sK10_skl,sK10_skl))|~sQ304_spl)),
% 55.79/7.59 inference(resolution,[status(thm)],[f5955,f1028])).
% 55.79/7.59 fof(f6247,plain,(
% 55.79/7.59 ~relation(relation_composition(sK10_skl,sK10_skl))|relation_composition(sK10_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK10_skl,sK10_skl)))|apply(identity_relation(relation_dom(relation_composition(sK10_skl,sK10_skl))),sK11_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)))=sK11_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl))|~sQ304_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5955,f406])).
% 55.79/7.59 fof(f6248,plain,(
% 55.79/7.59 ~relation(relation_composition(sK10_skl,sK10_skl))|relation_composition(sK10_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK10_skl,sK10_skl)))|in(sK11_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)),relation_dom(relation_composition(sK10_skl,sK10_skl)))|~sQ304_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f5955,f189])).
% 55.79/7.59 fof(f6249,definition,(
% 55.79/7.59 sQ318_spl <=> (empty(relation_composition(empty_set,function_inverse(relation_composition(sK10_skl,sK10_skl)))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6252,plain,(
% 55.79/7.59 sQ318_spl|~sQ303_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6243,f6249,f5951,f5954])).
% 55.79/7.59 fof(f6253,definition,(
% 55.79/7.59 sQ319_spl <=> (element(sK11_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)),relation_dom(relation_composition(sK10_skl,sK10_skl))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6256,definition,(
% 55.79/7.59 sQ320_spl <=> (relation_composition(sK10_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK10_skl,sK10_skl))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6259,plain,(
% 55.79/7.59 sQ319_spl|~sQ303_spl|sQ320_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6244,f6253,f5951,f6256,f5954])).
% 55.79/7.59 fof(f6260,definition,(
% 55.79/7.59 sQ321_spl <=> (function_inverse(relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(function_inverse(relation_composition(sK10_skl,sK10_skl)))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6263,definition,(
% 55.79/7.59 sQ322_spl <=> (apply(identity_relation(relation_dom(function_inverse(relation_composition(sK10_skl,sK10_skl)))),sK11_skl(relation_dom(function_inverse(relation_composition(sK10_skl,sK10_skl))),function_inverse(relation_composition(sK10_skl,sK10_skl))))=sK11_skl(relation_dom(function_inverse(relation_composition(sK10_skl,sK10_skl))),function_inverse(relation_composition(sK10_skl,sK10_skl))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6266,plain,(
% 55.79/7.59 sQ321_spl|sQ322_spl|~sQ303_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6245,f6260,f6263,f5951,f5954])).
% 55.79/7.59 fof(f6267,definition,(
% 55.79/7.59 ![X0]: (sQ323_spl <=> (relation_composition(X0,relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(relation_composition(X0,relation_composition(sK10_skl,sK10_skl))))|apply(identity_relation(relation_dom(relation_composition(X0,relation_composition(sK10_skl,sK10_skl)))),sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK10_skl,sK10_skl))),relation_composition(X0,relation_composition(sK10_skl,sK10_skl))))=sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK10_skl,sK10_skl))),relation_composition(X0,relation_composition(sK10_skl,sK10_skl)))|~relation(X0)|~function(X0)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6270,plain,(
% 55.79/7.59 sQ323_spl|~sQ303_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6246,f6267,f5951,f5954])).
% 55.79/7.59 fof(f6271,definition,(
% 55.79/7.59 sQ324_spl <=> (apply(identity_relation(relation_dom(relation_composition(sK10_skl,sK10_skl))),sK11_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)))=sK11_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6274,plain,(
% 55.79/7.59 ~sQ303_spl|sQ320_spl|sQ324_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6247,f5951,f6256,f6271,f5954])).
% 55.79/7.59 fof(f6275,definition,(
% 55.79/7.59 sQ325_spl <=> (in(sK11_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)),relation_dom(relation_composition(sK10_skl,sK10_skl))))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6278,plain,(
% 55.79/7.59 ~sQ303_spl|sQ320_spl|sQ325_spl|~sQ304_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6248,f5951,f6256,f6275,f5954])).
% 55.79/7.59 fof(f6293,plain,(
% 55.79/7.59 empty(relation_composition(function_inverse(sK12_skl),empty_set))|~relation(sK12_skl)),
% 55.79/7.59 inference(resolution,[status(thm)],[f4019,f166])).
% 55.79/7.59 fof(f6294,plain,(
% 55.79/7.59 empty(relation_composition(function_inverse(relation_composition(sK12_skl,sK12_skl)),empty_set))|~relation(relation_composition(sK12_skl,sK12_skl))|~sQ282_spl),
% 55.79/7.59 inference(resolution,[status(thm)],[f4019,f5370])).
% 55.79/7.59 fof(f6296,plain,(
% 55.79/7.59 empty(relation_composition(function_inverse(empty_set),empty_set))|~relation(empty_set)),
% 55.79/7.59 inference(resolution,[status(thm)],[f4019,f709])).
% 55.79/7.59 fof(f6297,plain,(
% 55.79/7.59 empty(relation_composition(function_inverse(sK1_skl),empty_set))|~relation(sK1_skl)),
% 55.79/7.59 inference(resolution,[status(thm)],[f4019,f96])).
% 55.79/7.59 fof(f6302,definition,(
% 55.79/7.59 sQ326_spl <=> (empty(relation_composition(function_inverse(sK12_skl),empty_set)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6305,plain,(
% 55.79/7.59 sQ326_spl|~sQ4_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6293,f6302,f226])).
% 55.79/7.59 fof(f6306,definition,(
% 55.79/7.59 sQ327_spl <=> (empty(relation_composition(function_inverse(relation_composition(sK12_skl,sK12_skl)),empty_set)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6309,plain,(
% 55.79/7.59 sQ327_spl|~sQ281_spl|~sQ282_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6294,f6306,f5366,f5369])).
% 55.79/7.59 fof(f6311,plain,(
% 55.79/7.59 sQ160_spl|~sQ27_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6296,f2656,f371])).
% 55.79/7.59 fof(f6312,definition,(
% 55.79/7.59 sQ328_spl <=> (empty(relation_composition(function_inverse(sK1_skl),empty_set)))),
% 55.79/7.59 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 55.79/7.59 fof(f6315,plain,(
% 55.79/7.59 sQ328_spl|~sQ97_spl),
% 55.79/7.59 inference(split_clause,[status(thm)],[f6297,f6312,f1029])).
% 55.79/7.60 fof(f6332,plain,(
% 55.79/7.60 ![X0]: (relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))=identity_relation(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))))|~relation(empty_set)|~function(empty_set)|~relation(relation_composition(sK10_skl,sK10_skl))|~function(relation_composition(sK10_skl,sK10_skl))|~element(relation_dom(empty_set),powerset(X0))|element(sK11_skl(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),X0))),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f5925,f4209])).
% 55.79/7.60 fof(f6342,definition,(
% 55.79/7.60 ![X0]: (sQ331_spl <=> (~element(relation_dom(empty_set),powerset(X0))|element(sK11_skl(relation_dom(relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK10_skl,sK10_skl))),X0)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6345,plain,(
% 55.79/7.60 sQ301_spl|~sQ27_spl|~sQ111_spl|~sQ303_spl|~sQ304_spl|sQ331_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6332,f5945,f371,f1175,f5951,f5954,f6342])).
% 55.79/7.60 fof(f6350,plain,(
% 55.79/7.60 ![X0]: (relation_composition(X0,sK12_skl)=identity_relation(relation_dom(relation_composition(X0,sK12_skl)))|~relation(X0)|~function(X0)|~relation(sK12_skl)|~in(relation_dom(relation_composition(X0,sK12_skl)),sK11_skl(relation_dom(relation_composition(X0,sK12_skl)),relation_composition(X0,sK12_skl))))),
% 55.79/7.60 inference(resolution,[status(thm)],[f4211,f166])).
% 55.79/7.60 fof(f6351,plain,(
% 55.79/7.60 ![X0]: (relation_composition(X0,relation_composition(sK12_skl,sK12_skl))=identity_relation(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))))|~relation(X0)|~function(X0)|~relation(relation_composition(sK12_skl,sK12_skl))|~in(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))),sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))),relation_composition(X0,relation_composition(sK12_skl,sK12_skl))))|~sQ282_spl)),
% 55.79/7.60 inference(resolution,[status(thm)],[f4211,f5370])).
% 55.79/7.60 fof(f6353,plain,(
% 55.79/7.60 ![X0]: (relation_composition(X0,empty_set)=identity_relation(relation_dom(relation_composition(X0,empty_set)))|~relation(X0)|~function(X0)|~relation(empty_set)|~in(relation_dom(relation_composition(X0,empty_set)),sK11_skl(relation_dom(relation_composition(X0,empty_set)),relation_composition(X0,empty_set))))),
% 55.79/7.60 inference(resolution,[status(thm)],[f4211,f709])).
% 55.79/7.60 fof(f6354,plain,(
% 55.79/7.60 ![X0]: (relation_composition(X0,sK1_skl)=identity_relation(relation_dom(relation_composition(X0,sK1_skl)))|~relation(X0)|~function(X0)|~relation(sK1_skl)|~in(relation_dom(relation_composition(X0,sK1_skl)),sK11_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl))))),
% 55.79/7.60 inference(resolution,[status(thm)],[f4211,f96])).
% 55.79/7.60 fof(f6359,definition,(
% 55.79/7.60 ![X0]: (sQ333_spl <=> (relation_composition(X0,sK12_skl)=identity_relation(relation_dom(relation_composition(X0,sK12_skl)))|~relation(X0)|~function(X0)|~in(relation_dom(relation_composition(X0,sK12_skl)),sK11_skl(relation_dom(relation_composition(X0,sK12_skl)),relation_composition(X0,sK12_skl)))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6362,plain,(
% 55.79/7.60 sQ333_spl|~sQ4_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6350,f6359,f226])).
% 55.79/7.60 fof(f6363,definition,(
% 55.79/7.60 ![X0]: (sQ334_spl <=> (relation_composition(X0,relation_composition(sK12_skl,sK12_skl))=identity_relation(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))))|~relation(X0)|~function(X0)|~in(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))),sK11_skl(relation_dom(relation_composition(X0,relation_composition(sK12_skl,sK12_skl))),relation_composition(X0,relation_composition(sK12_skl,sK12_skl))))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6366,plain,(
% 55.79/7.60 sQ334_spl|~sQ281_spl|~sQ282_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6351,f6363,f5366,f5369])).
% 55.79/7.60 fof(f6368,definition,(
% 55.79/7.60 ![X0]: (sQ335_spl <=> (relation_composition(X0,empty_set)=identity_relation(relation_dom(relation_composition(X0,empty_set)))|~relation(X0)|~function(X0)|~in(relation_dom(relation_composition(X0,empty_set)),sK11_skl(relation_dom(relation_composition(X0,empty_set)),relation_composition(X0,empty_set)))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6371,plain,(
% 55.79/7.60 sQ335_spl|~sQ27_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6353,f6368,f371])).
% 55.79/7.60 fof(f6372,definition,(
% 55.79/7.60 ![X0]: (sQ336_spl <=> (relation_composition(X0,sK1_skl)=identity_relation(relation_dom(relation_composition(X0,sK1_skl)))|~relation(X0)|~function(X0)|~in(relation_dom(relation_composition(X0,sK1_skl)),sK11_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl)))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6375,plain,(
% 55.79/7.60 sQ336_spl|~sQ97_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6354,f6372,f1029])).
% 55.79/7.60 fof(f6415,definition,(
% 55.79/7.60 sQ340_spl <=> (function(sK1_skl))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6417,plain,(
% 55.79/7.60 ~function(sK1_skl)|sQ340_spl),
% 55.79/7.60 inference(component_clause,[status(thm)],[f6415])).
% 55.79/7.60 fof(f6424,plain,(
% 55.79/7.60 ![X0]: (relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)=identity_relation(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)))|~relation(relation_composition(sK10_skl,sK10_skl))|~function(relation_composition(sK10_skl,sK10_skl))|~relation(empty_set)|~function(empty_set)|~element(relation_dom(empty_set),powerset(X0))|element(sK11_skl(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),X0)|~sQ303_spl)),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f6195,f4209])).
% 55.79/7.60 fof(f6425,plain,(
% 55.79/7.60 relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)=identity_relation(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)))|in(sK11_skl(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),relation_dom(empty_set))|~relation(relation_composition(sK10_skl,sK10_skl))|~function(relation_composition(sK10_skl,sK10_skl))|~relation(empty_set)|~function(empty_set)|~sQ303_spl),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f6195,f3922])).
% 55.79/7.60 fof(f6426,plain,(
% 55.79/7.60 relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)=identity_relation(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)))|in(sK11_skl(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),empty_set),relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)))|~relation(relation_composition(sK10_skl,sK10_skl))|~function(relation_composition(sK10_skl,sK10_skl))|~relation(empty_set)|~function(empty_set)|~sQ303_spl),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f6195,f3922])).
% 55.79/7.60 fof(f6427,plain,(
% 55.79/7.60 relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)=identity_relation(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)))|in(sK11_skl(relation_dom(empty_set),relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)))|~relation(relation_composition(sK10_skl,sK10_skl))|~function(relation_composition(sK10_skl,sK10_skl))|~relation(empty_set)|~function(empty_set)|~sQ303_spl),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f6195,f3922])).
% 55.79/7.60 fof(f6433,definition,(
% 55.79/7.60 sQ342_spl <=> (relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)=identity_relation(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6436,definition,(
% 55.79/7.60 ![X0]: (sQ343_spl <=> (~element(relation_dom(empty_set),powerset(X0))|element(sK11_skl(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),X0)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6439,plain,(
% 55.79/7.60 sQ342_spl|~sQ303_spl|~sQ304_spl|~sQ27_spl|~sQ111_spl|sQ343_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6424,f6433,f5951,f5954,f371,f1175,f6436])).
% 55.79/7.60 fof(f6440,definition,(
% 55.79/7.60 sQ344_spl <=> (in(sK11_skl(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),relation_dom(empty_set)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6443,plain,(
% 55.79/7.60 sQ342_spl|sQ344_spl|~sQ303_spl|~sQ304_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6425,f6433,f6440,f5951,f5954,f371,f1175])).
% 55.79/7.60 fof(f6444,definition,(
% 55.79/7.60 sQ345_spl <=> (in(sK11_skl(relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),empty_set),relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6447,plain,(
% 55.79/7.60 sQ342_spl|sQ345_spl|~sQ303_spl|~sQ304_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6426,f6433,f6444,f5951,f5954,f371,f1175])).
% 55.79/7.60 fof(f6448,definition,(
% 55.79/7.60 sQ346_spl <=> (in(sK11_skl(relation_dom(empty_set),relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set)),relation_dom(relation_composition(relation_composition(sK10_skl,sK10_skl),empty_set))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6451,plain,(
% 55.79/7.60 sQ342_spl|sQ346_spl|~sQ303_spl|~sQ304_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6427,f6433,f6448,f5951,f5954,f371,f1175])).
% 55.79/7.60 fof(f6528,plain,(
% 55.79/7.60 empty(relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl)))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6113,f123])).
% 55.79/7.60 fof(f6529,plain,(
% 55.79/7.60 empty(relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl)))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6113,f112])).
% 55.79/7.60 fof(f6530,plain,(
% 55.79/7.60 empty(relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl)))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6113,f95])).
% 55.79/7.60 fof(f6552,plain,(
% 55.79/7.60 ![X0]: (~function(relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl)))|~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl))),relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl))),X0))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6528,f4071])).
% 55.79/7.60 fof(f6564,plain,(
% 55.79/7.60 relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl))=empty_set),
% 55.79/7.60 inference(resolution,[status(thm)],[f6528,f170])).
% 55.79/7.60 fof(f6577,definition,(
% 55.79/7.60 sQ349_spl <=> (function(relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6579,plain,(
% 55.79/7.60 ~function(relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl)))|sQ349_spl),
% 55.79/7.60 inference(component_clause,[status(thm)],[f6577])).
% 55.79/7.60 fof(f6580,definition,(
% 55.79/7.60 ![X0]: (sQ350_spl <=> (~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl))),relation_composition(empty_set,relation_composition(sK10_skl,sK12_skl))),X0)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6583,plain,(
% 55.79/7.60 ~sQ349_spl|sQ350_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6552,f6577,f6580])).
% 55.79/7.60 fof(f6643,plain,(
% 55.79/7.60 ~function(empty_set)|sQ349_spl),
% 55.79/7.60 inference(forward_demodulation,[status(thm)],[f6564,f6579])).
% 55.79/7.60 fof(f6644,plain,(
% 55.79/7.60 $false|sQ349_spl),
% 55.79/7.60 inference(forward_subsumption_resolution,[status(thm)],[f6643,f709])).
% 55.79/7.60 fof(f6645,plain,(
% 55.79/7.60 sQ349_spl),
% 55.79/7.60 inference(contradiction_clause,[status(thm)],[f6644])).
% 55.79/7.60 fof(f6667,plain,(
% 55.79/7.60 ![X0]: (~function(relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl)))|~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl))),relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl))),X0))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6529,f4071])).
% 55.79/7.60 fof(f6679,plain,(
% 55.79/7.60 relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl))=empty_set),
% 55.79/7.60 inference(resolution,[status(thm)],[f6529,f170])).
% 55.79/7.60 fof(f6692,definition,(
% 55.79/7.60 sQ354_spl <=> (function(relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6694,plain,(
% 55.79/7.60 ~function(relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl)))|sQ354_spl),
% 55.79/7.60 inference(component_clause,[status(thm)],[f6692])).
% 55.79/7.60 fof(f6695,definition,(
% 55.79/7.60 ![X0]: (sQ355_spl <=> (~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl))),relation_composition(empty_set,relation_composition(sK6_skl,sK12_skl))),X0)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6698,plain,(
% 55.79/7.60 ~sQ354_spl|sQ355_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6667,f6692,f6695])).
% 55.79/7.60 fof(f6758,plain,(
% 55.79/7.60 ~function(empty_set)|sQ354_spl),
% 55.79/7.60 inference(forward_demodulation,[status(thm)],[f6679,f6694])).
% 55.79/7.60 fof(f6759,plain,(
% 55.79/7.60 $false|sQ354_spl),
% 55.79/7.60 inference(forward_subsumption_resolution,[status(thm)],[f6758,f709])).
% 55.79/7.60 fof(f6760,plain,(
% 55.79/7.60 sQ354_spl),
% 55.79/7.60 inference(contradiction_clause,[status(thm)],[f6759])).
% 55.79/7.60 fof(f6780,plain,(
% 55.79/7.60 ![X0]: (~function(relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl)))|~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl))),relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl))),X0))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6530,f4071])).
% 55.79/7.60 fof(f6792,plain,(
% 55.79/7.60 relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl))=empty_set),
% 55.79/7.60 inference(resolution,[status(thm)],[f6530,f170])).
% 55.79/7.60 fof(f6805,definition,(
% 55.79/7.60 sQ359_spl <=> (function(relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6807,plain,(
% 55.79/7.60 ~function(relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl)))|sQ359_spl),
% 55.79/7.60 inference(component_clause,[status(thm)],[f6805])).
% 55.79/7.60 fof(f6808,definition,(
% 55.79/7.60 ![X0]: (sQ360_spl <=> (~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl))),relation_composition(empty_set,relation_composition(sK1_skl,sK12_skl))),X0)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f6811,plain,(
% 55.79/7.60 ~sQ359_spl|sQ360_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f6780,f6805,f6808])).
% 55.79/7.60 fof(f6871,plain,(
% 55.79/7.60 ~function(empty_set)|sQ359_spl),
% 55.79/7.60 inference(forward_demodulation,[status(thm)],[f6792,f6807])).
% 55.79/7.60 fof(f6872,plain,(
% 55.79/7.60 $false|sQ359_spl),
% 55.79/7.60 inference(forward_subsumption_resolution,[status(thm)],[f6871,f709])).
% 55.79/7.60 fof(f6873,plain,(
% 55.79/7.60 sQ359_spl),
% 55.79/7.60 inference(contradiction_clause,[status(thm)],[f6872])).
% 55.79/7.60 fof(f6999,plain,(
% 55.79/7.60 empty(relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl)))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6119,f165])).
% 55.79/7.60 fof(f7008,plain,(
% 55.79/7.60 empty(relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl)))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6119,f112])).
% 55.79/7.60 fof(f7009,plain,(
% 55.79/7.60 empty(relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl)))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6119,f95])).
% 55.79/7.60 fof(f7019,plain,(
% 55.79/7.60 ~relation(function_inverse(sK12_skl))|~function(function_inverse(sK12_skl))|~relation(sK12_skl)|~function(sK12_skl)|sQ28_spl),
% 55.79/7.60 inference(resolution,[status(thm)],[f409,f73])).
% 55.79/7.60 fof(f7021,plain,(
% 55.79/7.60 ~sQ37_spl|~sQ63_spl|~sQ4_spl|~sQ5_spl|sQ28_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f7019,f445,f848,f226,f229,f407])).
% 55.79/7.60 fof(f7133,plain,(
% 55.79/7.60 ![X0]: (~function(relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl)))|~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl))),X0))),
% 55.79/7.60 inference(resolution,[status(thm)],[f6999,f4071])).
% 55.79/7.60 fof(f7145,plain,(
% 55.79/7.60 relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl))=empty_set),
% 55.79/7.60 inference(resolution,[status(thm)],[f6999,f170])).
% 55.79/7.60 fof(f7158,definition,(
% 55.79/7.60 sQ390_spl <=> (function(relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7160,plain,(
% 55.79/7.60 ~function(relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl)))|sQ390_spl),
% 55.79/7.60 inference(component_clause,[status(thm)],[f7158])).
% 55.79/7.60 fof(f7161,definition,(
% 55.79/7.60 ![X0]: (sQ391_spl <=> (~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK12_skl,sK10_skl))),X0)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7164,plain,(
% 55.79/7.60 ~sQ390_spl|sQ391_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f7133,f7158,f7161])).
% 55.79/7.60 fof(f7224,plain,(
% 55.79/7.60 ~function(empty_set)|sQ390_spl),
% 55.79/7.60 inference(forward_demodulation,[status(thm)],[f7145,f7160])).
% 55.79/7.60 fof(f7225,plain,(
% 55.79/7.60 $false|sQ390_spl),
% 55.79/7.60 inference(forward_subsumption_resolution,[status(thm)],[f7224,f709])).
% 55.79/7.60 fof(f7226,plain,(
% 55.79/7.60 sQ390_spl),
% 55.79/7.60 inference(contradiction_clause,[status(thm)],[f7225])).
% 55.79/7.60 fof(f7246,plain,(
% 55.79/7.60 ![X0]: (~function(relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl)))|~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl))),X0))),
% 55.79/7.60 inference(resolution,[status(thm)],[f7008,f4071])).
% 55.79/7.60 fof(f7258,plain,(
% 55.79/7.60 relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl))=empty_set),
% 55.79/7.60 inference(resolution,[status(thm)],[f7008,f170])).
% 55.79/7.60 fof(f7271,definition,(
% 55.79/7.60 sQ395_spl <=> (function(relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ395_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7273,plain,(
% 55.79/7.60 ~function(relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl)))|sQ395_spl),
% 55.79/7.60 inference(component_clause,[status(thm)],[f7271])).
% 55.79/7.60 fof(f7274,definition,(
% 55.79/7.60 ![X0]: (sQ396_spl <=> (~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK6_skl,sK10_skl))),X0)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ396_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7277,plain,(
% 55.79/7.60 ~sQ395_spl|sQ396_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f7246,f7271,f7274])).
% 55.79/7.60 fof(f7337,plain,(
% 55.79/7.60 ~function(empty_set)|sQ395_spl),
% 55.79/7.60 inference(forward_demodulation,[status(thm)],[f7258,f7273])).
% 55.79/7.60 fof(f7338,plain,(
% 55.79/7.60 $false|sQ395_spl),
% 55.79/7.60 inference(forward_subsumption_resolution,[status(thm)],[f7337,f709])).
% 55.79/7.60 fof(f7339,plain,(
% 55.79/7.60 sQ395_spl),
% 55.79/7.60 inference(contradiction_clause,[status(thm)],[f7338])).
% 55.79/7.60 fof(f7359,plain,(
% 55.79/7.60 ![X0]: (~function(relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl)))|~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl))),X0))),
% 55.79/7.60 inference(resolution,[status(thm)],[f7009,f4071])).
% 55.79/7.60 fof(f7371,plain,(
% 55.79/7.60 relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl))=empty_set),
% 55.79/7.60 inference(resolution,[status(thm)],[f7009,f170])).
% 55.79/7.60 fof(f7384,definition,(
% 55.79/7.60 sQ400_spl <=> (function(relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ400_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7386,plain,(
% 55.79/7.60 ~function(relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl)))|sQ400_spl),
% 55.79/7.60 inference(component_clause,[status(thm)],[f7384])).
% 55.79/7.60 fof(f7387,definition,(
% 55.79/7.60 ![X0]: (sQ401_spl <=> (~in(X0,relation_rng(relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl))))|X0=apply(relation_composition(function_inverse(relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl))),relation_composition(empty_set,relation_composition(sK1_skl,sK10_skl))),X0)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ401_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7390,plain,(
% 55.79/7.60 ~sQ400_spl|sQ401_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f7359,f7384,f7387])).
% 55.79/7.60 fof(f7450,plain,(
% 55.79/7.60 ~function(empty_set)|sQ400_spl),
% 55.79/7.60 inference(forward_demodulation,[status(thm)],[f7371,f7386])).
% 55.79/7.60 fof(f7451,plain,(
% 55.79/7.60 $false|sQ400_spl),
% 55.79/7.60 inference(forward_subsumption_resolution,[status(thm)],[f7450,f709])).
% 55.79/7.60 fof(f7452,plain,(
% 55.79/7.60 sQ400_spl),
% 55.79/7.60 inference(contradiction_clause,[status(thm)],[f7451])).
% 55.79/7.60 fof(f7505,definition,(
% 55.79/7.60 sQ408_spl <=> (relation(sK6_skl))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7507,plain,(
% 55.79/7.60 ~relation(sK6_skl)|sQ408_spl),
% 55.79/7.60 inference(component_clause,[status(thm)],[f7505])).
% 55.79/7.60 fof(f7538,plain,(
% 55.79/7.60 $false|sQ408_spl),
% 55.79/7.60 inference(forward_subsumption_resolution,[status(thm)],[f7507,f112])).
% 55.79/7.60 fof(f7539,plain,(
% 55.79/7.60 sQ408_spl),
% 55.79/7.60 inference(contradiction_clause,[status(thm)],[f7538])).
% 55.79/7.60 fof(f7573,plain,(
% 55.79/7.60 $false|sQ340_spl),
% 55.79/7.60 inference(forward_subsumption_resolution,[status(thm)],[f6417,f96])).
% 55.79/7.60 fof(f7574,plain,(
% 55.79/7.60 sQ340_spl),
% 55.79/7.60 inference(contradiction_clause,[status(thm)],[f7573])).
% 55.79/7.60 fof(f7582,plain,(
% 55.79/7.60 ![X0,X1]: (relation_composition(empty_set,identity_relation(X0))=identity_relation(relation_dom(relation_composition(empty_set,identity_relation(X0))))|~relation(empty_set)|~function(empty_set)|~relation(identity_relation(X0))|~function(identity_relation(X0))|~element(relation_dom(empty_set),powerset(X1))|element(sK11_skl(relation_dom(relation_composition(empty_set,identity_relation(X0))),relation_composition(empty_set,identity_relation(X0))),X1))),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f2274,f4209])).
% 55.79/7.60 fof(f7583,plain,(
% 55.79/7.60 ![X0]: (relation_composition(empty_set,identity_relation(X0))=identity_relation(relation_dom(relation_composition(empty_set,identity_relation(X0))))|in(sK11_skl(relation_dom(relation_composition(empty_set,identity_relation(X0))),relation_composition(empty_set,identity_relation(X0))),relation_dom(empty_set))|~relation(empty_set)|~function(empty_set)|~relation(identity_relation(X0))|~function(identity_relation(X0)))),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f2274,f3922])).
% 55.79/7.60 fof(f7584,plain,(
% 55.79/7.60 ![X0]: (relation_composition(empty_set,identity_relation(X0))=identity_relation(relation_dom(relation_composition(empty_set,identity_relation(X0))))|in(sK11_skl(relation_dom(relation_composition(empty_set,identity_relation(X0))),empty_set),relation_dom(relation_composition(empty_set,identity_relation(X0))))|~relation(empty_set)|~function(empty_set)|~relation(identity_relation(X0))|~function(identity_relation(X0)))),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f2274,f3922])).
% 55.79/7.60 fof(f7585,plain,(
% 55.79/7.60 ![X0]: (relation_composition(empty_set,identity_relation(X0))=identity_relation(relation_dom(relation_composition(empty_set,identity_relation(X0))))|in(sK11_skl(relation_dom(empty_set),relation_composition(empty_set,identity_relation(X0))),relation_dom(relation_composition(empty_set,identity_relation(X0))))|~relation(empty_set)|~function(empty_set)|~relation(identity_relation(X0))|~function(identity_relation(X0)))),
% 55.79/7.60 inference(paramodulation,[status(thm)],[f2274,f3922])).
% 55.79/7.60 fof(f7594,definition,(
% 55.79/7.60 ![X0,X1]: (sQ422_spl <=> (relation_composition(empty_set,identity_relation(X0))=identity_relation(relation_dom(relation_composition(empty_set,identity_relation(X0))))|~relation(identity_relation(X0))|~function(identity_relation(X0))|~element(relation_dom(empty_set),powerset(X1))|element(sK11_skl(relation_dom(relation_composition(empty_set,identity_relation(X0))),relation_composition(empty_set,identity_relation(X0))),X1)))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7597,plain,(
% 55.79/7.60 sQ422_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f7582,f7594,f371,f1175])).
% 55.79/7.60 fof(f7598,definition,(
% 55.79/7.60 ![X0]: (sQ423_spl <=> (relation_composition(empty_set,identity_relation(X0))=identity_relation(relation_dom(relation_composition(empty_set,identity_relation(X0))))|in(sK11_skl(relation_dom(relation_composition(empty_set,identity_relation(X0))),relation_composition(empty_set,identity_relation(X0))),relation_dom(empty_set))|~relation(identity_relation(X0))|~function(identity_relation(X0))))),
% 55.79/7.60 introduced(definition,[new_symbols(definition,[sQ423_spl])],[split_symbol_definition])).
% 55.79/7.60 fof(f7601,plain,(
% 55.79/7.60 sQ423_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.60 inference(split_clause,[status(thm)],[f7583,f7598,f371,f1175])).
% 55.79/7.60 fof(f7602,definition,(
% 55.79/7.62 ![X0]: (sQ424_spl <=> (relation_composition(empty_set,identity_relation(X0))=identity_relation(relation_dom(relation_composition(empty_set,identity_relation(X0))))|in(sK11_skl(relation_dom(relation_composition(empty_set,identity_relation(X0))),empty_set),relation_dom(relation_composition(empty_set,identity_relation(X0))))|~relation(identity_relation(X0))|~function(identity_relation(X0))))),
% 55.79/7.62 introduced(definition,[new_symbols(definition,[sQ424_spl])],[split_symbol_definition])).
% 55.79/7.62 fof(f7605,plain,(
% 55.79/7.62 sQ424_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.62 inference(split_clause,[status(thm)],[f7584,f7602,f371,f1175])).
% 55.79/7.62 fof(f7606,definition,(
% 55.79/7.62 ![X0]: (sQ425_spl <=> (relation_composition(empty_set,identity_relation(X0))=identity_relation(relation_dom(relation_composition(empty_set,identity_relation(X0))))|in(sK11_skl(relation_dom(empty_set),relation_composition(empty_set,identity_relation(X0))),relation_dom(relation_composition(empty_set,identity_relation(X0))))|~relation(identity_relation(X0))|~function(identity_relation(X0))))),
% 55.79/7.62 introduced(definition,[new_symbols(definition,[sQ425_spl])],[split_symbol_definition])).
% 55.79/7.62 fof(f7609,plain,(
% 55.79/7.62 sQ425_spl|~sQ27_spl|~sQ111_spl),
% 55.79/7.62 inference(split_clause,[status(thm)],[f7585,f7606,f371,f1175])).
% 55.79/7.62 fof(f7668,plain,(
% 55.79/7.62 ~relation(sK12_skl)|~function(sK12_skl)|sQ63_spl),
% 55.79/7.62 inference(resolution,[status(thm)],[f850,f59])).
% 55.79/7.62 fof(f7670,plain,(
% 55.79/7.62 ~sQ4_spl|~sQ5_spl|sQ63_spl),
% 55.79/7.62 inference(split_clause,[status(thm)],[f7668,f226,f229,f848])).
% 55.79/7.62 fof(f7777,plain,(
% 55.79/7.62 sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl)))=apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))))|~sQ6_spl|~sQ33_spl|~sQ45_spl),
% 55.79/7.62 inference(resolution,[status(thm)],[f997,f541])).
% 55.79/7.62 fof(f7782,plain,(
% 55.79/7.62 $false|sQ41_spl|~sQ6_spl|~sQ33_spl|~sQ45_spl),
% 55.79/7.62 inference(forward_subsumption_resolution,[status(thm)],[f7777,f999])).
% 55.79/7.62 fof(f7783,plain,(
% 55.79/7.62 sQ41_spl|~sQ6_spl|~sQ33_spl|~sQ45_spl),
% 55.79/7.62 inference(contradiction_clause,[status(thm)],[f7782])).
% 55.79/7.62 fof(f7784,plain,(
% 55.79/7.62 $false),
% 55.79/7.62 inference(sat_refutation,[status(thm)],[f183,f213,f235,f243,f247,f249,f255,f263,f279,f283,f287,f291,f293,f295,f354,f356,f374,f376,f416,f426,f453,f456,f485,f513,f526,f530,f539,f543,f558,f578,f590,f603,f623,f642,f851,f1075,f1086,f1124,f1169,f1171,f1181,f1183,f1191,f1526,f2430,f2784,f2798,f2977,f2982,f2988,f3206,f3214,f3305,f3313,f3381,f3513,f3821,f3843,f4070,f4238,f4242,f4665,f4668,f4750,f4753,f4767,f4776,f4975,f5555,f5570,f5830,f5957,f5961,f5965,f5994,f6034,f6036,f6138,f6142,f6144,f6148,f6173,f6182,f6252,f6259,f6266,f6270,f6274,f6278,f6305,f6309,f6311,f6315,f6345,f6362,f6366,f6371,f6375,f6439,f6443,f6447,f6451,f6583,f6645,f6698,f6760,f6811,f6873,f7021,f7164,f7226,f7277,f7339,f7390,f7452,f7539,f7574,f7597,f7601,f7605,f7609,f7670,f7783])).
% 55.79/7.62 % SZS output end CNFRefutation for theBenchmark.p
% 15.81/7.67 % Elapsed time: 7.194590 seconds
% 15.81/7.67 % CPU time: 56.401537 seconds
% 15.81/7.67 % Total memory used: 579.053 MB
% 15.81/7.67 % Net memory used: 559.616 MB
%------------------------------------------------------------------------------