%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU028+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:19:06 PM UTC 2026
% Result : Theorem 1.00s 0.70s
% Output : CNFRefutation 1.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 143
% Syntax : Number of formulae : 602 ( 48 unt; 108 def)
% Number of atoms : 1815 ( 270 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2172 ( 959 ~; 985 |; 88 &)
% ( 110 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 117 ( 115 usr; 109 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-2 aty)
% Number of variables : 269 ( 260 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( ( function(A)
& empty(A)
& relation(A) )
=> ( one_to_one(A)
& function(A)
& relation(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( function(function_inverse(A))
& relation(function_inverse(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(relation_composition(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( ( relation(B)
& empty(A) )
=> ( relation(relation_composition(B,A))
& empty(relation_composition(B,A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] :
( ( function(B)
& relation(B)
& function(A)
& relation(A) )
=> ( function(relation_composition(A,B))
& relation(relation_composition(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_dom(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_rng(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( empty(A)
=> ( relation(relation_dom(A))
& empty(relation_dom(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( empty(A)
=> ( relation(relation_rng(A))
& empty(relation_rng(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B] :
( ( relation(B)
& empty(A) )
=> ( relation(relation_composition(A,B))
& empty(relation_composition(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( B = identity_relation(A)
<=> ( ! [C] :
( in(C,A)
=> apply(B,C) = C )
& relation_dom(B) = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( ( in(A,relation_dom(B))
& one_to_one(B) )
=> ( A = apply(relation_composition(B,function_inverse(B)),A)
& A = apply(function_inverse(B),apply(B,A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( ( in(A,relation_rng(B))
& one_to_one(B) )
=> ( A = apply(relation_composition(function_inverse(B),B),A)
& A = apply(B,apply(function_inverse(B),A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_rng(relation_composition(A,function_inverse(A))) = relation_dom(A)
& relation_dom(relation_composition(A,function_inverse(A))) = relation_dom(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_rng(relation_composition(function_inverse(A),A)) = relation_rng(A)
& relation_dom(relation_composition(function_inverse(A),A)) = relation_rng(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_composition(function_inverse(A),A) = identity_relation(relation_rng(A))
& relation_composition(A,function_inverse(A)) = identity_relation(relation_dom(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_composition(function_inverse(A),A) = identity_relation(relation_rng(A))
& relation_composition(A,function_inverse(A)) = identity_relation(relation_dom(A)) ) ) ),
inference(negated_conjecture,[status(cth)],[f42]) ).
fof(f44,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f48,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f50,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f52,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f53,plain,
! [A] :
( ( one_to_one(A)
& function(A)
& relation(A) )
| ~ function(A)
| ~ empty(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f56,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f57,plain,
! [A] :
( ( function(function_inverse(A))
& relation(function_inverse(A)) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f58,plain,
! [X0] :
( relation(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0] :
( function(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f60,plain,
! [A,B] :
( relation(relation_composition(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f61,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f63,plain,
! [A] : element(sK0_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f8]) ).
fof(f64,plain,
! [X0] : element(sK0_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [A,B] :
( ( relation(relation_composition(B,A))
& empty(relation_composition(B,A)) )
| ~ relation(B)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f66,plain,
! [X0,X1] :
( empty(relation_composition(X1,X0))
| ~ relation(X1)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f68,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f71,plain,
! [A,B] :
( ( function(relation_composition(A,B))
& relation(relation_composition(A,B)) )
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f73,plain,
! [X0,X1] :
( function(relation_composition(X0,X1))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f76,plain,
( ! [A] : function(identity_relation(A))
& ! [A] : relation(identity_relation(A)) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f78,plain,
! [X0] : function(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f81,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f82,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [A] :
( ~ empty(relation_rng(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f84,plain,
! [X0] :
( ~ empty(relation_rng(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
! [A] :
( ( relation(relation_dom(A))
& empty(relation_dom(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f86,plain,
! [X0] :
( empty(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
! [X0] :
( relation(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f88,plain,
! [A] :
( ( relation(relation_rng(A))
& empty(relation_rng(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f89,plain,
! [X0] :
( empty(relation_rng(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [X0] :
( relation(relation_rng(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f91,plain,
! [A,B] :
( ( relation(relation_composition(A,B))
& empty(relation_composition(A,B)) )
| ~ relation(B)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f92,plain,
! [X0,X1] :
( empty(relation_composition(X0,X1))
| ~ relation(X1)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f94,plain,
( function(sK1_skl)
& relation(sK1_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f21]) ).
fof(f95,plain,
relation(sK1_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f97,plain,
( relation(sK2_skl)
& empty(sK2_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f22]) ).
fof(f98,plain,
empty(sK2_skl),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f99,plain,
relation(sK2_skl),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f106,plain,
( function(sK5_skl)
& empty(sK5_skl)
& relation(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f25]) ).
fof(f108,plain,
empty(sK5_skl),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f109,plain,
function(sK5_skl),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f113,plain,
! [A] :
( empty(sK7_skl(A))
& element(sK7_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f27]) ).
fof(f114,plain,
! [X0] : element(sK7_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0] : empty(sK7_skl(X0)),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f118,plain,
( one_to_one(sK9_skl)
& function(sK9_skl)
& relation(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f29]) ).
fof(f119,plain,
relation(sK9_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
function(sK9_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f121,plain,
one_to_one(sK9_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f127,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f128,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f130,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f131,plain,
! [A,B] :
( ( B = identity_relation(A)
<=> ( ! [C] :
( apply(B,C) = C
| ~ in(C,A) )
& relation_dom(B) = A ) )
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f132,plain,
! [A,B] :
( ( ( ? [C] :
( apply(B,C) != C
& in(C,A) )
| relation_dom(B) != A
| B = identity_relation(A) )
& ( ( ! [C] :
( apply(B,C) = C
| ~ in(C,A) )
& relation_dom(B) = A )
| B != identity_relation(A) ) )
| ~ function(B)
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [B] :
( ( ! [A] :
( ? [C] :
( apply(B,C) != C
& in(C,A) )
| relation_dom(B) != A
| B = identity_relation(A) )
& ! [A] :
( ( ! [C] :
( apply(B,C) = C
| ~ in(C,A) )
& relation_dom(B) = A )
| B != identity_relation(A) ) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f132]) ).
fof(f134,plain,
! [B] :
( ( ! [A] :
( ( apply(B,sK11_skl(A,B)) != sK11_skl(A,B)
& in(sK11_skl(A,B),A) )
| relation_dom(B) != A
| B = identity_relation(A) )
& ! [A] :
( ( ! [C] :
( apply(B,C) = C
| ~ in(C,A) )
& relation_dom(B) = A )
| B != identity_relation(A) ) )
| ~ function(B)
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(C,sK11_skl(A,B))],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( relation_dom(X0) = X1
| X0 != identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
! [X0,X1,X2] :
( apply(X0,X2) = X2
| ~ in(X2,X1)
| X0 != identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
! [X0,X1] :
( in(sK11_skl(X1,X0),X1)
| relation_dom(X0) != X1
| X0 = identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f138,plain,
! [X0,X1] :
( apply(X0,sK11_skl(X1,X0)) != sK11_skl(X1,X0)
| relation_dom(X0) != X1
| X0 = identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f146,plain,
! [A,B] :
( ( A = apply(relation_composition(B,function_inverse(B)),A)
& A = apply(function_inverse(B),apply(B,A)) )
| ~ in(A,relation_dom(B))
| ~ one_to_one(B)
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f147,plain,
! [B] :
( ! [A] :
( ( A = apply(relation_composition(B,function_inverse(B)),A)
& A = apply(function_inverse(B),apply(B,A)) )
| ~ in(A,relation_dom(B))
| ~ one_to_one(B) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0,X1] :
( X1 = apply(function_inverse(X0),apply(X0,X1))
| ~ in(X1,relation_dom(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [X0,X1] :
( X1 = apply(relation_composition(X0,function_inverse(X0)),X1)
| ~ in(X1,relation_dom(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f150,plain,
! [A,B] :
( ( A = apply(relation_composition(function_inverse(B),B),A)
& A = apply(B,apply(function_inverse(B),A)) )
| ~ in(A,relation_rng(B))
| ~ one_to_one(B)
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f151,plain,
! [B] :
( ! [A] :
( ( A = apply(relation_composition(function_inverse(B),B),A)
& A = apply(B,apply(function_inverse(B),A)) )
| ~ in(A,relation_rng(B))
| ~ one_to_one(B) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f152,plain,
! [X0,X1] :
( X1 = apply(X0,apply(function_inverse(X0),X1))
| ~ in(X1,relation_rng(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [X0,X1] :
( X1 = apply(relation_composition(function_inverse(X0),X0),X1)
| ~ in(X1,relation_rng(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f154,plain,
! [A] :
( ( relation_rng(relation_composition(A,function_inverse(A))) = relation_dom(A)
& relation_dom(relation_composition(A,function_inverse(A))) = relation_dom(A) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f155,plain,
! [X0] :
( relation_dom(relation_composition(X0,function_inverse(X0))) = relation_dom(X0)
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [X0] :
( relation_rng(relation_composition(X0,function_inverse(X0))) = relation_dom(X0)
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f157,plain,
! [A] :
( ( relation_rng(relation_composition(function_inverse(A),A)) = relation_rng(A)
& relation_dom(relation_composition(function_inverse(A),A)) = relation_rng(A) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f158,plain,
! [X0] :
( relation_dom(relation_composition(function_inverse(X0),X0)) = relation_rng(X0)
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,plain,
! [X0] :
( relation_rng(relation_composition(function_inverse(X0),X0)) = relation_rng(X0)
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f160,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f161,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f160]) ).
fof(f162,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f163,plain,
? [A] :
( ( relation_composition(function_inverse(A),A) != identity_relation(relation_rng(A))
| relation_composition(A,function_inverse(A)) != identity_relation(relation_dom(A)) )
& one_to_one(A)
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f164,plain,
( ( relation_composition(function_inverse(sK12_skl),sK12_skl) != identity_relation(relation_rng(sK12_skl))
| relation_composition(sK12_skl,function_inverse(sK12_skl)) != identity_relation(relation_dom(sK12_skl)) )
& one_to_one(sK12_skl)
& function(sK12_skl)
& relation(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f163]) ).
fof(f165,plain,
relation(sK12_skl),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f166,plain,
function(sK12_skl),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f167,plain,
one_to_one(sK12_skl),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f168,plain,
( relation_composition(function_inverse(sK12_skl),sK12_skl) != identity_relation(relation_rng(sK12_skl))
| relation_composition(sK12_skl,function_inverse(sK12_skl)) != identity_relation(relation_dom(sK12_skl)) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f169,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f170,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f171,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f172,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f171]) ).
fof(f173,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f175,plain,
! [B] :
( ~ empty(B)
| ! [A] :
( A = B
| ~ empty(A) ) ),
inference(miniscoping,[status(thm)],[f174]) ).
fof(f176,plain,
! [X0,X1] :
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f177,definition,
( sQ0_spl
<=> relation_composition(sK12_skl,function_inverse(sK12_skl)) = identity_relation(relation_dom(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( sQ0_spl
| relation_composition(sK12_skl,function_inverse(sK12_skl)) != identity_relation(relation_dom(sK12_skl)) ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f180,definition,
( sQ1_spl
<=> relation_composition(function_inverse(sK12_skl),sK12_skl) = identity_relation(relation_rng(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f182,plain,
( sQ1_spl
| relation_composition(function_inverse(sK12_skl),sK12_skl) != identity_relation(relation_rng(sK12_skl)) ),
inference(component_clause,[status(thm)],[f180]) ).
fof(f183,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f168,f177,f180]) ).
fof(f184,plain,
! [X0] :
( relation_dom(identity_relation(X0)) = X0
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f135]) ).
fof(f185,plain,
! [X0,X1] :
( apply(identity_relation(X0),X1) = X1
| ~ in(X1,X0)
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f136]) ).
fof(f186,plain,
! [X0] :
( in(sK11_skl(relation_dom(X0),X0),relation_dom(X0))
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f137]) ).
fof(f187,plain,
! [X0] :
( apply(X0,sK11_skl(relation_dom(X0),X0)) != sK11_skl(relation_dom(X0),X0)
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f138]) ).
fof(f188,plain,
! [X0] :
( one_to_one(X0)
| ~ empty(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f56,f50]) ).
fof(f189,plain,
! [X0] :
( one_to_one(X0)
| ~ empty(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f188,f52]) ).
fof(f200,plain,
! [X0] :
( relation_dom(identity_relation(X0)) = X0
| ~ function(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f184,f62]) ).
fof(f201,plain,
! [X0] : relation_dom(identity_relation(X0)) = X0,
inference(resolution,[status(thm)],[f200,f78]) ).
fof(f203,plain,
( relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))) = relation_dom(sK12_skl)
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f155,f167]) ).
fof(f205,definition,
( sQ2_spl
<=> relation(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( sQ2_spl
| ~ relation(sK12_skl) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,definition,
( sQ3_spl
<=> function(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f210,plain,
( sQ3_spl
| ~ function(sK12_skl) ),
inference(component_clause,[status(thm)],[f208]) ).
fof(f211,definition,
( sQ4_spl
<=> relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))) = relation_dom(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f212,plain,
( ~ sQ4_spl
| relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))) = relation_dom(sK12_skl) ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f214,plain,
( sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f203,f205,f208,f211]) ).
fof(f217,plain,
! [X0] :
( ~ empty(X0)
| ~ relation(identity_relation(X0))
| empty(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f201,f82]) ).
fof(f219,plain,
! [X0] :
( empty(X0)
| ~ empty(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f201,f86]) ).
fof(f220,plain,
! [X0] :
( ~ empty(X0)
| empty(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f62]) ).
fof(f230,definition,
( sQ6_spl
<=> relation(relation_composition(sK12_skl,function_inverse(sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f232,plain,
( sQ6_spl
| ~ relation(relation_composition(sK12_skl,function_inverse(sK12_skl))) ),
inference(component_clause,[status(thm)],[f230]) ).
fof(f242,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f210,f166]) ).
fof(f243,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f242]) ).
fof(f244,plain,
( relation_rng(relation_composition(sK12_skl,function_inverse(sK12_skl))) = relation_dom(sK12_skl)
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f156,f167]) ).
fof(f246,definition,
( sQ9_spl
<=> relation_rng(relation_composition(sK12_skl,function_inverse(sK12_skl))) = relation_dom(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f249,plain,
( sQ9_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f244,f205,f208,f246]) ).
fof(f251,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f207,f165]) ).
fof(f252,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f251]) ).
fof(f253,plain,
( relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)) = relation_rng(sK12_skl)
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f158,f167]) ).
fof(f255,definition,
( sQ10_spl
<=> relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)) = relation_rng(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( ~ sQ10_spl
| relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)) = relation_rng(sK12_skl) ),
inference(component_clause,[status(thm)],[f255]) ).
fof(f258,plain,
( sQ10_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f253,f205,f208,f255]) ).
fof(f260,plain,
( relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)) = relation_rng(sK9_skl)
| ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f121,f158]) ).
fof(f261,plain,
( relation_rng(relation_composition(sK9_skl,function_inverse(sK9_skl))) = relation_dom(sK9_skl)
| ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f121,f156]) ).
fof(f262,plain,
( relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))) = relation_dom(sK9_skl)
| ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f121,f155]) ).
fof(f263,definition,
( sQ11_spl
<=> relation(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f265,plain,
( sQ11_spl
| ~ relation(sK9_skl) ),
inference(component_clause,[status(thm)],[f263]) ).
fof(f266,definition,
( sQ12_spl
<=> function(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f268,plain,
( sQ12_spl
| ~ function(sK9_skl) ),
inference(component_clause,[status(thm)],[f266]) ).
fof(f269,definition,
( sQ13_spl
<=> relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)) = relation_rng(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f270,plain,
( ~ sQ13_spl
| relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)) = relation_rng(sK9_skl) ),
inference(component_clause,[status(thm)],[f269]) ).
fof(f272,plain,
( sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f260,f263,f266,f269]) ).
fof(f273,definition,
( sQ14_spl
<=> relation_rng(relation_composition(sK9_skl,function_inverse(sK9_skl))) = relation_dom(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( ~ sQ14_spl
| relation_rng(relation_composition(sK9_skl,function_inverse(sK9_skl))) = relation_dom(sK9_skl) ),
inference(component_clause,[status(thm)],[f273]) ).
fof(f276,plain,
( sQ14_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f261,f263,f266,f273]) ).
fof(f277,definition,
( sQ15_spl
<=> relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))) = relation_dom(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( ~ sQ15_spl
| relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))) = relation_dom(sK9_skl) ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f280,plain,
( sQ15_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f262,f263,f266,f277]) ).
fof(f281,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f268,f120]) ).
fof(f282,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f281]) ).
fof(f283,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f265,f119]) ).
fof(f284,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f283]) ).
fof(f288,plain,
( sQ6_spl
| ~ relation(function_inverse(sK12_skl))
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f232,f61]) ).
fof(f292,definition,
( sQ17_spl
<=> relation(function_inverse(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( ~ sQ17_spl
| relation(function_inverse(sK12_skl)) ),
inference(component_clause,[status(thm)],[f292]) ).
fof(f294,plain,
( sQ17_spl
| ~ relation(function_inverse(sK12_skl)) ),
inference(component_clause,[status(thm)],[f292]) ).
fof(f300,plain,
( sQ6_spl
| ~ sQ17_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f288,f205,f292,f230]) ).
fof(f301,plain,
( sQ17_spl
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f294,f58]) ).
fof(f302,plain,
( sQ17_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f301,f205,f208,f292]) ).
fof(f320,plain,
( relation_rng(relation_composition(function_inverse(sK9_skl),sK9_skl)) = relation_rng(sK9_skl)
| ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f159,f121]) ).
fof(f321,plain,
( relation_rng(relation_composition(function_inverse(sK12_skl),sK12_skl)) = relation_rng(sK12_skl)
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f159,f167]) ).
fof(f323,definition,
( sQ19_spl
<=> relation_rng(relation_composition(function_inverse(sK9_skl),sK9_skl)) = relation_rng(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f324,plain,
( ~ sQ19_spl
| relation_rng(relation_composition(function_inverse(sK9_skl),sK9_skl)) = relation_rng(sK9_skl) ),
inference(component_clause,[status(thm)],[f323]) ).
fof(f326,plain,
( sQ19_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f320,f263,f266,f323]) ).
fof(f327,definition,
( sQ20_spl
<=> relation_rng(relation_composition(function_inverse(sK12_skl),sK12_skl)) = relation_rng(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( sQ20_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f321,f205,f208,f327]) ).
fof(f351,plain,
sK5_skl = empty_set,
inference(resolution,[status(thm)],[f170,f108]) ).
fof(f354,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ empty(X0)
| relation_composition(X0,X1) = empty_set ),
inference(resolution,[status(thm)],[f170,f92]) ).
fof(f355,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ empty(X1)
| relation_composition(X0,X1) = empty_set ),
inference(resolution,[status(thm)],[f170,f66]) ).
fof(f356,plain,
! [X0] :
( ~ empty(X0)
| relation_rng(X0) = empty_set ),
inference(resolution,[status(thm)],[f170,f89]) ).
fof(f357,plain,
sK2_skl = empty_set,
inference(resolution,[status(thm)],[f170,f98]) ).
fof(f360,plain,
! [X0] :
( ~ empty(X0)
| relation_dom(X0) = empty_set ),
inference(resolution,[status(thm)],[f170,f86]) ).
fof(f399,plain,
! [X0] :
( in(sK0_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f130,f64]) ).
fof(f402,plain,
! [X0,X1] :
( apply(identity_relation(X0),X1) = X1
| ~ in(X1,X0)
| ~ function(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f185,f62]) ).
fof(f469,plain,
! [X0] :
( ~ in(X0,sK0_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f399,f48]) ).
fof(f475,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f186,f173]) ).
fof(f476,plain,
! [X0] :
( apply(identity_relation(relation_dom(X0)),sK11_skl(relation_dom(X0),X0)) = sK11_skl(relation_dom(X0),X0)
| ~ function(identity_relation(relation_dom(X0)))
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f186,f402]) ).
fof(f477,plain,
! [X0] :
( ~ in(relation_dom(X0),sK11_skl(relation_dom(X0),X0))
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f186,f48]) ).
fof(f482,plain,
! [X0] :
( apply(identity_relation(relation_dom(X0)),sK11_skl(relation_dom(X0),X0)) = sK11_skl(relation_dom(X0),X0)
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f78]) ).
fof(f503,plain,
! [X0] :
( ~ empty(X0)
| relation_dom(identity_relation(X0)) = empty_set ),
inference(resolution,[status(thm)],[f360,f220]) ).
fof(f508,plain,
! [X0] :
( ~ empty(X0)
| X0 = empty_set ),
inference(forward_demodulation,[status(thm)],[f201,f503]) ).
fof(f530,plain,
( ~ sQ10_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))
| relation_composition(function_inverse(sK12_skl),sK12_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)))
| ~ function(relation_composition(function_inverse(sK12_skl),sK12_skl))
| ~ relation(relation_composition(function_inverse(sK12_skl),sK12_skl)) ),
inference(paramodulation,[status(thm)],[f256,f187]) ).
fof(f531,plain,
( ~ sQ10_spl
| in(sK11_skl(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_rng(sK12_skl))
| relation_composition(function_inverse(sK12_skl),sK12_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)))
| ~ function(relation_composition(function_inverse(sK12_skl),sK12_skl))
| ~ relation(relation_composition(function_inverse(sK12_skl),sK12_skl)) ),
inference(paramodulation,[status(thm)],[f256,f186]) ).
fof(f536,definition,
( sQ24_spl
<=> relation(relation_composition(function_inverse(sK12_skl),sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f538,plain,
( sQ24_spl
| ~ relation(relation_composition(function_inverse(sK12_skl),sK12_skl)) ),
inference(component_clause,[status(thm)],[f536]) ).
fof(f539,definition,
( sQ25_spl
<=> function(relation_composition(function_inverse(sK12_skl),sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f541,plain,
( sQ25_spl
| ~ function(relation_composition(function_inverse(sK12_skl),sK12_skl)) ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f542,definition,
( sQ26_spl
<=> relation_composition(function_inverse(sK12_skl),sK12_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( ~ sQ26_spl
| relation_composition(function_inverse(sK12_skl),sK12_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl))) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f545,definition,
( sQ27_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)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f547,plain,
( sQ27_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)) ),
inference(component_clause,[status(thm)],[f545]) ).
fof(f548,plain,
( ~ sQ10_spl
| ~ sQ27_spl
| sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f530,f536,f539,f542,f545,f255]) ).
fof(f549,definition,
( sQ28_spl
<=> in(sK11_skl(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_rng(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f550,plain,
( ~ sQ28_spl
| in(sK11_skl(relation_dom(relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_rng(sK12_skl)) ),
inference(component_clause,[status(thm)],[f549]) ).
fof(f552,plain,
( ~ sQ10_spl
| sQ28_spl
| sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f531,f536,f539,f542,f549,f255]) ).
fof(f571,plain,
relation_rng(sK2_skl) = empty_set,
inference(resolution,[status(thm)],[f98,f356]) ).
fof(f573,plain,
relation_dom(sK2_skl) = empty_set,
inference(resolution,[status(thm)],[f98,f360]) ).
fof(f580,plain,
! [X0] :
( ~ empty(X0)
| X0 = sK2_skl ),
inference(backward_demodulation,[status(thm)],[f357,f508]) ).
fof(f597,plain,
! [X0] :
( X0 = apply(function_inverse(sK9_skl),apply(sK9_skl,X0))
| ~ in(X0,relation_dom(sK9_skl))
| ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f148,f121]) ).
fof(f598,plain,
! [X0] :
( X0 = apply(function_inverse(sK12_skl),apply(sK12_skl,X0))
| ~ in(X0,relation_dom(sK12_skl))
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f148,f167]) ).
fof(f600,definition,
! [X0] :
( sQ33_spl
<=> ( X0 = apply(function_inverse(sK9_skl),apply(sK9_skl,X0))
| ~ in(X0,relation_dom(sK9_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f601,plain,
! [X0] :
( ~ sQ33_spl
| X0 = apply(function_inverse(sK9_skl),apply(sK9_skl,X0))
| ~ in(X0,relation_dom(sK9_skl)) ),
inference(component_clause,[status(thm)],[f600]) ).
fof(f603,plain,
( sQ33_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f597,f263,f266,f600]) ).
fof(f604,definition,
! [X0] :
( sQ34_spl
<=> ( X0 = apply(function_inverse(sK12_skl),apply(sK12_skl,X0))
| ~ in(X0,relation_dom(sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f607,plain,
( sQ34_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f598,f205,f208,f604]) ).
fof(f609,plain,
! [X0] :
( X0 = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),X0)
| ~ in(X0,relation_dom(sK9_skl))
| ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f149,f121]) ).
fof(f610,plain,
! [X0] :
( X0 = apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),X0)
| ~ in(X0,relation_dom(sK12_skl))
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f149,f167]) ).
fof(f612,definition,
! [X0] :
( sQ35_spl
<=> ( X0 = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),X0)
| ~ in(X0,relation_dom(sK9_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f613,plain,
! [X0] :
( ~ sQ35_spl
| X0 = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),X0)
| ~ in(X0,relation_dom(sK9_skl)) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( sQ35_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f609,f263,f266,f612]) ).
fof(f616,definition,
! [X0] :
( sQ36_spl
<=> ( X0 = apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),X0)
| ~ in(X0,relation_dom(sK12_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f617,plain,
! [X0] :
( ~ sQ36_spl
| X0 = apply(relation_composition(sK12_skl,function_inverse(sK12_skl)),X0)
| ~ in(X0,relation_dom(sK12_skl)) ),
inference(component_clause,[status(thm)],[f616]) ).
fof(f619,plain,
( sQ36_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f610,f205,f208,f616]) ).
fof(f623,plain,
( sQ24_spl
| ~ relation(sK12_skl)
| ~ relation(function_inverse(sK12_skl)) ),
inference(resolution,[status(thm)],[f538,f61]) ).
fof(f626,plain,
( sQ24_spl
| ~ sQ2_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f623,f292,f205,f536]) ).
fof(f627,plain,
( ~ sQ26_spl
| ~ sQ10_spl
| relation_composition(function_inverse(sK12_skl),sK12_skl) = identity_relation(relation_rng(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f256,f543]) ).
fof(f672,plain,
! [X0,X1] :
( X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0)
| ~ empty(X1)
| ~ element(relation_dom(X0),powerset(X1)) ),
inference(resolution,[status(thm)],[f162,f186]) ).
fof(f697,definition,
( sQ37_spl
<=> one_to_one(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f699,plain,
( sQ37_spl
| ~ one_to_one(sK12_skl) ),
inference(component_clause,[status(thm)],[f697]) ).
fof(f711,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f699,f167]) ).
fof(f712,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f711]) ).
fof(f734,plain,
( ~ sQ13_spl
| apply(relation_composition(function_inverse(sK9_skl),sK9_skl),sK11_skl(relation_rng(sK9_skl),relation_composition(function_inverse(sK9_skl),sK9_skl))) != sK11_skl(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_composition(function_inverse(sK9_skl),sK9_skl))
| relation_composition(function_inverse(sK9_skl),sK9_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)))
| ~ function(relation_composition(function_inverse(sK9_skl),sK9_skl))
| ~ relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f270,f187]) ).
fof(f735,plain,
( ~ sQ13_spl
| in(sK11_skl(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_rng(sK9_skl))
| relation_composition(function_inverse(sK9_skl),sK9_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)))
| ~ function(relation_composition(function_inverse(sK9_skl),sK9_skl))
| ~ relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f270,f186]) ).
fof(f736,plain,
( ~ sQ13_spl
| in(sK11_skl(relation_rng(sK9_skl),relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)))
| relation_composition(function_inverse(sK9_skl),sK9_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)))
| ~ function(relation_composition(function_inverse(sK9_skl),sK9_skl))
| ~ relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f270,f186]) ).
fof(f737,plain,
( ~ sQ13_spl
| ~ empty(relation_rng(sK9_skl))
| ~ relation(relation_composition(function_inverse(sK9_skl),sK9_skl))
| empty(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f270,f82]) ).
fof(f738,plain,
( ~ sQ13_spl
| relation(relation_rng(sK9_skl))
| ~ empty(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f270,f87]) ).
fof(f739,plain,
( ~ sQ13_spl
| empty(relation_rng(sK9_skl))
| ~ empty(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f270,f86]) ).
fof(f740,definition,
( sQ41_spl
<=> relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f741,plain,
( ~ sQ41_spl
| relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(component_clause,[status(thm)],[f740]) ).
fof(f742,plain,
( sQ41_spl
| ~ relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(component_clause,[status(thm)],[f740]) ).
fof(f743,definition,
( sQ42_spl
<=> function(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f745,plain,
( sQ42_spl
| ~ function(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(component_clause,[status(thm)],[f743]) ).
fof(f746,definition,
( sQ43_spl
<=> relation_composition(function_inverse(sK9_skl),sK9_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f749,definition,
( sQ44_spl
<=> apply(relation_composition(function_inverse(sK9_skl),sK9_skl),sK11_skl(relation_rng(sK9_skl),relation_composition(function_inverse(sK9_skl),sK9_skl))) = sK11_skl(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f752,plain,
( ~ sQ13_spl
| ~ sQ44_spl
| sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f734,f740,f743,f746,f749,f269]) ).
fof(f753,definition,
( sQ45_spl
<=> in(sK11_skl(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_rng(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f756,plain,
( ~ sQ13_spl
| sQ45_spl
| sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f735,f740,f743,f746,f753,f269]) ).
fof(f757,definition,
( sQ46_spl
<=> in(sK11_skl(relation_rng(sK9_skl),relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f760,plain,
( ~ sQ13_spl
| sQ46_spl
| sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f736,f740,f743,f746,f757,f269]) ).
fof(f761,definition,
( sQ47_spl
<=> empty(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f764,definition,
( sQ48_spl
<=> empty(relation_rng(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f765,plain,
( ~ sQ48_spl
| empty(relation_rng(sK9_skl)) ),
inference(component_clause,[status(thm)],[f764]) ).
fof(f767,plain,
( ~ sQ13_spl
| ~ sQ48_spl
| ~ sQ41_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f737,f761,f740,f764,f269]) ).
fof(f768,definition,
( sQ49_spl
<=> relation(relation_rng(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f771,plain,
( ~ sQ13_spl
| sQ49_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f738,f761,f768,f269]) ).
fof(f772,plain,
( ~ sQ13_spl
| sQ48_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f739,f761,f764,f269]) ).
fof(f774,plain,
! [X0] :
( ~ sQ14_spl
| X0 = apply(relation_composition(function_inverse(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl))),X0)
| ~ in(X0,relation_dom(sK9_skl))
| ~ one_to_one(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| ~ function(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f274,f153]) ).
fof(f775,plain,
! [X0] :
( ~ sQ14_spl
| X0 = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),apply(function_inverse(relation_composition(sK9_skl,function_inverse(sK9_skl))),X0))
| ~ in(X0,relation_dom(sK9_skl))
| ~ one_to_one(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| ~ function(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f274,f152]) ).
fof(f776,plain,
( ~ sQ14_spl
| ~ empty(relation_dom(sK9_skl))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| empty(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f274,f84]) ).
fof(f777,plain,
( ~ sQ14_spl
| relation(relation_dom(sK9_skl))
| ~ empty(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f274,f90]) ).
fof(f778,plain,
( ~ sQ14_spl
| empty(relation_dom(sK9_skl))
| ~ empty(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f274,f89]) ).
fof(f779,definition,
( sQ50_spl
<=> relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f781,plain,
( sQ50_spl
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(component_clause,[status(thm)],[f779]) ).
fof(f782,definition,
( sQ51_spl
<=> function(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f783,plain,
( ~ sQ51_spl
| function(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(component_clause,[status(thm)],[f782]) ).
fof(f784,plain,
( sQ51_spl
| ~ function(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(component_clause,[status(thm)],[f782]) ).
fof(f785,definition,
( sQ52_spl
<=> one_to_one(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f788,definition,
! [X0] :
( sQ53_spl
<=> ( X0 = apply(relation_composition(function_inverse(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl))),X0)
| ~ in(X0,relation_dom(sK9_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f791,plain,
( ~ sQ14_spl
| sQ53_spl
| ~ sQ52_spl
| ~ sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f774,f779,f782,f785,f788,f273]) ).
fof(f792,definition,
! [X0] :
( sQ54_spl
<=> ( X0 = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),apply(function_inverse(relation_composition(sK9_skl,function_inverse(sK9_skl))),X0))
| ~ in(X0,relation_dom(sK9_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f795,plain,
( ~ sQ14_spl
| sQ54_spl
| ~ sQ52_spl
| ~ sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f775,f779,f782,f785,f792,f273]) ).
fof(f796,definition,
( sQ55_spl
<=> empty(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f799,definition,
( sQ56_spl
<=> empty(relation_dom(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f802,plain,
( ~ sQ14_spl
| ~ sQ56_spl
| ~ sQ50_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f776,f796,f779,f799,f273]) ).
fof(f803,definition,
( sQ57_spl
<=> relation(relation_dom(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f806,plain,
( ~ sQ14_spl
| sQ57_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f777,f796,f803,f273]) ).
fof(f807,plain,
( ~ sQ14_spl
| sQ56_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f778,f796,f799,f273]) ).
fof(f814,plain,
( ~ sQ15_spl
| apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),sK11_skl(relation_dom(sK9_skl),relation_composition(sK9_skl,function_inverse(sK9_skl)))) != sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl)))
| relation_composition(sK9_skl,function_inverse(sK9_skl)) = identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))))
| ~ function(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f278,f187]) ).
fof(f815,plain,
( ~ sQ15_spl
| in(sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_dom(sK9_skl))
| relation_composition(sK9_skl,function_inverse(sK9_skl)) = identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))))
| ~ function(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f278,f186]) ).
fof(f816,plain,
( ~ sQ15_spl
| in(sK11_skl(relation_dom(sK9_skl),relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))))
| relation_composition(sK9_skl,function_inverse(sK9_skl)) = identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))))
| ~ function(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f278,f186]) ).
fof(f820,definition,
( sQ58_spl
<=> relation_composition(sK9_skl,function_inverse(sK9_skl)) = identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f823,definition,
( sQ59_spl
<=> apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),sK11_skl(relation_dom(sK9_skl),relation_composition(sK9_skl,function_inverse(sK9_skl)))) = sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f826,plain,
( ~ sQ15_spl
| ~ sQ59_spl
| sQ58_spl
| ~ sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f814,f779,f782,f820,f823,f277]) ).
fof(f827,definition,
( sQ60_spl
<=> in(sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_dom(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f830,plain,
( ~ sQ15_spl
| sQ60_spl
| sQ58_spl
| ~ sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f815,f779,f782,f820,f827,f277]) ).
fof(f831,definition,
( sQ61_spl
<=> in(sK11_skl(relation_dom(sK9_skl),relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f834,plain,
( ~ sQ15_spl
| sQ61_spl
| sQ58_spl
| ~ sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f816,f779,f782,f820,f831,f277]) ).
fof(f878,plain,
( relation(empty_set)
| ~ empty(sK2_skl) ),
inference(paramodulation,[status(thm)],[f573,f87]) ).
fof(f879,plain,
( empty(empty_set)
| ~ empty(sK2_skl) ),
inference(paramodulation,[status(thm)],[f573,f86]) ).
fof(f880,definition,
( sQ65_spl
<=> relation(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f882,plain,
( sQ65_spl
| ~ relation(sK2_skl) ),
inference(component_clause,[status(thm)],[f880]) ).
fof(f883,definition,
( sQ66_spl
<=> function(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f885,plain,
( sQ66_spl
| ~ function(sK2_skl) ),
inference(component_clause,[status(thm)],[f883]) ).
fof(f901,definition,
( sQ71_spl
<=> empty(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f902,plain,
( ~ sQ71_spl
| empty(sK2_skl) ),
inference(component_clause,[status(thm)],[f901]) ).
fof(f903,plain,
( sQ71_spl
| ~ empty(sK2_skl) ),
inference(component_clause,[status(thm)],[f901]) ).
fof(f904,definition,
( sQ72_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f908,definition,
( sQ73_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f911,plain,
( sQ73_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f878,f901,f908]) ).
fof(f912,plain,
( sQ72_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f879,f901,f904]) ).
fof(f913,plain,
! [X0] :
( ~ sQ19_spl
| X0 = apply(relation_composition(function_inverse(relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_composition(function_inverse(sK9_skl),sK9_skl)),X0)
| ~ in(X0,relation_rng(sK9_skl))
| ~ one_to_one(relation_composition(function_inverse(sK9_skl),sK9_skl))
| ~ function(relation_composition(function_inverse(sK9_skl),sK9_skl))
| ~ relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f324,f153]) ).
fof(f914,plain,
! [X0] :
( ~ sQ19_spl
| X0 = apply(relation_composition(function_inverse(sK9_skl),sK9_skl),apply(function_inverse(relation_composition(function_inverse(sK9_skl),sK9_skl)),X0))
| ~ in(X0,relation_rng(sK9_skl))
| ~ one_to_one(relation_composition(function_inverse(sK9_skl),sK9_skl))
| ~ function(relation_composition(function_inverse(sK9_skl),sK9_skl))
| ~ relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f324,f152]) ).
fof(f918,definition,
( sQ74_spl
<=> one_to_one(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f921,definition,
! [X0] :
( sQ75_spl
<=> ( X0 = apply(relation_composition(function_inverse(relation_composition(function_inverse(sK9_skl),sK9_skl)),relation_composition(function_inverse(sK9_skl),sK9_skl)),X0)
| ~ in(X0,relation_rng(sK9_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f924,plain,
( ~ sQ19_spl
| sQ75_spl
| ~ sQ74_spl
| ~ sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f913,f740,f743,f918,f921,f323]) ).
fof(f925,definition,
! [X0] :
( sQ76_spl
<=> ( X0 = apply(relation_composition(function_inverse(sK9_skl),sK9_skl),apply(function_inverse(relation_composition(function_inverse(sK9_skl),sK9_skl)),X0))
| ~ in(X0,relation_rng(sK9_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f928,plain,
( ~ sQ19_spl
| sQ76_spl
| ~ sQ74_spl
| ~ sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f914,f740,f743,f918,f925,f323]) ).
fof(f932,plain,
empty_set = sK2_skl,
inference(resolution,[status(thm)],[f68,f580]) ).
fof(f942,plain,
relation_dom(sK2_skl) = sK5_skl,
inference(backward_demodulation,[status(thm)],[f351,f573]) ).
fof(f943,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f98,f903]) ).
fof(f944,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f943]) ).
fof(f947,plain,
( sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f99,f882]) ).
fof(f948,plain,
sQ65_spl,
inference(contradiction_clause,[status(thm)],[f947]) ).
fof(f952,plain,
! [X0] :
( X0 = sK5_skl
| ~ empty(X0) ),
inference(forward_demodulation,[status(thm)],[f351,f170]) ).
fof(f959,plain,
! [X0] : sK7_skl(X0) = sK2_skl,
inference(resolution,[status(thm)],[f115,f580]) ).
fof(f980,plain,
sK5_skl = sK2_skl,
inference(forward_demodulation,[status(thm)],[f351,f932]) ).
fof(f981,plain,
( ~ sQ71_spl
| empty(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f980,f902]) ).
fof(f991,plain,
! [X0] : element(sK5_skl,powerset(X0)),
inference(backward_demodulation,[status(thm)],[f992,f114]) ).
fof(f992,plain,
! [X0] : sK7_skl(X0) = sK5_skl,
inference(forward_demodulation,[status(thm)],[f980,f959]) ).
fof(f996,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ empty(X0)
| relation_composition(X0,X1) = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f351,f354]) ).
fof(f997,plain,
! [X0] :
( ~ sQ71_spl
| ~ relation(X0)
| relation_composition(sK5_skl,X0) = sK5_skl ),
inference(resolution,[status(thm)],[f996,f981]) ).
fof(f1008,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ empty(X1)
| relation_composition(X0,X1) = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f351,f355]) ).
fof(f1009,plain,
! [X0] :
( ~ sQ71_spl
| ~ relation(X0)
| relation_composition(X0,sK5_skl) = sK5_skl ),
inference(resolution,[status(thm)],[f1008,f981]) ).
fof(f1026,plain,
( sQ25_spl
| ~ function(sK12_skl)
| ~ relation(sK12_skl)
| ~ function(function_inverse(sK12_skl))
| ~ relation(function_inverse(sK12_skl)) ),
inference(resolution,[status(thm)],[f541,f73]) ).
fof(f1028,definition,
( sQ77_spl
<=> function(function_inverse(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1030,plain,
( sQ77_spl
| ~ function(function_inverse(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1028]) ).
fof(f1031,plain,
( sQ25_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ77_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1026,f292,f1028,f205,f208,f539]) ).
fof(f1032,plain,
( ~ sQ4_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)))
| relation_composition(sK12_skl,function_inverse(sK12_skl)) = identity_relation(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))))
| ~ function(relation_composition(sK12_skl,function_inverse(sK12_skl)))
| ~ relation(relation_composition(sK12_skl,function_inverse(sK12_skl))) ),
inference(paramodulation,[status(thm)],[f212,f187]) ).
fof(f1033,plain,
( ~ sQ4_spl
| in(sK11_skl(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_dom(sK12_skl))
| relation_composition(sK12_skl,function_inverse(sK12_skl)) = identity_relation(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))))
| ~ function(relation_composition(sK12_skl,function_inverse(sK12_skl)))
| ~ relation(relation_composition(sK12_skl,function_inverse(sK12_skl))) ),
inference(paramodulation,[status(thm)],[f212,f186]) ).
fof(f1038,definition,
( sQ78_spl
<=> function(relation_composition(sK12_skl,function_inverse(sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1040,plain,
( sQ78_spl
| ~ function(relation_composition(sK12_skl,function_inverse(sK12_skl))) ),
inference(component_clause,[status(thm)],[f1038]) ).
fof(f1041,definition,
( sQ79_spl
<=> relation_composition(sK12_skl,function_inverse(sK12_skl)) = identity_relation(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1042,plain,
( ~ sQ79_spl
| relation_composition(sK12_skl,function_inverse(sK12_skl)) = identity_relation(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl)))) ),
inference(component_clause,[status(thm)],[f1041]) ).
fof(f1044,definition,
( sQ80_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))) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1046,plain,
( sQ80_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))) ),
inference(component_clause,[status(thm)],[f1044]) ).
fof(f1047,plain,
( ~ sQ4_spl
| ~ sQ80_spl
| sQ79_spl
| ~ sQ78_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1032,f230,f1038,f1041,f1044,f211]) ).
fof(f1048,definition,
( sQ81_spl
<=> in(sK11_skl(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_dom(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1049,plain,
( ~ sQ81_spl
| in(sK11_skl(relation_dom(relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_dom(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1048]) ).
fof(f1051,plain,
( ~ sQ4_spl
| sQ81_spl
| sQ79_spl
| ~ sQ78_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1033,f230,f1038,f1041,f1048,f211]) ).
fof(f1059,plain,
( ~ sQ79_spl
| ~ sQ4_spl
| relation_composition(sK12_skl,function_inverse(sK12_skl)) = identity_relation(relation_dom(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f212,f1042]) ).
fof(f1060,plain,
( ~ sQ79_spl
| ~ sQ4_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1059,f179]) ).
fof(f1061,plain,
( ~ sQ79_spl
| ~ sQ4_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1060]) ).
fof(f1063,plain,
relation_rng(sK5_skl) = empty_set,
inference(forward_demodulation,[status(thm)],[f980,f571]) ).
fof(f1064,plain,
relation_rng(sK5_skl) = sK5_skl,
inference(forward_demodulation,[status(thm)],[f351,f1063]) ).
fof(f1065,plain,
! [X0] :
( X0 = apply(relation_composition(function_inverse(sK5_skl),sK5_skl),X0)
| ~ in(X0,sK5_skl)
| ~ one_to_one(sK5_skl)
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(paramodulation,[status(thm)],[f1064,f153]) ).
fof(f1066,plain,
! [X0] :
( X0 = apply(sK5_skl,apply(function_inverse(sK5_skl),X0))
| ~ in(X0,sK5_skl)
| ~ one_to_one(sK5_skl)
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(paramodulation,[status(thm)],[f1064,f152]) ).
fof(f1070,definition,
( sQ83_spl
<=> relation(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1073,definition,
( sQ84_spl
<=> function(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1075,plain,
( sQ84_spl
| ~ function(sK5_skl) ),
inference(component_clause,[status(thm)],[f1073]) ).
fof(f1076,definition,
( sQ85_spl
<=> one_to_one(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1077,plain,
( ~ sQ85_spl
| one_to_one(sK5_skl) ),
inference(component_clause,[status(thm)],[f1076]) ).
fof(f1078,plain,
( sQ85_spl
| ~ one_to_one(sK5_skl) ),
inference(component_clause,[status(thm)],[f1076]) ).
fof(f1079,definition,
! [X0] :
( sQ86_spl
<=> ( X0 = apply(relation_composition(function_inverse(sK5_skl),sK5_skl),X0)
| ~ in(X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1082,plain,
( sQ86_spl
| ~ sQ85_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1065,f1070,f1073,f1076,f1079]) ).
fof(f1083,definition,
! [X0] :
( sQ87_spl
<=> ( X0 = apply(sK5_skl,apply(function_inverse(sK5_skl),X0))
| ~ in(X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1086,plain,
( sQ87_spl
| ~ sQ85_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1066,f1070,f1073,f1076,f1083]) ).
fof(f1087,definition,
( sQ88_spl
<=> empty(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1089,plain,
( sQ88_spl
| ~ empty(sK5_skl) ),
inference(component_clause,[status(thm)],[f1087]) ).
fof(f1093,plain,
( sQ66_spl
| ~ function(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f980,f885]) ).
fof(f1094,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1093,f109]) ).
fof(f1095,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f1094]) ).
fof(f1096,plain,
( sQ88_spl
| ~ sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1089,f981]) ).
fof(f1097,plain,
( sQ88_spl
| ~ sQ71_spl ),
inference(contradiction_clause,[status(thm)],[f1096]) ).
fof(f1099,plain,
( sQ85_spl
| ~ empty(sK5_skl) ),
inference(resolution,[status(thm)],[f1078,f189]) ).
fof(f1100,plain,
( sQ85_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f1099,f1087,f1076]) ).
fof(f1101,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1075,f109]) ).
fof(f1102,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f1101]) ).
fof(f1103,plain,
! [X0] :
( ~ sQ85_spl
| X0 = apply(relation_composition(sK5_skl,function_inverse(sK5_skl)),X0)
| ~ in(X0,relation_dom(sK5_skl))
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f1077,f149]) ).
fof(f1104,plain,
! [X0] :
( ~ sQ85_spl
| X0 = apply(function_inverse(sK5_skl),apply(sK5_skl,X0))
| ~ in(X0,relation_dom(sK5_skl))
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f1077,f148]) ).
fof(f1105,plain,
( ~ sQ85_spl
| relation_rng(relation_composition(function_inverse(sK5_skl),sK5_skl)) = relation_rng(sK5_skl)
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f1077,f159]) ).
fof(f1106,plain,
( ~ sQ85_spl
| relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl)) = relation_rng(sK5_skl)
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f1077,f158]) ).
fof(f1107,plain,
( ~ sQ85_spl
| relation_rng(relation_composition(sK5_skl,function_inverse(sK5_skl))) = relation_dom(sK5_skl)
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f1077,f156]) ).
fof(f1108,plain,
( ~ sQ85_spl
| relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl))) = relation_dom(sK5_skl)
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f1077,f155]) ).
fof(f1109,definition,
! [X0] :
( sQ89_spl
<=> ( X0 = apply(relation_composition(sK5_skl,function_inverse(sK5_skl)),X0)
| ~ in(X0,relation_dom(sK5_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1112,plain,
( ~ sQ85_spl
| sQ89_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1103,f1070,f1073,f1109,f1076]) ).
fof(f1113,definition,
! [X0] :
( sQ90_spl
<=> ( X0 = apply(function_inverse(sK5_skl),apply(sK5_skl,X0))
| ~ in(X0,relation_dom(sK5_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1116,plain,
( ~ sQ85_spl
| sQ90_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1104,f1070,f1073,f1113,f1076]) ).
fof(f1117,definition,
( sQ91_spl
<=> relation_rng(relation_composition(function_inverse(sK5_skl),sK5_skl)) = relation_rng(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1120,plain,
( ~ sQ85_spl
| sQ91_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1105,f1070,f1073,f1117,f1076]) ).
fof(f1121,definition,
( sQ92_spl
<=> relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl)) = relation_rng(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1124,plain,
( ~ sQ85_spl
| sQ92_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1106,f1070,f1073,f1121,f1076]) ).
fof(f1125,definition,
( sQ93_spl
<=> relation_rng(relation_composition(sK5_skl,function_inverse(sK5_skl))) = relation_dom(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1128,plain,
( ~ sQ85_spl
| sQ93_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1107,f1070,f1073,f1125,f1076]) ).
fof(f1129,definition,
( sQ94_spl
<=> relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl))) = relation_dom(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1132,plain,
( ~ sQ85_spl
| sQ94_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1108,f1070,f1073,f1129,f1076]) ).
fof(f1146,plain,
relation_dom(sK5_skl) = sK5_skl,
inference(forward_demodulation,[status(thm)],[f980,f942]) ).
fof(f1153,definition,
( sQ95_spl
<=> sK5_skl = identity_relation(relation_dom(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1255,plain,
( apply(identity_relation(relation_dom(sK9_skl)),sK11_skl(relation_dom(sK9_skl),sK9_skl)) = sK11_skl(relation_dom(sK9_skl),sK9_skl)
| sK9_skl = identity_relation(relation_dom(sK9_skl))
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f482,f120]) ).
fof(f1267,definition,
( sQ103_spl
<=> sK9_skl = identity_relation(relation_dom(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1268,plain,
( ~ sQ103_spl
| sK9_skl = identity_relation(relation_dom(sK9_skl)) ),
inference(component_clause,[status(thm)],[f1267]) ).
fof(f1270,definition,
( sQ104_spl
<=> apply(identity_relation(relation_dom(sK9_skl)),sK11_skl(relation_dom(sK9_skl),sK9_skl)) = sK11_skl(relation_dom(sK9_skl),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1273,plain,
( sQ104_spl
| sQ103_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1255,f263,f1267,f1270]) ).
fof(f1280,definition,
( sQ106_spl
<=> relation(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1282,plain,
( sQ106_spl
| ~ relation(sK1_skl) ),
inference(component_clause,[status(thm)],[f1280]) ).
fof(f1316,plain,
( ~ empty(sK5_skl)
| sK5_skl = identity_relation(relation_dom(sK5_skl))
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(paramodulation,[status(thm)],[f1146,f475]) ).
fof(f1318,plain,
( ~ sQ15_spl
| ~ empty(relation_dom(sK9_skl))
| relation_composition(sK9_skl,function_inverse(sK9_skl)) = identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))))
| ~ function(relation_composition(sK9_skl,function_inverse(sK9_skl)))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f278,f475]) ).
fof(f1319,plain,
( ~ sQ13_spl
| ~ empty(relation_rng(sK9_skl))
| relation_composition(function_inverse(sK9_skl),sK9_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)))
| ~ function(relation_composition(function_inverse(sK9_skl),sK9_skl))
| ~ relation(relation_composition(function_inverse(sK9_skl),sK9_skl)) ),
inference(paramodulation,[status(thm)],[f270,f475]) ).
fof(f1322,plain,
( ~ sQ88_spl
| sQ95_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f1316,f1070,f1073,f1153,f1087]) ).
fof(f1324,plain,
( ~ sQ15_spl
| ~ sQ56_spl
| sQ58_spl
| ~ sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1318,f779,f782,f820,f799,f277]) ).
fof(f1325,plain,
( ~ sQ13_spl
| ~ sQ48_spl
| sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f1319,f740,f743,f746,f764,f269]) ).
fof(f1327,plain,
( ~ in(relation_dom(sK9_skl),sK11_skl(relation_dom(sK9_skl),sK9_skl))
| sK9_skl = identity_relation(relation_dom(sK9_skl))
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f477,f120]) ).
fof(f1339,definition,
( sQ111_spl
<=> in(relation_dom(sK9_skl),sK11_skl(relation_dom(sK9_skl),sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1342,plain,
( ~ sQ111_spl
| sQ103_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1327,f263,f1267,f1339]) ).
fof(f1367,plain,
( sQ78_spl
| ~ function(function_inverse(sK12_skl))
| ~ relation(function_inverse(sK12_skl))
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f1040,f73]) ).
fof(f1369,plain,
( sQ78_spl
| ~ sQ77_spl
| ~ sQ17_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1367,f205,f208,f292,f1028,f1038]) ).
fof(f1372,plain,
( sQ77_spl
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f1030,f59]) ).
fof(f1374,plain,
( sQ77_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1372,f205,f208,f1028]) ).
fof(f1404,plain,
( ~ sQ103_spl
| empty(relation_dom(sK9_skl))
| ~ empty(sK9_skl) ),
inference(paramodulation,[status(thm)],[f1268,f219]) ).
fof(f1406,plain,
( ~ sQ103_spl
| ~ empty(relation_dom(sK9_skl))
| empty(sK9_skl) ),
inference(paramodulation,[status(thm)],[f1268,f220]) ).
fof(f1410,definition,
( sQ118_spl
<=> empty(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1411,plain,
( ~ sQ118_spl
| empty(sK9_skl) ),
inference(component_clause,[status(thm)],[f1410]) ).
fof(f1413,plain,
( ~ sQ103_spl
| sQ56_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f1404,f1410,f799,f1267]) ).
fof(f1415,plain,
( ~ sQ103_spl
| ~ sQ56_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1406,f1410,f799,f1267]) ).
fof(f1455,plain,
( sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1282,f95]) ).
fof(f1456,plain,
sQ106_spl,
inference(contradiction_clause,[status(thm)],[f1455]) ).
fof(f1635,plain,
( sQ41_spl
| ~ relation(sK9_skl)
| ~ relation(function_inverse(sK9_skl)) ),
inference(resolution,[status(thm)],[f742,f61]) ).
fof(f1640,definition,
( sQ133_spl
<=> relation(function_inverse(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1642,plain,
( sQ133_spl
| ~ relation(function_inverse(sK9_skl)) ),
inference(component_clause,[status(thm)],[f1640]) ).
fof(f1644,plain,
( sQ41_spl
| ~ sQ11_spl
| ~ sQ133_spl ),
inference(split_clause,[status(thm)],[f1635,f1640,f263,f740]) ).
fof(f1645,plain,
( sQ133_spl
| ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f1642,f58]) ).
fof(f1646,plain,
( sQ133_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1645,f263,f266,f1640]) ).
fof(f1654,plain,
( ~ sQ33_spl
| sK9_skl = identity_relation(relation_dom(sK9_skl))
| ~ function(sK9_skl)
| ~ relation(sK9_skl)
| sK11_skl(relation_dom(sK9_skl),sK9_skl) = apply(function_inverse(sK9_skl),apply(sK9_skl,sK11_skl(relation_dom(sK9_skl),sK9_skl))) ),
inference(resolution,[status(thm)],[f601,f186]) ).
fof(f1655,plain,
( ~ sQ33_spl
| empty(relation_dom(sK9_skl))
| sK0_skl(relation_dom(sK9_skl)) = apply(function_inverse(sK9_skl),apply(sK9_skl,sK0_skl(relation_dom(sK9_skl)))) ),
inference(resolution,[status(thm)],[f601,f399]) ).
fof(f1656,definition,
( sQ134_spl
<=> sK11_skl(relation_dom(sK9_skl),sK9_skl) = apply(function_inverse(sK9_skl),apply(sK9_skl,sK11_skl(relation_dom(sK9_skl),sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1659,plain,
( ~ sQ33_spl
| sQ103_spl
| ~ sQ12_spl
| ~ sQ11_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f1654,f1656,f263,f266,f1267,f600]) ).
fof(f1660,definition,
( sQ135_spl
<=> sK0_skl(relation_dom(sK9_skl)) = apply(function_inverse(sK9_skl),apply(sK9_skl,sK0_skl(relation_dom(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f1663,plain,
( ~ sQ33_spl
| sQ56_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f1655,f1660,f799,f600]) ).
fof(f1717,plain,
( ~ sQ28_spl
| ~ sQ10_spl
| in(sK11_skl(relation_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)),relation_rng(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f256,f550]) ).
fof(f1718,plain,
( sQ27_spl
| ~ sQ10_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_rng(sK12_skl),relation_composition(function_inverse(sK12_skl),sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f256,f547]) ).
fof(f1774,plain,
( ~ sQ48_spl
| ~ relation(sK9_skl)
| empty(sK9_skl) ),
inference(resolution,[status(thm)],[f765,f84]) ).
fof(f1802,plain,
( ~ sQ48_spl
| ~ sQ11_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1774,f1410,f263,f764]) ).
fof(f1823,plain,
( ~ sQ118_spl
| sK9_skl = sK5_skl ),
inference(resolution,[status(thm)],[f1411,f952]) ).
fof(f1836,plain,
( ~ sQ19_spl
| ~ sQ118_spl
| relation_rng(relation_composition(function_inverse(sK9_skl),sK9_skl)) = relation_rng(sK5_skl) ),
inference(backward_demodulation,[status(thm)],[f1823,f324]) ).
fof(f1837,plain,
( ~ sQ15_spl
| ~ sQ118_spl
| relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))) = relation_dom(sK5_skl) ),
inference(backward_demodulation,[status(thm)],[f1823,f278]) ).
fof(f1838,plain,
( ~ sQ14_spl
| ~ sQ118_spl
| relation_rng(relation_composition(sK9_skl,function_inverse(sK9_skl))) = relation_dom(sK5_skl) ),
inference(backward_demodulation,[status(thm)],[f1823,f274]) ).
fof(f1839,plain,
( ~ sQ13_spl
| ~ sQ118_spl
| relation_dom(relation_composition(function_inverse(sK9_skl),sK9_skl)) = relation_rng(sK5_skl) ),
inference(backward_demodulation,[status(thm)],[f1823,f270]) ).
fof(f1849,plain,
( ~ sQ19_spl
| ~ sQ118_spl
| relation_rng(relation_composition(function_inverse(sK5_skl),sK9_skl)) = relation_rng(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1823,f1836]) ).
fof(f1850,plain,
( ~ sQ19_spl
| ~ sQ118_spl
| relation_rng(relation_composition(function_inverse(sK5_skl),sK5_skl)) = relation_rng(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1823,f1849]) ).
fof(f1851,plain,
( ~ sQ19_spl
| ~ sQ118_spl
| relation_rng(relation_composition(function_inverse(sK5_skl),sK5_skl)) = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f1064,f1850]) ).
fof(f1852,plain,
( ~ sQ15_spl
| ~ sQ118_spl
| relation_dom(relation_composition(sK5_skl,function_inverse(sK9_skl))) = relation_dom(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1823,f1837]) ).
fof(f1853,plain,
( ~ sQ15_spl
| ~ sQ118_spl
| relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl))) = relation_dom(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1823,f1852]) ).
fof(f1854,plain,
( ~ sQ15_spl
| ~ sQ118_spl
| relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl))) = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f1146,f1853]) ).
fof(f1855,plain,
( ~ sQ14_spl
| ~ sQ118_spl
| relation_rng(relation_composition(sK5_skl,function_inverse(sK9_skl))) = relation_dom(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1823,f1838]) ).
fof(f1856,plain,
( ~ sQ14_spl
| ~ sQ118_spl
| relation_rng(relation_composition(sK5_skl,function_inverse(sK5_skl))) = relation_dom(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1823,f1855]) ).
fof(f1857,plain,
( ~ sQ14_spl
| ~ sQ118_spl
| relation_rng(relation_composition(sK5_skl,function_inverse(sK5_skl))) = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f1146,f1856]) ).
fof(f1858,plain,
( ~ sQ13_spl
| ~ sQ118_spl
| relation_dom(relation_composition(function_inverse(sK5_skl),sK9_skl)) = relation_rng(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1823,f1839]) ).
fof(f1859,plain,
( ~ sQ13_spl
| ~ sQ118_spl
| relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl)) = relation_rng(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1823,f1858]) ).
fof(f1860,plain,
( ~ sQ13_spl
| ~ sQ118_spl
| relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl)) = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f1064,f1859]) ).
fof(f1885,definition,
! [X0] :
( sQ146_spl
<=> ( ~ empty(X0)
| ~ element(sK5_skl,powerset(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1886,plain,
! [X0] :
( ~ sQ146_spl
| ~ empty(X0)
| ~ element(sK5_skl,powerset(X0)) ),
inference(component_clause,[status(thm)],[f1885]) ).
fof(f1896,plain,
( ~ sQ26_spl
| ~ sQ10_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f627,f182]) ).
fof(f1897,plain,
( ~ sQ26_spl
| ~ sQ10_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1896]) ).
fof(f1916,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ118_spl
| X0 = apply(relation_composition(function_inverse(relation_composition(function_inverse(sK5_skl),sK5_skl)),relation_composition(function_inverse(sK5_skl),sK5_skl)),X0)
| ~ in(X0,sK5_skl)
| ~ one_to_one(relation_composition(function_inverse(sK5_skl),sK5_skl))
| ~ function(relation_composition(function_inverse(sK5_skl),sK5_skl))
| ~ relation(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
inference(paramodulation,[status(thm)],[f1851,f153]) ).
fof(f1917,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ118_spl
| X0 = apply(relation_composition(function_inverse(sK5_skl),sK5_skl),apply(function_inverse(relation_composition(function_inverse(sK5_skl),sK5_skl)),X0))
| ~ in(X0,sK5_skl)
| ~ one_to_one(relation_composition(function_inverse(sK5_skl),sK5_skl))
| ~ function(relation_composition(function_inverse(sK5_skl),sK5_skl))
| ~ relation(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
inference(paramodulation,[status(thm)],[f1851,f152]) ).
fof(f1918,plain,
( ~ sQ19_spl
| ~ sQ118_spl
| ~ empty(sK5_skl)
| ~ relation(relation_composition(function_inverse(sK5_skl),sK5_skl))
| empty(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
inference(paramodulation,[status(thm)],[f1851,f84]) ).
fof(f1921,definition,
( sQ149_spl
<=> relation(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1923,plain,
( sQ149_spl
| ~ relation(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
inference(component_clause,[status(thm)],[f1921]) ).
fof(f1924,definition,
( sQ150_spl
<=> function(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1926,plain,
( sQ150_spl
| ~ function(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
inference(component_clause,[status(thm)],[f1924]) ).
fof(f1927,definition,
( sQ151_spl
<=> one_to_one(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1929,plain,
( sQ151_spl
| ~ one_to_one(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
inference(component_clause,[status(thm)],[f1927]) ).
fof(f1930,definition,
! [X0] :
( sQ152_spl
<=> ( X0 = apply(relation_composition(function_inverse(relation_composition(function_inverse(sK5_skl),sK5_skl)),relation_composition(function_inverse(sK5_skl),sK5_skl)),X0)
| ~ in(X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1933,plain,
( ~ sQ19_spl
| ~ sQ118_spl
| sQ152_spl
| ~ sQ151_spl
| ~ sQ150_spl
| ~ sQ149_spl ),
inference(split_clause,[status(thm)],[f1916,f1921,f1924,f1927,f1930,f1410,f323]) ).
fof(f1934,definition,
! [X0] :
( sQ153_spl
<=> ( X0 = apply(relation_composition(function_inverse(sK5_skl),sK5_skl),apply(function_inverse(relation_composition(function_inverse(sK5_skl),sK5_skl)),X0))
| ~ in(X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1937,plain,
( ~ sQ19_spl
| ~ sQ118_spl
| sQ153_spl
| ~ sQ151_spl
| ~ sQ150_spl
| ~ sQ149_spl ),
inference(split_clause,[status(thm)],[f1917,f1921,f1924,f1927,f1934,f1410,f323]) ).
fof(f1938,definition,
( sQ154_spl
<=> empty(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1941,plain,
( ~ sQ19_spl
| ~ sQ118_spl
| ~ sQ88_spl
| ~ sQ149_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f1918,f1938,f1921,f1087,f1410,f323]) ).
fof(f1962,plain,
! [X0] :
( ~ sQ15_spl
| ~ sQ118_spl
| relation_composition(sK5_skl,function_inverse(sK5_skl)) = identity_relation(relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl))))
| ~ function(relation_composition(sK5_skl,function_inverse(sK5_skl)))
| ~ relation(relation_composition(sK5_skl,function_inverse(sK5_skl)))
| ~ empty(X0)
| ~ element(sK5_skl,powerset(X0)) ),
inference(paramodulation,[status(thm)],[f1854,f672]) ).
fof(f1967,plain,
( ~ sQ15_spl
| ~ sQ118_spl
| ~ empty(sK5_skl)
| ~ relation(relation_composition(sK5_skl,function_inverse(sK5_skl)))
| empty(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
inference(paramodulation,[status(thm)],[f1854,f82]) ).
fof(f1970,definition,
( sQ155_spl
<=> relation(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1972,plain,
( sQ155_spl
| ~ relation(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
inference(component_clause,[status(thm)],[f1970]) ).
fof(f1973,definition,
( sQ156_spl
<=> function(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1975,plain,
( sQ156_spl
| ~ function(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
inference(component_clause,[status(thm)],[f1973]) ).
fof(f1976,definition,
( sQ157_spl
<=> relation_composition(sK5_skl,function_inverse(sK5_skl)) = identity_relation(relation_dom(relation_composition(sK5_skl,function_inverse(sK5_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1979,plain,
( ~ sQ15_spl
| ~ sQ118_spl
| sQ157_spl
| ~ sQ156_spl
| ~ sQ155_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f1962,f1885,f1970,f1973,f1976,f1410,f277]) ).
fof(f1993,definition,
( sQ161_spl
<=> empty(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f1996,plain,
( ~ sQ15_spl
| ~ sQ118_spl
| ~ sQ88_spl
| ~ sQ155_spl
| sQ161_spl ),
inference(split_clause,[status(thm)],[f1967,f1993,f1970,f1087,f1410,f277]) ).
fof(f1999,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ118_spl
| X0 = apply(relation_composition(function_inverse(relation_composition(sK5_skl,function_inverse(sK5_skl))),relation_composition(sK5_skl,function_inverse(sK5_skl))),X0)
| ~ in(X0,sK5_skl)
| ~ one_to_one(relation_composition(sK5_skl,function_inverse(sK5_skl)))
| ~ function(relation_composition(sK5_skl,function_inverse(sK5_skl)))
| ~ relation(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
inference(paramodulation,[status(thm)],[f1857,f153]) ).
fof(f2000,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ118_spl
| X0 = apply(relation_composition(sK5_skl,function_inverse(sK5_skl)),apply(function_inverse(relation_composition(sK5_skl,function_inverse(sK5_skl))),X0))
| ~ in(X0,sK5_skl)
| ~ one_to_one(relation_composition(sK5_skl,function_inverse(sK5_skl)))
| ~ function(relation_composition(sK5_skl,function_inverse(sK5_skl)))
| ~ relation(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
inference(paramodulation,[status(thm)],[f1857,f152]) ).
fof(f2004,definition,
( sQ162_spl
<=> one_to_one(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f2006,plain,
( sQ162_spl
| ~ one_to_one(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
inference(component_clause,[status(thm)],[f2004]) ).
fof(f2007,definition,
! [X0] :
( sQ163_spl
<=> ( X0 = apply(relation_composition(function_inverse(relation_composition(sK5_skl,function_inverse(sK5_skl))),relation_composition(sK5_skl,function_inverse(sK5_skl))),X0)
| ~ in(X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f2010,plain,
( ~ sQ14_spl
| ~ sQ118_spl
| sQ163_spl
| ~ sQ162_spl
| ~ sQ156_spl
| ~ sQ155_spl ),
inference(split_clause,[status(thm)],[f1999,f1970,f1973,f2004,f2007,f1410,f273]) ).
fof(f2011,definition,
! [X0] :
( sQ164_spl
<=> ( X0 = apply(relation_composition(sK5_skl,function_inverse(sK5_skl)),apply(function_inverse(relation_composition(sK5_skl,function_inverse(sK5_skl))),X0))
| ~ in(X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f2014,plain,
( ~ sQ14_spl
| ~ sQ118_spl
| sQ164_spl
| ~ sQ162_spl
| ~ sQ156_spl
| ~ sQ155_spl ),
inference(split_clause,[status(thm)],[f2000,f1970,f1973,f2004,f2011,f1410,f273]) ).
fof(f2018,plain,
! [X0] :
( ~ sQ13_spl
| ~ sQ118_spl
| relation_composition(function_inverse(sK5_skl),sK5_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl)))
| ~ function(relation_composition(function_inverse(sK5_skl),sK5_skl))
| ~ relation(relation_composition(function_inverse(sK5_skl),sK5_skl))
| ~ empty(X0)
| ~ element(sK5_skl,powerset(X0)) ),
inference(paramodulation,[status(thm)],[f1860,f672]) ).
fof(f2026,definition,
( sQ165_spl
<=> relation_composition(function_inverse(sK5_skl),sK5_skl) = identity_relation(relation_dom(relation_composition(function_inverse(sK5_skl),sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f2029,plain,
( ~ sQ13_spl
| ~ sQ118_spl
| sQ165_spl
| ~ sQ150_spl
| ~ sQ149_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f2018,f1885,f1921,f1924,f2026,f1410,f269]) ).
fof(f2063,plain,
( sQ50_spl
| ~ sQ118_spl
| ~ relation(relation_composition(sK5_skl,function_inverse(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f1823,f781]) ).
fof(f2064,plain,
( sQ50_spl
| ~ sQ118_spl
| ~ relation(relation_composition(sK5_skl,function_inverse(sK5_skl))) ),
inference(forward_demodulation,[status(thm)],[f1823,f2063]) ).
fof(f2065,plain,
( sQ50_spl
| ~ sQ118_spl
| ~ relation(function_inverse(sK5_skl))
| ~ empty(sK5_skl) ),
inference(resolution,[status(thm)],[f2064,f93]) ).
fof(f2068,definition,
( sQ171_spl
<=> relation(function_inverse(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f2069,plain,
( ~ sQ171_spl
| relation(function_inverse(sK5_skl)) ),
inference(component_clause,[status(thm)],[f2068]) ).
fof(f2070,plain,
( sQ171_spl
| ~ relation(function_inverse(sK5_skl)) ),
inference(component_clause,[status(thm)],[f2068]) ).
fof(f2071,plain,
( sQ50_spl
| ~ sQ118_spl
| ~ sQ171_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f2065,f1087,f2068,f1410,f779]) ).
fof(f2095,plain,
( ~ sQ17_spl
| ~ sQ71_spl
| relation_composition(sK5_skl,function_inverse(sK12_skl)) = sK5_skl ),
inference(resolution,[status(thm)],[f997,f293]) ).
fof(f2350,plain,
( sQ42_spl
| ~ sQ118_spl
| ~ function(relation_composition(function_inverse(sK5_skl),sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f1823,f745]) ).
fof(f2351,plain,
( sQ42_spl
| ~ sQ118_spl
| ~ function(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
inference(forward_demodulation,[status(thm)],[f1823,f2350]) ).
fof(f2352,plain,
( sQ42_spl
| ~ sQ118_spl
| ~ function(sK5_skl)
| ~ relation(sK5_skl)
| ~ function(function_inverse(sK5_skl))
| ~ relation(function_inverse(sK5_skl)) ),
inference(resolution,[status(thm)],[f2351,f73]) ).
fof(f2354,definition,
( sQ183_spl
<=> function(function_inverse(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f2356,plain,
( sQ183_spl
| ~ function(function_inverse(sK5_skl)) ),
inference(component_clause,[status(thm)],[f2354]) ).
fof(f2357,plain,
( sQ42_spl
| ~ sQ118_spl
| ~ sQ84_spl
| ~ sQ83_spl
| ~ sQ183_spl
| ~ sQ171_spl ),
inference(split_clause,[status(thm)],[f2352,f2068,f2354,f1070,f1073,f1410,f743]) ).
fof(f2367,plain,
( ~ sQ41_spl
| ~ sQ118_spl
| relation(relation_composition(function_inverse(sK5_skl),sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f1823,f741]) ).
fof(f2368,plain,
( ~ sQ41_spl
| ~ sQ118_spl
| relation(relation_composition(function_inverse(sK5_skl),sK5_skl)) ),
inference(forward_demodulation,[status(thm)],[f1823,f2367]) ).
fof(f2510,plain,
( sQ149_spl
| ~ sQ41_spl
| ~ sQ118_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1923,f2368]) ).
fof(f2511,plain,
( sQ149_spl
| ~ sQ41_spl
| ~ sQ118_spl ),
inference(contradiction_clause,[status(thm)],[f2510]) ).
fof(f2514,plain,
( sQ155_spl
| ~ relation(function_inverse(sK5_skl))
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f1972,f61]) ).
fof(f2517,plain,
( sQ155_spl
| ~ sQ171_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f2514,f1070,f2068,f1970]) ).
fof(f2518,plain,
! [X0] :
( ~ sQ146_spl
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1886,f991]) ).
fof(f2540,plain,
( ~ sQ71_spl
| ~ sQ146_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f981,f2518]) ).
fof(f2541,plain,
( ~ sQ71_spl
| ~ sQ146_spl ),
inference(contradiction_clause,[status(thm)],[f2540]) ).
fof(f2563,plain,
! [X0] :
( ~ sQ71_spl
| X0 = sK5_skl
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f981,f176]) ).
fof(f2564,plain,
! [X0,X1] :
( ~ sQ71_spl
| ~ element(X1,powerset(sK5_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f981,f162]) ).
fof(f2565,plain,
! [X0] :
( ~ sQ71_spl
| relation(relation_composition(sK5_skl,X0))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f93,f981]) ).
fof(f2629,plain,
( sQ150_spl
| ~ function(sK5_skl)
| ~ relation(sK5_skl)
| ~ function(function_inverse(sK5_skl))
| ~ relation(function_inverse(sK5_skl)) ),
inference(resolution,[status(thm)],[f1926,f73]) ).
fof(f2630,plain,
( sQ150_spl
| ~ sQ84_spl
| ~ sQ83_spl
| ~ sQ183_spl
| ~ sQ171_spl ),
inference(split_clause,[status(thm)],[f2629,f2068,f2354,f1070,f1073,f1924]) ).
fof(f2631,plain,
( sQ183_spl
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f2356,f59]) ).
fof(f2632,plain,
( sQ183_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f2631,f1070,f1073,f2354]) ).
fof(f2646,plain,
( sQ171_spl
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f2070,f58]) ).
fof(f2647,plain,
( sQ171_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f2646,f1070,f1073,f2068]) ).
fof(f2648,plain,
( ~ sQ71_spl
| ~ sQ171_spl
| relation_composition(function_inverse(sK5_skl),sK5_skl) = sK5_skl ),
inference(resolution,[status(thm)],[f2069,f1009]) ).
fof(f2649,plain,
( ~ sQ71_spl
| ~ sQ171_spl
| relation_composition(sK5_skl,function_inverse(sK5_skl)) = sK5_skl ),
inference(resolution,[status(thm)],[f2069,f997]) ).
fof(f2677,plain,
( sQ156_spl
| ~ function(function_inverse(sK5_skl))
| ~ relation(function_inverse(sK5_skl))
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f1975,f73]) ).
fof(f2678,plain,
( sQ156_spl
| ~ sQ183_spl
| ~ sQ171_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f2677,f1070,f1073,f2068,f2354,f1973]) ).
fof(f2681,plain,
( ~ sQ35_spl
| sK9_skl = identity_relation(relation_dom(sK9_skl))
| ~ function(sK9_skl)
| ~ relation(sK9_skl)
| sK11_skl(relation_dom(sK9_skl),sK9_skl) = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),sK11_skl(relation_dom(sK9_skl),sK9_skl)) ),
inference(resolution,[status(thm)],[f613,f186]) ).
fof(f2682,plain,
( ~ sQ35_spl
| empty(relation_dom(sK9_skl))
| sK0_skl(relation_dom(sK9_skl)) = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),sK0_skl(relation_dom(sK9_skl))) ),
inference(resolution,[status(thm)],[f613,f399]) ).
fof(f2683,definition,
( sQ187_spl
<=> sK11_skl(relation_dom(sK9_skl),sK9_skl) = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),sK11_skl(relation_dom(sK9_skl),sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f2686,plain,
( ~ sQ35_spl
| sQ103_spl
| ~ sQ12_spl
| ~ sQ11_spl
| sQ187_spl ),
inference(split_clause,[status(thm)],[f2681,f2683,f263,f266,f1267,f612]) ).
fof(f2687,definition,
( sQ188_spl
<=> sK0_skl(relation_dom(sK9_skl)) = apply(relation_composition(sK9_skl,function_inverse(sK9_skl)),sK0_skl(relation_dom(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f2690,plain,
( ~ sQ35_spl
| sQ56_spl
| sQ188_spl ),
inference(split_clause,[status(thm)],[f2682,f2687,f799,f612]) ).
fof(f2722,plain,
( sQ51_spl
| ~ function(function_inverse(sK9_skl))
| ~ relation(function_inverse(sK9_skl))
| ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(resolution,[status(thm)],[f784,f73]) ).
fof(f2723,definition,
( sQ190_spl
<=> function(function_inverse(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f2726,plain,
( sQ51_spl
| ~ sQ190_spl
| ~ sQ133_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2722,f263,f266,f1640,f2723,f782]) ).
fof(f2774,plain,
( ~ sQ28_spl
| ~ sQ10_spl
| 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)))
| ~ one_to_one(sK12_skl)
| ~ function(sK12_skl)
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f1717,f153]) ).
fof(f2779,definition,
( sQ192_spl
<=> 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))) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f2780,plain,
( ~ sQ192_spl
| 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))) ),
inference(component_clause,[status(thm)],[f2779]) ).
fof(f2782,plain,
( ~ sQ28_spl
| ~ sQ10_spl
| sQ192_spl
| ~ sQ37_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f2774,f205,f208,f697,f2779,f255,f549]) ).
fof(f2794,plain,
( ~ sQ192_spl
| sQ27_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2780,f1718]) ).
fof(f2795,plain,
( ~ sQ192_spl
| sQ27_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f2794]) ).
fof(f2817,plain,
( ~ sQ17_spl
| ~ sQ71_spl
| relation(sK5_skl)
| ~ relation(function_inverse(sK12_skl)) ),
inference(paramodulation,[status(thm)],[f2095,f2565]) ).
fof(f2827,plain,
( ~ sQ71_spl
| sQ83_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f2817,f292,f1070,f901]) ).
fof(f3005,plain,
( sQ162_spl
| ~ sQ71_spl
| ~ sQ171_spl
| ~ one_to_one(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f2649,f2006]) ).
fof(f3006,plain,
( sQ162_spl
| ~ sQ71_spl
| ~ sQ171_spl
| ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3005,f1077]) ).
fof(f3007,plain,
( sQ162_spl
| ~ sQ71_spl
| ~ sQ171_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f3006]) ).
fof(f3009,plain,
( sQ151_spl
| ~ sQ71_spl
| ~ sQ171_spl
| ~ one_to_one(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f2648,f1929]) ).
fof(f3010,plain,
( sQ151_spl
| ~ sQ71_spl
| ~ sQ171_spl
| ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3009,f1077]) ).
fof(f3011,plain,
( sQ151_spl
| ~ sQ71_spl
| ~ sQ171_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f3010]) ).
fof(f3013,plain,
( ~ sQ51_spl
| ~ in(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl))))
| relation_composition(sK9_skl,function_inverse(sK9_skl)) = identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(resolution,[status(thm)],[f783,f477]) ).
fof(f3014,plain,
( ~ sQ51_spl
| apply(identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl)))),sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl)))) = sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl)))
| relation_composition(sK9_skl,function_inverse(sK9_skl)) = identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))))
| ~ relation(relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
inference(resolution,[status(thm)],[f783,f482]) ).
fof(f3015,definition,
( sQ201_spl
<=> in(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f3018,plain,
( ~ sQ51_spl
| ~ sQ201_spl
| sQ58_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f3013,f779,f820,f3015,f782]) ).
fof(f3019,definition,
( sQ202_spl
<=> apply(identity_relation(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl)))),sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl)))) = sK11_skl(relation_dom(relation_composition(sK9_skl,function_inverse(sK9_skl))),relation_composition(sK9_skl,function_inverse(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f3022,plain,
( ~ sQ51_spl
| sQ202_spl
| sQ58_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f3014,f779,f820,f3019,f782]) ).
fof(f3086,plain,
! [X0] :
( ~ sQ71_spl
| empty(X0)
| ~ element(X0,powerset(sK5_skl)) ),
inference(resolution,[status(thm)],[f2564,f399]) ).
fof(f3090,plain,
( ~ sQ71_spl
| empty(sK0_skl(powerset(sK5_skl))) ),
inference(resolution,[status(thm)],[f3086,f64]) ).
fof(f3093,plain,
! [X0] :
( ~ sQ71_spl
| ~ in(X0,powerset(sK5_skl))
| empty(X0) ),
inference(resolution,[status(thm)],[f3086,f128]) ).
fof(f3127,plain,
( ~ sQ71_spl
| sK0_skl(powerset(sK5_skl)) = sK5_skl ),
inference(resolution,[status(thm)],[f3090,f2563]) ).
fof(f3159,plain,
( ~ sQ71_spl
| in(sK5_skl,powerset(sK5_skl))
| empty(powerset(sK5_skl)) ),
inference(paramodulation,[status(thm)],[f3127,f399]) ).
fof(f3160,plain,
( ~ sQ71_spl
| ~ in(powerset(sK5_skl),sK5_skl)
| empty(powerset(sK5_skl)) ),
inference(paramodulation,[status(thm)],[f3127,f469]) ).
fof(f3162,definition,
( sQ210_spl
<=> empty(powerset(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f3163,plain,
( ~ sQ210_spl
| empty(powerset(sK5_skl)) ),
inference(component_clause,[status(thm)],[f3162]) ).
fof(f3165,definition,
( sQ211_spl
<=> in(sK5_skl,powerset(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f3168,plain,
( ~ sQ71_spl
| sQ211_spl
| sQ210_spl ),
inference(split_clause,[status(thm)],[f3159,f3162,f3165,f901]) ).
fof(f3169,definition,
( sQ212_spl
<=> in(powerset(sK5_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f3172,plain,
( ~ sQ71_spl
| ~ sQ212_spl
| sQ210_spl ),
inference(split_clause,[status(thm)],[f3160,f3162,f3169,f901]) ).
fof(f3173,plain,
( ~ sQ210_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3163,f74]) ).
fof(f3174,plain,
~ sQ210_spl,
inference(contradiction_clause,[status(thm)],[f3173]) ).
fof(f3180,plain,
( ~ sQ71_spl
| empty(powerset(sK5_skl))
| empty(sK0_skl(powerset(sK5_skl))) ),
inference(resolution,[status(thm)],[f3093,f399]) ).
fof(f3183,definition,
( sQ213_spl
<=> empty(sK0_skl(powerset(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f3186,plain,
( ~ sQ71_spl
| sQ210_spl
| sQ213_spl ),
inference(split_clause,[status(thm)],[f3180,f3183,f3162,f901]) ).
fof(f3211,plain,
( sQ80_spl
| ~ sQ4_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(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))) ),
inference(forward_demodulation,[status(thm)],[f212,f1046]) ).
fof(f3410,plain,
( ~ sQ81_spl
| ~ sQ4_spl
| in(sK11_skl(relation_dom(sK12_skl),relation_composition(sK12_skl,function_inverse(sK12_skl))),relation_dom(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f212,f1049]) ).
fof(f3411,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ4_spl
| 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)))) ),
inference(resolution,[status(thm)],[f3410,f617]) ).
fof(f3417,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ4_spl
| sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3411,f3211]) ).
fof(f3418,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ4_spl
| sQ80_spl ),
inference(contradiction_clause,[status(thm)],[f3417]) ).
fof(f3419,plain,
$false,
inference(sat_refutation,[status(thm)],[f183,f214,f243,f249,f252,f258,f272,f276,f280,f282,f284,f300,f302,f326,f330,f548,f552,f603,f607,f615,f619,f626,f712,f752,f756,f760,f767,f771,f772,f791,f795,f802,f806,f807,f826,f830,f834,f911,f912,f924,f928,f944,f948,f1031,f1047,f1051,f1061,f1082,f1086,f1095,f1097,f1100,f1102,f1112,f1116,f1120,f1124,f1128,f1132,f1273,f1322,f1324,f1325,f1342,f1369,f1374,f1413,f1415,f1456,f1644,f1646,f1659,f1663,f1802,f1897,f1933,f1937,f1941,f1979,f1996,f2010,f2014,f2029,f2071,f2357,f2511,f2517,f2541,f2630,f2632,f2647,f2678,f2686,f2690,f2726,f2782,f2795,f2827,f3007,f3011,f3018,f3022,f3168,f3172,f3174,f3186,f3418]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU028+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 05:42:43 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 1.00/0.70 % Refutation found
% 1.00/0.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.00/0.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.00/0.74 % Elapsed time: 0.357034 seconds
% 1.00/0.74 % CPU time: 2.463049 seconds
% 1.00/0.74 % Total memory used: 123.261 MB
% 1.00/0.74 % Net memory used: 120.229 MB
%------------------------------------------------------------------------------