%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU004+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:47:02 PM UTC 2026
% Result : Theorem 86.81s 13.14s
% Output : Refutation 87.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 67
% Syntax : Number of formulae : 516 ( 58 unt; 54 def)
% Number of atoms : 2192 ( 564 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 2912 (1236 ~;1407 |; 160 &)
% ( 62 <=>; 47 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 61 ( 59 usr; 54 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-2 aty)
% Number of variables : 462 ( 0 sgn 421 !; 41 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subset(X0,X1)
& subset(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f5,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f6,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_funct_1) ).
fof(f7,axiom,
! [X0,X1] :
( ( relation(X0)
& relation(X1) )
=> relation(relation_composition(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_relat_1) ).
fof(f11,axiom,
! [X0,X1] :
( ( relation(X0)
& function(X0)
& relation(X1)
& function(X1) )
=> ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_funct_1) ).
fof(f29,axiom,
! [X0,X1] :
( ( ! [X2,X3,X4] :
( ( in(X2,X0)
& ( X2 = X1
=> X3 = n1 )
& ( X2 != X1
=> X3 = n0 )
& ( X2 = X1
=> X4 = n1 )
& ( X2 != X1
=> X4 = n0 ) )
=> X3 = X4 )
& ! [X2] :
~ ( in(X2,X0)
& ! [X3] :
~ ( ( X2 = X1
=> X3 = n1 )
& ( X2 != X1
=> X3 = n0 ) ) ) )
=> ? [X2] :
( relation(X2)
& function(X2)
& relation_dom(X2) = X0
& ! [X3] :
( in(X3,X0)
=> ( ( X3 = X1
=> apply(X2,X3) = n1 )
& ( X3 != X1
=> apply(X2,X3) = n0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s2_funct_1__e8_26_1__funct_1) ).
fof(f30,axiom,
! [X0] :
? [X1] :
( relation(X1)
& function(X1)
& relation_dom(X1) = X0
& ! [X2] :
( in(X2,X0)
=> apply(X1,X2) = n0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_funct_1__e3_26_1__funct_1) ).
fof(f31,axiom,
empty(n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',spc0_boole) ).
fof(f32,axiom,
~ empty(n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',spc1_boole) ).
fof(f34,axiom,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
=> apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t22_funct_1) ).
fof(f36,conjecture,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ( ( subset(relation_rng(X1),X0)
& ! [X2] :
( ( relation(X2)
& function(X2) )
=> ! [X3] :
( ( relation(X3)
& function(X3) )
=> ( ( relation_dom(X2) = X0
& relation_dom(X3) = X0
& relation_composition(X1,X2) = relation_composition(X1,X3) )
=> X2 = X3 ) ) ) )
=> X0 = relation_rng(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t33_funct_1) ).
fof(f37,negated_conjecture,
~ ! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ( ( subset(relation_rng(X1),X0)
& ! [X2] :
( ( relation(X2)
& function(X2) )
=> ! [X3] :
( ( relation(X3)
& function(X3) )
=> ( ( relation_dom(X2) = X0
& relation_dom(X3) = X0
& relation_composition(X1,X2) = relation_composition(X1,X3) )
=> X2 = X3 ) ) ) )
=> X0 = relation_rng(X1) ) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f39,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ( subset(relation_rng(X0),relation_dom(X1))
=> relation_dom(relation_composition(X0,X1)) = relation_dom(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t46_relat_1) ).
fof(f45,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1] :
( ( relation(X1)
& function(X1) )
=> ( ( relation_dom(X0) = relation_dom(X1)
& ! [X2] :
( in(X2,relation_dom(X0))
=> apply(X0,X2) = apply(X1,X2) ) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_funct_1) ).
fof(f47,plain,
! [X0,X1] :
( ( ! [X2,X3,X4] :
( ( in(X2,X0)
& ( X2 = X1
=> X3 = n1 )
& ( X2 != X1
=> X3 = n0 )
& ( X2 = X1
=> X4 = n1 )
& ( X2 != X1
=> X4 = n0 ) )
=> X3 = X4 )
& ! [X5] :
~ ( in(X5,X0)
& ! [X6] :
~ ( ( X1 = X5
=> n1 = X6 )
& ( X1 != X5
=> n0 = X6 ) ) ) )
=> ? [X7] :
( relation(X7)
& function(X7)
& relation_dom(X7) = X0
& ! [X8] :
( in(X8,X0)
=> ( ( X1 = X8
=> n1 = apply(X7,X8) )
& ( X1 != X8
=> n0 = apply(X7,X8) ) ) ) ) ),
inference(rectify,[],[f29]) ).
fof(f53,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f54,plain,
! [X0] :
( ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f55,plain,
! [X0] :
( ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f54]) ).
fof(f56,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f7]) ).
fof(f57,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(flattening,[],[f56]) ).
fof(f60,plain,
! [X0,X1] :
( ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) )
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f61,plain,
! [X0,X1] :
( ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) )
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f60]) ).
fof(f71,plain,
! [X0,X1] :
( ? [X7] :
( relation(X7)
& function(X7)
& relation_dom(X7) = X0
& ! [X8] :
( ( ( n1 = apply(X7,X8)
| X1 != X8 )
& ( n0 = apply(X7,X8)
| X1 = X8 ) )
| ~ in(X8,X0) ) )
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,X0)
& ( X3 = n1
| X1 != X2 )
& ( X3 = n0
| X1 = X2 )
& ( X4 = n1
| X1 != X2 )
& ( X4 = n0
| X1 = X2 ) )
| ? [X5] :
( in(X5,X0)
& ! [X6] :
( ( n1 != X6
& X1 = X5 )
| ( n0 != X6
& X1 != X5 ) ) ) ),
inference(ennf_transformation,[],[f47]) ).
fof(f72,plain,
! [X0,X1] :
( ? [X7] :
( relation(X7)
& function(X7)
& relation_dom(X7) = X0
& ! [X8] :
( ( ( n1 = apply(X7,X8)
| X1 != X8 )
& ( n0 = apply(X7,X8)
| X1 = X8 ) )
| ~ in(X8,X0) ) )
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,X0)
& ( X3 = n1
| X1 != X2 )
& ( X3 = n0
| X1 = X2 )
& ( X4 = n1
| X1 != X2 )
& ( X4 = n0
| X1 = X2 ) )
| ? [X5] :
( in(X5,X0)
& ! [X6] :
( ( n1 != X6
& X1 = X5 )
| ( n0 != X6
& X1 != X5 ) ) ) ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
! [X0] :
? [X1] :
( relation(X1)
& function(X1)
& relation_dom(X1) = X0
& ! [X2] :
( apply(X1,X2) = n0
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f30]) ).
fof(f75,plain,
! [X0,X1] :
( ! [X2] :
( apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0))
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1)
| ~ function(X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f76,plain,
! [X0,X1] :
( ! [X2] :
( apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0))
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f75]) ).
fof(f79,plain,
? [X0,X1] :
( relation_rng(X1) != X0
& subset(relation_rng(X1),X0)
& ! [X2] :
( ! [X3] :
( X2 = X3
| relation_dom(X2) != X0
| relation_dom(X3) != X0
| relation_composition(X1,X2) != relation_composition(X1,X3)
| ~ relation(X3)
| ~ function(X3) )
| ~ relation(X2)
| ~ function(X2) )
& relation(X1)
& function(X1) ),
inference(ennf_transformation,[],[f37]) ).
fof(f80,plain,
? [X0,X1] :
( relation_rng(X1) != X0
& subset(relation_rng(X1),X0)
& ! [X2] :
( ! [X3] :
( X2 = X3
| relation_dom(X2) != X0
| relation_dom(X3) != X0
| relation_composition(X1,X2) != relation_composition(X1,X3)
| ~ relation(X3)
| ~ function(X3) )
| ~ relation(X2)
| ~ function(X2) )
& relation(X1)
& function(X1) ),
inference(flattening,[],[f79]) ).
fof(f81,plain,
! [X0] :
( ! [X1] :
( relation_dom(relation_composition(X0,X1)) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_dom(X1))
| ~ relation(X1) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f82,plain,
! [X0] :
( ! [X1] :
( relation_dom(relation_composition(X0,X1)) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_dom(X1))
| ~ relation(X1) )
| ~ relation(X0) ),
inference(flattening,[],[f81]) ).
fof(f89,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| relation_dom(X0) != relation_dom(X1)
| ? [X2] :
( apply(X1,X2) != apply(X0,X2)
& in(X2,relation_dom(X0)) )
| ~ relation(X1)
| ~ function(X1) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f45]) ).
fof(f90,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| relation_dom(X0) != relation_dom(X1)
| ? [X2] :
( apply(X1,X2) != apply(X0,X2)
& in(X2,relation_dom(X0)) )
| ~ relation(X1)
| ~ function(X1) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f89]) ).
fof(f91,definition,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& in(X2,X0)
& ( X3 = n1
| X1 != X2 )
& ( X3 = n0
| X1 = X2 )
& ( X4 = n1
| X1 != X2 )
& ( X4 = n0
| X1 = X2 ) )
| ~ sP0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f92,plain,
! [X0,X1] :
( ? [X7] :
( relation(X7)
& function(X7)
& relation_dom(X7) = X0
& ! [X8] :
( ( ( n1 = apply(X7,X8)
| X1 != X8 )
& ( n0 = apply(X7,X8)
| X1 = X8 ) )
| ~ in(X8,X0) ) )
| sP0(X0,X1)
| ? [X5] :
( in(X5,X0)
& ! [X6] :
( ( n1 != X6
& X1 = X5 )
| ( n0 != X6
& X1 != X5 ) ) ) ),
inference(definition_folding,[],[f72,f91]) ).
fof(f93,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f94,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f53]) ).
fof(f96,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f95]) ).
fof(f97,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK1(X0,X1),X1)
& in(sK1(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f96]) ).
fof(f98,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_rng(X0)
| ? [X2] :
( ( ! [X3] :
( ~ in(X3,relation_dom(X0))
| apply(X0,X3) != X2 )
| ~ in(X2,X1) )
& ( ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) )
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| ! [X3] :
( ~ in(X3,relation_dom(X0))
| apply(X0,X3) != X2 ) )
& ( ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) )
| ~ in(X2,X1) ) )
| relation_rng(X0) != X1 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f55]) ).
fof(f99,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_rng(X0)
| ? [X2] :
( ( ! [X3] :
( ~ in(X3,relation_dom(X0))
| apply(X0,X3) != X2 )
| ~ in(X2,X1) )
& ( ? [X4] :
( in(X4,relation_dom(X0))
& apply(X0,X4) = X2 )
| in(X2,X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] :
( ~ in(X6,relation_dom(X0))
| apply(X0,X6) != X5 ) )
& ( ? [X7] :
( in(X7,relation_dom(X0))
& apply(X0,X7) = X5 )
| ~ in(X5,X1) ) )
| relation_rng(X0) != X1 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(rectify,[],[f98]) ).
fof(f100,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_rng(X0)
| ( ( ! [X3] :
( ~ in(X3,relation_dom(X0))
| apply(X0,X3) != sK2(X0,X1) )
| ~ in(sK2(X0,X1),X1) )
& ( ( in(sK3(X0,X1),relation_dom(X0))
& sK2(X0,X1) = apply(X0,sK3(X0,X1)) )
| in(sK2(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] :
( ~ in(X6,relation_dom(X0))
| apply(X0,X6) != X5 ) )
& ( ( in(sK4(X0,X5),relation_dom(X0))
& apply(X0,sK4(X0,X5)) = X5 )
| ~ in(X5,X1) ) )
| relation_rng(X0) != X1 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X2,sK2(X0,X1)),skolemize(X4,sK3(X0,X1)),skolemize(X7,sK4(X0,X5))],[f99]) ).
fof(f110,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& in(X2,X0)
& ( X3 = n1
| X1 != X2 )
& ( X3 = n0
| X1 = X2 )
& ( X4 = n1
| X1 != X2 )
& ( X4 = n0
| X1 = X2 ) )
| ~ sP0(X0,X1) ),
inference(nnf_transformation,[],[f91]) ).
fof(f111,plain,
! [X0,X1] :
( ( sK15(X0,X1) != sK16(X0,X1)
& in(sK14(X0,X1),X0)
& ( n1 = sK15(X0,X1)
| sK14(X0,X1) != X1 )
& ( n0 = sK15(X0,X1)
| sK14(X0,X1) = X1 )
& ( n1 = sK16(X0,X1)
| sK14(X0,X1) != X1 )
& ( n0 = sK16(X0,X1)
| sK14(X0,X1) = X1 ) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16]),skolemize(X2,sK14(X0,X1)),skolemize(X3,sK15(X0,X1)),skolemize(X4,sK16(X0,X1))],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( ? [X2] :
( relation(X2)
& function(X2)
& relation_dom(X2) = X0
& ! [X3] :
( ( ( n1 = apply(X2,X3)
| X1 != X3 )
& ( n0 = apply(X2,X3)
| X1 = X3 ) )
| ~ in(X3,X0) ) )
| sP0(X0,X1)
| ? [X4] :
( in(X4,X0)
& ! [X5] :
( ( n1 != X5
& X1 = X4 )
| ( n0 != X5
& X1 != X4 ) ) ) ),
inference(rectify,[],[f92]) ).
fof(f113,plain,
! [X0,X1] :
( ( relation(sK17(X0,X1))
& function(sK17(X0,X1))
& relation_dom(sK17(X0,X1)) = X0
& ! [X3] :
( ( ( n1 = apply(sK17(X0,X1),X3)
| X1 != X3 )
& ( n0 = apply(sK17(X0,X1),X3)
| X1 = X3 ) )
| ~ in(X3,X0) ) )
| sP0(X0,X1)
| ( in(sK18(X0,X1),X0)
& ! [X5] :
( ( n1 != X5
& sK18(X0,X1) = X1 )
| ( n0 != X5
& sK18(X0,X1) != X1 ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18]),skolemize(X2,sK17(X0,X1)),skolemize(X4,sK18(X0,X1))],[f112]) ).
fof(f114,plain,
! [X0] :
( relation(sK19(X0))
& function(sK19(X0))
& relation_dom(sK19(X0)) = X0
& ! [X2] :
( n0 = apply(sK19(X0),X2)
| ~ in(X2,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X1,sK19(X0))],[f73]) ).
fof(f115,plain,
( sK20 != relation_rng(sK21)
& subset(relation_rng(sK21),sK20)
& ! [X2] :
( ! [X3] :
( X2 = X3
| relation_dom(X2) != sK20
| relation_dom(X3) != sK20
| relation_composition(sK21,X2) != relation_composition(sK21,X3)
| ~ relation(X3)
| ~ function(X3) )
| ~ relation(X2)
| ~ function(X2) )
& relation(sK21)
& function(sK21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21]),skolemize(X0,sK20),skolemize(X1,sK21)],[f80]) ).
fof(f117,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| relation_dom(X0) != relation_dom(X1)
| ( apply(X1,sK22(X0,X1)) != apply(X0,sK22(X0,X1))
& in(sK22(X0,X1),relation_dom(X0)) )
| ~ relation(X1)
| ~ function(X1) )
| ~ relation(X0)
| ~ function(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X2,sK22(X0,X1))],[f90]) ).
fof(f122,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f94]) ).
fof(f124,plain,
! [X3,X0,X1] :
( in(X3,X1)
| ~ in(X3,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f97]) ).
fof(f129,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(X6,relation_dom(X0))
| apply(X0,X6) != X5
| relation_rng(X0) != X1
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f130,plain,
! [X0,X1] :
( relation_rng(X0) = X1
| sK2(X0,X1) = apply(X0,sK3(X0,X1))
| in(sK2(X0,X1),X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f131,plain,
! [X0,X1] :
( relation_rng(X0) = X1
| in(sK3(X0,X1),relation_dom(X0))
| in(sK2(X0,X1),X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f132,plain,
! [X3,X0,X1] :
( relation_rng(X0) = X1
| ~ in(X3,relation_dom(X0))
| apply(X0,X3) != sK2(X0,X1)
| ~ in(sK2(X0,X1),X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f133,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f57]) ).
fof(f139,plain,
! [X0,X1] :
( function(relation_composition(X0,X1))
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f140,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f167,plain,
! [X0,X1] :
( n0 = sK16(X0,X1)
| sK14(X0,X1) = X1
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f168,plain,
! [X0,X1] :
( n1 = sK16(X0,X1)
| sK14(X0,X1) != X1
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f169,plain,
! [X0,X1] :
( n0 = sK15(X0,X1)
| sK14(X0,X1) = X1
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f170,plain,
! [X0,X1] :
( n1 = sK15(X0,X1)
| sK14(X0,X1) != X1
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f172,plain,
! [X0,X1] :
( sK15(X0,X1) != sK16(X0,X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f174,plain,
! [X3,X0,X1,X5] :
( n0 = apply(sK17(X0,X1),X3)
| X1 = X3
| ~ in(X3,X0)
| sP0(X0,X1)
| sK18(X0,X1) = X1
| n0 != X5 ),
inference(cnf_transformation,[],[f113]) ).
fof(f175,plain,
! [X3,X0,X1,X5] :
( n0 = apply(sK17(X0,X1),X3)
| X1 = X3
| ~ in(X3,X0)
| sP0(X0,X1)
| n1 != X5
| sK18(X0,X1) != X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f179,plain,
! [X3,X0,X1,X5] :
( n1 = apply(sK17(X0,X1),X3)
| X1 != X3
| ~ in(X3,X0)
| sP0(X0,X1)
| sK18(X0,X1) = X1
| n0 != X5 ),
inference(cnf_transformation,[],[f113]) ).
fof(f180,plain,
! [X3,X0,X1,X5] :
( n1 = apply(sK17(X0,X1),X3)
| X1 != X3
| ~ in(X3,X0)
| sP0(X0,X1)
| n1 != X5
| sK18(X0,X1) != X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f184,plain,
! [X0,X1,X5] :
( relation_dom(sK17(X0,X1)) = X0
| sP0(X0,X1)
| sK18(X0,X1) = X1
| n0 != X5 ),
inference(cnf_transformation,[],[f113]) ).
fof(f185,plain,
! [X0,X1,X5] :
( relation_dom(sK17(X0,X1)) = X0
| sP0(X0,X1)
| n1 != X5
| sK18(X0,X1) != X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f189,plain,
! [X0,X1,X5] :
( function(sK17(X0,X1))
| sP0(X0,X1)
| sK18(X0,X1) = X1
| n0 != X5 ),
inference(cnf_transformation,[],[f113]) ).
fof(f190,plain,
! [X0,X1,X5] :
( function(sK17(X0,X1))
| sP0(X0,X1)
| n1 != X5
| sK18(X0,X1) != X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f194,plain,
! [X0,X1,X5] :
( relation(sK17(X0,X1))
| sP0(X0,X1)
| sK18(X0,X1) = X1
| n0 != X5 ),
inference(cnf_transformation,[],[f113]) ).
fof(f195,plain,
! [X0,X1,X5] :
( relation(sK17(X0,X1))
| sP0(X0,X1)
| n1 != X5
| sK18(X0,X1) != X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f198,plain,
! [X2,X0] :
( n0 = apply(sK19(X0),X2)
| ~ in(X2,X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f199,plain,
! [X0] : relation_dom(sK19(X0)) = X0,
inference(cnf_transformation,[],[f114]) ).
fof(f200,plain,
! [X0] : function(sK19(X0)),
inference(cnf_transformation,[],[f114]) ).
fof(f201,plain,
! [X0] : relation(sK19(X0)),
inference(cnf_transformation,[],[f114]) ).
fof(f202,plain,
empty(n0),
inference(cnf_transformation,[],[f31]) ).
fof(f203,plain,
~ empty(n1),
inference(cnf_transformation,[],[f32]) ).
fof(f205,plain,
! [X2,X0,X1] :
( apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0))
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| ~ relation(X2)
| ~ function(X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f76]) ).
fof(f207,plain,
function(sK21),
inference(cnf_transformation,[],[f115]) ).
fof(f208,plain,
relation(sK21),
inference(cnf_transformation,[],[f115]) ).
fof(f209,plain,
! [X2,X3] :
( X2 = X3
| relation_dom(X2) != sK20
| relation_dom(X3) != sK20
| relation_composition(sK21,X2) != relation_composition(sK21,X3)
| ~ relation(X3)
| ~ function(X3)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f210,plain,
subset(relation_rng(sK21),sK20),
inference(cnf_transformation,[],[f115]) ).
fof(f211,plain,
sK20 != relation_rng(sK21),
inference(cnf_transformation,[],[f115]) ).
fof(f214,plain,
! [X0,X1] :
( relation_dom(X0) = relation_dom(relation_composition(X0,X1))
| ~ subset(relation_rng(X0),relation_dom(X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f220,plain,
! [X0,X1] :
( X0 = X1
| relation_dom(X0) != relation_dom(X1)
| in(sK22(X0,X1),relation_dom(X0))
| ~ relation(X1)
| ~ function(X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f221,plain,
! [X0,X1] :
( X0 = X1
| relation_dom(X0) != relation_dom(X1)
| apply(X1,sK22(X0,X1)) != apply(X0,sK22(X0,X1))
| ~ relation(X1)
| ~ function(X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f222,plain,
! [X1] : subset(X1,X1),
inference(equality_resolution,[],[f122]) ).
fof(f224,plain,
! [X0,X1,X6] :
( in(apply(X0,X6),X1)
| ~ in(X6,relation_dom(X0))
| relation_rng(X0) != X1
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f129]) ).
fof(f225,plain,
! [X0,X6] :
( in(apply(X0,X6),relation_rng(X0))
| ~ in(X6,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f224]) ).
fof(f229,plain,
! [X0,X1] :
( relation(sK17(X0,X1))
| sP0(X0,X1)
| sK18(X0,X1) != X1 ),
inference(equality_resolution,[],[f195]) ).
fof(f230,plain,
! [X0,X1] :
( relation(sK17(X0,X1))
| sP0(X0,X1)
| sK18(X0,X1) = X1 ),
inference(equality_resolution,[],[f194]) ).
fof(f232,plain,
! [X0,X1] :
( function(sK17(X0,X1))
| sP0(X0,X1)
| sK18(X0,X1) != X1 ),
inference(equality_resolution,[],[f190]) ).
fof(f233,plain,
! [X0,X1] :
( function(sK17(X0,X1))
| sP0(X0,X1)
| sK18(X0,X1) = X1 ),
inference(equality_resolution,[],[f189]) ).
fof(f235,plain,
! [X0,X1] :
( relation_dom(sK17(X0,X1)) = X0
| sP0(X0,X1)
| sK18(X0,X1) != X1 ),
inference(equality_resolution,[],[f185]) ).
fof(f236,plain,
! [X0,X1] :
( relation_dom(sK17(X0,X1)) = X0
| sP0(X0,X1)
| sK18(X0,X1) = X1 ),
inference(equality_resolution,[],[f184]) ).
fof(f240,plain,
! [X3,X0,X5] :
( n1 = apply(sK17(X0,X3),X3)
| ~ in(X3,X0)
| sP0(X0,X3)
| n1 != X5
| sK18(X0,X3) != X3 ),
inference(equality_resolution,[],[f180]) ).
fof(f241,plain,
! [X3,X0] :
( n1 = apply(sK17(X0,X3),X3)
| ~ in(X3,X0)
| sP0(X0,X3)
| sK18(X0,X3) != X3 ),
inference(equality_resolution,[],[f240]) ).
fof(f242,plain,
! [X3,X0,X5] :
( n1 = apply(sK17(X0,X3),X3)
| ~ in(X3,X0)
| sP0(X0,X3)
| sK18(X0,X3) = X3
| n0 != X5 ),
inference(equality_resolution,[],[f179]) ).
fof(f243,plain,
! [X3,X0] :
( n1 = apply(sK17(X0,X3),X3)
| ~ in(X3,X0)
| sP0(X0,X3)
| sK18(X0,X3) = X3 ),
inference(equality_resolution,[],[f242]) ).
fof(f246,plain,
! [X3,X0,X1] :
( n0 = apply(sK17(X0,X1),X3)
| X1 = X3
| ~ in(X3,X0)
| sP0(X0,X1)
| sK18(X0,X1) != X1 ),
inference(equality_resolution,[],[f175]) ).
fof(f247,plain,
! [X3,X0,X1] :
( n0 = apply(sK17(X0,X1),X3)
| X1 = X3
| ~ in(X3,X0)
| sP0(X0,X1)
| sK18(X0,X1) = X1 ),
inference(equality_resolution,[],[f174]) ).
fof(f251,definition,
( spl24_1
<=> relation(sK21) ),
introduced(definition,[new_symbols(definition,[spl24_1])],[avatar_definition]) ).
fof(f253,plain,
( relation(sK21)
| ~ spl24_1 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f254,plain,
spl24_1,
inference(avatar_split_clause,[],[f208,f251]) ).
fof(f258,plain,
( ! [X0] :
( relation(relation_composition(sK21,X0))
| ~ relation(X0) )
| ~ spl24_1 ),
inference(resolution,[],[f253,f133]) ).
fof(f262,plain,
( ! [X0] :
( function(relation_composition(sK21,X0))
| ~ function(sK21)
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_1 ),
inference(resolution,[],[f253,f139]) ).
fof(f271,plain,
( ! [X0,X1] :
( apply(relation_composition(sK21,X0),X1) = apply(X0,apply(sK21,X1))
| ~ in(X1,relation_dom(relation_composition(sK21,X0)))
| ~ function(sK21)
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_1 ),
inference(resolution,[],[f253,f205]) ).
fof(f272,plain,
( ! [X0] :
( relation_dom(sK21) = relation_dom(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) )
| ~ spl24_1 ),
inference(resolution,[],[f253,f214]) ).
fof(f278,plain,
( ! [X0] :
( in(apply(sK21,X0),relation_rng(sK21))
| ~ in(X0,relation_dom(sK21))
| ~ function(sK21) )
| ~ spl24_1 ),
inference(resolution,[],[f253,f225]) ).
fof(f283,plain,
( ! [X0] :
( in(apply(sK21,X0),relation_rng(sK21))
| ~ in(X0,relation_dom(sK21)) )
| ~ spl24_1 ),
inference(forward_subsumption_resolution,[],[f278,f207]) ).
fof(f288,plain,
( ! [X0,X1] :
( apply(relation_composition(sK21,X0),X1) = apply(X0,apply(sK21,X1))
| ~ in(X1,relation_dom(relation_composition(sK21,X0)))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_1 ),
inference(forward_subsumption_resolution,[],[f271,f207]) ).
fof(f293,plain,
( ! [X0] :
( function(relation_composition(sK21,X0))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_1 ),
inference(forward_subsumption_resolution,[],[f262,f207]) ).
fof(f298,definition,
( spl24_2
<=> function(sK21) ),
introduced(definition,[new_symbols(definition,[spl24_2])],[avatar_definition]) ).
fof(f300,plain,
( function(sK21)
| ~ spl24_2 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f301,plain,
spl24_2,
inference(avatar_split_clause,[],[f207,f298]) ).
fof(f319,definition,
( spl24_3
<=> sK20 = relation_rng(sK21) ),
introduced(definition,[new_symbols(definition,[spl24_3])],[avatar_definition]) ).
fof(f321,plain,
( sK20 != relation_rng(sK21)
| spl24_3 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f322,plain,
~ spl24_3,
inference(avatar_split_clause,[],[f211,f319]) ).
fof(f324,plain,
( ! [X0] :
( sK20 != X0
| in(sK3(sK21,X0),relation_dom(sK21))
| in(sK2(sK21,X0),X0)
| ~ relation(sK21)
| ~ function(sK21) )
| spl24_3 ),
inference(superposition,[],[f321,f131]) ).
fof(f327,plain,
( ! [X0] :
( sK20 != X0
| in(sK3(sK21,X0),relation_dom(sK21))
| in(sK2(sK21,X0),X0)
| ~ function(sK21) )
| ~ spl24_1
| spl24_3 ),
inference(forward_subsumption_resolution,[],[f324,f253]) ).
fof(f330,plain,
( ! [X0] :
( sK20 != X0
| in(sK3(sK21,X0),relation_dom(sK21))
| in(sK2(sK21,X0),X0) )
| ~ spl24_1
| ~ spl24_2
| spl24_3 ),
inference(forward_subsumption_resolution,[],[f327,f300]) ).
fof(f333,definition,
( spl24_4
<=> subset(relation_rng(sK21),sK20) ),
introduced(definition,[new_symbols(definition,[spl24_4])],[avatar_definition]) ).
fof(f335,plain,
( subset(relation_rng(sK21),sK20)
| ~ spl24_4 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f336,plain,
spl24_4,
inference(avatar_split_clause,[],[f210,f333]) ).
fof(f338,plain,
( ! [X0] :
( in(X0,sK20)
| ~ in(X0,relation_rng(sK21)) )
| ~ spl24_4 ),
inference(resolution,[],[f335,f124]) ).
fof(f427,definition,
( spl24_9
<=> ! [X0] :
( in(X0,sK20)
| ~ in(X0,relation_rng(sK21)) ) ),
introduced(definition,[new_symbols(definition,[spl24_9])],[avatar_definition]) ).
fof(f428,plain,
( ! [X0] :
( ~ in(X0,relation_rng(sK21))
| in(X0,sK20) )
| ~ spl24_9 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f429,plain,
( spl24_9
| ~ spl24_4 ),
inference(avatar_split_clause,[],[f338,f333,f427]) ).
fof(f432,plain,
( ! [X0] :
( in(apply(sK21,X0),sK20)
| ~ in(X0,relation_dom(sK21))
| ~ relation(sK21)
| ~ function(sK21) )
| ~ spl24_9 ),
inference(resolution,[],[f428,f225]) ).
fof(f448,plain,
( ! [X0] :
( in(apply(sK21,X0),sK20)
| ~ in(X0,relation_dom(sK21))
| ~ function(sK21) )
| ~ spl24_1
| ~ spl24_9 ),
inference(forward_subsumption_resolution,[],[f432,f253]) ).
fof(f452,plain,
( ! [X0] :
( in(apply(sK21,X0),sK20)
| ~ in(X0,relation_dom(sK21)) )
| ~ spl24_1
| ~ spl24_2
| ~ spl24_9 ),
inference(forward_subsumption_resolution,[],[f448,f300]) ).
fof(f530,definition,
( spl24_14
<=> ! [X0] :
( in(apply(sK21,X0),relation_rng(sK21))
| ~ in(X0,relation_dom(sK21)) ) ),
introduced(definition,[new_symbols(definition,[spl24_14])],[avatar_definition]) ).
fof(f531,plain,
( ! [X0] :
( in(apply(sK21,X0),relation_rng(sK21))
| ~ in(X0,relation_dom(sK21)) )
| ~ spl24_14 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f532,plain,
( spl24_14
| ~ spl24_1 ),
inference(avatar_split_clause,[],[f283,f251,f530]) ).
fof(f538,plain,
( ! [X0,X1] :
( ~ in(X0,relation_dom(sK21))
| in(apply(sK21,X0),X1)
| ~ subset(relation_rng(sK21),X1) )
| ~ spl24_14 ),
inference(resolution,[],[f531,f124]) ).
fof(f574,definition,
( spl24_15
<=> ! [X2,X3] :
( X2 = X3
| relation_dom(X2) != sK20
| relation_dom(X3) != sK20
| relation_composition(sK21,X2) != relation_composition(sK21,X3)
| ~ relation(X3)
| ~ function(X3)
| ~ relation(X2)
| ~ function(X2) ) ),
introduced(definition,[new_symbols(definition,[spl24_15])],[avatar_definition]) ).
fof(f575,plain,
( ! [X2,X3] :
( relation_composition(sK21,X2) != relation_composition(sK21,X3)
| relation_dom(X2) != sK20
| relation_dom(X3) != sK20
| X2 = X3
| ~ relation(X3)
| ~ function(X3)
| ~ relation(X2)
| ~ function(X2) )
| ~ spl24_15 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f576,plain,
spl24_15,
inference(avatar_split_clause,[],[f209,f574]) ).
fof(f591,definition,
( spl24_17
<=> ! [X0] :
( sK20 != X0
| in(sK3(sK21,X0),relation_dom(sK21))
| in(sK2(sK21,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_17])],[avatar_definition]) ).
fof(f592,plain,
( ! [X0] :
( sK20 != X0
| in(sK3(sK21,X0),relation_dom(sK21))
| in(sK2(sK21,X0),X0) )
| ~ spl24_17 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f593,plain,
( spl24_17
| ~ spl24_1
| ~ spl24_2
| spl24_3 ),
inference(avatar_split_clause,[],[f330,f319,f298,f251,f591]) ).
fof(f594,plain,
( in(sK3(sK21,sK20),relation_dom(sK21))
| in(sK2(sK21,sK20),sK20)
| ~ spl24_17 ),
inference(equality_resolution,[],[f592]) ).
fof(f596,definition,
( spl24_18
<=> in(sK2(sK21,sK20),sK20) ),
introduced(definition,[new_symbols(definition,[spl24_18])],[avatar_definition]) ).
fof(f597,plain,
( ~ in(sK2(sK21,sK20),sK20)
| spl24_18 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f598,plain,
( in(sK2(sK21,sK20),sK20)
| ~ spl24_18 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f600,definition,
( spl24_19
<=> in(sK3(sK21,sK20),relation_dom(sK21)) ),
introduced(definition,[new_symbols(definition,[spl24_19])],[avatar_definition]) ).
fof(f602,plain,
( in(sK3(sK21,sK20),relation_dom(sK21))
| ~ spl24_19 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f603,plain,
( spl24_18
| spl24_19
| ~ spl24_17 ),
inference(avatar_split_clause,[],[f594,f591,f600,f596]) ).
fof(f627,definition,
( spl24_20
<=> sP0(sK20,sK2(sK21,sK20)) ),
introduced(definition,[new_symbols(definition,[spl24_20])],[avatar_definition]) ).
fof(f628,plain,
( ~ sP0(sK20,sK2(sK21,sK20))
| spl24_20 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f629,plain,
( sP0(sK20,sK2(sK21,sK20))
| ~ spl24_20 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f635,plain,
( in(apply(sK21,sK3(sK21,sK20)),relation_rng(sK21))
| ~ relation(sK21)
| ~ function(sK21)
| ~ spl24_19 ),
inference(resolution,[],[f602,f225]) ).
fof(f656,plain,
( in(apply(sK21,sK3(sK21,sK20)),relation_rng(sK21))
| ~ function(sK21)
| ~ spl24_1
| ~ spl24_19 ),
inference(forward_subsumption_resolution,[],[f635,f253]) ).
fof(f658,plain,
( in(apply(sK21,sK3(sK21,sK20)),relation_rng(sK21))
| ~ spl24_1
| ~ spl24_2
| ~ spl24_19 ),
inference(forward_subsumption_resolution,[],[f656,f300]) ).
fof(f659,plain,
( sK20 = relation_rng(sK21)
| sK2(sK21,sK20) = apply(sK21,sK3(sK21,sK20))
| ~ relation(sK21)
| ~ function(sK21)
| spl24_18 ),
inference(resolution,[],[f597,f130]) ).
fof(f664,plain,
( sK2(sK21,sK20) = apply(sK21,sK3(sK21,sK20))
| ~ relation(sK21)
| ~ function(sK21)
| spl24_3
| spl24_18 ),
inference(forward_subsumption_resolution,[],[f659,f321]) ).
fof(f665,plain,
( sK2(sK21,sK20) = apply(sK21,sK3(sK21,sK20))
| ~ function(sK21)
| ~ spl24_1
| spl24_3
| spl24_18 ),
inference(forward_subsumption_resolution,[],[f664,f253]) ).
fof(f666,plain,
( sK2(sK21,sK20) = apply(sK21,sK3(sK21,sK20))
| ~ spl24_1
| ~ spl24_2
| spl24_3
| spl24_18 ),
inference(forward_subsumption_resolution,[],[f665,f300]) ).
fof(f668,definition,
( spl24_22
<=> sK2(sK21,sK20) = apply(sK21,sK3(sK21,sK20)) ),
introduced(definition,[new_symbols(definition,[spl24_22])],[avatar_definition]) ).
fof(f670,plain,
( sK2(sK21,sK20) = apply(sK21,sK3(sK21,sK20))
| ~ spl24_22 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f671,plain,
( spl24_22
| ~ spl24_1
| ~ spl24_2
| spl24_3
| spl24_18 ),
inference(avatar_split_clause,[],[f666,f596,f319,f298,f251,f668]) ).
fof(f677,plain,
( n0 = apply(sK19(sK20),sK2(sK21,sK20))
| ~ spl24_18 ),
inference(resolution,[],[f598,f198]) ).
fof(f725,definition,
( spl24_24
<=> in(apply(sK21,sK3(sK21,sK20)),relation_rng(sK21)) ),
introduced(definition,[new_symbols(definition,[spl24_24])],[avatar_definition]) ).
fof(f727,plain,
( in(apply(sK21,sK3(sK21,sK20)),relation_rng(sK21))
| ~ spl24_24 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f728,plain,
( spl24_24
| ~ spl24_1
| ~ spl24_2
| ~ spl24_19 ),
inference(avatar_split_clause,[],[f658,f600,f298,f251,f725]) ).
fof(f734,definition,
( spl24_25
<=> n0 = apply(sK19(sK20),sK2(sK21,sK20)) ),
introduced(definition,[new_symbols(definition,[spl24_25])],[avatar_definition]) ).
fof(f736,plain,
( n0 = apply(sK19(sK20),sK2(sK21,sK20))
| ~ spl24_25 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f737,plain,
( spl24_25
| ~ spl24_18 ),
inference(avatar_split_clause,[],[f677,f596,f734]) ).
fof(f738,plain,
( in(sK2(sK21,sK20),relation_rng(sK21))
| ~ spl24_22
| ~ spl24_24 ),
inference(forward_demodulation,[],[f727,f670]) ).
fof(f753,plain,
( relation(sK17(sK20,sK2(sK21,sK20)))
| sK2(sK21,sK20) != sK18(sK20,sK2(sK21,sK20))
| spl24_20 ),
inference(resolution,[],[f628,f229]) ).
fof(f754,plain,
( relation(sK17(sK20,sK2(sK21,sK20)))
| sK2(sK21,sK20) = sK18(sK20,sK2(sK21,sK20))
| spl24_20 ),
inference(resolution,[],[f628,f230]) ).
fof(f756,plain,
( function(sK17(sK20,sK2(sK21,sK20)))
| sK2(sK21,sK20) != sK18(sK20,sK2(sK21,sK20))
| spl24_20 ),
inference(resolution,[],[f628,f232]) ).
fof(f757,plain,
( function(sK17(sK20,sK2(sK21,sK20)))
| sK2(sK21,sK20) = sK18(sK20,sK2(sK21,sK20))
| spl24_20 ),
inference(resolution,[],[f628,f233]) ).
fof(f759,plain,
( sK20 = relation_dom(sK17(sK20,sK2(sK21,sK20)))
| sK2(sK21,sK20) != sK18(sK20,sK2(sK21,sK20))
| spl24_20 ),
inference(resolution,[],[f628,f235]) ).
fof(f760,plain,
( sK20 = relation_dom(sK17(sK20,sK2(sK21,sK20)))
| sK2(sK21,sK20) = sK18(sK20,sK2(sK21,sK20))
| spl24_20 ),
inference(resolution,[],[f628,f236]) ).
fof(f769,plain,
( sK20 = relation_dom(sK17(sK20,sK2(sK21,sK20)))
| spl24_20 ),
inference(forward_subsumption_resolution,[],[f759,f760]) ).
fof(f770,plain,
( function(sK17(sK20,sK2(sK21,sK20)))
| spl24_20 ),
inference(forward_subsumption_resolution,[],[f756,f757]) ).
fof(f771,plain,
( relation(sK17(sK20,sK2(sK21,sK20)))
| spl24_20 ),
inference(forward_subsumption_resolution,[],[f753,f754]) ).
fof(f806,definition,
( spl24_27
<=> sK20 = relation_dom(sK17(sK20,sK2(sK21,sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_27])],[avatar_definition]) ).
fof(f808,plain,
( sK20 = relation_dom(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_27 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f809,plain,
( spl24_27
| spl24_20 ),
inference(avatar_split_clause,[],[f769,f627,f806]) ).
fof(f815,plain,
( ! [X0] :
( ~ subset(relation_rng(X0),sK20)
| relation_dom(X0) = relation_dom(relation_composition(X0,sK17(sK20,sK2(sK21,sK20))))
| ~ relation(sK17(sK20,sK2(sK21,sK20)))
| ~ relation(X0) )
| ~ spl24_27 ),
inference(superposition,[],[f214,f808]) ).
fof(f830,plain,
( ! [X0] :
( ~ subset(relation_rng(X0),sK20)
| relation_dom(X0) = relation_dom(relation_composition(X0,sK17(sK20,sK2(sK21,sK20))))
| ~ relation(X0) )
| spl24_20
| ~ spl24_27 ),
inference(forward_subsumption_resolution,[],[f815,f771]) ).
fof(f859,definition,
( spl24_30
<=> in(sK2(sK21,sK20),relation_rng(sK21)) ),
introduced(definition,[new_symbols(definition,[spl24_30])],[avatar_definition]) ).
fof(f861,plain,
( in(sK2(sK21,sK20),relation_rng(sK21))
| ~ spl24_30 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f862,plain,
( spl24_30
| ~ spl24_22
| ~ spl24_24 ),
inference(avatar_split_clause,[],[f738,f725,f668,f859]) ).
fof(f863,plain,
( in(sK2(sK21,sK20),sK20)
| ~ spl24_9
| ~ spl24_30 ),
inference(resolution,[],[f861,f428]) ).
fof(f894,plain,
( $false
| ~ spl24_9
| spl24_18
| ~ spl24_30 ),
inference(forward_subsumption_resolution,[],[f863,f597]) ).
fof(f895,plain,
( ~ spl24_9
| spl24_18
| ~ spl24_30 ),
inference(avatar_contradiction_clause,[],[f894]) ).
fof(f901,plain,
( ! [X0] :
( sK20 = relation_rng(sK21)
| ~ in(X0,relation_dom(sK21))
| apply(sK21,X0) != sK2(sK21,sK20)
| ~ relation(sK21)
| ~ function(sK21) )
| ~ spl24_18 ),
inference(resolution,[],[f598,f132]) ).
fof(f904,plain,
( ! [X0] :
( in(sK2(sK21,sK20),X0)
| ~ subset(sK20,X0) )
| ~ spl24_18 ),
inference(resolution,[],[f598,f124]) ).
fof(f919,plain,
( ! [X0] :
( ~ in(X0,relation_dom(sK21))
| apply(sK21,X0) != sK2(sK21,sK20)
| ~ relation(sK21)
| ~ function(sK21) )
| spl24_3
| ~ spl24_18 ),
inference(forward_subsumption_resolution,[],[f901,f321]) ).
fof(f920,plain,
( ! [X0] :
( ~ in(X0,relation_dom(sK21))
| apply(sK21,X0) != sK2(sK21,sK20)
| ~ function(sK21) )
| ~ spl24_1
| spl24_3
| ~ spl24_18 ),
inference(forward_subsumption_resolution,[],[f919,f253]) ).
fof(f921,plain,
( ! [X0] :
( ~ in(X0,relation_dom(sK21))
| apply(sK21,X0) != sK2(sK21,sK20) )
| ~ spl24_1
| ~ spl24_2
| spl24_3
| ~ spl24_18 ),
inference(forward_subsumption_resolution,[],[f920,f300]) ).
fof(f1051,definition,
( spl24_33
<=> function(sK17(sK20,sK2(sK21,sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_33])],[avatar_definition]) ).
fof(f1053,plain,
( function(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_33 ),
inference(avatar_component_clause,[],[f1051]) ).
fof(f1054,plain,
( spl24_33
| spl24_20 ),
inference(avatar_split_clause,[],[f770,f627,f1051]) ).
fof(f1056,definition,
( spl24_34
<=> relation(sK17(sK20,sK2(sK21,sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_34])],[avatar_definition]) ).
fof(f1058,plain,
( relation(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_34 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1059,plain,
( spl24_34
| spl24_20 ),
inference(avatar_split_clause,[],[f771,f627,f1056]) ).
fof(f1187,definition,
( spl24_37
<=> ! [X0] :
( ~ in(X0,relation_dom(sK21))
| apply(sK21,X0) != sK2(sK21,sK20) ) ),
introduced(definition,[new_symbols(definition,[spl24_37])],[avatar_definition]) ).
fof(f1188,plain,
( ! [X0] :
( apply(sK21,X0) != sK2(sK21,sK20)
| ~ in(X0,relation_dom(sK21)) )
| ~ spl24_37 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1189,plain,
( spl24_37
| ~ spl24_1
| ~ spl24_2
| spl24_3
| ~ spl24_18 ),
inference(avatar_split_clause,[],[f921,f596,f319,f298,f251,f1187]) ).
fof(f1369,definition,
( spl24_46
<=> ! [X0] :
( in(apply(sK21,X0),sK20)
| ~ in(X0,relation_dom(sK21)) ) ),
introduced(definition,[new_symbols(definition,[spl24_46])],[avatar_definition]) ).
fof(f1370,plain,
( ! [X0] :
( in(apply(sK21,X0),sK20)
| ~ in(X0,relation_dom(sK21)) )
| ~ spl24_46 ),
inference(avatar_component_clause,[],[f1369]) ).
fof(f1371,plain,
( spl24_46
| ~ spl24_1
| ~ spl24_2
| ~ spl24_9 ),
inference(avatar_split_clause,[],[f452,f427,f298,f251,f1369]) ).
fof(f1376,plain,
( ! [X0] :
( ~ in(X0,relation_dom(sK21))
| n0 = apply(sK19(sK20),apply(sK21,X0)) )
| ~ spl24_46 ),
inference(resolution,[],[f1370,f198]) ).
fof(f1415,definition,
( spl24_50
<=> sP0(sK20,sK14(sK20,sK2(sK21,sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_50])],[avatar_definition]) ).
fof(f1416,plain,
( ~ sP0(sK20,sK14(sK20,sK2(sK21,sK20)))
| spl24_50 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1417,plain,
( sP0(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ spl24_50 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1424,plain,
( n1 = sK16(sK20,sK14(sK20,sK2(sK21,sK20)))
| sK14(sK20,sK2(sK21,sK20)) != sK14(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ spl24_50 ),
inference(resolution,[],[f1417,f168]) ).
fof(f1426,plain,
( n1 = sK15(sK20,sK14(sK20,sK2(sK21,sK20)))
| sK14(sK20,sK2(sK21,sK20)) != sK14(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ spl24_50 ),
inference(resolution,[],[f1417,f170]) ).
fof(f1464,definition,
( spl24_54
<=> ! [X0] :
( relation(relation_composition(sK21,X0))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_54])],[avatar_definition]) ).
fof(f1465,plain,
( ! [X0] :
( relation(relation_composition(sK21,X0))
| ~ relation(X0) )
| ~ spl24_54 ),
inference(avatar_component_clause,[],[f1464]) ).
fof(f1466,plain,
( spl24_54
| ~ spl24_1 ),
inference(avatar_split_clause,[],[f258,f251,f1464]) ).
fof(f1540,definition,
( spl24_60
<=> n1 = n0 ),
introduced(definition,[new_symbols(definition,[spl24_60])],[avatar_definition]) ).
fof(f1541,plain,
( n1 = n0
| ~ spl24_60 ),
inference(avatar_component_clause,[],[f1540]) ).
fof(f1542,plain,
( n1 != n0
| spl24_60 ),
inference(avatar_component_clause,[],[f1540]) ).
fof(f1673,definition,
( spl24_65
<=> ! [X0] :
( in(sK2(sK21,sK20),X0)
| ~ subset(sK20,X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_65])],[avatar_definition]) ).
fof(f1674,plain,
( ! [X0] :
( in(sK2(sK21,sK20),X0)
| ~ subset(sK20,X0) )
| ~ spl24_65 ),
inference(avatar_component_clause,[],[f1673]) ).
fof(f1675,plain,
( spl24_65
| ~ spl24_18 ),
inference(avatar_split_clause,[],[f904,f596,f1673]) ).
fof(f1687,plain,
( ! [X0] :
( ~ subset(sK20,X0)
| n1 = apply(sK17(X0,sK2(sK21,sK20)),sK2(sK21,sK20))
| sP0(X0,sK2(sK21,sK20))
| sK2(sK21,sK20) != sK18(X0,sK2(sK21,sK20)) )
| ~ spl24_65 ),
inference(resolution,[],[f1674,f241]) ).
fof(f1688,plain,
( ! [X0] :
( ~ subset(sK20,X0)
| n1 = apply(sK17(X0,sK2(sK21,sK20)),sK2(sK21,sK20))
| sP0(X0,sK2(sK21,sK20))
| sK2(sK21,sK20) = sK18(X0,sK2(sK21,sK20)) )
| ~ spl24_65 ),
inference(resolution,[],[f1674,f243]) ).
fof(f1702,plain,
( ! [X0] :
( ~ subset(sK20,X0)
| n1 = apply(sK17(X0,sK2(sK21,sK20)),sK2(sK21,sK20))
| sP0(X0,sK2(sK21,sK20)) )
| ~ spl24_65 ),
inference(forward_subsumption_resolution,[],[f1687,f1688]) ).
fof(f1704,definition,
( spl24_66
<=> ! [X0] :
( ~ subset(sK20,X0)
| n1 = apply(sK17(X0,sK2(sK21,sK20)),sK2(sK21,sK20))
| sP0(X0,sK2(sK21,sK20)) ) ),
introduced(definition,[new_symbols(definition,[spl24_66])],[avatar_definition]) ).
fof(f1705,plain,
( ! [X0] :
( n1 = apply(sK17(X0,sK2(sK21,sK20)),sK2(sK21,sK20))
| ~ subset(sK20,X0)
| sP0(X0,sK2(sK21,sK20)) )
| ~ spl24_66 ),
inference(avatar_component_clause,[],[f1704]) ).
fof(f1706,plain,
( spl24_66
| ~ spl24_65 ),
inference(avatar_split_clause,[],[f1702,f1673,f1704]) ).
fof(f3953,plain,
( ~ empty(n0)
| ~ spl24_60 ),
inference(superposition,[],[f203,f1541]) ).
fof(f3958,plain,
( $false
| ~ spl24_60 ),
inference(forward_subsumption_resolution,[],[f3953,f202]) ).
fof(f3959,plain,
~ spl24_60,
inference(avatar_contradiction_clause,[],[f3958]) ).
fof(f4896,definition,
( spl24_185
<=> ! [X0] :
( ~ in(X0,relation_dom(sK21))
| n0 = apply(sK19(sK20),apply(sK21,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl24_185])],[avatar_definition]) ).
fof(f4897,plain,
( ! [X0] :
( n0 = apply(sK19(sK20),apply(sK21,X0))
| ~ in(X0,relation_dom(sK21)) )
| ~ spl24_185 ),
inference(avatar_component_clause,[],[f4896]) ).
fof(f4898,plain,
( spl24_185
| ~ spl24_46 ),
inference(avatar_split_clause,[],[f1376,f1369,f4896]) ).
fof(f4973,definition,
( spl24_189
<=> ! [X0,X1] :
( ~ in(X0,relation_dom(sK21))
| in(apply(sK21,X0),X1)
| ~ subset(relation_rng(sK21),X1) ) ),
introduced(definition,[new_symbols(definition,[spl24_189])],[avatar_definition]) ).
fof(f4974,plain,
( ! [X0,X1] :
( in(apply(sK21,X0),X1)
| ~ in(X0,relation_dom(sK21))
| ~ subset(relation_rng(sK21),X1) )
| ~ spl24_189 ),
inference(avatar_component_clause,[],[f4973]) ).
fof(f4975,plain,
( spl24_189
| ~ spl24_14 ),
inference(avatar_split_clause,[],[f538,f530,f4973]) ).
fof(f5549,definition,
( spl24_214
<=> ! [X0,X1] :
( apply(relation_composition(sK21,X0),X1) = apply(X0,apply(sK21,X1))
| ~ in(X1,relation_dom(relation_composition(sK21,X0)))
| ~ relation(X0)
| ~ function(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_214])],[avatar_definition]) ).
fof(f5550,plain,
( ! [X0,X1] :
( apply(relation_composition(sK21,X0),X1) = apply(X0,apply(sK21,X1))
| ~ in(X1,relation_dom(relation_composition(sK21,X0)))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_214 ),
inference(avatar_component_clause,[],[f5549]) ).
fof(f5551,plain,
( spl24_214
| ~ spl24_1 ),
inference(avatar_split_clause,[],[f288,f251,f5549]) ).
fof(f5560,plain,
( ! [X0,X1] :
( apply(X1,sK22(relation_composition(sK21,X0),X1)) != apply(X0,apply(sK21,sK22(relation_composition(sK21,X0),X1)))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(relation_composition(sK21,X0))
| ~ relation(X1)
| ~ function(X1)
| ~ relation(relation_composition(sK21,X0))
| ~ function(relation_composition(sK21,X0))
| ~ in(sK22(relation_composition(sK21,X0),X1),relation_dom(relation_composition(sK21,X0)))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_214 ),
inference(superposition,[],[f221,f5550]) ).
fof(f5567,plain,
( ! [X0,X1] :
( apply(X1,sK22(relation_composition(sK21,X0),X1)) != apply(X0,apply(sK21,sK22(relation_composition(sK21,X0),X1)))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(relation_composition(sK21,X0))
| ~ relation(X1)
| ~ function(X1)
| ~ relation(relation_composition(sK21,X0))
| ~ function(relation_composition(sK21,X0))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_214 ),
inference(forward_subsumption_resolution,[],[f5560,f220]) ).
fof(f5578,plain,
( ! [X0,X1] :
( apply(X1,sK22(relation_composition(sK21,X0),X1)) != apply(X0,apply(sK21,sK22(relation_composition(sK21,X0),X1)))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(relation_composition(sK21,X0))
| ~ relation(X1)
| ~ function(X1)
| ~ function(relation_composition(sK21,X0))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_54
| ~ spl24_214 ),
inference(forward_subsumption_resolution,[],[f5567,f1465]) ).
fof(f5588,plain,
( ! [X0,X1] :
( apply(X1,sK22(relation_composition(sK21,X0),X1)) != apply(X0,apply(sK21,sK22(relation_composition(sK21,X0),X1)))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(relation_composition(sK21,X0))
| ~ relation(X1)
| ~ function(X1)
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_1
| ~ spl24_54
| ~ spl24_214 ),
inference(forward_subsumption_resolution,[],[f5578,f293]) ).
fof(f7649,definition,
( spl24_268
<=> ! [X0] :
( relation_dom(sK21) = relation_dom(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_268])],[avatar_definition]) ).
fof(f7650,plain,
( ! [X0] :
( relation_dom(sK21) = relation_dom(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) )
| ~ spl24_268 ),
inference(avatar_component_clause,[],[f7649]) ).
fof(f7651,plain,
( spl24_268
| ~ spl24_1 ),
inference(avatar_split_clause,[],[f272,f251,f7649]) ).
fof(f7661,plain,
( ! [X0,X1] :
( in(sK22(relation_composition(sK21,X0),X1),relation_dom(sK21))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(sK21)
| ~ relation(X1)
| ~ function(X1)
| ~ relation(relation_composition(sK21,X0))
| ~ function(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) )
| ~ spl24_268 ),
inference(superposition,[],[f220,f7650]) ).
fof(f7677,plain,
( ! [X0,X1] :
( in(sK22(relation_composition(sK21,X0),X1),relation_dom(sK21))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(sK21)
| ~ relation(X1)
| ~ function(X1)
| ~ function(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) )
| ~ spl24_54
| ~ spl24_268 ),
inference(forward_subsumption_resolution,[],[f7661,f1465]) ).
fof(f7713,definition,
( spl24_270
<=> sK14(sK20,sK2(sK21,sK20)) = sK14(sK20,sK14(sK20,sK2(sK21,sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_270])],[avatar_definition]) ).
fof(f7714,plain,
( sK14(sK20,sK2(sK21,sK20)) = sK14(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ spl24_270 ),
inference(avatar_component_clause,[],[f7713]) ).
fof(f7715,plain,
( sK14(sK20,sK2(sK21,sK20)) != sK14(sK20,sK14(sK20,sK2(sK21,sK20)))
| spl24_270 ),
inference(avatar_component_clause,[],[f7713]) ).
fof(f7717,definition,
( spl24_271
<=> n1 = sK16(sK20,sK14(sK20,sK2(sK21,sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_271])],[avatar_definition]) ).
fof(f7719,plain,
( n1 = sK16(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ spl24_271 ),
inference(avatar_component_clause,[],[f7717]) ).
fof(f7720,plain,
( ~ spl24_270
| spl24_271
| ~ spl24_50 ),
inference(avatar_split_clause,[],[f1424,f1415,f7717,f7713]) ).
fof(f7723,plain,
( sK2(sK21,sK20) != sK14(sK20,sK2(sK21,sK20))
| n0 = sK16(sK20,sK2(sK21,sK20))
| ~ sP0(sK20,sK2(sK21,sK20))
| spl24_270 ),
inference(superposition,[],[f7715,f167]) ).
fof(f7724,plain,
( sK2(sK21,sK20) != sK14(sK20,sK2(sK21,sK20))
| n0 = sK15(sK20,sK2(sK21,sK20))
| ~ sP0(sK20,sK2(sK21,sK20))
| spl24_270 ),
inference(superposition,[],[f7715,f169]) ).
fof(f7729,plain,
( n0 = sK15(sK20,sK2(sK21,sK20))
| ~ sP0(sK20,sK2(sK21,sK20))
| spl24_270 ),
inference(forward_subsumption_resolution,[],[f7724,f169]) ).
fof(f7730,plain,
( n0 = sK16(sK20,sK2(sK21,sK20))
| ~ sP0(sK20,sK2(sK21,sK20))
| spl24_270 ),
inference(forward_subsumption_resolution,[],[f7723,f167]) ).
fof(f7736,plain,
( n1 = sK15(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ spl24_50
| ~ spl24_270 ),
inference(backward_subsumption_resolution,[],[f1426,f7714]) ).
fof(f7749,plain,
( n1 != sK15(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ sP0(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ spl24_271 ),
inference(superposition,[],[f172,f7719]) ).
fof(f7750,plain,
( ~ sP0(sK20,sK14(sK20,sK2(sK21,sK20)))
| ~ spl24_50
| ~ spl24_270
| ~ spl24_271 ),
inference(forward_subsumption_resolution,[],[f7749,f7736]) ).
fof(f7751,plain,
( $false
| ~ spl24_50
| ~ spl24_270
| ~ spl24_271 ),
inference(forward_subsumption_resolution,[],[f7750,f1417]) ).
fof(f7752,plain,
( ~ spl24_50
| ~ spl24_270
| ~ spl24_271 ),
inference(avatar_contradiction_clause,[],[f7751]) ).
fof(f7780,plain,
( ~ sP0(sK20,sK2(sK21,sK20))
| n0 = sK16(sK20,sK2(sK21,sK20))
| ~ sP0(sK20,sK2(sK21,sK20))
| spl24_50 ),
inference(superposition,[],[f1416,f167]) ).
fof(f7781,plain,
( ~ sP0(sK20,sK2(sK21,sK20))
| n0 = sK15(sK20,sK2(sK21,sK20))
| ~ sP0(sK20,sK2(sK21,sK20))
| spl24_50 ),
inference(superposition,[],[f1416,f169]) ).
fof(f7782,plain,
( ~ sP0(sK20,sK2(sK21,sK20))
| n0 = sK15(sK20,sK2(sK21,sK20))
| spl24_50 ),
inference(duplicate_literal_removal,[],[f7781]) ).
fof(f7783,plain,
( ~ sP0(sK20,sK2(sK21,sK20))
| n0 = sK16(sK20,sK2(sK21,sK20))
| spl24_50 ),
inference(duplicate_literal_removal,[],[f7780]) ).
fof(f9953,definition,
( spl24_346
<=> ! [X0] :
( function(relation_composition(sK21,X0))
| ~ relation(X0)
| ~ function(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_346])],[avatar_definition]) ).
fof(f9954,plain,
( ! [X0] :
( function(relation_composition(sK21,X0))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_346 ),
inference(avatar_component_clause,[],[f9953]) ).
fof(f9955,plain,
( spl24_346
| ~ spl24_1 ),
inference(avatar_split_clause,[],[f293,f251,f9953]) ).
fof(f18176,definition,
( spl24_502
<=> ! [X0] :
( ~ subset(relation_rng(X0),sK20)
| relation_dom(X0) = relation_dom(relation_composition(X0,sK17(sK20,sK2(sK21,sK20))))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_502])],[avatar_definition]) ).
fof(f18177,plain,
( ! [X0] :
( relation_dom(X0) = relation_dom(relation_composition(X0,sK17(sK20,sK2(sK21,sK20))))
| ~ subset(relation_rng(X0),sK20)
| ~ relation(X0) )
| ~ spl24_502 ),
inference(avatar_component_clause,[],[f18176]) ).
fof(f18178,plain,
( spl24_502
| spl24_20
| ~ spl24_27 ),
inference(avatar_split_clause,[],[f830,f806,f627,f18176]) ).
fof(f19864,definition,
( spl24_563
<=> ! [X0,X1] :
( apply(X1,sK22(relation_composition(sK21,X0),X1)) != apply(X0,apply(sK21,sK22(relation_composition(sK21,X0),X1)))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(relation_composition(sK21,X0))
| ~ relation(X1)
| ~ function(X1)
| ~ relation(X0)
| ~ function(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_563])],[avatar_definition]) ).
fof(f19865,plain,
( ! [X0,X1] :
( apply(X1,sK22(relation_composition(sK21,X0),X1)) != apply(X0,apply(sK21,sK22(relation_composition(sK21,X0),X1)))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(relation_composition(sK21,X0))
| ~ relation(X1)
| ~ function(X1)
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_563 ),
inference(avatar_component_clause,[],[f19864]) ).
fof(f19866,plain,
( spl24_563
| ~ spl24_1
| ~ spl24_54
| ~ spl24_214 ),
inference(avatar_split_clause,[],[f5588,f5549,f1464,f251,f19864]) ).
fof(f19888,plain,
( ! [X0,X1] :
( n0 != apply(X1,apply(sK21,sK22(relation_composition(sK21,X1),sK19(X0))))
| sK19(X0) = relation_composition(sK21,X1)
| relation_dom(sK19(X0)) != relation_dom(relation_composition(sK21,X1))
| ~ relation(sK19(X0))
| ~ function(sK19(X0))
| ~ relation(X1)
| ~ function(X1)
| ~ in(sK22(relation_composition(sK21,X1),sK19(X0)),X0) )
| ~ spl24_563 ),
inference(superposition,[],[f19865,f198]) ).
fof(f19939,plain,
( ! [X0,X1] :
( n0 != apply(X1,apply(sK21,sK22(relation_composition(sK21,X1),sK19(X0))))
| sK19(X0) = relation_composition(sK21,X1)
| relation_dom(sK19(X0)) != relation_dom(relation_composition(sK21,X1))
| ~ function(sK19(X0))
| ~ relation(X1)
| ~ function(X1)
| ~ in(sK22(relation_composition(sK21,X1),sK19(X0)),X0) )
| ~ spl24_563 ),
inference(forward_subsumption_resolution,[],[f19888,f201]) ).
fof(f19980,plain,
( ! [X0,X1] :
( n0 != apply(X1,apply(sK21,sK22(relation_composition(sK21,X1),sK19(X0))))
| sK19(X0) = relation_composition(sK21,X1)
| relation_dom(sK19(X0)) != relation_dom(relation_composition(sK21,X1))
| ~ relation(X1)
| ~ function(X1)
| ~ in(sK22(relation_composition(sK21,X1),sK19(X0)),X0) )
| ~ spl24_563 ),
inference(forward_subsumption_resolution,[],[f19939,f200]) ).
fof(f20000,plain,
( ! [X0,X1] :
( relation_dom(relation_composition(sK21,X1)) != X0
| n0 != apply(X1,apply(sK21,sK22(relation_composition(sK21,X1),sK19(X0))))
| sK19(X0) = relation_composition(sK21,X1)
| ~ relation(X1)
| ~ function(X1)
| ~ in(sK22(relation_composition(sK21,X1),sK19(X0)),X0) )
| ~ spl24_563 ),
inference(forward_demodulation,[],[f19980,f199]) ).
fof(f20175,definition,
( spl24_568
<=> ! [X0,X1] :
( relation_dom(relation_composition(sK21,X1)) != X0
| n0 != apply(X1,apply(sK21,sK22(relation_composition(sK21,X1),sK19(X0))))
| sK19(X0) = relation_composition(sK21,X1)
| ~ relation(X1)
| ~ function(X1)
| ~ in(sK22(relation_composition(sK21,X1),sK19(X0)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_568])],[avatar_definition]) ).
fof(f20176,plain,
( ! [X0,X1] :
( n0 != apply(X1,apply(sK21,sK22(relation_composition(sK21,X1),sK19(X0))))
| relation_dom(relation_composition(sK21,X1)) != X0
| sK19(X0) = relation_composition(sK21,X1)
| ~ relation(X1)
| ~ function(X1)
| ~ in(sK22(relation_composition(sK21,X1),sK19(X0)),X0) )
| ~ spl24_568 ),
inference(avatar_component_clause,[],[f20175]) ).
fof(f20177,plain,
( spl24_568
| ~ spl24_563 ),
inference(avatar_split_clause,[],[f20000,f19864,f20175]) ).
fof(f20183,plain,
( ! [X2,X0,X1] :
( n0 != n0
| relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1)
| sK18(X0,X1) = X1 )
| ~ spl24_568 ),
inference(superposition,[],[f20176,f247]) ).
fof(f20184,plain,
( ! [X2,X0,X1] :
( n0 != n0
| relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1)
| sK18(X0,X1) != X1 )
| ~ spl24_568 ),
inference(superposition,[],[f20176,f246]) ).
fof(f20202,plain,
( ! [X0] :
( n0 != n0
| relation_dom(relation_composition(sK21,sK19(sK20))) != X0
| sK19(X0) = relation_composition(sK21,sK19(sK20))
| ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),X0)
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),relation_dom(sK21)) )
| ~ spl24_185
| ~ spl24_568 ),
inference(superposition,[],[f20176,f4897]) ).
fof(f20209,plain,
( ! [X0] :
( relation_dom(relation_composition(sK21,sK19(sK20))) != X0
| sK19(X0) = relation_composition(sK21,sK19(sK20))
| ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),X0)
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),relation_dom(sK21)) )
| ~ spl24_185
| ~ spl24_568 ),
inference(trivial_inequality_removal,[],[f20202]) ).
fof(f20227,plain,
( ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1)
| sK18(X0,X1) != X1 )
| ~ spl24_568 ),
inference(trivial_inequality_removal,[],[f20184]) ).
fof(f20228,plain,
( ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1)
| sK18(X0,X1) = X1 )
| ~ spl24_568 ),
inference(trivial_inequality_removal,[],[f20183]) ).
fof(f20233,plain,
( ! [X0] :
( relation_dom(relation_composition(sK21,sK19(sK20))) != X0
| sK19(X0) = relation_composition(sK21,sK19(sK20))
| ~ function(sK19(sK20))
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),X0)
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),relation_dom(sK21)) )
| ~ spl24_185
| ~ spl24_568 ),
inference(forward_subsumption_resolution,[],[f20209,f201]) ).
fof(f20247,plain,
( ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ function(sK17(X0,X1))
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1)
| sK18(X0,X1) != X1 )
| ~ spl24_568 ),
inference(forward_subsumption_resolution,[],[f20227,f229]) ).
fof(f20248,plain,
( ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ function(sK17(X0,X1))
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1)
| sK18(X0,X1) = X1 )
| ~ spl24_568 ),
inference(forward_subsumption_resolution,[],[f20228,f230]) ).
fof(f20254,plain,
( ! [X0] :
( relation_dom(relation_composition(sK21,sK19(sK20))) != X0
| sK19(X0) = relation_composition(sK21,sK19(sK20))
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),X0)
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),relation_dom(sK21)) )
| ~ spl24_185
| ~ spl24_568 ),
inference(forward_subsumption_resolution,[],[f20233,f200]) ).
fof(f20268,plain,
( ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1)
| sK18(X0,X1) != X1 )
| ~ spl24_568 ),
inference(forward_subsumption_resolution,[],[f20247,f232]) ).
fof(f20269,plain,
( ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1)
| sK18(X0,X1) = X1 )
| ~ spl24_568 ),
inference(forward_subsumption_resolution,[],[f20248,f233]) ).
fof(f20273,plain,
( ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1) )
| ~ spl24_568 ),
inference(forward_subsumption_resolution,[],[f20269,f20268]) ).
fof(f20275,definition,
( spl24_569
<=> ! [X0] :
( relation_dom(relation_composition(sK21,sK19(sK20))) != X0
| sK19(X0) = relation_composition(sK21,sK19(sK20))
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),X0)
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),relation_dom(sK21)) ) ),
introduced(definition,[new_symbols(definition,[spl24_569])],[avatar_definition]) ).
fof(f20276,plain,
( ! [X0] :
( relation_dom(relation_composition(sK21,sK19(sK20))) != X0
| sK19(X0) = relation_composition(sK21,sK19(sK20))
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),X0)
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(X0)),relation_dom(sK21)) )
| ~ spl24_569 ),
inference(avatar_component_clause,[],[f20275]) ).
fof(f20277,plain,
( spl24_569
| ~ spl24_185
| ~ spl24_568 ),
inference(avatar_split_clause,[],[f20254,f20175,f4896,f20275]) ).
fof(f20280,plain,
( relation_composition(sK21,sK19(sK20)) = sK19(relation_dom(relation_composition(sK21,sK19(sK20))))
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(relation_composition(sK21,sK19(sK20))))),relation_dom(relation_composition(sK21,sK19(sK20))))
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(relation_composition(sK21,sK19(sK20))))),relation_dom(sK21))
| ~ spl24_569 ),
inference(equality_resolution,[],[f20276]) ).
fof(f20289,definition,
( spl24_570
<=> in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(relation_composition(sK21,sK19(sK20))))),relation_dom(sK21)) ),
introduced(definition,[new_symbols(definition,[spl24_570])],[avatar_definition]) ).
fof(f20291,plain,
( ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(relation_composition(sK21,sK19(sK20))))),relation_dom(sK21))
| spl24_570 ),
inference(avatar_component_clause,[],[f20289]) ).
fof(f20293,definition,
( spl24_571
<=> in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(relation_composition(sK21,sK19(sK20))))),relation_dom(relation_composition(sK21,sK19(sK20)))) ),
introduced(definition,[new_symbols(definition,[spl24_571])],[avatar_definition]) ).
fof(f20294,plain,
( in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(relation_composition(sK21,sK19(sK20))))),relation_dom(relation_composition(sK21,sK19(sK20))))
| ~ spl24_571 ),
inference(avatar_component_clause,[],[f20293]) ).
fof(f20295,plain,
( ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(relation_composition(sK21,sK19(sK20))))),relation_dom(relation_composition(sK21,sK19(sK20))))
| spl24_571 ),
inference(avatar_component_clause,[],[f20293]) ).
fof(f20297,definition,
( spl24_572
<=> relation_composition(sK21,sK19(sK20)) = sK19(relation_dom(relation_composition(sK21,sK19(sK20)))) ),
introduced(definition,[new_symbols(definition,[spl24_572])],[avatar_definition]) ).
fof(f20299,plain,
( relation_composition(sK21,sK19(sK20)) = sK19(relation_dom(relation_composition(sK21,sK19(sK20))))
| ~ spl24_572 ),
inference(avatar_component_clause,[],[f20297]) ).
fof(f20300,plain,
( ~ spl24_570
| ~ spl24_571
| spl24_572
| ~ spl24_569 ),
inference(avatar_split_clause,[],[f20280,f20275,f20297,f20293,f20289]) ).
fof(f20302,plain,
( ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(sK21))),relation_dom(sK21))
| ~ subset(relation_rng(sK21),relation_dom(sK19(sK20)))
| ~ relation(sK19(sK20))
| ~ spl24_268
| spl24_570 ),
inference(superposition,[],[f20291,f7650]) ).
fof(f20305,plain,
( ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(sK21))),relation_dom(sK21))
| ~ subset(relation_rng(sK21),relation_dom(sK19(sK20)))
| ~ spl24_268
| spl24_570 ),
inference(forward_subsumption_resolution,[],[f20302,f201]) ).
fof(f20307,plain,
( ~ subset(relation_rng(sK21),sK20)
| ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(sK21))),relation_dom(sK21))
| ~ spl24_268
| spl24_570 ),
inference(forward_demodulation,[],[f20305,f199]) ).
fof(f20309,plain,
( ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(sK21))),relation_dom(sK21))
| ~ spl24_4
| ~ spl24_268
| spl24_570 ),
inference(forward_subsumption_resolution,[],[f20307,f335]) ).
fof(f20312,definition,
( spl24_573
<=> in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(sK21))),relation_dom(sK21)) ),
introduced(definition,[new_symbols(definition,[spl24_573])],[avatar_definition]) ).
fof(f20314,plain,
( ~ in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(sK21))),relation_dom(sK21))
| spl24_573 ),
inference(avatar_component_clause,[],[f20312]) ).
fof(f20315,plain,
( ~ spl24_573
| ~ spl24_4
| ~ spl24_268
| spl24_570 ),
inference(avatar_split_clause,[],[f20309,f20289,f7649,f333,f20312]) ).
fof(f20412,plain,
( relation_composition(sK21,sK19(sK20)) = sK19(relation_dom(relation_composition(sK21,sK19(sK20))))
| relation_dom(relation_composition(sK21,sK19(sK20))) != relation_dom(sK19(relation_dom(relation_composition(sK21,sK19(sK20)))))
| ~ relation(sK19(relation_dom(relation_composition(sK21,sK19(sK20)))))
| ~ function(sK19(relation_dom(relation_composition(sK21,sK19(sK20)))))
| ~ relation(relation_composition(sK21,sK19(sK20)))
| ~ function(relation_composition(sK21,sK19(sK20)))
| spl24_571 ),
inference(resolution,[],[f20295,f220]) ).
fof(f20416,plain,
( relation_composition(sK21,sK19(sK20)) = sK19(relation_dom(relation_composition(sK21,sK19(sK20))))
| ~ relation(sK19(relation_dom(relation_composition(sK21,sK19(sK20)))))
| ~ function(sK19(relation_dom(relation_composition(sK21,sK19(sK20)))))
| ~ relation(relation_composition(sK21,sK19(sK20)))
| ~ function(relation_composition(sK21,sK19(sK20)))
| spl24_571 ),
inference(forward_subsumption_resolution,[],[f20412,f199]) ).
fof(f20417,plain,
( relation_composition(sK21,sK19(sK20)) = sK19(relation_dom(relation_composition(sK21,sK19(sK20))))
| ~ function(sK19(relation_dom(relation_composition(sK21,sK19(sK20)))))
| ~ relation(relation_composition(sK21,sK19(sK20)))
| ~ function(relation_composition(sK21,sK19(sK20)))
| spl24_571 ),
inference(forward_subsumption_resolution,[],[f20416,f201]) ).
fof(f20418,plain,
( relation_composition(sK21,sK19(sK20)) = sK19(relation_dom(relation_composition(sK21,sK19(sK20))))
| ~ relation(relation_composition(sK21,sK19(sK20)))
| ~ function(relation_composition(sK21,sK19(sK20)))
| spl24_571 ),
inference(forward_subsumption_resolution,[],[f20417,f200]) ).
fof(f20420,definition,
( spl24_582
<=> function(relation_composition(sK21,sK19(sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_582])],[avatar_definition]) ).
fof(f20422,plain,
( ~ function(relation_composition(sK21,sK19(sK20)))
| spl24_582 ),
inference(avatar_component_clause,[],[f20420]) ).
fof(f20424,definition,
( spl24_583
<=> relation(relation_composition(sK21,sK19(sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_583])],[avatar_definition]) ).
fof(f20426,plain,
( ~ relation(relation_composition(sK21,sK19(sK20)))
| spl24_583 ),
inference(avatar_component_clause,[],[f20424]) ).
fof(f20427,plain,
( ~ spl24_582
| ~ spl24_583
| spl24_572
| spl24_571 ),
inference(avatar_split_clause,[],[f20418,f20293,f20297,f20424,f20420]) ).
fof(f20429,plain,
( ~ relation(sK21)
| ~ function(sK21)
| ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| spl24_582 ),
inference(resolution,[],[f20422,f139]) ).
fof(f20431,plain,
( ~ function(sK21)
| ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| ~ spl24_1
| spl24_582 ),
inference(forward_subsumption_resolution,[],[f20429,f253]) ).
fof(f20433,plain,
( ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| ~ spl24_1
| ~ spl24_2
| spl24_582 ),
inference(forward_subsumption_resolution,[],[f20431,f300]) ).
fof(f20436,plain,
( ~ function(sK19(sK20))
| ~ spl24_1
| ~ spl24_2
| spl24_582 ),
inference(forward_subsumption_resolution,[],[f20433,f201]) ).
fof(f20437,plain,
( $false
| ~ spl24_1
| ~ spl24_2
| spl24_582 ),
inference(forward_subsumption_resolution,[],[f20436,f200]) ).
fof(f20438,plain,
( ~ spl24_1
| ~ spl24_2
| spl24_582 ),
inference(avatar_contradiction_clause,[],[f20437]) ).
fof(f20441,plain,
( ~ relation(sK21)
| ~ function(sK21)
| ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| spl24_583 ),
inference(resolution,[],[f20426,f140]) ).
fof(f20447,plain,
( ~ function(sK21)
| ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| ~ spl24_1
| spl24_583 ),
inference(forward_subsumption_resolution,[],[f20441,f253]) ).
fof(f20453,plain,
( ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| ~ spl24_1
| ~ spl24_2
| spl24_583 ),
inference(forward_subsumption_resolution,[],[f20447,f300]) ).
fof(f20454,plain,
( ~ function(sK19(sK20))
| ~ spl24_1
| ~ spl24_2
| spl24_583 ),
inference(forward_subsumption_resolution,[],[f20453,f201]) ).
fof(f20455,plain,
( $false
| ~ spl24_1
| ~ spl24_2
| spl24_583 ),
inference(forward_subsumption_resolution,[],[f20454,f200]) ).
fof(f20456,plain,
( ~ spl24_1
| ~ spl24_2
| spl24_583 ),
inference(avatar_contradiction_clause,[],[f20455]) ).
fof(f20457,plain,
( sK19(relation_dom(sK21)) = relation_composition(sK21,sK19(sK20))
| ~ subset(relation_rng(sK21),relation_dom(sK19(sK20)))
| ~ relation(sK19(sK20))
| ~ spl24_268
| ~ spl24_572 ),
inference(superposition,[],[f20299,f7650]) ).
fof(f20479,plain,
( sK19(relation_dom(sK21)) = relation_composition(sK21,sK19(sK20))
| ~ subset(relation_rng(sK21),relation_dom(sK19(sK20)))
| ~ spl24_268
| ~ spl24_572 ),
inference(forward_subsumption_resolution,[],[f20457,f201]) ).
fof(f20481,plain,
( ~ subset(relation_rng(sK21),sK20)
| sK19(relation_dom(sK21)) = relation_composition(sK21,sK19(sK20))
| ~ spl24_268
| ~ spl24_572 ),
inference(forward_demodulation,[],[f20479,f199]) ).
fof(f20483,plain,
( sK19(relation_dom(sK21)) = relation_composition(sK21,sK19(sK20))
| ~ spl24_4
| ~ spl24_268
| ~ spl24_572 ),
inference(forward_subsumption_resolution,[],[f20481,f335]) ).
fof(f20678,definition,
( spl24_588
<=> sK19(relation_dom(sK21)) = relation_composition(sK21,sK19(sK20)) ),
introduced(definition,[new_symbols(definition,[spl24_588])],[avatar_definition]) ).
fof(f20680,plain,
( sK19(relation_dom(sK21)) = relation_composition(sK21,sK19(sK20))
| ~ spl24_588 ),
inference(avatar_component_clause,[],[f20678]) ).
fof(f20681,plain,
( spl24_588
| ~ spl24_4
| ~ spl24_268
| ~ spl24_572 ),
inference(avatar_split_clause,[],[f20483,f20297,f7649,f333,f20678]) ).
fof(f20836,plain,
( in(sK22(relation_composition(sK21,sK19(sK20)),sK19(relation_dom(sK21))),relation_dom(sK21))
| ~ subset(relation_rng(sK21),relation_dom(sK19(sK20)))
| ~ relation(sK19(sK20))
| ~ relation(sK21)
| ~ spl24_571 ),
inference(superposition,[],[f20294,f214]) ).
fof(f20837,plain,
( ~ subset(relation_rng(sK21),relation_dom(sK19(sK20)))
| ~ relation(sK19(sK20))
| ~ relation(sK21)
| ~ spl24_571
| spl24_573 ),
inference(forward_subsumption_resolution,[],[f20836,f20314]) ).
fof(f20845,plain,
( ~ subset(relation_rng(sK21),relation_dom(sK19(sK20)))
| ~ relation(sK21)
| ~ spl24_571
| spl24_573 ),
inference(forward_subsumption_resolution,[],[f20837,f201]) ).
fof(f20850,plain,
( ~ subset(relation_rng(sK21),relation_dom(sK19(sK20)))
| ~ spl24_1
| ~ spl24_571
| spl24_573 ),
inference(forward_subsumption_resolution,[],[f20845,f253]) ).
fof(f20853,plain,
( ~ subset(relation_rng(sK21),sK20)
| ~ spl24_1
| ~ spl24_571
| spl24_573 ),
inference(forward_demodulation,[],[f20850,f199]) ).
fof(f20857,plain,
( $false
| ~ spl24_1
| ~ spl24_4
| ~ spl24_571
| spl24_573 ),
inference(forward_subsumption_resolution,[],[f20853,f335]) ).
fof(f20858,plain,
( ~ spl24_1
| ~ spl24_4
| ~ spl24_571
| spl24_573 ),
inference(avatar_contradiction_clause,[],[f20857]) ).
fof(f20959,plain,
( ! [X0] :
( relation_composition(sK21,X0) != sK19(relation_dom(sK21))
| relation_dom(X0) != sK20
| sK20 != relation_dom(sK19(sK20))
| sK19(sK20) = X0
| ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_15
| ~ spl24_588 ),
inference(superposition,[],[f575,f20680]) ).
fof(f20984,plain,
( ! [X0] :
( relation_composition(sK21,X0) != sK19(relation_dom(sK21))
| relation_dom(X0) != sK20
| sK19(sK20) = X0
| ~ relation(sK19(sK20))
| ~ function(sK19(sK20))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_15
| ~ spl24_588 ),
inference(forward_subsumption_resolution,[],[f20959,f199]) ).
fof(f21004,plain,
( ! [X0] :
( relation_composition(sK21,X0) != sK19(relation_dom(sK21))
| relation_dom(X0) != sK20
| sK19(sK20) = X0
| ~ function(sK19(sK20))
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_15
| ~ spl24_588 ),
inference(forward_subsumption_resolution,[],[f20984,f201]) ).
fof(f21013,plain,
( ! [X0] :
( relation_composition(sK21,X0) != sK19(relation_dom(sK21))
| relation_dom(X0) != sK20
| sK19(sK20) = X0
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_15
| ~ spl24_588 ),
inference(forward_subsumption_resolution,[],[f21004,f200]) ).
fof(f21038,definition,
( spl24_593
<=> ! [X0] :
( relation_composition(sK21,X0) != sK19(relation_dom(sK21))
| relation_dom(X0) != sK20
| sK19(sK20) = X0
| ~ relation(X0)
| ~ function(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_593])],[avatar_definition]) ).
fof(f21039,plain,
( ! [X0] :
( relation_composition(sK21,X0) != sK19(relation_dom(sK21))
| relation_dom(X0) != sK20
| sK19(sK20) = X0
| ~ relation(X0)
| ~ function(X0) )
| ~ spl24_593 ),
inference(avatar_component_clause,[],[f21038]) ).
fof(f21040,plain,
( spl24_593
| ~ spl24_15
| ~ spl24_588 ),
inference(avatar_split_clause,[],[f21013,f20678,f574,f21038]) ).
fof(f22881,definition,
( spl24_669
<=> ! [X0,X1] :
( in(sK22(relation_composition(sK21,X0),X1),relation_dom(sK21))
| relation_composition(sK21,X0) = X1
| relation_dom(X1) != relation_dom(sK21)
| ~ relation(X1)
| ~ function(X1)
| ~ function(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_669])],[avatar_definition]) ).
fof(f22882,plain,
( ! [X0,X1] :
( relation_dom(X1) != relation_dom(sK21)
| relation_composition(sK21,X0) = X1
| in(sK22(relation_composition(sK21,X0),X1),relation_dom(sK21))
| ~ relation(X1)
| ~ function(X1)
| ~ function(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) )
| ~ spl24_669 ),
inference(avatar_component_clause,[],[f22881]) ).
fof(f22883,plain,
( spl24_669
| ~ spl24_54
| ~ spl24_268 ),
inference(avatar_split_clause,[],[f7677,f7649,f1464,f22881]) ).
fof(f22900,plain,
( ! [X0,X1] :
( relation_dom(sK21) != X0
| sK19(X0) = relation_composition(sK21,X1)
| in(sK22(relation_composition(sK21,X1),sK19(X0)),relation_dom(sK21))
| ~ relation(sK19(X0))
| ~ function(sK19(X0))
| ~ function(relation_composition(sK21,X1))
| ~ subset(relation_rng(sK21),relation_dom(X1))
| ~ relation(X1) )
| ~ spl24_669 ),
inference(superposition,[],[f22882,f199]) ).
fof(f22918,plain,
( ! [X0,X1] :
( relation_dom(sK21) != X0
| sK19(X0) = relation_composition(sK21,X1)
| in(sK22(relation_composition(sK21,X1),sK19(X0)),relation_dom(sK21))
| ~ function(sK19(X0))
| ~ function(relation_composition(sK21,X1))
| ~ subset(relation_rng(sK21),relation_dom(X1))
| ~ relation(X1) )
| ~ spl24_669 ),
inference(forward_subsumption_resolution,[],[f22900,f201]) ).
fof(f22928,plain,
( ! [X0,X1] :
( relation_dom(sK21) != X0
| sK19(X0) = relation_composition(sK21,X1)
| in(sK22(relation_composition(sK21,X1),sK19(X0)),relation_dom(sK21))
| ~ function(relation_composition(sK21,X1))
| ~ subset(relation_rng(sK21),relation_dom(X1))
| ~ relation(X1) )
| ~ spl24_669 ),
inference(forward_subsumption_resolution,[],[f22918,f200]) ).
fof(f25495,definition,
( spl24_738
<=> ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl24_738])],[avatar_definition]) ).
fof(f25496,plain,
( ! [X2,X0,X1] :
( relation_dom(relation_composition(sK21,sK17(X0,X1))) != X2
| relation_composition(sK21,sK17(X0,X1)) = sK19(X2)
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2)),X2)
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(X2))),X0)
| sP0(X0,X1) )
| ~ spl24_738 ),
inference(avatar_component_clause,[],[f25495]) ).
fof(f25497,plain,
( spl24_738
| ~ spl24_568 ),
inference(avatar_split_clause,[],[f20273,f20175,f25495]) ).
fof(f25503,plain,
( ! [X0,X1] :
( relation_composition(sK21,sK17(X0,X1)) = sK19(relation_dom(relation_composition(sK21,sK17(X0,X1))))
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1))))),relation_dom(relation_composition(sK21,sK17(X0,X1))))
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1)))))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1)))))),X0)
| sP0(X0,X1) )
| ~ spl24_738 ),
inference(equality_resolution,[],[f25496]) ).
fof(f25514,definition,
( spl24_739
<=> ! [X0,X1] :
( relation_composition(sK21,sK17(X0,X1)) = sK19(relation_dom(relation_composition(sK21,sK17(X0,X1))))
| ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1))))),relation_dom(relation_composition(sK21,sK17(X0,X1))))
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1)))))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1)))))),X0)
| sP0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl24_739])],[avatar_definition]) ).
fof(f25515,plain,
( ! [X0,X1] :
( ~ in(sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1))))),relation_dom(relation_composition(sK21,sK17(X0,X1))))
| relation_composition(sK21,sK17(X0,X1)) = sK19(relation_dom(relation_composition(sK21,sK17(X0,X1))))
| apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1)))))) = X1
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(X0,X1)),sK19(relation_dom(relation_composition(sK21,sK17(X0,X1)))))),X0)
| sP0(X0,X1) )
| ~ spl24_739 ),
inference(avatar_component_clause,[],[f25514]) ).
fof(f25516,plain,
( spl24_739
| ~ spl24_738 ),
inference(avatar_split_clause,[],[f25503,f25495,f25514]) ).
fof(f25521,plain,
( ~ in(sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))),relation_dom(sK21))
| sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| sK2(sK21,sK20) = apply(sK21,sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))))
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21)))),sK20)
| sP0(sK20,sK2(sK21,sK20))
| ~ subset(relation_rng(sK21),sK20)
| ~ relation(sK21)
| ~ spl24_502
| ~ spl24_739 ),
inference(superposition,[],[f25515,f18177]) ).
fof(f25527,plain,
( ~ in(sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))),relation_dom(sK21))
| sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ in(apply(sK21,sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21)))),sK20)
| sP0(sK20,sK2(sK21,sK20))
| ~ subset(relation_rng(sK21),sK20)
| ~ relation(sK21)
| ~ spl24_37
| ~ spl24_502
| ~ spl24_739 ),
inference(forward_subsumption_resolution,[],[f25521,f1188]) ).
fof(f25531,plain,
( ~ in(sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))),relation_dom(sK21))
| sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| sP0(sK20,sK2(sK21,sK20))
| ~ subset(relation_rng(sK21),sK20)
| ~ relation(sK21)
| ~ spl24_37
| ~ spl24_189
| ~ spl24_502
| ~ spl24_739 ),
inference(forward_subsumption_resolution,[],[f25527,f4974]) ).
fof(f25535,plain,
( ~ in(sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))),relation_dom(sK21))
| sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ subset(relation_rng(sK21),sK20)
| ~ relation(sK21)
| spl24_20
| ~ spl24_37
| ~ spl24_189
| ~ spl24_502
| ~ spl24_739 ),
inference(forward_subsumption_resolution,[],[f25531,f628]) ).
fof(f25539,plain,
( ~ in(sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))),relation_dom(sK21))
| sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ relation(sK21)
| ~ spl24_4
| spl24_20
| ~ spl24_37
| ~ spl24_189
| ~ spl24_502
| ~ spl24_739 ),
inference(forward_subsumption_resolution,[],[f25535,f335]) ).
fof(f25540,plain,
( ~ in(sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))),relation_dom(sK21))
| sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_1
| ~ spl24_4
| spl24_20
| ~ spl24_37
| ~ spl24_189
| ~ spl24_502
| ~ spl24_739 ),
inference(forward_subsumption_resolution,[],[f25539,f253]) ).
fof(f25542,definition,
( spl24_740
<=> sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))) ),
introduced(definition,[new_symbols(definition,[spl24_740])],[avatar_definition]) ).
fof(f25544,plain,
( sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_740 ),
inference(avatar_component_clause,[],[f25542]) ).
fof(f25546,definition,
( spl24_741
<=> in(sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))),relation_dom(sK21)) ),
introduced(definition,[new_symbols(definition,[spl24_741])],[avatar_definition]) ).
fof(f25548,plain,
( ~ in(sK22(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))),sK19(relation_dom(sK21))),relation_dom(sK21))
| spl24_741 ),
inference(avatar_component_clause,[],[f25546]) ).
fof(f25549,plain,
( spl24_740
| ~ spl24_741
| ~ spl24_1
| ~ spl24_4
| spl24_20
| ~ spl24_37
| ~ spl24_189
| ~ spl24_502
| ~ spl24_739 ),
inference(avatar_split_clause,[],[f25540,f25514,f18176,f4973,f1187,f627,f333,f251,f25546,f25542]) ).
fof(f109009,definition,
( spl24_1656
<=> sK19(sK20) = sK17(sK20,sK2(sK21,sK20)) ),
introduced(definition,[new_symbols(definition,[spl24_1656])],[avatar_definition]) ).
fof(f109011,plain,
( sK19(sK20) = sK17(sK20,sK2(sK21,sK20))
| ~ spl24_1656 ),
inference(avatar_component_clause,[],[f109009]) ).
fof(f110148,definition,
( spl24_1725
<=> ! [X0,X1] :
( relation_dom(sK21) != X0
| sK19(X0) = relation_composition(sK21,X1)
| in(sK22(relation_composition(sK21,X1),sK19(X0)),relation_dom(sK21))
| ~ function(relation_composition(sK21,X1))
| ~ subset(relation_rng(sK21),relation_dom(X1))
| ~ relation(X1) ) ),
introduced(definition,[new_symbols(definition,[spl24_1725])],[avatar_definition]) ).
fof(f110149,plain,
( ! [X0,X1] :
( relation_dom(sK21) != X0
| sK19(X0) = relation_composition(sK21,X1)
| in(sK22(relation_composition(sK21,X1),sK19(X0)),relation_dom(sK21))
| ~ function(relation_composition(sK21,X1))
| ~ subset(relation_rng(sK21),relation_dom(X1))
| ~ relation(X1) )
| ~ spl24_1725 ),
inference(avatar_component_clause,[],[f110148]) ).
fof(f110150,plain,
( spl24_1725
| ~ spl24_669 ),
inference(avatar_split_clause,[],[f22928,f22881,f110148]) ).
fof(f110151,plain,
( ! [X0] :
( relation_composition(sK21,X0) = sK19(relation_dom(sK21))
| in(sK22(relation_composition(sK21,X0),sK19(relation_dom(sK21))),relation_dom(sK21))
| ~ function(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) )
| ~ spl24_1725 ),
inference(equality_resolution,[],[f110149]) ).
fof(f110153,definition,
( spl24_1726
<=> ! [X0] :
( relation_composition(sK21,X0) = sK19(relation_dom(sK21))
| in(sK22(relation_composition(sK21,X0),sK19(relation_dom(sK21))),relation_dom(sK21))
| ~ function(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_1726])],[avatar_definition]) ).
fof(f110154,plain,
( ! [X0] :
( in(sK22(relation_composition(sK21,X0),sK19(relation_dom(sK21))),relation_dom(sK21))
| relation_composition(sK21,X0) = sK19(relation_dom(sK21))
| ~ function(relation_composition(sK21,X0))
| ~ subset(relation_rng(sK21),relation_dom(X0))
| ~ relation(X0) )
| ~ spl24_1726 ),
inference(avatar_component_clause,[],[f110153]) ).
fof(f110155,plain,
( spl24_1726
| ~ spl24_1725 ),
inference(avatar_split_clause,[],[f110151,f110148,f110153]) ).
fof(f110159,plain,
( sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ function(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))))
| ~ subset(relation_rng(sK21),relation_dom(sK17(sK20,sK2(sK21,sK20))))
| ~ relation(sK17(sK20,sK2(sK21,sK20)))
| spl24_741
| ~ spl24_1726 ),
inference(resolution,[],[f110154,f25548]) ).
fof(f110185,plain,
( sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ function(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))))
| ~ subset(relation_rng(sK21),relation_dom(sK17(sK20,sK2(sK21,sK20))))
| ~ spl24_34
| spl24_741
| ~ spl24_1726 ),
inference(forward_subsumption_resolution,[],[f110159,f1058]) ).
fof(f110190,plain,
( ~ subset(relation_rng(sK21),sK20)
| sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ function(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))))
| ~ spl24_27
| ~ spl24_34
| spl24_741
| ~ spl24_1726 ),
inference(forward_demodulation,[],[f110185,f808]) ).
fof(f110194,plain,
( sK19(relation_dom(sK21)) = relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))
| ~ function(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))))
| ~ spl24_4
| ~ spl24_27
| ~ spl24_34
| spl24_741
| ~ spl24_1726 ),
inference(forward_subsumption_resolution,[],[f110190,f335]) ).
fof(f110428,definition,
( spl24_1732
<=> function(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20)))) ),
introduced(definition,[new_symbols(definition,[spl24_1732])],[avatar_definition]) ).
fof(f110430,plain,
( ~ function(relation_composition(sK21,sK17(sK20,sK2(sK21,sK20))))
| spl24_1732 ),
inference(avatar_component_clause,[],[f110428]) ).
fof(f110431,plain,
( ~ spl24_1732
| spl24_740
| ~ spl24_4
| ~ spl24_27
| ~ spl24_34
| spl24_741
| ~ spl24_1726 ),
inference(avatar_split_clause,[],[f110194,f110153,f25546,f1056,f806,f333,f25542,f110428]) ).
fof(f110432,plain,
( ~ relation(sK17(sK20,sK2(sK21,sK20)))
| ~ function(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_346
| spl24_1732 ),
inference(resolution,[],[f110430,f9954]) ).
fof(f110436,plain,
( ~ function(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_34
| ~ spl24_346
| spl24_1732 ),
inference(forward_subsumption_resolution,[],[f110432,f1058]) ).
fof(f110438,plain,
( $false
| ~ spl24_33
| ~ spl24_34
| ~ spl24_346
| spl24_1732 ),
inference(forward_subsumption_resolution,[],[f110436,f1053]) ).
fof(f110439,plain,
( ~ spl24_33
| ~ spl24_34
| ~ spl24_346
| spl24_1732 ),
inference(avatar_contradiction_clause,[],[f110438]) ).
fof(f110461,plain,
( sK19(relation_dom(sK21)) != sK19(relation_dom(sK21))
| sK20 != relation_dom(sK17(sK20,sK2(sK21,sK20)))
| sK19(sK20) = sK17(sK20,sK2(sK21,sK20))
| ~ relation(sK17(sK20,sK2(sK21,sK20)))
| ~ function(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_593
| ~ spl24_740 ),
inference(superposition,[],[f21039,f25544]) ).
fof(f110489,plain,
( sK20 != relation_dom(sK17(sK20,sK2(sK21,sK20)))
| sK19(sK20) = sK17(sK20,sK2(sK21,sK20))
| ~ relation(sK17(sK20,sK2(sK21,sK20)))
| ~ function(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_593
| ~ spl24_740 ),
inference(trivial_inequality_removal,[],[f110461]) ).
fof(f110498,plain,
( sK19(sK20) = sK17(sK20,sK2(sK21,sK20))
| ~ relation(sK17(sK20,sK2(sK21,sK20)))
| ~ function(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_27
| ~ spl24_593
| ~ spl24_740 ),
inference(forward_subsumption_resolution,[],[f110489,f808]) ).
fof(f110517,plain,
( sK19(sK20) = sK17(sK20,sK2(sK21,sK20))
| ~ function(sK17(sK20,sK2(sK21,sK20)))
| ~ spl24_27
| ~ spl24_34
| ~ spl24_593
| ~ spl24_740 ),
inference(forward_subsumption_resolution,[],[f110498,f1058]) ).
fof(f110534,plain,
( sK19(sK20) = sK17(sK20,sK2(sK21,sK20))
| ~ spl24_27
| ~ spl24_33
| ~ spl24_34
| ~ spl24_593
| ~ spl24_740 ),
inference(forward_subsumption_resolution,[],[f110517,f1053]) ).
fof(f110557,plain,
( spl24_1656
| ~ spl24_27
| ~ spl24_33
| ~ spl24_34
| ~ spl24_593
| ~ spl24_740 ),
inference(avatar_split_clause,[],[f110534,f25542,f21038,f1056,f1051,f806,f109009]) ).
fof(f110634,plain,
( n1 = apply(sK19(sK20),sK2(sK21,sK20))
| ~ subset(sK20,sK20)
| sP0(sK20,sK2(sK21,sK20))
| ~ spl24_66
| ~ spl24_1656 ),
inference(superposition,[],[f1705,f109011]) ).
fof(f110742,plain,
( n1 = apply(sK19(sK20),sK2(sK21,sK20))
| sP0(sK20,sK2(sK21,sK20))
| ~ spl24_66
| ~ spl24_1656 ),
inference(forward_subsumption_resolution,[],[f110634,f222]) ).
fof(f110778,plain,
( n1 = apply(sK19(sK20),sK2(sK21,sK20))
| spl24_20
| ~ spl24_66
| ~ spl24_1656 ),
inference(forward_subsumption_resolution,[],[f110742,f628]) ).
fof(f110805,plain,
( n1 = n0
| spl24_20
| ~ spl24_25
| ~ spl24_66
| ~ spl24_1656 ),
inference(forward_demodulation,[],[f110778,f736]) ).
fof(f110826,plain,
( $false
| spl24_20
| ~ spl24_25
| spl24_60
| ~ spl24_66
| ~ spl24_1656 ),
inference(forward_subsumption_resolution,[],[f110805,f1542]) ).
fof(f110827,plain,
( spl24_20
| ~ spl24_25
| spl24_60
| ~ spl24_66
| ~ spl24_1656 ),
inference(avatar_contradiction_clause,[],[f110826]) ).
fof(f110859,plain,
( n0 = sK15(sK20,sK2(sK21,sK20))
| ~ spl24_20
| spl24_270 ),
inference(forward_subsumption_resolution,[],[f7729,f629]) ).
fof(f110860,plain,
( n0 = sK16(sK20,sK2(sK21,sK20))
| ~ spl24_20
| spl24_270 ),
inference(forward_subsumption_resolution,[],[f7730,f629]) ).
fof(f110861,plain,
( n0 = sK15(sK20,sK2(sK21,sK20))
| ~ spl24_20
| spl24_50 ),
inference(forward_subsumption_resolution,[],[f7782,f629]) ).
fof(f110862,plain,
( n0 = sK16(sK20,sK2(sK21,sK20))
| ~ spl24_20
| spl24_50 ),
inference(forward_subsumption_resolution,[],[f7783,f629]) ).
fof(f110912,plain,
( sK16(sK20,sK2(sK21,sK20)) != sK15(sK20,sK2(sK21,sK20))
| ~ spl24_20 ),
inference(resolution,[],[f629,f172]) ).
fof(f110913,plain,
( n0 != sK16(sK20,sK2(sK21,sK20))
| ~ spl24_20
| spl24_270 ),
inference(forward_demodulation,[],[f110912,f110859]) ).
fof(f110916,plain,
( $false
| ~ spl24_20
| spl24_270 ),
inference(forward_subsumption_resolution,[],[f110913,f110860]) ).
fof(f110917,plain,
( ~ spl24_20
| spl24_270 ),
inference(avatar_contradiction_clause,[],[f110916]) ).
fof(f110923,plain,
( n0 != sK16(sK20,sK2(sK21,sK20))
| ~ spl24_20
| spl24_50 ),
inference(forward_demodulation,[],[f110912,f110861]) ).
fof(f110926,plain,
( $false
| ~ spl24_20
| spl24_50 ),
inference(forward_subsumption_resolution,[],[f110923,f110862]) ).
fof(f110927,plain,
( ~ spl24_20
| spl24_50 ),
inference(avatar_contradiction_clause,[],[f110926]) ).
cnf(s1,plain,
spl24_1,
inference(sat_conversion,[],[f254]) ).
cnf(s2,plain,
spl24_2,
inference(sat_conversion,[],[f301]) ).
cnf(s3,plain,
~ spl24_3,
inference(sat_conversion,[],[f322]) ).
cnf(s4,plain,
spl24_4,
inference(sat_conversion,[],[f336]) ).
cnf(s9,plain,
( ~ spl24_4
| spl24_9 ),
inference(sat_conversion,[],[f429]) ).
cnf(s13,plain,
( ~ spl24_1
| spl24_14 ),
inference(sat_conversion,[],[f532]) ).
cnf(s14,plain,
spl24_15,
inference(sat_conversion,[],[f576]) ).
cnf(s16,plain,
( ~ spl24_1
| ~ spl24_2
| spl24_3
| spl24_17 ),
inference(sat_conversion,[],[f593]) ).
cnf(s17,plain,
( ~ spl24_17
| spl24_18
| spl24_19 ),
inference(sat_conversion,[],[f603]) ).
cnf(s19,plain,
( ~ spl24_1
| ~ spl24_2
| spl24_3
| spl24_18
| spl24_22 ),
inference(sat_conversion,[],[f671]) ).
cnf(s21,plain,
( ~ spl24_1
| ~ spl24_2
| ~ spl24_19
| spl24_24 ),
inference(sat_conversion,[],[f728]) ).
cnf(s22,plain,
( ~ spl24_18
| spl24_25 ),
inference(sat_conversion,[],[f737]) ).
cnf(s24,plain,
( spl24_20
| spl24_27 ),
inference(sat_conversion,[],[f809]) ).
cnf(s26,plain,
( ~ spl24_22
| ~ spl24_24
| spl24_30 ),
inference(sat_conversion,[],[f862]) ).
cnf(s27,plain,
( ~ spl24_9
| spl24_18
| ~ spl24_30 ),
inference(sat_conversion,[],[f895]) ).
cnf(s30,plain,
( spl24_20
| spl24_33 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s31,plain,
( spl24_20
| spl24_34 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s34,plain,
( ~ spl24_1
| ~ spl24_2
| spl24_3
| ~ spl24_18
| spl24_37 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s44,plain,
( ~ spl24_1
| ~ spl24_2
| ~ spl24_9
| spl24_46 ),
inference(sat_conversion,[],[f1371]) ).
cnf(s51,plain,
( ~ spl24_1
| spl24_54 ),
inference(sat_conversion,[],[f1466]) ).
cnf(s66,plain,
( ~ spl24_18
| spl24_65 ),
inference(sat_conversion,[],[f1675]) ).
cnf(s67,plain,
( ~ spl24_65
| spl24_66 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s164,plain,
~ spl24_60,
inference(sat_conversion,[],[f3959]) ).
cnf(s206,plain,
( ~ spl24_46
| spl24_185 ),
inference(sat_conversion,[],[f4898]) ).
cnf(s210,plain,
( ~ spl24_14
| spl24_189 ),
inference(sat_conversion,[],[f4975]) ).
cnf(s233,plain,
( ~ spl24_1
| spl24_214 ),
inference(sat_conversion,[],[f5551]) ).
cnf(s321,plain,
( ~ spl24_1
| spl24_268 ),
inference(sat_conversion,[],[f7651]) ).
cnf(s323,plain,
( ~ spl24_50
| ~ spl24_270
| spl24_271 ),
inference(sat_conversion,[],[f7720]) ).
cnf(s325,plain,
( ~ spl24_50
| ~ spl24_270
| ~ spl24_271 ),
inference(sat_conversion,[],[f7752]) ).
cnf(s406,plain,
( ~ spl24_1
| spl24_346 ),
inference(sat_conversion,[],[f9955]) ).
cnf(s678,plain,
( spl24_20
| ~ spl24_27
| spl24_502 ),
inference(sat_conversion,[],[f18178]) ).
cnf(s739,plain,
( ~ spl24_1
| ~ spl24_54
| ~ spl24_214
| spl24_563 ),
inference(sat_conversion,[],[f19866]) ).
cnf(s744,plain,
( ~ spl24_563
| spl24_568 ),
inference(sat_conversion,[],[f20177]) ).
cnf(s745,plain,
( ~ spl24_185
| ~ spl24_568
| spl24_569 ),
inference(sat_conversion,[],[f20277]) ).
cnf(s746,plain,
( ~ spl24_569
| ~ spl24_570
| ~ spl24_571
| spl24_572 ),
inference(sat_conversion,[],[f20300]) ).
cnf(s747,plain,
( ~ spl24_4
| ~ spl24_268
| spl24_570
| ~ spl24_573 ),
inference(sat_conversion,[],[f20315]) ).
cnf(s754,plain,
( spl24_571
| spl24_572
| ~ spl24_582
| ~ spl24_583 ),
inference(sat_conversion,[],[f20427]) ).
cnf(s756,plain,
( ~ spl24_1
| ~ spl24_2
| spl24_582 ),
inference(sat_conversion,[],[f20438]) ).
cnf(s759,plain,
( ~ spl24_1
| ~ spl24_2
| spl24_583 ),
inference(sat_conversion,[],[f20456]) ).
cnf(s764,plain,
( ~ spl24_4
| ~ spl24_268
| ~ spl24_572
| spl24_588 ),
inference(sat_conversion,[],[f20681]) ).
cnf(s766,plain,
( ~ spl24_1
| ~ spl24_4
| ~ spl24_571
| spl24_573 ),
inference(sat_conversion,[],[f20858]) ).
cnf(s772,plain,
( ~ spl24_15
| ~ spl24_588
| spl24_593 ),
inference(sat_conversion,[],[f21040]) ).
cnf(s850,plain,
( ~ spl24_54
| ~ spl24_268
| spl24_669 ),
inference(sat_conversion,[],[f22883]) ).
cnf(s915,plain,
( ~ spl24_568
| spl24_738 ),
inference(sat_conversion,[],[f25497]) ).
cnf(s916,plain,
( ~ spl24_738
| spl24_739 ),
inference(sat_conversion,[],[f25516]) ).
cnf(s917,plain,
( ~ spl24_1
| ~ spl24_4
| spl24_20
| ~ spl24_37
| ~ spl24_189
| ~ spl24_502
| ~ spl24_739
| spl24_740
| ~ spl24_741 ),
inference(sat_conversion,[],[f25549]) ).
cnf(s2481,plain,
( ~ spl24_669
| spl24_1725 ),
inference(sat_conversion,[],[f110150]) ).
cnf(s2482,plain,
( ~ spl24_1725
| spl24_1726 ),
inference(sat_conversion,[],[f110155]) ).
cnf(s2488,plain,
( ~ spl24_4
| ~ spl24_27
| ~ spl24_34
| spl24_740
| spl24_741
| ~ spl24_1726
| ~ spl24_1732 ),
inference(sat_conversion,[],[f110431]) ).
cnf(s2489,plain,
( ~ spl24_33
| ~ spl24_34
| ~ spl24_346
| spl24_1732 ),
inference(sat_conversion,[],[f110439]) ).
cnf(s2491,plain,
( ~ spl24_27
| ~ spl24_33
| ~ spl24_34
| ~ spl24_593
| ~ spl24_740
| spl24_1656 ),
inference(sat_conversion,[],[f110557]) ).
cnf(s2494,plain,
( spl24_20
| ~ spl24_25
| spl24_60
| ~ spl24_66
| ~ spl24_1656 ),
inference(sat_conversion,[],[f110827]) ).
cnf(s2499,plain,
( ~ spl24_20
| spl24_270 ),
inference(sat_conversion,[],[f110917]) ).
cnf(s2500,plain,
( ~ spl24_20
| spl24_50 ),
inference(sat_conversion,[],[f110927]) ).
cnf(s2507,plain,
spl24_9,
inference(rat,[],[s9,s4]) ).
cnf(s2595,plain,
spl24_583,
inference(rat,[],[s759,s2,s1]) ).
cnf(s2596,plain,
spl24_582,
inference(rat,[],[s756,s2,s1]) ).
cnf(s2599,plain,
spl24_346,
inference(rat,[],[s406,s1]) ).
cnf(s2603,plain,
spl24_268,
inference(rat,[],[s321,s1]) ).
cnf(s2605,plain,
spl24_214,
inference(rat,[],[s233,s1]) ).
cnf(s2618,plain,
spl24_54,
inference(rat,[],[s51,s1]) ).
cnf(s2619,plain,
spl24_46,
inference(rat,[],[s44,s2,s2507,s1]) ).
cnf(s2621,plain,
spl24_17,
inference(rat,[],[s16,s2,s3,s1]) ).
cnf(s2623,plain,
spl24_14,
inference(rat,[],[s13,s1]) ).
cnf(s2664,plain,
spl24_669,
inference(rat,[],[s850,s2603,s2618]) ).
cnf(s2665,plain,
spl24_563,
inference(rat,[],[s739,s2605,s1,s2618]) ).
cnf(s2677,plain,
spl24_185,
inference(rat,[],[s206,s2619]) ).
cnf(s2687,plain,
spl24_189,
inference(rat,[],[s210,s2623]) ).
cnf(s2731,plain,
spl24_1725,
inference(rat,[],[s2481,s2664]) ).
cnf(s2737,plain,
spl24_568,
inference(rat,[],[s744,s2665]) ).
cnf(s2798,plain,
spl24_1726,
inference(rat,[],[s2482,s2731]) ).
cnf(s2805,plain,
spl24_738,
inference(rat,[],[s915,s2737]) ).
cnf(s2808,plain,
spl24_569,
inference(rat,[],[s745,s2677,s2737]) ).
cnf(s2842,plain,
spl24_739,
inference(rat,[],[s916,s2805]) ).
cnf(s2912,plain,
spl24_18,
inference(rat,[],[s26,s21,s19,s17,s27,s2,s1,s3,s2621,s2507]) ).
cnf(s2916,plain,
spl24_65,
inference(rat,[],[s66,s2912]) ).
cnf(s2919,plain,
spl24_25,
inference(rat,[],[s22,s2912]) ).
cnf(s2920,plain,
spl24_37,
inference(rat,[],[s34,s1,s2,s3,s2912]) ).
cnf(s2929,plain,
spl24_66,
inference(rat,[],[s67,s2916]) ).
cnf(s3007,plain,
( spl24_740
| spl24_20 ),
inference(rat,[],[s917,s2488,s2489,s30,s31,s678,s24,s4,s1,s2687,s2842,s2920,s2798,s2599]) ).
cnf(s3008,plain,
spl24_572,
inference(rat,[],[s747,s746,s766,s754,s4,s2603,s2808,s1,s2596,s2595]) ).
cnf(s3012,plain,
spl24_588,
inference(rat,[],[s764,s2603,s4,s3008]) ).
cnf(s3025,plain,
spl24_593,
inference(rat,[],[s772,s14,s3012]) ).
cnf(s3035,plain,
spl24_20,
inference(rat,[],[s2491,s3007,s2494,s24,s30,s31,s3025,s164,s2929,s2919]) ).
cnf(s3036,plain,
spl24_50,
inference(rat,[],[s2500,s3035]) ).
cnf(s3037,plain,
spl24_270,
inference(rat,[],[s2499,s3035]) ).
cnf(s3040,plain,
~ spl24_271,
inference(rat,[],[s325,s3036,s3037]) ).
cnf(s3041,plain,
$false,
inference(rat,[],[s323,s3036,s3040,s3037]) ).
fof(f110933,plain,
$false,
inference(avatar_sat_refutation,[],[s3041]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU004+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n017.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 03:17:21 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.72/2.48 % (3176510)Detected formulas, will run a generic FOF schedule.
% 10.72/2.48 % (3176519)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1444749953:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.72/2.48 % (3176518)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2242670569:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.72/2.48 % (3176516)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1876154268:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.72/2.48 % (3176515)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1949524087:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.72/2.48 % (3176517)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2209537392:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.72/2.48 % (3176520)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3039065368:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.72/2.48 % (3176518)Refutation not found, incomplete strategy
% 10.72/2.48 % (3176518)------------------------------
% 10.72/2.48 % (3176518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.48 % (3176518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.48 % (3176518)CaDiCaL version: 2.1.3
% 10.72/2.48 % (3176518)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.48 % (3176518)Time elapsed: 0.004 s
% 10.72/2.48 % (3176518)Peak memory usage: 88 MB
% 10.72/2.48 % (3176518)Instructions burned: 3 (million)
% 10.72/2.48 % (3176519)Instruction limit reached!
% 10.72/2.48 % (3176519)------------------------------
% 10.72/2.48 % (3176519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.48 % (3176519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.48 % (3176519)CaDiCaL version: 2.1.3
% 10.72/2.48 % (3176519)Termination reason: Instruction limit
% 10.72/2.48 % (3176519)Termination phase: Saturation
% 10.72/2.48 % (3176519)Time elapsed: 0.037 s
% 10.72/2.48 % (3176519)Peak memory usage: 88 MB
% 10.72/2.48 % (3176519)Instructions burned: 119 (million)
% 10.72/2.48 % (3176521)dis-21_1_sil=8000:lcm=predicate:random_seed=1618293499:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.72/2.48 % (3176521)Instruction limit reached!
% 10.72/2.48 % (3176521)------------------------------
% 10.72/2.48 % (3176521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.48 % (3176521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.48 % (3176521)CaDiCaL version: 2.1.3
% 10.72/2.48 % (3176521)Termination reason: Instruction limit
% 10.72/2.48 % (3176521)Termination phase: Saturation
% 10.72/2.48 % (3176521)Time elapsed: 0.077 s
% 10.72/2.48 % (3176521)Peak memory usage: 90 MB
% 10.72/2.48 % (3176521)Instructions burned: 129 (million)
% 10.72/2.48 % (3176520)Instruction limit reached!
% 10.72/2.48 % (3176520)------------------------------
% 10.72/2.48 % (3176520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.48 % (3176520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.48 % (3176520)CaDiCaL version: 2.1.3
% 10.72/2.48 % (3176520)Termination reason: Instruction limit
% 10.72/2.48 % (3176520)Termination phase: Saturation
% 10.72/2.48 % (3176520)Time elapsed: 0.094 s
% 10.72/2.48 % (3176520)Peak memory usage: 90 MB
% 10.72/2.48 % (3176520)Instructions burned: 139 (million)
% 10.72/2.48 % (3176529)lrs+10_1_sil=8000:sp=occurrence:random_seed=1336269688:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.72/2.48 % (3176529)Instruction limit reached!
% 10.72/2.48 % (3176529)------------------------------
% 10.72/2.48 % (3176529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.48 % (3176529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.48 % (3176529)CaDiCaL version: 2.1.3
% 10.72/2.48 % (3176529)Termination reason: Instruction limit
% 10.72/2.48 % (3176529)Termination phase: Saturation
% 10.72/2.48 % (3176529)Time elapsed: 0.089 s
% 10.72/2.48 % (3176529)Peak memory usage: 91 MB
% 10.72/2.48 % (3176529)Instructions burned: 285 (million)
% 18.64/3.59 % (3176531)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1379688764:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 18.64/3.59 % (3176530)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2189427275:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 18.64/3.59 % (3176518)------------------------------
% 18.64/3.59 % (3176518)------------------------------
% 18.64/3.59 % (3176533)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1707591570:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 18.64/3.59 % (3176530)Instruction limit reached!
% 18.64/3.59 % (3176530)------------------------------
% 18.64/3.59 % (3176530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.64/3.59 % (3176530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.64/3.59 % (3176530)CaDiCaL version: 2.1.3
% 18.64/3.59 % (3176530)Termination reason: Instruction limit
% 18.64/3.59 % (3176530)Termination phase: Saturation
% 18.64/3.59 % (3176530)Time elapsed: 0.077 s
% 18.64/3.59 % (3176530)Peak memory usage: 89 MB
% 18.64/3.59 % (3176530)Instructions burned: 159 (million)
% 18.64/3.59 % (3176533)Instruction limit reached!
% 18.64/3.59 % (3176533)------------------------------
% 18.64/3.59 % (3176533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.64/3.59 % (3176533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.64/3.59 % (3176533)CaDiCaL version: 2.1.3
% 18.64/3.59 % (3176533)Termination reason: Instruction limit
% 18.64/3.59 % (3176533)Termination phase: Saturation
% 18.64/3.59 % (3176533)Time elapsed: 0.074 s
% 18.64/3.59 % (3176533)Peak memory usage: 93 MB
% 18.64/3.59 % (3176533)Instructions burned: 248 (million)
% 18.64/3.59 % (3176536)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=378432833:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 18.64/3.59 % (3176536)Refutation not found, incomplete strategy
% 18.64/3.59 % (3176536)------------------------------
% 18.64/3.59 % (3176536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.64/3.59 % (3176536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.64/3.59 % (3176536)CaDiCaL version: 2.1.3
% 18.64/3.59 % (3176536)Termination reason: Refutation not found, incomplete strategy
% 18.64/3.59 % (3176536)Time elapsed: 0.006 s
% 18.64/3.59 % (3176536)Peak memory usage: 88 MB
% 18.64/3.59 % (3176536)Instructions burned: 8 (million)
% 18.64/3.59 % (3176531)Instruction limit reached!
% 18.64/3.59 % (3176531)------------------------------
% 18.64/3.59 % (3176531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.64/3.59 % (3176531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.64/3.59 % (3176531)CaDiCaL version: 2.1.3
% 18.64/3.59 % (3176531)Termination reason: Instruction limit
% 18.64/3.59 % (3176531)Termination phase: Saturation
% 18.64/3.59 % (3176531)Time elapsed: 0.200 s
% 18.64/3.59 % (3176531)Peak memory usage: 91 MB
% 18.64/3.59 % (3176531)Instructions burned: 326 (million)
% 18.64/3.59 % (3176538)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2256116119:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 18.64/3.59 % (3176539)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2755127501:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 18.64/3.59 % (3176539)Instruction limit reached!
% 18.64/3.59 % (3176539)------------------------------
% 18.64/3.59 % (3176539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.64/3.59 % (3176539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.64/3.59 % (3176539)CaDiCaL version: 2.1.3
% 18.64/3.59 % (3176539)Termination reason: Instruction limit
% 18.64/3.59 % (3176539)Termination phase: Saturation
% 18.64/3.59 % (3176539)Time elapsed: 0.041 s
% 18.64/3.59 % (3176539)Peak memory usage: 91 MB
% 18.64/3.59 % (3176539)Instructions burned: 117 (million)
% 18.64/3.59 % (3176542)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=357725970:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 18.64/3.59 % (3176544)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1265519071:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 18.64/3.59 % (3176544)Instruction limit reached!
% 18.64/3.59 % (3176544)------------------------------
% 18.64/3.59 % (3176544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.85/6.79 % (3176544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.85/6.79 % (3176544)CaDiCaL version: 2.1.3
% 41.85/6.79 % (3176544)Termination reason: Instruction limit
% 41.85/6.79 % (3176544)Termination phase: Saturation
% 41.85/6.79 % (3176544)Time elapsed: 0.035 s
% 41.85/6.79 % (3176544)Peak memory usage: 89 MB
% 41.85/6.79 % (3176544)Instructions burned: 117 (million)
% 41.85/6.79 % (3176542)Instruction limit reached!
% 41.85/6.79 % (3176542)------------------------------
% 41.85/6.79 % (3176542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.85/6.79 % (3176542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.85/6.79 % (3176542)CaDiCaL version: 2.1.3
% 41.85/6.79 % (3176542)Termination reason: Instruction limit
% 41.85/6.79 % (3176542)Termination phase: Saturation
% 41.85/6.79 % (3176542)Time elapsed: 0.066 s
% 41.85/6.79 % (3176542)Peak memory usage: 89 MB
% 41.85/6.79 % (3176542)Instructions burned: 129 (million)
% 41.85/6.79 % (3176536)------------------------------
% 41.85/6.79 % (3176536)------------------------------
% 41.85/6.79 % (3176547)lrs+10_1_sil=8000:sp=occurrence:random_seed=644818735:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 41.85/6.79 % (3176548)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1821819365:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 41.85/6.79 % (3176548)Refutation not found, incomplete strategy
% 41.85/6.79 % (3176548)------------------------------
% 41.85/6.79 % (3176548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.85/6.79 % (3176548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.85/6.79 % (3176548)CaDiCaL version: 2.1.3
% 41.85/6.79 % (3176548)Termination reason: Refutation not found, incomplete strategy
% 41.85/6.79 % (3176548)Time elapsed: 0.004 s
% 41.85/6.79 % (3176548)Peak memory usage: 88 MB
% 41.85/6.79 % (3176548)Instructions burned: 4 (million)
% 41.85/6.79 % (3176549)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1227299649:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 41.85/6.79 % (3176547)Instruction limit reached!
% 41.85/6.79 % (3176547)------------------------------
% 41.85/6.79 % (3176547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.85/6.79 % (3176547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.85/6.79 % (3176547)CaDiCaL version: 2.1.3
% 41.85/6.79 % (3176547)Termination reason: Instruction limit
% 41.85/6.79 % (3176547)Termination phase: Saturation
% 41.85/6.79 % (3176547)Time elapsed: 0.276 s
% 41.85/6.79 % (3176547)Peak memory usage: 97 MB
% 41.85/6.79 % (3176547)Instructions burned: 909 (million)
% 41.85/6.79 % (3176548)------------------------------
% 41.85/6.79 % (3176548)------------------------------
% 41.85/6.79 % (3176553)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=527881647:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 41.85/6.79 % (3176554)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3001146484:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 41.85/6.79 % (3176553)Instruction limit reached!
% 41.85/6.79 % (3176553)------------------------------
% 41.85/6.79 % (3176553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.85/6.79 % (3176553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.85/6.79 % (3176553)CaDiCaL version: 2.1.3
% 41.85/6.79 % (3176553)Termination reason: Instruction limit
% 41.85/6.79 % (3176553)Termination phase: Saturation
% 41.85/6.79 % (3176553)Time elapsed: 0.040 s
% 41.85/6.79 % (3176553)Peak memory usage: 91 MB
% 41.85/6.79 % (3176553)Instructions burned: 135 (million)
% 41.85/6.79 % (3176557)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1806291253:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 41.85/6.79 % (3176554)Instruction limit reached!
% 41.85/6.79 % (3176554)------------------------------
% 41.85/6.79 % (3176554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.85/6.79 % (3176554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.85/6.79 % (3176554)CaDiCaL version: 2.1.3
% 41.85/6.79 % (3176554)Termination reason: Instruction limit
% 41.85/6.79 % (3176554)Termination phase: Saturation
% 41.85/6.79 % (3176554)Time elapsed: 0.357 s
% 41.85/6.79 % (3176554)Peak memory usage: 93 MB
% 41.85/6.79 % (3176554)Instructions burned: 592 (million)
% 70.87/10.85 % (3176559)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=962909229:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 70.87/10.85 % (3176559)Instruction limit reached!
% 70.87/10.85 % (3176559)------------------------------
% 70.87/10.85 % (3176559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.87/10.85 % (3176559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.87/10.85 % (3176559)CaDiCaL version: 2.1.3
% 70.87/10.85 % (3176559)Termination reason: Instruction limit
% 70.87/10.85 % (3176559)Termination phase: Saturation
% 70.87/10.85 % (3176559)Time elapsed: 0.077 s
% 70.87/10.85 % (3176559)Peak memory usage: 90 MB
% 70.87/10.85 % (3176559)Instructions burned: 125 (million)
% 70.87/10.85 % (3176561)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1336325094:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 70.87/10.85 % (3176561)Instruction limit reached!
% 70.87/10.85 % (3176561)------------------------------
% 70.87/10.85 % (3176561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.87/10.85 % (3176561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.87/10.85 % (3176561)CaDiCaL version: 2.1.3
% 70.87/10.85 % (3176561)Termination reason: Instruction limit
% 70.87/10.85 % (3176561)Termination phase: Saturation
% 70.87/10.85 % (3176561)Time elapsed: 0.075 s
% 70.87/10.85 % (3176561)Peak memory usage: 90 MB
% 70.87/10.85 % (3176561)Instructions burned: 136 (million)
% 70.87/10.85 % (3176538)Instruction limit reached!
% 70.87/10.85 % (3176538)------------------------------
% 70.87/10.85 % (3176538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.87/10.85 % (3176538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.87/10.85 % (3176538)CaDiCaL version: 2.1.3
% 70.87/10.85 % (3176538)Termination reason: Instruction limit
% 70.87/10.85 % (3176538)Termination phase: Saturation
% 70.87/10.85 % (3176538)Time elapsed: 1.565 s
% 70.87/10.85 % (3176538)Peak memory usage: 141 MB
% 70.87/10.85 % (3176538)Instructions burned: 2352 (million)
% 70.87/10.85 % (3176563)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4168538806:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 70.87/10.85 % (3176563)Instruction limit reached!
% 70.87/10.85 % (3176563)------------------------------
% 70.87/10.85 % (3176563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.87/10.85 % (3176563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.87/10.85 % (3176563)CaDiCaL version: 2.1.3
% 70.87/10.85 % (3176563)Termination reason: Instruction limit
% 70.87/10.85 % (3176563)Termination phase: Saturation
% 70.87/10.85 % (3176563)Time elapsed: 0.084 s
% 70.87/10.85 % (3176563)Peak memory usage: 91 MB
% 70.87/10.85 % (3176563)Instructions burned: 142 (million)
% 70.87/10.85 % (3176564)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=444200608:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 70.87/10.85 % (3176564)Refutation not found, incomplete strategy
% 70.87/10.85 % (3176564)------------------------------
% 70.87/10.85 % (3176564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.87/10.85 % (3176564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.87/10.85 % (3176564)CaDiCaL version: 2.1.3
% 70.87/10.85 % (3176564)Termination reason: Refutation not found, incomplete strategy
% 70.87/10.85 % (3176564)Time elapsed: 0.003 s
% 70.87/10.85 % (3176564)Peak memory usage: 89 MB
% 70.87/10.85 % (3176564)Instructions burned: 3 (million)
% 70.87/10.85 % (3176566)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4132385426:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 70.87/10.85 % (3176564)------------------------------
% 70.87/10.85 % (3176564)------------------------------
% 70.87/10.85 % (3176569)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=54029988:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 70.87/10.85 % (3176569)Instruction limit reached!
% 70.87/10.85 % (3176569)------------------------------
% 70.87/10.85 % (3176569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.13 % (3176569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.13 % (3176569)CaDiCaL version: 2.1.3
% 86.81/13.13 % (3176569)Termination reason: Instruction limit
% 86.81/13.13 % (3176569)Termination phase: Saturation
% 86.81/13.13 % (3176569)Time elapsed: 0.084 s
% 86.81/13.13 % (3176569)Peak memory usage: 92 MB
% 86.81/13.13 % (3176569)Instructions burned: 151 (million)
% 86.81/13.13 % (3176571)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1786812304:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 86.81/13.13 % (3176549)Instruction limit reached!
% 86.81/13.13 % (3176549)------------------------------
% 86.81/13.13 % (3176549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.13 % (3176549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.13 % (3176549)CaDiCaL version: 2.1.3
% 86.81/13.13 % (3176549)Termination reason: Instruction limit
% 86.81/13.13 % (3176549)Termination phase: Saturation
% 86.81/13.13 % (3176549)Time elapsed: 2.995 s
% 86.81/13.13 % (3176549)Peak memory usage: 149 MB
% 86.81/13.13 % (3176549)Instructions burned: 5204 (million)
% 86.81/13.13 % (3176573)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3712772201:i=667:av=off:fsr=off_2960 on theBenchmark for (2960ds/667Mi)
% 86.81/13.13 % (3176573)Instruction limit reached!
% 86.81/13.13 % (3176573)------------------------------
% 86.81/13.13 % (3176573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.13 % (3176573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.13 % (3176573)CaDiCaL version: 2.1.3
% 86.81/13.13 % (3176573)Termination reason: Instruction limit
% 86.81/13.13 % (3176573)Termination phase: Saturation
% 86.81/13.13 % (3176573)Time elapsed: 0.334 s
% 86.81/13.13 % (3176573)Peak memory usage: 110 MB
% 86.81/13.13 % (3176573)Instructions burned: 667 (million)
% 86.81/13.13 % (3176575)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1915452288:s2a=on:i=185:s2at=1.8:fdi=4_2955 on theBenchmark for (2955ds/185Mi)
% 86.81/13.13 % (3176575)Instruction limit reached!
% 86.81/13.14 % (3176575)------------------------------
% 86.81/13.14 % (3176575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176575)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176575)Termination reason: Instruction limit
% 86.81/13.14 % (3176575)Termination phase: Saturation
% 86.81/13.14 % (3176575)Time elapsed: 0.095 s
% 86.81/13.14 % (3176575)Peak memory usage: 92 MB
% 86.81/13.14 % (3176575)Instructions burned: 185 (million)
% 86.81/13.14 % (3176577)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2679173482:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2953 on theBenchmark for (2953ds/193Mi)
% 86.81/13.14 % (3176577)Instruction limit reached!
% 86.81/13.14 % (3176577)------------------------------
% 86.81/13.14 % (3176577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176577)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176577)Termination reason: Instruction limit
% 86.81/13.14 % (3176577)Termination phase: Saturation
% 86.81/13.14 % (3176577)Time elapsed: 0.104 s
% 86.81/13.14 % (3176577)Peak memory usage: 90 MB
% 86.81/13.14 % (3176577)Instructions burned: 194 (million)
% 86.81/13.14 % (3176579)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3136614416:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2951 on theBenchmark for (2951ds/4850Mi)
% 86.81/13.14 % (3176557)Instruction limit reached!
% 86.81/13.14 % (3176557)------------------------------
% 86.81/13.14 % (3176557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176557)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176557)Termination reason: Instruction limit
% 86.81/13.14 % (3176557)Termination phase: Saturation
% 86.81/13.14 % (3176557)Time elapsed: 4.450 s
% 86.81/13.14 % (3176557)Peak memory usage: 217 MB
% 86.81/13.14 % (3176557)Instructions burned: 13195 (million)
% 86.81/13.14 % (3176583)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2049988005:i=12111:sd=1:ss=included_2941 on theBenchmark for (2941ds/12111Mi)
% 86.81/13.14 % (3176566)Instruction limit reached!
% 86.81/13.14 % (3176566)------------------------------
% 86.81/13.14 % (3176566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176566)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176566)Termination reason: Instruction limit
% 86.81/13.14 % (3176566)Termination phase: Saturation
% 86.81/13.14 % (3176566)Time elapsed: 3.842 s
% 86.81/13.14 % (3176566)Peak memory usage: 158 MB
% 86.81/13.14 % (3176566)Instructions burned: 6062 (million)
% 86.81/13.14 % (3176585)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=744440753:i=319:kws=precedence:fsr=off_2937 on theBenchmark for (2937ds/319Mi)
% 86.81/13.14 % (3176585)Instruction limit reached!
% 86.81/13.14 % (3176585)------------------------------
% 86.81/13.14 % (3176585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176585)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176585)Termination reason: Instruction limit
% 86.81/13.14 % (3176585)Termination phase: Saturation
% 86.81/13.14 % (3176585)Time elapsed: 0.199 s
% 86.81/13.14 % (3176585)Peak memory usage: 93 MB
% 86.81/13.14 % (3176585)Instructions burned: 319 (million)
% 86.81/13.14 % (3176587)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=685152394:i=2064:ep=RST_2934 on theBenchmark for (2934ds/2064Mi)
% 86.81/13.14 % (3176587)Instruction limit reached!
% 86.81/13.14 % (3176587)------------------------------
% 86.81/13.14 % (3176587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176587)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176587)Termination reason: Instruction limit
% 86.81/13.14 % (3176587)Termination phase: Saturation
% 86.81/13.14 % (3176587)Time elapsed: 1.062 s
% 86.81/13.14 % (3176587)Peak memory usage: 128 MB
% 86.81/13.14 % (3176587)Instructions burned: 2064 (million)
% 86.81/13.14 % (3176579)Instruction limit reached!
% 86.81/13.14 % (3176579)------------------------------
% 86.81/13.14 % (3176579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176579)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176579)Termination reason: Instruction limit
% 86.81/13.14 % (3176579)Termination phase: Saturation
% 86.81/13.14 % (3176579)Time elapsed: 2.860 s
% 86.81/13.14 % (3176579)Peak memory usage: 132 MB
% 86.81/13.14 % (3176579)Instructions burned: 4851 (million)
% 86.81/13.14 % (3176589)dis-1011_128_sil=32000:random_seed=1934904713:i=3706:ep=RST:av=off_2922 on theBenchmark for (2922ds/3706Mi)
% 86.81/13.14 % (3176591)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2507243088:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2921 on theBenchmark for (2921ds/757Mi)
% 86.81/13.14 % (3176591)Instruction limit reached!
% 86.81/13.14 % (3176591)------------------------------
% 86.81/13.14 % (3176591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176591)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176591)Termination reason: Instruction limit
% 86.81/13.14 % (3176591)Termination phase: Saturation
% 86.81/13.14 % (3176591)Time elapsed: 0.398 s
% 86.81/13.14 % (3176591)Peak memory usage: 111 MB
% 86.81/13.14 % (3176591)Instructions burned: 757 (million)
% 86.81/13.14 % (3176593)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=438064535:i=13913:ss=axioms:sgt=8_2915 on theBenchmark for (2915ds/13913Mi)
% 86.81/13.14 % (3176589)Instruction limit reached!
% 86.81/13.14 % (3176589)------------------------------
% 86.81/13.14 % (3176589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176589)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176589)Termination reason: Instruction limit
% 86.81/13.14 % (3176589)Termination phase: Saturation
% 86.81/13.14 % (3176589)Time elapsed: 1.974 s
% 86.81/13.14 % (3176589)Peak memory usage: 98 MB
% 86.81/13.14 % (3176589)Instructions burned: 3707 (million)
% 86.81/13.14 % (3176595)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=489699986:i=9925:aac=none_2901 on theBenchmark for (2901ds/9925Mi)
% 86.81/13.14 % (3176583)Instruction limit reached!
% 86.81/13.14 % (3176583)------------------------------
% 86.81/13.14 % (3176583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176583)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176583)Termination reason: Instruction limit
% 86.81/13.14 % (3176583)Termination phase: Saturation
% 86.81/13.14 % (3176583)Time elapsed: 4.253 s
% 86.81/13.14 % (3176583)Peak memory usage: 220 MB
% 86.81/13.14 % (3176583)Instructions burned: 12113 (million)
% 86.81/13.14 % (3176597)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2061192726:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2898 on theBenchmark for (2898ds/2479Mi)
% 86.81/13.14 % (3176597)Refutation not found, incomplete strategy
% 86.81/13.14 % (3176597)------------------------------
% 86.81/13.14 % (3176597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176597)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176597)Termination reason: Refutation not found, incomplete strategy
% 86.81/13.14 % (3176597)Time elapsed: 0.002 s
% 86.81/13.14 % (3176597)Peak memory usage: 88 MB
% 86.81/13.14 % (3176597)Instructions burned: 4 (million)
% 86.81/13.14 % (3176597)------------------------------
% 86.81/13.14 % (3176597)------------------------------
% 86.81/13.14 % (3176599)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1853908017:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2895 on theBenchmark for (2895ds/440Mi)
% 86.81/13.14 % (3176599)Instruction limit reached!
% 86.81/13.14 % (3176599)------------------------------
% 86.81/13.14 % (3176599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176599)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176599)Termination reason: Instruction limit
% 86.81/13.14 % (3176599)Termination phase: Saturation
% 86.81/13.14 % (3176599)Time elapsed: 0.127 s
% 86.81/13.14 % (3176599)Peak memory usage: 93 MB
% 86.81/13.14 % (3176599)Instructions burned: 441 (million)
% 86.81/13.14 % (3176601)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=635901767:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2893 on theBenchmark for (2893ds/11145Mi)
% 86.81/13.14 % (3176571)Instruction limit reached!
% 86.81/13.14 % (3176571)------------------------------
% 86.81/13.14 % (3176571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.81/13.14 % (3176571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.81/13.14 % (3176571)CaDiCaL version: 2.1.3
% 86.81/13.14 % (3176571)Termination reason: Instruction limit
% 86.81/13.14 % (3176571)Termination phase: Saturation
% 86.81/13.14 % (3176571)Time elapsed: 8.678 s
% 86.81/13.14 % (3176571)Peak memory usage: 189 MB
% 86.81/13.14 % (3176571)Instructions burned: 14156 (million)
% 86.81/13.14 % (3176603)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3312616812:cts=off:i=3034:av=off:er=known:fsd=on_2884 on theBenchmark for (2884ds/3034Mi)
% 86.81/13.14 % (3176517)First to succeed.
% 86.81/13.14 % (3176517)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3176510"
% 86.81/13.14 % (3176517)Refutation found. Thanks to Tanya!
% 86.81/13.14 % SZS status Theorem for theBenchmark
% 86.81/13.14 % SZS output start Proof for theBenchmark
% See solution above
% 87.58/13.33 % (3176517)------------------------------
% 87.58/13.33 % (3176517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.58/13.33 % (3176517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.58/13.33 % (3176517)CaDiCaL version: 2.1.3
% 87.58/13.33 % (3176517)Termination reason: Refutation
% 87.58/13.33 % (3176517)Time elapsed: 11.798 s
% 87.58/13.33 % (3176517)Peak memory usage: 223 MB
% 87.58/13.33 % (3176517)Instructions burned: 17371 (million)
% 87.58/13.33 % (3176517)------------------------------
% 87.58/13.33 % (3176517)------------------------------
% 87.58/13.33 % (3176510)Success in time 12.279 s
% 87.58/13.33 % Vampire exiting
%------------------------------------------------------------------------------