%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU009+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:04 PM UTC 2026
% Result : Theorem 0.15s 0.47s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 83
% Syntax : Number of formulae : 348 ( 53 unt; 59 def)
% Number of atoms : 1050 ( 98 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1252 ( 550 ~; 553 |; 67 &)
% ( 65 <=>; 16 =>; 0 <=; 1 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 67 ( 65 usr; 60 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-2 aty)
% Number of variables : 269 ( 252 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(relation_composition(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( ( relation(B)
& empty(A) )
=> ( relation(relation_composition(B,A))
& empty(relation_composition(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( ( function(B)
& relation(B)
& function(A)
& relation(A) )
=> ( function(relation_composition(A,B))
& relation(relation_composition(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_dom(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( empty(A)
=> ( relation(relation_dom(A))
& empty(relation_dom(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A,B] :
( ( relation(B)
& empty(A) )
=> ( relation(relation_composition(A,B))
& empty(relation_composition(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
? [A] :
( relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(relation_composition(C,B)))
<=> ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,conjecture,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(B,relation_dom(relation_composition(C,identity_relation(A))))
<=> ( in(apply(C,B),A)
& in(B,relation_dom(C)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
~ ! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(B,relation_dom(relation_composition(C,identity_relation(A))))
<=> ( in(apply(C,B),A)
& in(B,relation_dom(C)) ) ) ),
inference(negated_conjecture,[status(cth)],[f31]) ).
fof(f34,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f39,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f40,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f41,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f44,plain,
! [A,B] :
( relation(relation_composition(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f45,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f47,plain,
! [A] : element(sK0_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f6]) ).
fof(f48,plain,
! [X0] : element(sK0_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [A,B] :
( ( relation(relation_composition(B,A))
& empty(relation_composition(B,A)) )
| ~ relation(B)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f50,plain,
! [X0,X1] :
( empty(relation_composition(X1,X0))
| ~ relation(X1)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f55,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)],[f9]) ).
fof(f57,plain,
! [X0,X1] :
( function(relation_composition(X0,X1))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f58,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f60,plain,
( ! [A] : function(identity_relation(A))
& ! [A] : relation(identity_relation(A)) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f62,plain,
! [X0] : function(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f65,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f66,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [A] :
( ( relation(relation_dom(A))
& empty(relation_dom(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f68,plain,
! [X0] :
( empty(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0] :
( relation(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f70,plain,
! [A,B] :
( ( relation(relation_composition(A,B))
& empty(relation_composition(A,B)) )
| ~ relation(B)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f71,plain,
! [X0,X1] :
( empty(relation_composition(X0,X1))
| ~ relation(X1)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f73,plain,
( function(sK1_skl)
& relation(sK1_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f17]) ).
fof(f74,plain,
relation(sK1_skl),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
function(sK1_skl),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f76,plain,
( relation(sK2_skl)
& empty(sK2_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f18]) ).
fof(f77,plain,
empty(sK2_skl),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
relation(sK2_skl),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f83,plain,
empty(sK4_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f20]) ).
fof(f84,plain,
empty(sK4_skl),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
( relation(sK5_skl)
& ~ empty(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f21]) ).
fof(f87,plain,
relation(sK5_skl),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f93,plain,
( relation_empty_yielding(sK8_skl)
& relation(sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f24]) ).
fof(f94,plain,
relation(sK8_skl),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f100,plain,
! [A,B] :
( ! [C] :
( ( in(A,relation_dom(relation_composition(C,B)))
<=> ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f101,plain,
! [A,B] :
( ! [C] :
( ( ( ~ in(apply(C,A),relation_dom(B))
| ~ in(A,relation_dom(C))
| in(A,relation_dom(relation_composition(C,B))) )
& ( ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) )
| ~ in(A,relation_dom(relation_composition(C,B))) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f100]) ).
fof(f102,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ~ in(apply(C,A),relation_dom(B))
| ~ in(A,relation_dom(C))
| in(A,relation_dom(relation_composition(C,B))) )
& ! [A] :
( ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) )
| ~ in(A,relation_dom(relation_composition(C,B))) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1,X2] :
( in(X2,relation_dom(X1))
| ~ in(X2,relation_dom(relation_composition(X1,X0)))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
! [X0,X1,X2] :
( in(apply(X1,X2),relation_dom(X0))
| ~ in(X2,relation_dom(relation_composition(X1,X0)))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ~ in(apply(X1,X2),relation_dom(X0))
| ~ in(X2,relation_dom(X1))
| in(X2,relation_dom(relation_composition(X1,X0)))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f106,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f107,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f108,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)],[f29]) ).
fof(f109,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)],[f108]) ).
fof(f110,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)],[f109]) ).
fof(f111,plain,
! [B] :
( ( ! [A] :
( ( apply(B,sK9_skl(A,B)) != sK9_skl(A,B)
& in(sK9_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,[sK9_skl]),skolemize(C,sK9_skl(A,B))],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( relation_dom(X0) = X1
| X0 != identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [X0,X1,X2] :
( apply(X0,X2) = X2
| ~ in(X2,X1)
| X0 != identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f114,plain,
! [X0,X1] :
( in(sK9_skl(X1,X0),X1)
| relation_dom(X0) != X1
| X0 = identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f115,plain,
! [X0,X1] :
( apply(X0,sK9_skl(X1,X0)) != sK9_skl(X1,X0)
| relation_dom(X0) != X1
| X0 = identity_relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f120,plain,
? [A,B,C] :
( ( in(B,relation_dom(relation_composition(C,identity_relation(A))))
<~> ( in(apply(C,B),A)
& in(B,relation_dom(C)) ) )
& function(C)
& relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f121,plain,
? [A,B,C] :
( ( ~ in(apply(C,B),A)
| ~ in(B,relation_dom(C))
| ~ in(B,relation_dom(relation_composition(C,identity_relation(A)))) )
& ( ( in(apply(C,B),A)
& in(B,relation_dom(C)) )
| in(B,relation_dom(relation_composition(C,identity_relation(A)))) )
& function(C)
& relation(C) ),
inference(NNF_transformation,[status(thm)],[f120]) ).
fof(f122,plain,
? [C] :
( ? [A,B] :
( ( ~ in(apply(C,B),A)
| ~ in(B,relation_dom(C))
| ~ in(B,relation_dom(relation_composition(C,identity_relation(A)))) )
& ( ( in(apply(C,B),A)
& in(B,relation_dom(C)) )
| in(B,relation_dom(relation_composition(C,identity_relation(A)))) ) )
& function(C)
& relation(C) ),
inference(miniscoping,[status(thm)],[f121]) ).
fof(f123,plain,
( ( ~ in(apply(sK10_skl,sK12_skl),sK11_skl)
| ~ in(sK12_skl,relation_dom(sK10_skl))
| ~ in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl)))) )
& ( ( in(apply(sK10_skl,sK12_skl),sK11_skl)
& in(sK12_skl,relation_dom(sK10_skl)) )
| in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl)))) )
& function(sK10_skl)
& relation(sK10_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(C,sK10_skl),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f122]) ).
fof(f124,plain,
relation(sK10_skl),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
function(sK10_skl),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f126,plain,
( in(sK12_skl,relation_dom(sK10_skl))
| in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl)))) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f127,plain,
( in(apply(sK10_skl,sK12_skl),sK11_skl)
| in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl)))) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f128,plain,
( ~ in(apply(sK10_skl,sK12_skl),sK11_skl)
| ~ in(sK12_skl,relation_dom(sK10_skl))
| ~ in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl)))) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f132,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f133,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f132]) ).
fof(f134,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f136,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f137,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f138,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f139,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f143,definition,
( sQ0_spl
<=> in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f144,plain,
( ~ sQ0_spl
| in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl)))) ),
inference(component_clause,[status(thm)],[f143]) ).
fof(f146,definition,
( sQ1_spl
<=> in(sK12_skl,relation_dom(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f147,plain,
( ~ sQ1_spl
| in(sK12_skl,relation_dom(sK10_skl)) ),
inference(component_clause,[status(thm)],[f146]) ).
fof(f149,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f126,f143,f146]) ).
fof(f150,definition,
( sQ2_spl
<=> in(apply(sK10_skl,sK12_skl),sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f151,plain,
( ~ sQ2_spl
| in(apply(sK10_skl,sK12_skl),sK11_skl) ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f152,plain,
( sQ2_spl
| ~ in(apply(sK10_skl,sK12_skl),sK11_skl) ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f153,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f127,f143,f150]) ).
fof(f154,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f128,f143,f146,f150]) ).
fof(f155,plain,
! [X0] :
( relation_dom(identity_relation(X0)) = X0
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f112]) ).
fof(f156,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)],[f113]) ).
fof(f157,plain,
! [X0] :
( in(sK9_skl(relation_dom(X0),X0),relation_dom(X0))
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f114]) ).
fof(f158,plain,
! [X0] :
( apply(X0,sK9_skl(relation_dom(X0),X0)) != sK9_skl(relation_dom(X0),X0)
| X0 = identity_relation(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f115]) ).
fof(f162,plain,
! [X0] :
( empty(relation_composition(X0,sK2_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f77,f50]) ).
fof(f165,plain,
! [X0,X1] :
( ~ in(X1,relation_dom(X0))
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f68,f139]) ).
fof(f166,plain,
( ~ sQ0_spl
| ~ empty(relation_composition(sK10_skl,identity_relation(sK11_skl))) ),
inference(resolution,[status(thm)],[f165,f144]) ).
fof(f170,plain,
! [X0,X1] :
( ~ in(X1,relation_composition(X0,sK2_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f162,f139]) ).
fof(f172,plain,
! [X0] :
( empty(relation_composition(X0,sK4_skl))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f84,f50]) ).
fof(f174,plain,
( ~ sQ0_spl
| ~ relation(identity_relation(sK11_skl))
| ~ empty(sK10_skl) ),
inference(resolution,[status(thm)],[f71,f166]) ).
fof(f177,definition,
( sQ3_spl
<=> empty(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f180,definition,
( sQ4_spl
<=> relation(identity_relation(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f182,plain,
( sQ4_spl
| ~ relation(identity_relation(sK11_skl)) ),
inference(component_clause,[status(thm)],[f180]) ).
fof(f183,plain,
( ~ sQ0_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f174,f177,f180,f143]) ).
fof(f186,plain,
( ~ sQ0_spl
| in(sK12_skl,relation_dom(sK10_skl))
| ~ function(sK10_skl)
| ~ relation(sK10_skl)
| ~ function(identity_relation(sK11_skl))
| ~ relation(identity_relation(sK11_skl)) ),
inference(resolution,[status(thm)],[f103,f144]) ).
fof(f187,definition,
( sQ5_spl
<=> function(identity_relation(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f189,plain,
( sQ5_spl
| ~ function(identity_relation(sK11_skl)) ),
inference(component_clause,[status(thm)],[f187]) ).
fof(f190,definition,
( sQ6_spl
<=> relation(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( sQ6_spl
| ~ relation(sK10_skl) ),
inference(component_clause,[status(thm)],[f190]) ).
fof(f193,definition,
( sQ7_spl
<=> function(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f195,plain,
( sQ7_spl
| ~ function(sK10_skl) ),
inference(component_clause,[status(thm)],[f193]) ).
fof(f196,plain,
( ~ sQ0_spl
| sQ1_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f186,f180,f187,f190,f193,f146,f143]) ).
fof(f197,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f182,f46]) ).
fof(f198,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f197]) ).
fof(f199,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f195,f125]) ).
fof(f200,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f199]) ).
fof(f201,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f189,f62]) ).
fof(f202,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f201]) ).
fof(f203,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192,f124]) ).
fof(f204,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f203]) ).
fof(f211,plain,
sK4_skl = empty_set,
inference(resolution,[status(thm)],[f136,f84]) ).
fof(f212,plain,
! [X0] :
( ~ relation(X0)
| relation_composition(X0,sK4_skl) = empty_set ),
inference(resolution,[status(thm)],[f136,f172]) ).
fof(f215,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ empty(X0)
| relation_composition(X0,X1) = empty_set ),
inference(resolution,[status(thm)],[f136,f71]) ).
fof(f216,plain,
! [X0] :
( ~ empty(X0)
| relation_dom(X0) = empty_set ),
inference(resolution,[status(thm)],[f136,f68]) ).
fof(f217,plain,
sK2_skl = empty_set,
inference(resolution,[status(thm)],[f136,f77]) ).
fof(f226,plain,
sK2_skl = empty_set,
inference(backward_demodulation,[status(thm)],[f230,f211]) ).
fof(f230,plain,
sK2_skl = sK4_skl,
inference(forward_demodulation,[status(thm)],[f211,f217]) ).
fof(f237,plain,
! [X0] :
( ~ empty(X0)
| relation_dom(X0) = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f226,f216]) ).
fof(f241,plain,
relation_dom(sK2_skl) = sK2_skl,
inference(resolution,[status(thm)],[f237,f77]) ).
fof(f242,plain,
! [X0,X1] :
( ~ in(apply(X0,X1),sK2_skl)
| ~ in(X1,relation_dom(X0))
| in(X1,relation_dom(relation_composition(X0,sK2_skl)))
| ~ function(X0)
| ~ relation(X0)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f241,f105]) ).
fof(f245,plain,
( relation(sK2_skl)
| ~ empty(sK2_skl) ),
inference(paramodulation,[status(thm)],[f241,f69]) ).
fof(f247,definition,
( sQ8_spl
<=> relation(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f250,definition,
( sQ9_spl
<=> function(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f251,plain,
( ~ sQ9_spl
| function(sK2_skl) ),
inference(component_clause,[status(thm)],[f250]) ).
fof(f252,plain,
( sQ9_spl
| ~ function(sK2_skl) ),
inference(component_clause,[status(thm)],[f250]) ).
fof(f253,definition,
! [X0,X1] :
( sQ10_spl
<=> ( ~ in(apply(X0,X1),sK2_skl)
| ~ in(X1,relation_dom(X0))
| in(X1,relation_dom(relation_composition(X0,sK2_skl)))
| ~ function(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f242,f247,f250,f253]) ).
fof(f257,definition,
( sQ11_spl
<=> empty(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f259,plain,
( sQ11_spl
| ~ empty(sK2_skl) ),
inference(component_clause,[status(thm)],[f257]) ).
fof(f261,definition,
! [X0] :
( sQ12_spl
<=> ~ in(X0,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f265,plain,
( sQ8_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f245,f257,f247]) ).
fof(f267,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f259,f77]) ).
fof(f268,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f267]) ).
fof(f269,plain,
! [X0] :
( relation_dom(identity_relation(X0)) = X0
| ~ function(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f155,f46]) ).
fof(f270,plain,
! [X0] : relation_dom(identity_relation(X0)) = X0,
inference(resolution,[status(thm)],[f269,f62]) ).
fof(f272,plain,
( sQ9_spl
| ~ empty(sK2_skl) ),
inference(resolution,[status(thm)],[f252,f41]) ).
fof(f273,plain,
( sQ9_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f272,f257,f250]) ).
fof(f275,plain,
! [X0,X1,X2] :
( ~ in(apply(X1,X2),X0)
| ~ in(X2,relation_dom(X1))
| in(X2,relation_dom(relation_composition(X1,identity_relation(X0))))
| ~ function(X1)
| ~ relation(X1)
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f270,f105]) ).
fof(f276,plain,
! [X0] :
( ~ empty(X0)
| ~ relation(identity_relation(X0))
| empty(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f270,f66]) ).
fof(f278,plain,
! [X0] :
( relation(X0)
| ~ empty(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f270,f69]) ).
fof(f280,plain,
! [X0,X1,X2] :
( ~ in(apply(X1,X2),X0)
| ~ in(X2,relation_dom(X1))
| in(X2,relation_dom(relation_composition(X1,identity_relation(X0))))
| ~ function(X1)
| ~ relation(X1)
| ~ function(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f275,f46]) ).
fof(f281,plain,
! [X0] :
( ~ empty(X0)
| empty(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f276,f46]) ).
fof(f282,plain,
! [X0] :
( relation_dom(identity_relation(X0)) = sK2_skl
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f281,f237]) ).
fof(f285,plain,
! [X0] :
( X0 = sK2_skl
| ~ empty(X0) ),
inference(forward_demodulation,[status(thm)],[f270,f282]) ).
fof(f286,plain,
! [X0] :
( ~ empty(X0)
| identity_relation(X0) = sK2_skl ),
inference(resolution,[status(thm)],[f285,f281]) ).
fof(f291,plain,
! [X0,X1] :
( apply(identity_relation(X0),X1) = X1
| ~ in(X1,X0)
| ~ function(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f156,f46]) ).
fof(f292,plain,
! [X0,X1] :
( apply(identity_relation(X1),X0) = X0
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f291,f62]) ).
fof(f312,plain,
identity_relation(sK2_skl) = sK2_skl,
inference(resolution,[status(thm)],[f286,f77]) ).
fof(f314,plain,
! [X0] :
( apply(identity_relation(sK2_skl),X0) = X0
| ~ in(X0,sK2_skl)
| ~ function(sK2_skl) ),
inference(paramodulation,[status(thm)],[f312,f291]) ).
fof(f320,definition,
! [X0] :
( sQ13_spl
<=> ( apply(identity_relation(sK2_skl),X0) = X0
| ~ in(X0,sK2_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f323,plain,
( sQ13_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f314,f250,f320]) ).
fof(f333,plain,
! [X0] :
( in(sK0_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f107,f48]) ).
fof(f339,plain,
( ~ sQ9_spl
| in(sK9_skl(relation_dom(sK2_skl),sK2_skl),relation_dom(sK2_skl))
| sK2_skl = identity_relation(relation_dom(sK2_skl))
| ~ relation(sK2_skl) ),
inference(resolution,[status(thm)],[f157,f251]) ).
fof(f340,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| in(sK9_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)),relation_dom(relation_composition(X0,X1)))
| relation_composition(X0,X1) = identity_relation(relation_dom(relation_composition(X0,X1)))
| ~ relation(relation_composition(X0,X1)) ),
inference(resolution,[status(thm)],[f157,f57]) ).
fof(f343,plain,
( in(sK9_skl(relation_dom(sK10_skl),sK10_skl),relation_dom(sK10_skl))
| sK10_skl = identity_relation(relation_dom(sK10_skl))
| ~ relation(sK10_skl) ),
inference(resolution,[status(thm)],[f157,f125]) ).
fof(f345,definition,
( sQ14_spl
<=> sK2_skl = identity_relation(relation_dom(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f348,definition,
( sQ15_spl
<=> in(sK9_skl(relation_dom(sK2_skl),sK2_skl),relation_dom(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( ~ sQ9_spl
| sQ15_spl
| sQ14_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f339,f247,f345,f348,f250]) ).
fof(f352,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| in(sK9_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)),relation_dom(relation_composition(X0,X1)))
| relation_composition(X0,X1) = identity_relation(relation_dom(relation_composition(X0,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f340,f45]) ).
fof(f353,definition,
( sQ16_spl
<=> relation(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f355,plain,
( sQ16_spl
| ~ relation(sK1_skl) ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f363,definition,
( sQ19_spl
<=> sK10_skl = identity_relation(relation_dom(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f364,plain,
( ~ sQ19_spl
| sK10_skl = identity_relation(relation_dom(sK10_skl)) ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f366,definition,
( sQ20_spl
<=> in(sK9_skl(relation_dom(sK10_skl),sK10_skl),relation_dom(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f369,plain,
( sQ20_spl
| sQ19_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f343,f190,f363,f366]) ).
fof(f373,plain,
( apply(sK2_skl,sK9_skl(sK2_skl,sK2_skl)) != sK9_skl(relation_dom(sK2_skl),sK2_skl)
| sK2_skl = identity_relation(relation_dom(sK2_skl))
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f241,f158]) ).
fof(f374,definition,
( sQ21_spl
<=> apply(sK2_skl,sK9_skl(sK2_skl,sK2_skl)) = sK9_skl(relation_dom(sK2_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( ~ sQ21_spl
| sQ14_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f373,f247,f250,f345,f374]) ).
fof(f382,plain,
! [X0] :
( ~ sQ19_spl
| apply(identity_relation(relation_dom(sK10_skl)),X0) = X0
| ~ in(X0,relation_dom(sK10_skl))
| ~ function(sK10_skl) ),
inference(paramodulation,[status(thm)],[f364,f291]) ).
fof(f383,plain,
( ~ sQ19_spl
| ~ empty(relation_dom(sK10_skl))
| empty(sK10_skl) ),
inference(paramodulation,[status(thm)],[f364,f281]) ).
fof(f387,definition,
( sQ22_spl
<=> empty(relation_dom(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f394,definition,
! [X0] :
( sQ24_spl
<=> ~ in(X0,relation_dom(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f395,plain,
! [X0] :
( ~ sQ24_spl
| ~ in(X0,relation_dom(sK10_skl)) ),
inference(component_clause,[status(thm)],[f394]) ).
fof(f399,definition,
! [X0] :
( sQ25_spl
<=> ( apply(identity_relation(relation_dom(sK10_skl)),X0) = X0
| ~ in(X0,relation_dom(sK10_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f402,plain,
( ~ sQ19_spl
| sQ25_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f382,f193,f399,f363]) ).
fof(f403,plain,
( ~ sQ19_spl
| ~ sQ22_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f383,f177,f387,f363]) ).
fof(f404,plain,
( ~ sQ1_spl
| ~ sQ24_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f147,f395]) ).
fof(f405,plain,
( ~ sQ1_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f404]) ).
fof(f408,plain,
! [X0] :
( ~ relation(X0)
| relation_composition(X0,sK2_skl) = empty_set ),
inference(forward_demodulation,[status(thm)],[f230,f212]) ).
fof(f409,plain,
! [X0] :
( ~ relation(X0)
| relation_composition(X0,sK2_skl) = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f226,f408]) ).
fof(f410,plain,
relation_composition(sK8_skl,sK2_skl) = sK2_skl,
inference(resolution,[status(thm)],[f409,f94]) ).
fof(f411,plain,
relation_composition(sK5_skl,sK2_skl) = sK2_skl,
inference(resolution,[status(thm)],[f409,f87]) ).
fof(f412,plain,
relation_composition(sK2_skl,sK2_skl) = sK2_skl,
inference(resolution,[status(thm)],[f409,f78]) ).
fof(f414,plain,
relation_composition(sK1_skl,sK2_skl) = sK2_skl,
inference(resolution,[status(thm)],[f409,f74]) ).
fof(f418,plain,
! [X0] : relation_composition(identity_relation(X0),sK2_skl) = sK2_skl,
inference(resolution,[status(thm)],[f409,f46]) ).
fof(f419,plain,
relation_composition(sK10_skl,sK2_skl) = sK2_skl,
inference(resolution,[status(thm)],[f409,f124]) ).
fof(f420,plain,
! [X0] :
( ~ empty(identity_relation(X0))
| relation_composition(X0,sK2_skl) = sK2_skl ),
inference(resolution,[status(thm)],[f409,f278]) ).
fof(f423,plain,
! [X0] :
( in(apply(sK8_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK8_skl)
| ~ relation(sK8_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f410,f104]) ).
fof(f424,plain,
! [X0] :
( in(X0,relation_dom(sK8_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK8_skl)
| ~ relation(sK8_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f410,f103]) ).
fof(f430,definition,
( sQ26_spl
<=> relation(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f432,plain,
( sQ26_spl
| ~ relation(sK8_skl) ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f434,definition,
( sQ27_spl
<=> function(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f437,definition,
! [X0] :
( sQ28_spl
<=> ( in(apply(sK8_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f440,plain,
( sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f423,f247,f250,f430,f434,f437]) ).
fof(f441,definition,
! [X0] :
( sQ29_spl
<=> ( in(X0,relation_dom(sK8_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( sQ29_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f424,f247,f250,f430,f434,f441]) ).
fof(f453,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f432,f94]) ).
fof(f454,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f453]) ).
fof(f469,plain,
! [X0] :
( in(apply(sK5_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK5_skl)
| ~ relation(sK5_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f411,f104]) ).
fof(f470,plain,
! [X0] :
( in(X0,relation_dom(sK5_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK5_skl)
| ~ relation(sK5_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f411,f103]) ).
fof(f476,definition,
( sQ31_spl
<=> relation(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f478,plain,
( sQ31_spl
| ~ relation(sK5_skl) ),
inference(component_clause,[status(thm)],[f476]) ).
fof(f484,definition,
( sQ33_spl
<=> function(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f487,definition,
! [X0] :
( sQ34_spl
<=> ( in(apply(sK5_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f490,plain,
( sQ34_spl
| ~ sQ33_spl
| ~ sQ31_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f469,f247,f250,f476,f484,f487]) ).
fof(f491,definition,
! [X0] :
( sQ35_spl
<=> ( in(X0,relation_dom(sK5_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( sQ35_spl
| ~ sQ33_spl
| ~ sQ31_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f470,f247,f250,f476,f484,f491]) ).
fof(f500,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f87]) ).
fof(f501,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f500]) ).
fof(f508,plain,
! [X0] :
( in(apply(sK2_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK2_skl)
| ~ relation(sK2_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f412,f104]) ).
fof(f509,plain,
! [X0] :
( in(X0,relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK2_skl)
| ~ relation(sK2_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f412,f103]) ).
fof(f517,definition,
! [X0] :
( sQ36_spl
<=> ( in(apply(sK2_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( sQ36_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f508,f247,f250,f517]) ).
fof(f521,definition,
! [X0] :
( sQ37_spl
<=> ( in(X0,relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f524,plain,
( sQ37_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f509,f247,f250,f521]) ).
fof(f534,plain,
! [X0] :
( in(apply(sK1_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK1_skl)
| ~ relation(sK1_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f414,f104]) ).
fof(f535,plain,
! [X0] :
( in(X0,relation_dom(sK1_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK1_skl)
| ~ relation(sK1_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f414,f103]) ).
fof(f546,definition,
( sQ39_spl
<=> function(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f548,plain,
( sQ39_spl
| ~ function(sK1_skl) ),
inference(component_clause,[status(thm)],[f546]) ).
fof(f549,definition,
! [X0] :
( sQ40_spl
<=> ( in(apply(sK1_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( sQ40_spl
| ~ sQ39_spl
| ~ sQ16_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f534,f247,f250,f353,f546,f549]) ).
fof(f553,definition,
! [X0] :
( sQ41_spl
<=> ( in(X0,relation_dom(sK1_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f556,plain,
( sQ41_spl
| ~ sQ39_spl
| ~ sQ16_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f535,f247,f250,f353,f546,f553]) ).
fof(f562,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f355,f74]) ).
fof(f563,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f562]) ).
fof(f564,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f548,f75]) ).
fof(f565,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f564]) ).
fof(f571,plain,
! [X0] :
( in(apply(sK10_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK10_skl)
| ~ relation(sK10_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f419,f104]) ).
fof(f572,plain,
! [X0] :
( in(X0,relation_dom(sK10_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK10_skl)
| ~ relation(sK10_skl)
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f419,f103]) ).
fof(f580,definition,
! [X0] :
( sQ42_spl
<=> ( in(apply(sK10_skl,X0),relation_dom(sK2_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f583,plain,
( sQ42_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f571,f247,f250,f190,f193,f580]) ).
fof(f584,definition,
! [X0] :
( sQ43_spl
<=> ( in(X0,relation_dom(sK10_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f587,plain,
( sQ43_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f572,f247,f250,f190,f193,f584]) ).
fof(f640,plain,
! [X0,X1] :
( in(apply(identity_relation(X0),X1),relation_dom(sK2_skl))
| ~ in(X1,relation_dom(sK2_skl))
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0))
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f418,f104]) ).
fof(f641,plain,
! [X0,X1] :
( in(X1,relation_dom(identity_relation(X0)))
| ~ in(X1,relation_dom(sK2_skl))
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0))
| ~ function(sK2_skl)
| ~ relation(sK2_skl) ),
inference(paramodulation,[status(thm)],[f418,f103]) ).
fof(f647,definition,
! [X0] :
( sQ48_spl
<=> ~ relation(identity_relation(X0)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f648,plain,
! [X0] :
( ~ sQ48_spl
| ~ relation(identity_relation(X0)) ),
inference(component_clause,[status(thm)],[f647]) ).
fof(f655,definition,
! [X0,X1] :
( sQ50_spl
<=> ( in(apply(identity_relation(X0),X1),relation_dom(sK2_skl))
| ~ in(X1,relation_dom(sK2_skl))
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f658,plain,
( sQ50_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f640,f247,f250,f655]) ).
fof(f659,definition,
! [X0,X1] :
( sQ51_spl
<=> ( in(X1,relation_dom(identity_relation(X0)))
| ~ in(X1,relation_dom(sK2_skl))
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f662,plain,
( sQ51_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f641,f247,f250,f659]) ).
fof(f685,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ empty(X0)
| relation_composition(X0,X1) = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f226,f215]) ).
fof(f690,plain,
! [X0] :
( ~ relation(X0)
| relation_composition(sK2_skl,X0) = sK2_skl ),
inference(resolution,[status(thm)],[f685,f77]) ).
fof(f697,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ element(X0,powerset(X1))
| empty(X0) ),
inference(resolution,[status(thm)],[f333,f134]) ).
fof(f698,plain,
! [X0] :
( ~ in(X0,sK0_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f333,f39]) ).
fof(f736,plain,
( ~ sQ1_spl
| apply(identity_relation(relation_dom(sK10_skl)),sK12_skl) = sK12_skl ),
inference(resolution,[status(thm)],[f292,f147]) ).
fof(f751,plain,
relation_composition(sK2_skl,sK8_skl) = sK2_skl,
inference(resolution,[status(thm)],[f690,f94]) ).
fof(f752,plain,
relation_composition(sK2_skl,sK5_skl) = sK2_skl,
inference(resolution,[status(thm)],[f690,f87]) ).
fof(f755,plain,
relation_composition(sK2_skl,sK1_skl) = sK2_skl,
inference(resolution,[status(thm)],[f690,f74]) ).
fof(f759,plain,
! [X0] : relation_composition(sK2_skl,identity_relation(X0)) = sK2_skl,
inference(resolution,[status(thm)],[f690,f46]) ).
fof(f760,plain,
relation_composition(sK2_skl,sK10_skl) = sK2_skl,
inference(resolution,[status(thm)],[f690,f124]) ).
fof(f764,plain,
! [X0] :
( in(apply(sK2_skl,X0),relation_dom(sK8_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK2_skl)
| ~ relation(sK2_skl)
| ~ function(sK8_skl)
| ~ relation(sK8_skl) ),
inference(paramodulation,[status(thm)],[f751,f104]) ).
fof(f772,definition,
! [X0] :
( sQ53_spl
<=> ( in(apply(sK2_skl,X0),relation_dom(sK8_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f775,plain,
( sQ53_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f764,f430,f434,f247,f250,f772]) ).
fof(f783,plain,
! [X0] :
( in(apply(sK2_skl,X0),relation_dom(sK5_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK2_skl)
| ~ relation(sK2_skl)
| ~ function(sK5_skl)
| ~ relation(sK5_skl) ),
inference(paramodulation,[status(thm)],[f752,f104]) ).
fof(f791,definition,
! [X0] :
( sQ54_spl
<=> ( in(apply(sK2_skl,X0),relation_dom(sK5_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f794,plain,
( sQ54_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ33_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f783,f476,f484,f247,f250,f791]) ).
fof(f802,plain,
! [X0] :
( in(apply(sK2_skl,X0),relation_dom(sK1_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK2_skl)
| ~ relation(sK2_skl)
| ~ function(sK1_skl)
| ~ relation(sK1_skl) ),
inference(paramodulation,[status(thm)],[f755,f104]) ).
fof(f810,definition,
! [X0] :
( sQ55_spl
<=> ( in(apply(sK2_skl,X0),relation_dom(sK1_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f813,plain,
( sQ55_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ39_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f802,f353,f546,f247,f250,f810]) ).
fof(f822,plain,
! [X0] :
( in(apply(sK2_skl,X0),relation_dom(sK10_skl))
| ~ in(X0,relation_dom(sK2_skl))
| ~ function(sK2_skl)
| ~ relation(sK2_skl)
| ~ function(sK10_skl)
| ~ relation(sK10_skl) ),
inference(paramodulation,[status(thm)],[f760,f104]) ).
fof(f830,definition,
! [X0] :
( sQ56_spl
<=> ( in(apply(sK2_skl,X0),relation_dom(sK10_skl))
| ~ in(X0,relation_dom(sK2_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f833,plain,
( sQ56_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f822,f190,f193,f247,f250,f830]) ).
fof(f844,plain,
! [X0,X1] :
( in(apply(sK2_skl,X1),relation_dom(identity_relation(X0)))
| ~ in(X1,relation_dom(sK2_skl))
| ~ function(sK2_skl)
| ~ relation(sK2_skl)
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f759,f104]) ).
fof(f852,definition,
! [X0,X1] :
( sQ57_spl
<=> ( in(apply(sK2_skl,X1),relation_dom(identity_relation(X0)))
| ~ in(X1,relation_dom(sK2_skl))
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f855,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f844,f852,f247,f250]) ).
fof(f864,plain,
! [X0] :
( ~ sQ9_spl
| ~ relation(sK2_skl)
| ~ function(X0)
| ~ relation(X0)
| in(sK9_skl(relation_dom(relation_composition(X0,sK2_skl)),relation_composition(X0,sK2_skl)),relation_dom(relation_composition(X0,sK2_skl)))
| relation_composition(X0,sK2_skl) = identity_relation(relation_dom(relation_composition(X0,sK2_skl))) ),
inference(resolution,[status(thm)],[f352,f251]) ).
fof(f866,plain,
! [X0] :
( ~ relation(sK1_skl)
| ~ function(X0)
| ~ relation(X0)
| in(sK9_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl)),relation_dom(relation_composition(X0,sK1_skl)))
| relation_composition(X0,sK1_skl) = identity_relation(relation_dom(relation_composition(X0,sK1_skl))) ),
inference(resolution,[status(thm)],[f352,f75]) ).
fof(f868,plain,
! [X0] :
( ~ relation(sK10_skl)
| ~ function(X0)
| ~ relation(X0)
| in(sK9_skl(relation_dom(relation_composition(X0,sK10_skl)),relation_composition(X0,sK10_skl)),relation_dom(relation_composition(X0,sK10_skl)))
| relation_composition(X0,sK10_skl) = identity_relation(relation_dom(relation_composition(X0,sK10_skl))) ),
inference(resolution,[status(thm)],[f352,f125]) ).
fof(f870,definition,
! [X0] :
( sQ58_spl
<=> ( ~ function(X0)
| ~ relation(X0)
| in(sK9_skl(relation_dom(relation_composition(X0,sK2_skl)),relation_composition(X0,sK2_skl)),relation_dom(relation_composition(X0,sK2_skl)))
| relation_composition(X0,sK2_skl) = identity_relation(relation_dom(relation_composition(X0,sK2_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f873,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f864,f870,f247,f250]) ).
fof(f875,definition,
! [X0] :
( sQ59_spl
<=> ( ~ function(X0)
| ~ relation(X0)
| in(sK9_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl)),relation_dom(relation_composition(X0,sK1_skl)))
| relation_composition(X0,sK1_skl) = identity_relation(relation_dom(relation_composition(X0,sK1_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f878,plain,
( ~ sQ16_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f866,f875,f353]) ).
fof(f880,definition,
! [X0] :
( sQ60_spl
<=> ( ~ function(X0)
| ~ relation(X0)
| in(sK9_skl(relation_dom(relation_composition(X0,sK10_skl)),relation_composition(X0,sK10_skl)),relation_dom(relation_composition(X0,sK10_skl)))
| relation_composition(X0,sK10_skl) = identity_relation(relation_dom(relation_composition(X0,sK10_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f883,plain,
( ~ sQ6_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f868,f880,f190]) ).
fof(f900,plain,
! [X0] :
( ~ in(X0,sK2_skl)
| ~ relation(sK10_skl) ),
inference(paramodulation,[status(thm)],[f419,f170]) ).
fof(f906,plain,
( sQ12_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f900,f190,f261]) ).
fof(f944,plain,
! [X0] :
( ~ sQ1_spl
| ~ in(sK12_skl,relation_dom(X0))
| ~ in(sK12_skl,relation_dom(identity_relation(relation_dom(sK10_skl))))
| in(sK12_skl,relation_dom(relation_composition(identity_relation(relation_dom(sK10_skl)),X0)))
| ~ function(identity_relation(relation_dom(sK10_skl)))
| ~ relation(identity_relation(relation_dom(sK10_skl)))
| ~ function(X0)
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f736,f105]) ).
fof(f945,definition,
! [X0] :
( sQ61_spl
<=> ( ~ in(sK12_skl,relation_dom(X0))
| in(sK12_skl,relation_dom(relation_composition(identity_relation(relation_dom(sK10_skl)),X0)))
| ~ function(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f948,definition,
( sQ62_spl
<=> relation(identity_relation(relation_dom(sK10_skl))) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( sQ62_spl
| ~ relation(identity_relation(relation_dom(sK10_skl))) ),
inference(component_clause,[status(thm)],[f948]) ).
fof(f951,definition,
( sQ63_spl
<=> function(identity_relation(relation_dom(sK10_skl))) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f953,plain,
( sQ63_spl
| ~ function(identity_relation(relation_dom(sK10_skl))) ),
inference(component_clause,[status(thm)],[f951]) ).
fof(f954,definition,
( sQ64_spl
<=> in(sK12_skl,relation_dom(identity_relation(relation_dom(sK10_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f956,plain,
( sQ64_spl
| ~ in(sK12_skl,relation_dom(identity_relation(relation_dom(sK10_skl)))) ),
inference(component_clause,[status(thm)],[f954]) ).
fof(f957,plain,
( ~ sQ1_spl
| ~ sQ64_spl
| ~ sQ63_spl
| ~ sQ62_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f944,f945,f948,f951,f954,f146]) ).
fof(f958,plain,
( ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f648,f46]) ).
fof(f959,plain,
~ sQ48_spl,
inference(contradiction_clause,[status(thm)],[f958]) ).
fof(f960,plain,
( sQ64_spl
| ~ in(sK12_skl,relation_dom(sK10_skl)) ),
inference(forward_demodulation,[status(thm)],[f270,f956]) ).
fof(f961,plain,
( sQ64_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f960,f147]) ).
fof(f962,plain,
( sQ64_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f961]) ).
fof(f963,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f953,f62]) ).
fof(f964,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f963]) ).
fof(f1024,plain,
( ~ empty(sK2_skl)
| relation_composition(sK2_skl,sK2_skl) = sK2_skl ),
inference(paramodulation,[status(thm)],[f312,f420]) ).
fof(f1029,definition,
( sQ66_spl
<=> relation_composition(sK2_skl,sK2_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1032,plain,
( ~ sQ11_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1024,f1029,f257]) ).
fof(f1045,plain,
! [X0] :
( ~ element(X0,powerset(sK2_skl))
| empty(X0) ),
inference(resolution,[status(thm)],[f697,f77]) ).
fof(f1048,plain,
empty(sK0_skl(powerset(sK2_skl))),
inference(resolution,[status(thm)],[f1045,f48]) ).
fof(f1075,plain,
sK0_skl(powerset(sK2_skl)) = sK2_skl,
inference(resolution,[status(thm)],[f1048,f285]) ).
fof(f1082,plain,
( ~ in(powerset(sK2_skl),sK2_skl)
| empty(powerset(sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1075,f698]) ).
fof(f1083,plain,
( in(sK2_skl,powerset(sK2_skl))
| empty(powerset(sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1075,f333]) ).
fof(f1085,definition,
( sQ68_spl
<=> empty(powerset(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1086,plain,
( ~ sQ68_spl
| empty(powerset(sK2_skl)) ),
inference(component_clause,[status(thm)],[f1085]) ).
fof(f1088,definition,
( sQ69_spl
<=> in(powerset(sK2_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1091,plain,
( ~ sQ69_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1082,f1085,f1088]) ).
fof(f1092,definition,
( sQ70_spl
<=> in(sK2_skl,powerset(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1095,plain,
( sQ70_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1083,f1085,f1092]) ).
fof(f1096,plain,
( ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1086,f58]) ).
fof(f1097,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f1096]) ).
fof(f1099,plain,
! [X0,X1,X2] :
( ~ in(apply(X0,X1),X2)
| ~ in(X1,relation_dom(X0))
| in(X1,relation_dom(relation_composition(X0,identity_relation(X2))))
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f280,f62]) ).
fof(f1100,plain,
( ~ sQ2_spl
| ~ in(sK12_skl,relation_dom(sK10_skl))
| in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl))))
| ~ function(sK10_skl)
| ~ relation(sK10_skl) ),
inference(resolution,[status(thm)],[f1099,f151]) ).
fof(f1102,plain,
! [X0] :
( ~ sQ1_spl
| ~ in(sK12_skl,X0)
| ~ in(sK12_skl,relation_dom(identity_relation(relation_dom(sK10_skl))))
| in(sK12_skl,relation_dom(relation_composition(identity_relation(relation_dom(sK10_skl)),identity_relation(X0))))
| ~ function(identity_relation(relation_dom(sK10_skl)))
| ~ relation(identity_relation(relation_dom(sK10_skl))) ),
inference(paramodulation,[status(thm)],[f736,f1099]) ).
fof(f1104,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ0_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1100,f190,f193,f143,f146,f150]) ).
fof(f1105,definition,
! [X0] :
( sQ71_spl
<=> ( ~ in(sK12_skl,X0)
| in(sK12_skl,relation_dom(relation_composition(identity_relation(relation_dom(sK10_skl)),identity_relation(X0)))) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1108,plain,
( ~ sQ1_spl
| ~ sQ64_spl
| sQ71_spl
| ~ sQ63_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f1102,f948,f951,f1105,f954,f146]) ).
fof(f1111,plain,
( sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f950,f46]) ).
fof(f1112,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f1111]) ).
fof(f1113,plain,
( ~ sQ0_spl
| in(apply(sK10_skl,sK12_skl),relation_dom(identity_relation(sK11_skl)))
| ~ function(sK10_skl)
| ~ relation(sK10_skl)
| ~ function(identity_relation(sK11_skl))
| ~ relation(identity_relation(sK11_skl)) ),
inference(resolution,[status(thm)],[f144,f104]) ).
fof(f1119,definition,
( sQ72_spl
<=> in(apply(sK10_skl,sK12_skl),relation_dom(identity_relation(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1120,plain,
( ~ sQ72_spl
| in(apply(sK10_skl,sK12_skl),relation_dom(identity_relation(sK11_skl))) ),
inference(component_clause,[status(thm)],[f1119]) ).
fof(f1122,plain,
( ~ sQ0_spl
| sQ72_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1113,f180,f187,f190,f193,f1119,f143]) ).
fof(f1124,plain,
( ~ sQ72_spl
| in(apply(sK10_skl,sK12_skl),sK11_skl) ),
inference(forward_demodulation,[status(thm)],[f270,f1120]) ).
fof(f1125,plain,
( ~ sQ72_spl
| sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1124,f152]) ).
fof(f1126,plain,
( ~ sQ72_spl
| sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1125]) ).
fof(f1127,plain,
$false,
inference(sat_refutation,[status(thm)],[f149,f153,f154,f183,f196,f198,f200,f202,f204,f256,f265,f268,f273,f323,f351,f369,f377,f402,f403,f405,f440,f444,f454,f490,f494,f501,f520,f524,f552,f556,f563,f565,f583,f587,f658,f662,f775,f794,f813,f833,f855,f873,f878,f883,f906,f957,f959,f962,f964,f1032,f1091,f1095,f1097,f1104,f1108,f1112,f1122,f1126]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU009+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 05:46:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 0.15/0.47 % Refutation found
% 0.15/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.78/0.50 % Elapsed time: 0.111521 seconds
% 0.78/0.50 % CPU time: 0.574042 seconds
% 0.78/0.50 % Total memory used: 93.204 MB
% 0.78/0.50 % Net memory used: 92.194 MB
%------------------------------------------------------------------------------