%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU012+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 : n018.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:05 PM UTC 2026
% Result : Theorem 15.14s 2.51s
% Output : CNFRefutation 11.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 70
% Syntax : Number of formulae : 326 ( 89 unt; 50 def)
% Number of atoms : 764 ( 108 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 719 ( 281 ~; 297 |; 68 &)
% ( 56 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 58 ( 56 usr; 51 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 7 con; 0-3 aty)
% Number of variables : 189 ( 171 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(relation_composition(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( empty(A)
=> ( relation(relation_dom(A))
& empty(relation_dom(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
? [A] :
( relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(B))
=> apply(relation_composition(B,C),A) = apply(C,apply(B,A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,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(f34,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( relation_composition(A,B) = A
& relation_rng(A) = relation_dom(B) )
=> B = identity_relation(relation_dom(B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( relation_composition(A,B) = A
& relation_rng(A) = relation_dom(B) )
=> B = identity_relation(relation_dom(B)) ) ) ),
inference(negated_conjecture,[status(cth)],[f34]) ).
fof(f37,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f46,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
! [A] :
( ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) ) ) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f48,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| in(C,B) )
& ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| in(C,B) )
& ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| in(C,B) )
& ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| in(C,B) )
& ! [C] :
( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f50,plain,
! [A] :
( ( ! [B] :
( ( ( ( sK1_skl(B,A) = apply(A,sK2_skl(B,A))
& in(sK2_skl(B,A),relation_dom(A)) )
| in(sK1_skl(B,A),B) )
& ( ! [D] :
( sK1_skl(B,A) != apply(A,D)
| ~ in(D,relation_dom(A)) )
| ~ in(sK1_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| in(C,B) )
& ! [C] :
( ( C = apply(A,sK0_skl(C,B,A))
& in(sK0_skl(C,B,A),relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(D,sK0_skl(C,B,A)),skolemize(C,sK1_skl(B,A)),skolemize(D,sK2_skl(B,A))],[f49]) ).
fof(f51,plain,
! [X0,X1,X2] :
( in(sK0_skl(X2,X1,X0),relation_dom(X0))
| ~ in(X2,X1)
| X1 != relation_rng(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [X0,X1,X2] :
( X2 = apply(X0,sK0_skl(X2,X1,X0))
| ~ in(X2,X1)
| X1 != relation_rng(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f57,plain,
! [A,B] :
( relation(relation_composition(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f58,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f60,plain,
! [A] : element(sK3_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B,sK3_skl(A))],[f7]) ).
fof(f61,plain,
! [X0] : element(sK3_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f71,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f73,plain,
( ! [A] : function(identity_relation(A))
& ! [A] : relation(identity_relation(A)) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f75,plain,
! [X0] : function(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f82,plain,
! [A] :
( ( relation(relation_dom(A))
& empty(relation_dom(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f83,plain,
! [X0] :
( empty(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f91,plain,
( function(sK4_skl)
& relation(sK4_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f20]) ).
fof(f92,plain,
relation(sK4_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
function(sK4_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f94,plain,
( relation(sK5_skl)
& empty(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f21]) ).
fof(f95,plain,
empty(sK5_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
relation(sK5_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f103,plain,
( relation(sK8_skl)
& ~ empty(sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f24]) ).
fof(f104,plain,
~ empty(sK8_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
relation(sK8_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f106,plain,
! [A] :
( empty(sK9_skl(A))
& element(sK9_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(B,sK9_skl(A))],[f25]) ).
fof(f107,plain,
! [X0] : element(sK9_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f108,plain,
! [X0] : empty(sK9_skl(X0)),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f111,plain,
( relation_empty_yielding(sK11_skl)
& relation(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f27]) ).
fof(f112,plain,
relation(sK11_skl),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f118,plain,
! [A,B] :
( ! [C] :
( apply(relation_composition(B,C),A) = apply(C,apply(B,A))
| ~ in(A,relation_dom(B))
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f119,plain,
! [B] :
( ! [C] :
( ! [A] :
( apply(relation_composition(B,C),A) = apply(C,apply(B,A))
| ~ in(A,relation_dom(B)) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f120,plain,
! [X0,X1,X2] :
( apply(relation_composition(X0,X1),X2) = apply(X1,apply(X0,X2))
| ~ in(X2,relation_dom(X0))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f122,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,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)],[f32]) ).
fof(f124,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)],[f123]) ).
fof(f125,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)],[f124]) ).
fof(f126,plain,
! [B] :
( ( ! [A] :
( ( apply(B,sK12_skl(A,B)) != sK12_skl(A,B)
& in(sK12_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,[sK12_skl]),skolemize(C,sK12_skl(A,B))],[f125]) ).
fof(f129,plain,
! [X0,X1] :
( in(sK12_skl(X1,X0),X1)
| relation_dom(X0) != X1
| X0 = identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f130,plain,
! [X0,X1] :
( apply(X0,sK12_skl(X1,X0)) != sK12_skl(X1,X0)
| relation_dom(X0) != X1
| X0 = identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f135,plain,
? [A] :
( ? [B] :
( B != identity_relation(relation_dom(B))
& relation_composition(A,B) = A
& relation_rng(A) = relation_dom(B)
& function(B)
& relation(B) )
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f136,plain,
( sK14_skl != identity_relation(relation_dom(sK14_skl))
& relation_composition(sK13_skl,sK14_skl) = sK13_skl
& relation_rng(sK13_skl) = relation_dom(sK14_skl)
& function(sK14_skl)
& relation(sK14_skl)
& function(sK13_skl)
& relation(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(A,sK13_skl),skolemize(B,sK14_skl)],[f135]) ).
fof(f137,plain,
relation(sK13_skl),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f138,plain,
function(sK13_skl),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f139,plain,
relation(sK14_skl),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f140,plain,
function(sK14_skl),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f141,plain,
relation_rng(sK13_skl) = relation_dom(sK14_skl),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f142,plain,
relation_composition(sK13_skl,sK14_skl) = sK13_skl,
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f143,plain,
sK14_skl != identity_relation(relation_dom(sK14_skl)),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f147,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f148,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f147]) ).
fof(f149,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f151,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f152,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f153,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f152]) ).
fof(f154,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f158,plain,
! [X0,X1] :
( in(sK0_skl(X1,relation_rng(X0),X0),relation_dom(X0))
| ~ in(X1,relation_rng(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f51]) ).
fof(f159,plain,
! [X0,X1] :
( X1 = apply(X0,sK0_skl(X1,relation_rng(X0),X0))
| ~ in(X1,relation_rng(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f52]) ).
fof(f163,plain,
! [X0] :
( in(sK12_skl(relation_dom(X0),X0),relation_dom(X0))
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f129]) ).
fof(f164,plain,
! [X0] :
( apply(X0,sK12_skl(relation_dom(X0),X0)) != sK12_skl(relation_dom(X0),X0)
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f130]) ).
fof(f165,plain,
! [X0] :
( in(sK0_skl(X0,relation_rng(sK13_skl),sK13_skl),relation_dom(sK13_skl))
| ~ in(X0,relation_dom(sK14_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(paramodulation,[status(thm)],[f141,f158]) ).
fof(f166,definition,
( sQ0_spl
<=> relation(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f168,plain,
( sQ0_spl
| ~ relation(sK13_skl) ),
inference(component_clause,[status(thm)],[f166]) ).
fof(f169,definition,
( sQ1_spl
<=> function(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f171,plain,
( sQ1_spl
| ~ function(sK13_skl) ),
inference(component_clause,[status(thm)],[f169]) ).
fof(f172,definition,
! [X0] :
( sQ2_spl
<=> ( in(sK0_skl(X0,relation_rng(sK13_skl),sK13_skl),relation_dom(sK13_skl))
| ~ in(X0,relation_dom(sK14_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f173,plain,
! [X0] :
( ~ sQ2_spl
| in(sK0_skl(X0,relation_rng(sK13_skl),sK13_skl),relation_dom(sK13_skl))
| ~ in(X0,relation_dom(sK14_skl)) ),
inference(component_clause,[status(thm)],[f172]) ).
fof(f175,plain,
( sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f165,f166,f169,f172]) ).
fof(f176,plain,
! [X0] :
( ~ sQ2_spl
| in(sK0_skl(X0,relation_dom(sK14_skl),sK13_skl),relation_dom(sK13_skl))
| ~ in(X0,relation_dom(sK14_skl)) ),
inference(forward_demodulation,[status(thm)],[f141,f173]) ).
fof(f178,definition,
( sQ3_spl
<=> relation(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f180,plain,
( sQ3_spl
| ~ relation(sK14_skl) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f190,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f168,f137]) ).
fof(f191,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f190]) ).
fof(f192,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f171,f138]) ).
fof(f193,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f192]) ).
fof(f196,plain,
! [X0] :
( X0 = apply(sK13_skl,sK0_skl(X0,relation_rng(sK13_skl),sK13_skl))
| ~ in(X0,relation_dom(sK14_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(paramodulation,[status(thm)],[f141,f159]) ).
fof(f197,definition,
! [X0] :
( sQ6_spl
<=> ( X0 = apply(sK13_skl,sK0_skl(X0,relation_rng(sK13_skl),sK13_skl))
| ~ in(X0,relation_dom(sK14_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f198,plain,
! [X0] :
( ~ sQ6_spl
| X0 = apply(sK13_skl,sK0_skl(X0,relation_rng(sK13_skl),sK13_skl))
| ~ in(X0,relation_dom(sK14_skl)) ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f200,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f196,f166,f169,f197]) ).
fof(f201,plain,
! [X0] :
( ~ sQ6_spl
| X0 = apply(sK13_skl,sK0_skl(X0,relation_dom(sK14_skl),sK13_skl))
| ~ in(X0,relation_dom(sK14_skl)) ),
inference(forward_demodulation,[status(thm)],[f141,f198]) ).
fof(f223,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f180,f139]) ).
fof(f224,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f223]) ).
fof(f258,plain,
! [X0] :
( in(sK3_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f122,f61]) ).
fof(f268,definition,
( sQ12_spl
<=> sK14_skl = identity_relation(relation_dom(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f269,plain,
( ~ sQ12_spl
| sK14_skl = identity_relation(relation_dom(sK14_skl)) ),
inference(component_clause,[status(thm)],[f268]) ).
fof(f282,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f269,f143]) ).
fof(f283,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f282]) ).
fof(f296,definition,
( sQ17_spl
<=> function(identity_relation(relation_dom(sK13_skl))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f298,plain,
( sQ17_spl
| ~ function(identity_relation(relation_dom(sK13_skl))) ),
inference(component_clause,[status(thm)],[f296]) ).
fof(f304,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f298,f75]) ).
fof(f305,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f304]) ).
fof(f343,plain,
! [X0] : sK9_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f151,f108]) ).
fof(f348,plain,
sK5_skl = empty_set,
inference(resolution,[status(thm)],[f151,f95]) ).
fof(f350,plain,
! [X0] :
( ~ empty(X0)
| relation_dom(X0) = empty_set ),
inference(resolution,[status(thm)],[f151,f83]) ).
fof(f523,definition,
( sQ34_spl
<=> relation(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f525,plain,
( sQ34_spl
| ~ relation(sK4_skl) ),
inference(component_clause,[status(thm)],[f523]) ).
fof(f587,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f525,f92]) ).
fof(f588,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f587]) ).
fof(f597,plain,
! [X0] : element(sK5_skl,powerset(X0)),
inference(backward_demodulation,[status(thm)],[f599,f107]) ).
fof(f599,plain,
! [X0] : sK9_skl(X0) = sK5_skl,
inference(forward_demodulation,[status(thm)],[f348,f343]) ).
fof(f644,definition,
( sQ46_spl
<=> empty(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f646,plain,
( sQ46_spl
| ~ empty(sK5_skl) ),
inference(component_clause,[status(thm)],[f644]) ).
fof(f664,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f646,f95]) ).
fof(f665,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f664]) ).
fof(f670,plain,
! [X0] :
( ~ empty(X0)
| relation_dom(X0) = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f348,f350]) ).
fof(f671,plain,
relation_dom(sK5_skl) = sK5_skl,
inference(resolution,[status(thm)],[f670,f95]) ).
fof(f1032,plain,
! [X0,X1] :
( ~ element(X1,powerset(sK5_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f95,f149]) ).
fof(f1033,plain,
! [X0] : ~ in(X0,sK5_skl),
inference(resolution,[status(thm)],[f95,f154]) ).
fof(f1184,definition,
( sQ85_spl
<=> function(identity_relation(relation_rng(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1186,plain,
( sQ85_spl
| ~ function(identity_relation(relation_rng(sK14_skl))) ),
inference(component_clause,[status(thm)],[f1184]) ).
fof(f1191,plain,
( sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1186,f75]) ).
fof(f1192,plain,
sQ85_spl,
inference(contradiction_clause,[status(thm)],[f1191]) ).
fof(f1245,definition,
( sQ90_spl
<=> function(identity_relation(relation_dom(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1247,plain,
( sQ90_spl
| ~ function(identity_relation(relation_dom(sK14_skl))) ),
inference(component_clause,[status(thm)],[f1245]) ).
fof(f1252,plain,
( sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1247,f75]) ).
fof(f1253,plain,
sQ90_spl,
inference(contradiction_clause,[status(thm)],[f1252]) ).
fof(f1297,plain,
! [X0] : ~ in(X0,sK3_skl(powerset(sK5_skl))),
inference(resolution,[status(thm)],[f1032,f61]) ).
fof(f1544,definition,
( sQ102_spl
<=> relation(identity_relation(relation_dom(sK13_skl))) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1546,plain,
( sQ102_spl
| ~ relation(identity_relation(relation_dom(sK13_skl))) ),
inference(component_clause,[status(thm)],[f1544]) ).
fof(f1551,plain,
( sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1546,f59]) ).
fof(f1552,plain,
sQ102_spl,
inference(contradiction_clause,[status(thm)],[f1551]) ).
fof(f1628,definition,
( sQ107_spl
<=> relation(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1630,plain,
( sQ107_spl
| ~ relation(sK11_skl) ),
inference(component_clause,[status(thm)],[f1628]) ).
fof(f1731,definition,
( sQ118_spl
<=> relation(identity_relation(relation_dom(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1733,plain,
( sQ118_spl
| ~ relation(identity_relation(relation_dom(sK14_skl))) ),
inference(component_clause,[status(thm)],[f1731]) ).
fof(f1738,plain,
( sQ118_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1733,f59]) ).
fof(f1739,plain,
sQ118_spl,
inference(contradiction_clause,[status(thm)],[f1738]) ).
fof(f1751,definition,
( sQ120_spl
<=> empty(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1752,plain,
( ~ sQ120_spl
| empty(sK8_skl) ),
inference(component_clause,[status(thm)],[f1751]) ).
fof(f1755,definition,
( sQ121_spl
<=> relation(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1757,plain,
( sQ121_spl
| ~ relation(sK8_skl) ),
inference(component_clause,[status(thm)],[f1755]) ).
fof(f1777,plain,
( sQ121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1757,f105]) ).
fof(f1778,plain,
sQ121_spl,
inference(contradiction_clause,[status(thm)],[f1777]) ).
fof(f1834,definition,
( sQ132_spl
<=> function(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1836,plain,
( sQ132_spl
| ~ function(sK4_skl) ),
inference(component_clause,[status(thm)],[f1834]) ).
fof(f1847,plain,
( sQ132_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1836,f93]) ).
fof(f1848,plain,
sQ132_spl,
inference(contradiction_clause,[status(thm)],[f1847]) ).
fof(f1922,plain,
empty(sK3_skl(powerset(sK5_skl))),
inference(resolution,[status(thm)],[f1297,f258]) ).
fof(f2053,definition,
( sQ153_spl
<=> relation(sK3_skl(powerset(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f2055,plain,
( sQ153_spl
| ~ relation(sK3_skl(powerset(sK5_skl))) ),
inference(component_clause,[status(thm)],[f2053]) ).
fof(f2083,plain,
( sQ153_spl
| ~ empty(sK3_skl(powerset(sK5_skl))) ),
inference(resolution,[status(thm)],[f2055,f46]) ).
fof(f2084,plain,
( sQ153_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2083,f1922]) ).
fof(f2085,plain,
sQ153_spl,
inference(contradiction_clause,[status(thm)],[f2084]) ).
fof(f2110,definition,
( sQ160_spl
<=> empty(powerset(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f2111,plain,
( ~ sQ160_spl
| empty(powerset(sK5_skl)) ),
inference(component_clause,[status(thm)],[f2110]) ).
fof(f2121,plain,
( ~ sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2111,f71]) ).
fof(f2122,plain,
~ sQ160_spl,
inference(contradiction_clause,[status(thm)],[f2121]) ).
fof(f2144,definition,
( sQ166_spl
<=> function(identity_relation(relation_rng(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f2146,plain,
( sQ166_spl
| ~ function(identity_relation(relation_rng(sK4_skl))) ),
inference(component_clause,[status(thm)],[f2144]) ).
fof(f2396,definition,
! [X0] :
( sQ182_spl
<=> ~ relation(identity_relation(X0)) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f2397,plain,
! [X0] :
( ~ sQ182_spl
| ~ relation(identity_relation(X0)) ),
inference(component_clause,[status(thm)],[f2396]) ).
fof(f2634,plain,
( sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1630,f112]) ).
fof(f2635,plain,
sQ107_spl,
inference(contradiction_clause,[status(thm)],[f2634]) ).
fof(f3499,definition,
( sQ267_spl
<=> empty(powerset(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition]) ).
fof(f3500,plain,
( ~ sQ267_spl
| empty(powerset(sK4_skl)) ),
inference(component_clause,[status(thm)],[f3499]) ).
fof(f3514,plain,
( ~ sQ267_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3500,f71]) ).
fof(f3515,plain,
~ sQ267_spl,
inference(contradiction_clause,[status(thm)],[f3514]) ).
fof(f3779,plain,
( ~ sQ120_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1752,f104]) ).
fof(f3780,plain,
~ sQ120_spl,
inference(contradiction_clause,[status(thm)],[f3779]) ).
fof(f4453,definition,
( sQ321_spl
<=> relation(identity_relation(relation_rng(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition]) ).
fof(f4455,plain,
( sQ321_spl
| ~ relation(identity_relation(relation_rng(sK14_skl))) ),
inference(component_clause,[status(thm)],[f4453]) ).
fof(f4467,plain,
( sQ321_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4455,f59]) ).
fof(f4468,plain,
sQ321_spl,
inference(contradiction_clause,[status(thm)],[f4467]) ).
fof(f5862,definition,
( sQ386_spl
<=> function(identity_relation(sK6_skl(powerset(sK4_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition]) ).
fof(f5864,plain,
( sQ386_spl
| ~ function(identity_relation(sK6_skl(powerset(sK4_skl)))) ),
inference(component_clause,[status(thm)],[f5862]) ).
fof(f5869,plain,
( sQ386_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5864,f75]) ).
fof(f5870,plain,
sQ386_spl,
inference(contradiction_clause,[status(thm)],[f5869]) ).
fof(f6702,definition,
( sQ428_spl
<=> function(identity_relation(relation_rng(identity_relation(relation_rng(sK14_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f6704,plain,
( sQ428_spl
| ~ function(identity_relation(relation_rng(identity_relation(relation_rng(sK14_skl))))) ),
inference(component_clause,[status(thm)],[f6702]) ).
fof(f6710,plain,
( sQ428_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6704,f75]) ).
fof(f6711,plain,
sQ428_spl,
inference(contradiction_clause,[status(thm)],[f6710]) ).
fof(f8138,definition,
! [X0] :
( sQ534_spl
<=> in(sK3_skl(sK5_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ534_spl])],[split_symbol_definition]) ).
fof(f8139,plain,
! [X0] :
( ~ sQ534_spl
| in(sK3_skl(sK5_skl),X0) ),
inference(component_clause,[status(thm)],[f8138]) ).
fof(f8152,definition,
( sQ535_spl
<=> relation(identity_relation(relation_dom(relation_composition(sK14_skl,sK5_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ535_spl])],[split_symbol_definition]) ).
fof(f8154,plain,
( sQ535_spl
| ~ relation(identity_relation(relation_dom(relation_composition(sK14_skl,sK5_skl)))) ),
inference(component_clause,[status(thm)],[f8152]) ).
fof(f8155,definition,
( sQ536_spl
<=> function(identity_relation(relation_dom(relation_composition(sK14_skl,sK5_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition]) ).
fof(f8157,plain,
( sQ536_spl
| ~ function(identity_relation(relation_dom(relation_composition(sK14_skl,sK5_skl)))) ),
inference(component_clause,[status(thm)],[f8155]) ).
fof(f8163,plain,
( sQ536_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8157,f75]) ).
fof(f8164,plain,
sQ536_spl,
inference(contradiction_clause,[status(thm)],[f8163]) ).
fof(f8165,plain,
( sQ535_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8154,f59]) ).
fof(f8166,plain,
sQ535_spl,
inference(contradiction_clause,[status(thm)],[f8165]) ).
fof(f8490,definition,
! [X0] :
( sQ546_spl
<=> ( in(sK12_skl(relation_dom(sK5_skl),sK5_skl),X0)
| ~ element(sK5_skl,powerset(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ546_spl])],[split_symbol_definition]) ).
fof(f8491,plain,
! [X0] :
( ~ sQ546_spl
| in(sK12_skl(relation_dom(sK5_skl),sK5_skl),X0)
| ~ element(sK5_skl,powerset(X0)) ),
inference(component_clause,[status(thm)],[f8490]) ).
fof(f8511,plain,
! [X0] :
( ~ sQ546_spl
| in(sK12_skl(sK5_skl,sK5_skl),X0)
| ~ element(sK5_skl,powerset(X0)) ),
inference(forward_demodulation,[status(thm)],[f671,f8491]) ).
fof(f8512,plain,
! [X0] :
( ~ sQ546_spl
| in(sK12_skl(sK5_skl,sK5_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8511,f597]) ).
fof(f8602,plain,
( ~ sQ534_spl
| $false ),
inference(resolution,[status(thm)],[f8139,f1033]) ).
fof(f8619,plain,
~ sQ534_spl,
inference(contradiction_clause,[status(thm)],[f8602]) ).
fof(f8716,definition,
( sQ557_spl
<=> relation(identity_relation(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ557_spl])],[split_symbol_definition]) ).
fof(f8718,plain,
( sQ557_spl
| ~ relation(identity_relation(sK4_skl)) ),
inference(component_clause,[status(thm)],[f8716]) ).
fof(f8721,definition,
( sQ558_spl
<=> function(identity_relation(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ558_spl])],[split_symbol_definition]) ).
fof(f8723,plain,
( sQ558_spl
| ~ function(identity_relation(sK4_skl)) ),
inference(component_clause,[status(thm)],[f8721]) ).
fof(f8732,plain,
( sQ557_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8718,f59]) ).
fof(f8733,plain,
sQ557_spl,
inference(contradiction_clause,[status(thm)],[f8732]) ).
fof(f8734,plain,
( sQ558_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8723,f75]) ).
fof(f8735,plain,
sQ558_spl,
inference(contradiction_clause,[status(thm)],[f8734]) ).
fof(f8782,definition,
! [X1] :
( sQ562_spl
<=> ~ relation(X1) ),
introduced(definition,[new_symbols(definition,[sQ562_spl])],[split_symbol_definition]) ).
fof(f8783,plain,
! [X0] :
( ~ sQ562_spl
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f8782]) ).
fof(f8792,plain,
( ~ sQ562_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f96,f8783]) ).
fof(f8803,plain,
~ sQ562_spl,
inference(contradiction_clause,[status(thm)],[f8792]) ).
fof(f8841,plain,
( apply(sK14_skl,sK12_skl(relation_dom(sK14_skl),sK14_skl)) != sK12_skl(relation_dom(sK14_skl),sK14_skl)
| sK14_skl = identity_relation(relation_dom(sK14_skl))
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f164,f140]) ).
fof(f8854,definition,
( sQ569_spl
<=> apply(sK14_skl,sK12_skl(relation_dom(sK14_skl),sK14_skl)) = sK12_skl(relation_dom(sK14_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ569_spl])],[split_symbol_definition]) ).
fof(f8856,plain,
( sQ569_spl
| apply(sK14_skl,sK12_skl(relation_dom(sK14_skl),sK14_skl)) != sK12_skl(relation_dom(sK14_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f8854]) ).
fof(f8857,plain,
( ~ sQ569_spl
| sQ12_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f8841,f178,f268,f8854]) ).
fof(f8862,plain,
( in(sK12_skl(relation_dom(sK14_skl),sK14_skl),relation_dom(sK14_skl))
| sK14_skl = identity_relation(relation_dom(sK14_skl))
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f163,f140]) ).
fof(f8875,definition,
( sQ573_spl
<=> in(sK12_skl(relation_dom(sK14_skl),sK14_skl),relation_dom(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ573_spl])],[split_symbol_definition]) ).
fof(f8876,plain,
( ~ sQ573_spl
| in(sK12_skl(relation_dom(sK14_skl),sK14_skl),relation_dom(sK14_skl)) ),
inference(component_clause,[status(thm)],[f8875]) ).
fof(f8878,plain,
( sQ573_spl
| sQ12_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f8862,f178,f268,f8875]) ).
fof(f8965,plain,
! [X0,X1] :
( apply(relation_composition(X0,sK14_skl),X1) = apply(sK14_skl,apply(X0,X1))
| ~ in(X1,relation_dom(X0))
| ~ relation(sK14_skl)
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f120,f140]) ).
fof(f8979,definition,
! [X0,X1] :
( sQ583_spl
<=> ( apply(relation_composition(X0,sK14_skl),X1) = apply(sK14_skl,apply(X0,X1))
| ~ in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ583_spl])],[split_symbol_definition]) ).
fof(f8980,plain,
! [X0,X1] :
( ~ sQ583_spl
| apply(relation_composition(X0,sK14_skl),X1) = apply(sK14_skl,apply(X0,X1))
| ~ in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f8979]) ).
fof(f8982,plain,
( ~ sQ3_spl
| sQ583_spl ),
inference(split_clause,[status(thm)],[f8965,f8979,f178]) ).
fof(f9058,plain,
! [X0] :
( relation(relation_composition(X0,sK4_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f58,f92]) ).
fof(f9062,plain,
! [X0] :
( relation(relation_composition(X0,sK14_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f58,f139]) ).
fof(f9063,plain,
! [X0] :
( relation(relation_composition(X0,sK13_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f58,f137]) ).
fof(f9164,plain,
( ~ sQ2_spl
| ~ sQ573_spl
| in(sK0_skl(sK12_skl(relation_dom(sK14_skl),sK14_skl),relation_dom(sK14_skl),sK13_skl),relation_dom(sK13_skl)) ),
inference(resolution,[status(thm)],[f8876,f176]) ).
fof(f9165,plain,
( ~ sQ6_spl
| ~ sQ573_spl
| sK12_skl(relation_dom(sK14_skl),sK14_skl) = apply(sK13_skl,sK0_skl(sK12_skl(relation_dom(sK14_skl),sK14_skl),relation_dom(sK14_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f8876,f201]) ).
fof(f9292,plain,
! [X0] :
( ~ sQ583_spl
| apply(relation_composition(sK13_skl,sK14_skl),X0) = apply(sK14_skl,apply(sK13_skl,X0))
| ~ in(X0,relation_dom(sK13_skl))
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f8980,f138]) ).
fof(f9300,definition,
! [X0] :
( sQ614_spl
<=> ( apply(relation_composition(sK13_skl,sK14_skl),X0) = apply(sK14_skl,apply(sK13_skl,X0))
| ~ in(X0,relation_dom(sK13_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition]) ).
fof(f9301,plain,
! [X0] :
( ~ sQ614_spl
| apply(relation_composition(sK13_skl,sK14_skl),X0) = apply(sK14_skl,apply(sK13_skl,X0))
| ~ in(X0,relation_dom(sK13_skl)) ),
inference(component_clause,[status(thm)],[f9300]) ).
fof(f9303,plain,
( ~ sQ583_spl
| sQ614_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f9292,f166,f9300,f8979]) ).
fof(f9313,plain,
! [X0] :
( ~ sQ614_spl
| apply(sK13_skl,X0) = apply(sK14_skl,apply(sK13_skl,X0))
| ~ in(X0,relation_dom(sK13_skl)) ),
inference(forward_demodulation,[status(thm)],[f142,f9301]) ).
fof(f9482,definition,
( sQ631_spl
<=> relation(relation_composition(sK13_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition]) ).
fof(f9484,plain,
( sQ631_spl
| ~ relation(relation_composition(sK13_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f9482]) ).
fof(f9600,definition,
( sQ654_spl
<=> relation(relation_composition(sK4_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f9602,plain,
( sQ654_spl
| ~ relation(relation_composition(sK4_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f9600]) ).
fof(f9693,definition,
( sQ673_spl
<=> relation(relation_composition(sK14_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ673_spl])],[split_symbol_definition]) ).
fof(f9695,plain,
( sQ673_spl
| ~ relation(relation_composition(sK14_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f9693]) ).
fof(f9812,definition,
( sQ692_spl
<=> relation(relation_composition(sK4_skl,sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ692_spl])],[split_symbol_definition]) ).
fof(f9814,plain,
( sQ692_spl
| ~ relation(relation_composition(sK4_skl,sK14_skl)) ),
inference(component_clause,[status(thm)],[f9812]) ).
fof(f9907,definition,
( sQ711_spl
<=> function(identity_relation(relation_dom(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ711_spl])],[split_symbol_definition]) ).
fof(f9909,plain,
( sQ711_spl
| ~ function(identity_relation(relation_dom(sK4_skl))) ),
inference(component_clause,[status(thm)],[f9907]) ).
fof(f9911,plain,
( sQ711_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9909,f75]) ).
fof(f9912,plain,
sQ711_spl,
inference(contradiction_clause,[status(thm)],[f9911]) ).
fof(f9931,definition,
( sQ712_spl
<=> relation(relation_composition(sK14_skl,sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ712_spl])],[split_symbol_definition]) ).
fof(f9933,plain,
( sQ712_spl
| ~ relation(relation_composition(sK14_skl,sK14_skl)) ),
inference(component_clause,[status(thm)],[f9931]) ).
fof(f10195,definition,
( sQ756_spl
<=> relation(relation_composition(sK14_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ756_spl])],[split_symbol_definition]) ).
fof(f10197,plain,
( sQ756_spl
| ~ relation(relation_composition(sK14_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f10195]) ).
fof(f10261,plain,
relation(relation_composition(sK4_skl,sK14_skl)),
inference(resolution,[status(thm)],[f9062,f92]) ).
fof(f10265,plain,
relation(relation_composition(sK14_skl,sK14_skl)),
inference(resolution,[status(thm)],[f9062,f139]) ).
fof(f10268,plain,
( sQ692_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10261,f9814]) ).
fof(f10269,plain,
sQ692_spl,
inference(contradiction_clause,[status(thm)],[f10268]) ).
fof(f10270,plain,
( sQ712_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10265,f9933]) ).
fof(f10271,plain,
sQ712_spl,
inference(contradiction_clause,[status(thm)],[f10270]) ).
fof(f10340,definition,
( sQ772_spl
<=> relation(relation_composition(sK4_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ772_spl])],[split_symbol_definition]) ).
fof(f10342,plain,
( sQ772_spl
| ~ relation(relation_composition(sK4_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f10340]) ).
fof(f10406,plain,
relation(relation_composition(sK4_skl,sK4_skl)),
inference(resolution,[status(thm)],[f9058,f92]) ).
fof(f10407,plain,
relation(relation_composition(sK8_skl,sK4_skl)),
inference(resolution,[status(thm)],[f9058,f105]) ).
fof(f10408,plain,
relation(relation_composition(sK11_skl,sK4_skl)),
inference(resolution,[status(thm)],[f9058,f112]) ).
fof(f10410,plain,
relation(relation_composition(sK14_skl,sK4_skl)),
inference(resolution,[status(thm)],[f9058,f139]) ).
fof(f10411,plain,
relation(relation_composition(sK13_skl,sK4_skl)),
inference(resolution,[status(thm)],[f9058,f137]) ).
fof(f10440,definition,
( sQ788_spl
<=> relation(relation_composition(sK13_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ788_spl])],[split_symbol_definition]) ).
fof(f10442,plain,
( sQ788_spl
| ~ relation(relation_composition(sK13_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f10440]) ).
fof(f10524,definition,
( sQ804_spl
<=> relation(relation_composition(sK11_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ804_spl])],[split_symbol_definition]) ).
fof(f10526,plain,
( sQ804_spl
| ~ relation(relation_composition(sK11_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f10524]) ).
fof(f10620,definition,
( sQ824_spl
<=> relation(relation_composition(sK8_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ824_spl])],[split_symbol_definition]) ).
fof(f10622,plain,
( sQ824_spl
| ~ relation(relation_composition(sK8_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f10620]) ).
fof(f10721,plain,
relation(relation_composition(sK4_skl,sK13_skl)),
inference(resolution,[status(thm)],[f9063,f92]) ).
fof(f10722,plain,
relation(relation_composition(sK8_skl,sK13_skl)),
inference(resolution,[status(thm)],[f9063,f105]) ).
fof(f10723,plain,
relation(relation_composition(sK11_skl,sK13_skl)),
inference(resolution,[status(thm)],[f9063,f112]) ).
fof(f10725,plain,
relation(relation_composition(sK14_skl,sK13_skl)),
inference(resolution,[status(thm)],[f9063,f139]) ).
fof(f10726,plain,
relation(relation_composition(sK13_skl,sK13_skl)),
inference(resolution,[status(thm)],[f9063,f137]) ).
fof(f10728,plain,
( sQ654_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10721,f9602]) ).
fof(f10729,plain,
sQ654_spl,
inference(contradiction_clause,[status(thm)],[f10728]) ).
fof(f10730,plain,
( sQ673_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10725,f9695]) ).
fof(f10731,plain,
sQ673_spl,
inference(contradiction_clause,[status(thm)],[f10730]) ).
fof(f10732,plain,
( sQ631_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10726,f9484]) ).
fof(f10733,plain,
sQ631_spl,
inference(contradiction_clause,[status(thm)],[f10732]) ).
fof(f10958,plain,
( sQ772_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10406,f10342]) ).
fof(f10959,plain,
sQ772_spl,
inference(contradiction_clause,[status(thm)],[f10958]) ).
fof(f11062,plain,
( sQ756_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10410,f10197]) ).
fof(f11063,plain,
sQ756_spl,
inference(contradiction_clause,[status(thm)],[f11062]) ).
fof(f11338,definition,
( sQ919_spl
<=> element(sK5_skl,powerset(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ919_spl])],[split_symbol_definition]) ).
fof(f11340,plain,
( sQ919_spl
| ~ element(sK5_skl,powerset(sK5_skl)) ),
inference(component_clause,[status(thm)],[f11338]) ).
fof(f11342,plain,
( sQ919_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11340,f597]) ).
fof(f11343,plain,
sQ919_spl,
inference(contradiction_clause,[status(thm)],[f11342]) ).
fof(f11364,plain,
( sQ788_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10442,f10411]) ).
fof(f11365,plain,
sQ788_spl,
inference(contradiction_clause,[status(thm)],[f11364]) ).
fof(f11369,plain,
( sQ804_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10526,f10408]) ).
fof(f11370,plain,
sQ804_spl,
inference(contradiction_clause,[status(thm)],[f11369]) ).
fof(f11371,plain,
( sQ824_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10622,f10407]) ).
fof(f11372,plain,
sQ824_spl,
inference(contradiction_clause,[status(thm)],[f11371]) ).
fof(f11957,plain,
( sQ166_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2146,f75]) ).
fof(f11958,plain,
sQ166_spl,
inference(contradiction_clause,[status(thm)],[f11957]) ).
fof(f12021,plain,
( ~ sQ182_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2397,f59]) ).
fof(f12022,plain,
~ sQ182_spl,
inference(contradiction_clause,[status(thm)],[f12021]) ).
fof(f12182,plain,
( ~ sQ546_spl
| $false ),
inference(resolution,[status(thm)],[f8512,f1033]) ).
fof(f12199,plain,
~ sQ546_spl,
inference(contradiction_clause,[status(thm)],[f12182]) ).
fof(f12366,definition,
( sQ989_spl
<=> relation(relation_composition(sK11_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ989_spl])],[split_symbol_definition]) ).
fof(f12368,plain,
( sQ989_spl
| ~ relation(relation_composition(sK11_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f12366]) ).
fof(f12444,plain,
( sQ989_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12368,f10723]) ).
fof(f12445,plain,
sQ989_spl,
inference(contradiction_clause,[status(thm)],[f12444]) ).
fof(f12487,definition,
( sQ1009_spl
<=> relation(relation_composition(sK8_skl,sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1009_spl])],[split_symbol_definition]) ).
fof(f12489,plain,
( sQ1009_spl
| ~ relation(relation_composition(sK8_skl,sK13_skl)) ),
inference(component_clause,[status(thm)],[f12487]) ).
fof(f12565,plain,
( sQ1009_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12489,f10722]) ).
fof(f12566,plain,
sQ1009_spl,
inference(contradiction_clause,[status(thm)],[f12565]) ).
fof(f13007,plain,
( ~ sQ2_spl
| ~ sQ573_spl
| ~ sQ614_spl
| apply(sK13_skl,sK0_skl(sK12_skl(relation_dom(sK14_skl),sK14_skl),relation_dom(sK14_skl),sK13_skl)) = apply(sK14_skl,apply(sK13_skl,sK0_skl(sK12_skl(relation_dom(sK14_skl),sK14_skl),relation_dom(sK14_skl),sK13_skl))) ),
inference(resolution,[status(thm)],[f9313,f9164]) ).
fof(f13017,plain,
( ~ sQ2_spl
| ~ sQ573_spl
| ~ sQ614_spl
| ~ sQ6_spl
| sK12_skl(relation_dom(sK14_skl),sK14_skl) = apply(sK14_skl,apply(sK13_skl,sK0_skl(sK12_skl(relation_dom(sK14_skl),sK14_skl),relation_dom(sK14_skl),sK13_skl))) ),
inference(forward_demodulation,[status(thm)],[f9165,f13007]) ).
fof(f13018,plain,
( ~ sQ2_spl
| ~ sQ573_spl
| ~ sQ614_spl
| ~ sQ6_spl
| sK12_skl(relation_dom(sK14_skl),sK14_skl) = apply(sK14_skl,sK12_skl(relation_dom(sK14_skl),sK14_skl)) ),
inference(forward_demodulation,[status(thm)],[f9165,f13017]) ).
fof(f13019,plain,
( ~ sQ2_spl
| ~ sQ573_spl
| ~ sQ614_spl
| ~ sQ6_spl
| sQ569_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13018,f8856]) ).
fof(f13020,plain,
( ~ sQ2_spl
| ~ sQ573_spl
| ~ sQ614_spl
| ~ sQ6_spl
| sQ569_spl ),
inference(contradiction_clause,[status(thm)],[f13019]) ).
fof(f13021,plain,
$false,
inference(sat_refutation,[status(thm)],[f175,f191,f193,f200,f224,f283,f305,f588,f665,f1192,f1253,f1552,f1739,f1778,f1848,f2085,f2122,f2635,f3515,f3780,f4468,f5870,f6711,f8164,f8166,f8619,f8733,f8735,f8803,f8857,f8878,f8982,f9303,f9912,f10269,f10271,f10729,f10731,f10733,f10959,f11063,f11343,f11365,f11370,f11372,f11958,f12022,f12199,f12445,f12566,f13020]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU012+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n018.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 05:48:58 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 15.14/2.51 % Refutation found
% 15.14/2.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.14/2.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.00/2.57 % Elapsed time: 2.096491 seconds
% 11.00/2.57 % CPU time: 16.100685 seconds
% 11.00/2.57 % Total memory used: 222.454 MB
% 11.00/2.57 % Net memory used: 211.468 MB
%------------------------------------------------------------------------------