%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU213+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:47:46 PM UTC 2026
% Result : Theorem 5.22s 2.13s
% Output : Refutation 9.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 19
% Syntax : Number of formulae : 180 ( 28 unt; 10 def)
% Number of atoms : 661 ( 61 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 839 ( 358 ~; 370 |; 78 &)
% ( 18 <=>; 13 =>; 0 <=; 2 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-4 aty)
% Number of variables : 287 ( 0 sgn 257 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_relat_1) ).
fof(f34,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tarski) ).
fof(f38,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( relation(X2)
=> ( X2 = relation_composition(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ? [X5] :
( in(ordered_pair(X3,X5),X0)
& in(ordered_pair(X5,X4),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_relat_1) ).
fof(f60,axiom,
! [X0,X1] :
( ( relation(X0)
& relation(X1) )
=> relation(relation_composition(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_relat_1) ).
fof(f73,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(f148,axiom,
! [X0,X1,X2] :
( relation(X2)
=> ( in(ordered_pair(X0,X1),X2)
=> ( in(X0,relation_dom(X2))
& in(X1,relation_rng(X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_relat_1) ).
fof(f149,conjecture,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_funct_1) ).
fof(f150,negated_conjecture,
~ ! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f149]) ).
fof(f198,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f209,axiom,
! [X0,X1,X2] :
( ( relation(X2)
& function(X2) )
=> ( in(ordered_pair(X0,X1),X2)
<=> ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_funct_1) ).
fof(f249,plain,
! [X0] :
( ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f254,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = relation_composition(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ? [X5] :
( in(ordered_pair(X3,X5),X0)
& in(ordered_pair(X5,X4),X1) ) ) )
| ~ relation(X2) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f260,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f261,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(flattening,[],[f260]) ).
fof(f271,plain,
! [X0,X1] :
( ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) )
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(ennf_transformation,[],[f73]) ).
fof(f272,plain,
! [X0,X1] :
( ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) )
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f271]) ).
fof(f335,plain,
! [X0,X1,X2] :
( ( in(X0,relation_dom(X2))
& in(X1,relation_rng(X2)) )
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(ennf_transformation,[],[f148]) ).
fof(f336,plain,
! [X0,X1,X2] :
( ( in(X0,relation_dom(X2))
& in(X1,relation_rng(X2)) )
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(flattening,[],[f335]) ).
fof(f337,plain,
? [X0,X1] :
( ? [X2] :
( ( in(X0,relation_dom(relation_composition(X2,X1)))
<~> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(ennf_transformation,[],[f150]) ).
fof(f338,plain,
? [X0,X1] :
( ? [X2] :
( ( in(X0,relation_dom(relation_composition(X2,X1)))
<~> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(flattening,[],[f337]) ).
fof(f392,plain,
! [X0,X1,X2] :
( ( in(ordered_pair(X0,X1),X2)
<=> ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) ) )
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f209]) ).
fof(f393,plain,
! [X0,X1,X2] :
( ( in(ordered_pair(X0,X1),X2)
<=> ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) ) )
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f392]) ).
fof(f465,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ? [X2] :
( ( ! [X3] : ~ in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) )
& ( ? [X3] : in(ordered_pair(X2,X3),X0)
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| ! [X3] : ~ in(ordered_pair(X2,X3),X0) )
& ( ? [X3] : in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f249]) ).
fof(f466,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ? [X2] :
( ( ! [X3] : ~ in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) )
& ( ? [X4] : in(ordered_pair(X2,X4),X0)
| in(X2,X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( ? [X7] : in(ordered_pair(X5,X7),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(rectify,[],[f465]) ).
fof(f467,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ( ( ! [X3] : ~ in(ordered_pair(sK34(X0,X1),X3),X0)
| ~ in(sK34(X0,X1),X1) )
& ( in(ordered_pair(sK34(X0,X1),sK35(X0,X1)),X0)
| in(sK34(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( in(ordered_pair(X5,sK36(X0,X5)),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35,sK36]),skolemize(X2,sK34(X0,X1)),skolemize(X4,sK35(X0,X1)),skolemize(X7,sK36(X0,X5))],[f466]) ).
fof(f482,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = relation_composition(X0,X1)
| ? [X3,X4] :
( ( ! [X5] :
( ~ in(ordered_pair(X3,X5),X0)
| ~ in(ordered_pair(X5,X4),X1) )
| ~ in(ordered_pair(X3,X4),X2) )
& ( ? [X5] :
( in(ordered_pair(X3,X5),X0)
& in(ordered_pair(X5,X4),X1) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ! [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ! [X5] :
( ~ in(ordered_pair(X3,X5),X0)
| ~ in(ordered_pair(X5,X4),X1) ) )
& ( ? [X5] :
( in(ordered_pair(X3,X5),X0)
& in(ordered_pair(X5,X4),X1) )
| ~ in(ordered_pair(X3,X4),X2) ) )
| relation_composition(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f254]) ).
fof(f483,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = relation_composition(X0,X1)
| ? [X3,X4] :
( ( ! [X5] :
( ~ in(ordered_pair(X3,X5),X0)
| ~ in(ordered_pair(X5,X4),X1) )
| ~ in(ordered_pair(X3,X4),X2) )
& ( ? [X6] :
( in(ordered_pair(X3,X6),X0)
& in(ordered_pair(X6,X4),X1) )
| in(ordered_pair(X3,X4),X2) ) ) )
& ( ! [X7,X8] :
( ( in(ordered_pair(X7,X8),X2)
| ! [X9] :
( ~ in(ordered_pair(X7,X9),X0)
| ~ in(ordered_pair(X9,X8),X1) ) )
& ( ? [X10] :
( in(ordered_pair(X7,X10),X0)
& in(ordered_pair(X10,X8),X1) )
| ~ in(ordered_pair(X7,X8),X2) ) )
| relation_composition(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(rectify,[],[f482]) ).
fof(f484,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = relation_composition(X0,X1)
| ( ( ! [X5] :
( ~ in(ordered_pair(sK46(X0,X1,X2),X5),X0)
| ~ in(ordered_pair(X5,sK47(X0,X1,X2)),X1) )
| ~ in(ordered_pair(sK46(X0,X1,X2),sK47(X0,X1,X2)),X2) )
& ( ( in(ordered_pair(sK46(X0,X1,X2),sK48(X0,X1,X2)),X0)
& in(ordered_pair(sK48(X0,X1,X2),sK47(X0,X1,X2)),X1) )
| in(ordered_pair(sK46(X0,X1,X2),sK47(X0,X1,X2)),X2) ) ) )
& ( ! [X7,X8] :
( ( in(ordered_pair(X7,X8),X2)
| ! [X9] :
( ~ in(ordered_pair(X7,X9),X0)
| ~ in(ordered_pair(X9,X8),X1) ) )
& ( ( in(ordered_pair(X7,sK49(X0,X1,X7,X8)),X0)
& in(ordered_pair(sK49(X0,X1,X7,X8),X8),X1) )
| ~ in(ordered_pair(X7,X8),X2) ) )
| relation_composition(X0,X1) != X2 ) )
| ~ relation(X2) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46,sK47,sK48,sK49]),skolemize(X3,sK46(X0,X1,X2)),skolemize(X4,sK47(X0,X1,X2)),skolemize(X6,sK48(X0,X1,X2)),skolemize(X10,sK49(X0,X1,X7,X8))],[f483]) ).
fof(f516,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ in(X0,relation_dom(X2))
| ~ in(apply(X2,X0),relation_dom(X1))
| ~ in(X0,relation_dom(relation_composition(X2,X1))) )
& ( ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) )
| in(X0,relation_dom(relation_composition(X2,X1))) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(nnf_transformation,[],[f338]) ).
fof(f517,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ in(X0,relation_dom(X2))
| ~ in(apply(X2,X0),relation_dom(X1))
| ~ in(X0,relation_dom(relation_composition(X2,X1))) )
& ( ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) )
| in(X0,relation_dom(relation_composition(X2,X1))) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(flattening,[],[f516]) ).
fof(f518,plain,
( ( ~ in(sK64,relation_dom(sK66))
| ~ in(apply(sK66,sK64),relation_dom(sK65))
| ~ in(sK64,relation_dom(relation_composition(sK66,sK65))) )
& ( ( in(sK64,relation_dom(sK66))
& in(apply(sK66,sK64),relation_dom(sK65)) )
| in(sK64,relation_dom(relation_composition(sK66,sK65))) )
& relation(sK66)
& function(sK66)
& relation(sK65)
& function(sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65,sK66]),skolemize(X0,sK64),skolemize(X1,sK65),skolemize(X2,sK66)],[f517]) ).
fof(f539,plain,
! [X0,X1,X2] :
( ( ( in(ordered_pair(X0,X1),X2)
| ~ in(X0,relation_dom(X2))
| apply(X2,X0) != X1 )
& ( ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) )
| ~ in(ordered_pair(X0,X1),X2) ) )
| ~ relation(X2)
| ~ function(X2) ),
inference(nnf_transformation,[],[f393]) ).
fof(f540,plain,
! [X0,X1,X2] :
( ( ( in(ordered_pair(X0,X1),X2)
| ~ in(X0,relation_dom(X2))
| apply(X2,X0) != X1 )
& ( ( in(X0,relation_dom(X2))
& X1 = apply(X2,X0) )
| ~ in(ordered_pair(X0,X1),X2) ) )
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f539]) ).
fof(f647,plain,
! [X0,X1,X5] :
( in(ordered_pair(X5,sK36(X0,X5)),X0)
| ~ in(X5,X1)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(cnf_transformation,[],[f467]) ).
fof(f669,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f34]) ).
fof(f677,plain,
! [X2,X0,X1,X8,X7] :
( in(ordered_pair(sK49(X0,X1,X7,X8),X8),X1)
| ~ in(ordered_pair(X7,X8),X2)
| relation_composition(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f484]) ).
fof(f678,plain,
! [X2,X0,X1,X8,X7] :
( in(ordered_pair(X7,sK49(X0,X1,X7,X8)),X0)
| ~ in(ordered_pair(X7,X8),X2)
| relation_composition(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f484]) ).
fof(f679,plain,
! [X2,X0,X1,X8,X9,X7] :
( in(ordered_pair(X7,X8),X2)
| ~ in(ordered_pair(X7,X9),X0)
| ~ in(ordered_pair(X9,X8),X1)
| relation_composition(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f484]) ).
fof(f692,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f261]) ).
fof(f705,plain,
! [X0,X1] :
( function(relation_composition(X0,X1))
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f272]) ).
fof(f706,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f272]) ).
fof(f811,plain,
! [X2,X0,X1] :
( in(X0,relation_dom(X2))
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f336]) ).
fof(f812,plain,
function(sK65),
inference(cnf_transformation,[],[f518]) ).
fof(f813,plain,
relation(sK65),
inference(cnf_transformation,[],[f518]) ).
fof(f814,plain,
function(sK66),
inference(cnf_transformation,[],[f518]) ).
fof(f815,plain,
relation(sK66),
inference(cnf_transformation,[],[f518]) ).
fof(f816,plain,
( in(apply(sK66,sK64),relation_dom(sK65))
| in(sK64,relation_dom(relation_composition(sK66,sK65))) ),
inference(cnf_transformation,[],[f518]) ).
fof(f817,plain,
( in(sK64,relation_dom(sK66))
| in(sK64,relation_dom(relation_composition(sK66,sK65))) ),
inference(cnf_transformation,[],[f518]) ).
fof(f818,plain,
( ~ in(sK64,relation_dom(sK66))
| ~ in(apply(sK66,sK64),relation_dom(sK65))
| ~ in(sK64,relation_dom(relation_composition(sK66,sK65))) ),
inference(cnf_transformation,[],[f518]) ).
fof(f886,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f198]) ).
fof(f903,plain,
! [X2,X0,X1] :
( apply(X2,X0) = X1
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f540]) ).
fof(f905,plain,
! [X2,X0,X1] :
( in(ordered_pair(X0,X1),X2)
| ~ in(X0,relation_dom(X2))
| apply(X2,X0) != X1
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f540]) ).
fof(f918,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f669,f886]) ).
fof(f974,plain,
! [X0,X1,X5] :
( in(unordered_pair(unordered_pair(X5,sK36(X0,X5)),unordered_pair(X5,X5)),X0)
| ~ in(X5,X1)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(definition_unfolding,[],[f647,f918]) ).
fof(f988,plain,
! [X2,X0,X1,X8,X9,X7] :
( in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),X2)
| ~ in(unordered_pair(unordered_pair(X7,X9),unordered_pair(X7,X7)),X0)
| ~ in(unordered_pair(unordered_pair(X9,X8),unordered_pair(X9,X9)),X1)
| relation_composition(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f679,f918,f918,f918]) ).
fof(f989,plain,
! [X2,X0,X1,X8,X7] :
( in(unordered_pair(unordered_pair(X7,sK49(X0,X1,X7,X8)),unordered_pair(X7,X7)),X0)
| ~ in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),X2)
| relation_composition(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f678,f918,f918]) ).
fof(f990,plain,
! [X2,X0,X1,X8,X7] :
( in(unordered_pair(unordered_pair(sK49(X0,X1,X7,X8),X8),unordered_pair(sK49(X0,X1,X7,X8),sK49(X0,X1,X7,X8))),X1)
| ~ in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),X2)
| relation_composition(X0,X1) != X2
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f677,f918,f918]) ).
fof(f1020,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| in(X0,relation_dom(X2))
| ~ relation(X2) ),
inference(definition_unfolding,[],[f811,f918]) ).
fof(f1044,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| ~ in(X0,relation_dom(X2))
| apply(X2,X0) != X1
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_unfolding,[],[f905,f918]) ).
fof(f1046,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| apply(X2,X0) = X1
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_unfolding,[],[f903,f918]) ).
fof(f1103,plain,
! [X0,X5] :
( in(unordered_pair(unordered_pair(X5,sK36(X0,X5)),unordered_pair(X5,X5)),X0)
| ~ in(X5,relation_dom(X0))
| ~ relation(X0) ),
inference(equality_resolution,[],[f974]) ).
fof(f1114,plain,
! [X0,X1,X8,X9,X7] :
( in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),relation_composition(X0,X1))
| ~ in(unordered_pair(unordered_pair(X7,X9),unordered_pair(X7,X7)),X0)
| ~ in(unordered_pair(unordered_pair(X9,X8),unordered_pair(X9,X9)),X1)
| ~ relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(equality_resolution,[],[f988]) ).
fof(f1115,plain,
! [X0,X1,X8,X7] :
( in(unordered_pair(unordered_pair(X7,sK49(X0,X1,X7,X8)),unordered_pair(X7,X7)),X0)
| ~ in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),relation_composition(X0,X1))
| ~ relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(equality_resolution,[],[f989]) ).
fof(f1116,plain,
! [X0,X1,X8,X7] :
( in(unordered_pair(unordered_pair(sK49(X0,X1,X7,X8),X8),unordered_pair(sK49(X0,X1,X7,X8),sK49(X0,X1,X7,X8))),X1)
| ~ in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),relation_composition(X0,X1))
| ~ relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(equality_resolution,[],[f990]) ).
fof(f1123,plain,
! [X2,X0] :
( in(unordered_pair(unordered_pair(X0,apply(X2,X0)),unordered_pair(X0,X0)),X2)
| ~ in(X0,relation_dom(X2))
| ~ relation(X2)
| ~ function(X2) ),
inference(equality_resolution,[],[f1044]) ).
fof(f1124,definition,
sF74 = relation_dom(sK66),
introduced(definition,[new_symbols(definition,[sF74])],[function_definition]) ).
fof(f1125,plain,
relation_dom(sK66) = sF74,
inference(reorient_equations,[],[f1124]) ).
fof(f1126,definition,
sF75 = apply(sK66,sK64),
introduced(definition,[new_symbols(definition,[sF75])],[function_definition]) ).
fof(f1127,plain,
apply(sK66,sK64) = sF75,
inference(reorient_equations,[],[f1126]) ).
fof(f1128,definition,
sF76 = relation_dom(sK65),
introduced(definition,[new_symbols(definition,[sF76])],[function_definition]) ).
fof(f1129,plain,
relation_dom(sK65) = sF76,
inference(reorient_equations,[],[f1128]) ).
fof(f1130,definition,
sF77 = relation_composition(sK66,sK65),
introduced(definition,[new_symbols(definition,[sF77])],[function_definition]) ).
fof(f1131,plain,
relation_composition(sK66,sK65) = sF77,
inference(reorient_equations,[],[f1130]) ).
fof(f1132,definition,
sF78 = relation_dom(sF77),
introduced(definition,[new_symbols(definition,[sF78])],[function_definition]) ).
fof(f1133,plain,
relation_dom(sF77) = sF78,
inference(reorient_equations,[],[f1132]) ).
fof(f1134,plain,
( ~ in(sK64,sF74)
| ~ in(sF75,sF76)
| ~ in(sK64,sF78) ),
inference(definition_folding,[],[f818,f1133,f1131,f1129,f1127,f1125]) ).
fof(f1135,plain,
( in(sK64,sF74)
| in(sK64,sF78) ),
inference(definition_folding,[],[f817,f1133,f1131,f1125]) ).
fof(f1136,plain,
( in(sF75,sF76)
| in(sK64,sF78) ),
inference(definition_folding,[],[f816,f1133,f1131,f1129,f1127]) ).
fof(f1141,definition,
( spl79_1
<=> in(sK64,sF78) ),
introduced(definition,[new_symbols(definition,[spl79_1])],[avatar_definition]) ).
fof(f1142,plain,
( ~ in(sK64,sF78)
| spl79_1 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1143,plain,
( in(sK64,sF78)
| ~ spl79_1 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1145,definition,
( spl79_2
<=> in(sF75,sF76) ),
introduced(definition,[new_symbols(definition,[spl79_2])],[avatar_definition]) ).
fof(f1146,plain,
( ~ in(sF75,sF76)
| spl79_2 ),
inference(avatar_component_clause,[],[f1145]) ).
fof(f1147,plain,
( in(sF75,sF76)
| ~ spl79_2 ),
inference(avatar_component_clause,[],[f1145]) ).
fof(f1148,plain,
( spl79_1
| spl79_2 ),
inference(avatar_split_clause,[],[f1136,f1145,f1141]) ).
fof(f1150,definition,
( spl79_3
<=> in(sK64,sF74) ),
introduced(definition,[new_symbols(definition,[spl79_3])],[avatar_definition]) ).
fof(f1151,plain,
( ~ in(sK64,sF74)
| spl79_3 ),
inference(avatar_component_clause,[],[f1150]) ).
fof(f1152,plain,
( in(sK64,sF74)
| ~ spl79_3 ),
inference(avatar_component_clause,[],[f1150]) ).
fof(f1153,plain,
( spl79_1
| spl79_3 ),
inference(avatar_split_clause,[],[f1135,f1150,f1141]) ).
fof(f1154,plain,
( ~ spl79_1
| ~ spl79_2
| ~ spl79_3 ),
inference(avatar_split_clause,[],[f1134,f1150,f1145,f1141]) ).
fof(f1159,plain,
! [X0,X1,X8,X7] :
( in(unordered_pair(unordered_pair(sK49(X0,X1,X7,X8),X8),unordered_pair(sK49(X0,X1,X7,X8),sK49(X0,X1,X7,X8))),X1)
| ~ in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[],[f1116,f692]) ).
fof(f1160,plain,
! [X0,X1,X8,X7] :
( in(unordered_pair(unordered_pair(X7,sK49(X0,X1,X7,X8)),unordered_pair(X7,X7)),X0)
| ~ in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[],[f1115,f692]) ).
fof(f1161,plain,
! [X0,X1,X8,X9,X7] :
( ~ in(unordered_pair(unordered_pair(X9,X8),unordered_pair(X9,X9)),X1)
| ~ in(unordered_pair(unordered_pair(X7,X9),unordered_pair(X7,X7)),X0)
| in(unordered_pair(unordered_pair(X7,X8),unordered_pair(X7,X7)),relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[],[f1114,f692]) ).
fof(f1174,plain,
( function(sF77)
| ~ relation(sK66)
| ~ function(sK66)
| ~ relation(sK65)
| ~ function(sK65) ),
inference(superposition,[],[f705,f1131]) ).
fof(f1175,plain,
( function(sF77)
| ~ function(sK66)
| ~ relation(sK65)
| ~ function(sK65) ),
inference(forward_subsumption_resolution,[],[f1174,f815]) ).
fof(f1176,plain,
( function(sF77)
| ~ relation(sK65)
| ~ function(sK65) ),
inference(forward_subsumption_resolution,[],[f1175,f814]) ).
fof(f1177,plain,
( function(sF77)
| ~ function(sK65) ),
inference(forward_subsumption_resolution,[],[f1176,f813]) ).
fof(f1178,plain,
function(sF77),
inference(forward_subsumption_resolution,[],[f1177,f812]) ).
fof(f1179,plain,
( relation(sF77)
| ~ relation(sK66)
| ~ function(sK66)
| ~ relation(sK65)
| ~ function(sK65) ),
inference(superposition,[],[f706,f1131]) ).
fof(f1180,plain,
( relation(sF77)
| ~ function(sK66)
| ~ relation(sK65)
| ~ function(sK65) ),
inference(forward_subsumption_resolution,[],[f1179,f815]) ).
fof(f1181,plain,
( relation(sF77)
| ~ relation(sK65)
| ~ function(sK65) ),
inference(forward_subsumption_resolution,[],[f1180,f814]) ).
fof(f1182,plain,
( relation(sF77)
| ~ function(sK65) ),
inference(forward_subsumption_resolution,[],[f1181,f813]) ).
fof(f1183,plain,
relation(sF77),
inference(forward_subsumption_resolution,[],[f1182,f812]) ).
fof(f1185,plain,
( in(unordered_pair(unordered_pair(sK64,sF75),unordered_pair(sK64,sK64)),sK66)
| ~ in(sK64,relation_dom(sK66))
| ~ relation(sK66)
| ~ function(sK66) ),
inference(superposition,[],[f1123,f1127]) ).
fof(f1188,plain,
( in(unordered_pair(unordered_pair(sK64,sF75),unordered_pair(sK64,sK64)),sK66)
| ~ in(sK64,relation_dom(sK66))
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f1185,f815]) ).
fof(f1189,plain,
( in(unordered_pair(unordered_pair(sK64,sF75),unordered_pair(sK64,sK64)),sK66)
| ~ in(sK64,relation_dom(sK66)) ),
inference(forward_subsumption_resolution,[],[f1188,f814]) ).
fof(f1190,plain,
( ~ in(sK64,sF74)
| in(unordered_pair(unordered_pair(sK64,sF75),unordered_pair(sK64,sK64)),sK66) ),
inference(forward_demodulation,[],[f1189,f1125]) ).
fof(f1191,plain,
( in(unordered_pair(unordered_pair(sK64,sF75),unordered_pair(sK64,sK64)),sK66)
| ~ spl79_3 ),
inference(forward_subsumption_resolution,[],[f1190,f1152]) ).
fof(f1200,plain,
! [X2,X3,X0,X1] :
( in(X0,relation_dom(X1))
| ~ relation(X1)
| ~ in(unordered_pair(unordered_pair(X0,X2),unordered_pair(X0,X0)),relation_composition(X1,X3))
| ~ relation(X3)
| ~ relation(X1) ),
inference(resolution,[],[f1020,f1160]) ).
fof(f1205,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X2),unordered_pair(X0,X0)),relation_composition(X1,X3))
| ~ relation(X1)
| in(X0,relation_dom(X1))
| ~ relation(X3) ),
inference(duplicate_literal_removal,[],[f1200]) ).
fof(f1240,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF77)
| ~ relation(sK66)
| in(X0,relation_dom(sK66))
| ~ relation(sK65) ),
inference(superposition,[],[f1205,f1131]) ).
fof(f1241,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF77)
| in(X0,relation_dom(sK66))
| ~ relation(sK65) ),
inference(forward_subsumption_resolution,[],[f1240,f815]) ).
fof(f1244,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF77)
| in(X0,relation_dom(sK66)) ),
inference(forward_subsumption_resolution,[],[f1241,f813]) ).
fof(f1245,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF77)
| in(X0,sF74) ),
inference(forward_demodulation,[],[f1244,f1125]) ).
fof(f1246,plain,
! [X0] :
( in(X0,sF74)
| ~ in(X0,relation_dom(sF77))
| ~ relation(sF77)
| ~ function(sF77) ),
inference(resolution,[],[f1245,f1123]) ).
fof(f1253,plain,
! [X0] :
( in(X0,sF74)
| ~ in(X0,relation_dom(sF77))
| ~ function(sF77) ),
inference(forward_subsumption_resolution,[],[f1246,f1183]) ).
fof(f1254,plain,
! [X0] :
( in(X0,sF74)
| ~ in(X0,relation_dom(sF77)) ),
inference(forward_subsumption_resolution,[],[f1253,f1178]) ).
fof(f1255,plain,
! [X0] :
( ~ in(X0,sF78)
| in(X0,sF74) ),
inference(forward_demodulation,[],[f1254,f1133]) ).
fof(f1383,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| in(unordered_pair(unordered_pair(X0,apply(X3,X1)),unordered_pair(X0,X0)),relation_composition(X2,X3))
| ~ relation(X3)
| ~ relation(X2)
| ~ in(X1,relation_dom(X3))
| ~ relation(X3)
| ~ function(X3) ),
inference(resolution,[],[f1161,f1123]) ).
fof(f1397,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(unordered_pair(X0,apply(X3,X1)),unordered_pair(X0,X0)),relation_composition(X2,X3))
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| ~ relation(X3)
| ~ relation(X2)
| ~ in(X1,relation_dom(X3))
| ~ function(X3) ),
inference(duplicate_literal_removal,[],[f1383]) ).
fof(f1437,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,apply(sK65,X1)),unordered_pair(X0,X0)),sF77)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK66)
| ~ relation(sK65)
| ~ relation(sK66)
| ~ in(X1,relation_dom(sK65))
| ~ function(sK65) ),
inference(superposition,[],[f1397,f1131]) ).
fof(f1440,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,apply(sK65,X1)),unordered_pair(X0,X0)),sF77)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK66)
| ~ relation(sK66)
| ~ in(X1,relation_dom(sK65))
| ~ function(sK65) ),
inference(forward_subsumption_resolution,[],[f1437,f813]) ).
fof(f1446,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,apply(sK65,X1)),unordered_pair(X0,X0)),sF77)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK66)
| ~ in(X1,relation_dom(sK65))
| ~ function(sK65) ),
inference(forward_subsumption_resolution,[],[f1440,f815]) ).
fof(f1447,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,apply(sK65,X1)),unordered_pair(X0,X0)),sF77)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK66)
| ~ in(X1,relation_dom(sK65)) ),
inference(forward_subsumption_resolution,[],[f1446,f812]) ).
fof(f1448,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,apply(sK65,X1)),unordered_pair(X0,X0)),sF77)
| ~ in(X1,sF76)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sK66) ),
inference(forward_demodulation,[],[f1447,f1129]) ).
fof(f1454,plain,
! [X0,X1] :
( ~ in(X0,sF76)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK66)
| in(X1,relation_dom(sF77))
| ~ relation(sF77) ),
inference(resolution,[],[f1448,f1020]) ).
fof(f1463,plain,
! [X0,X1] :
( ~ in(X0,sF76)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK66)
| in(X1,relation_dom(sF77)) ),
inference(forward_subsumption_resolution,[],[f1454,f1183]) ).
fof(f1468,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK66)
| ~ in(X0,sF76)
| in(X1,sF78) ),
inference(forward_demodulation,[],[f1463,f1133]) ).
fof(f1471,plain,
( ~ in(sF75,sF76)
| in(sK64,sF78)
| ~ spl79_3 ),
inference(resolution,[],[f1468,f1191]) ).
fof(f1484,plain,
( in(sK64,sF78)
| ~ spl79_2
| ~ spl79_3 ),
inference(forward_subsumption_resolution,[],[f1471,f1147]) ).
fof(f1487,plain,
( $false
| spl79_1
| ~ spl79_2
| ~ spl79_3 ),
inference(forward_subsumption_resolution,[],[f1484,f1142]) ).
fof(f1488,plain,
( spl79_1
| ~ spl79_2
| ~ spl79_3 ),
inference(avatar_contradiction_clause,[],[f1487]) ).
fof(f1493,plain,
( in(sK64,sF74)
| ~ spl79_1 ),
inference(resolution,[],[f1143,f1255]) ).
fof(f1494,plain,
( $false
| ~ spl79_1
| spl79_3 ),
inference(forward_subsumption_resolution,[],[f1493,f1151]) ).
fof(f1495,plain,
( ~ spl79_1
| spl79_3 ),
inference(avatar_contradiction_clause,[],[f1494]) ).
fof(f1829,plain,
! [X2,X3,X0,X1] :
( apply(X0,X1) = sK49(X0,X2,X1,X3)
| ~ relation(X0)
| ~ function(X0)
| ~ in(unordered_pair(unordered_pair(X1,X3),unordered_pair(X1,X1)),relation_composition(X0,X2))
| ~ relation(X2)
| ~ relation(X0) ),
inference(resolution,[],[f1046,f1160]) ).
fof(f1851,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X1,X3),unordered_pair(X1,X1)),relation_composition(X0,X2))
| ~ relation(X0)
| ~ function(X0)
| apply(X0,X1) = sK49(X0,X2,X1,X3)
| ~ relation(X2) ),
inference(duplicate_literal_removal,[],[f1829]) ).
fof(f1975,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF77)
| ~ relation(sK66)
| ~ function(sK66)
| apply(sK66,X0) = sK49(sK66,sK65,X0,X1)
| ~ relation(sK65) ),
inference(superposition,[],[f1851,f1131]) ).
fof(f1979,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF77)
| ~ function(sK66)
| apply(sK66,X0) = sK49(sK66,sK65,X0,X1)
| ~ relation(sK65) ),
inference(forward_subsumption_resolution,[],[f1975,f815]) ).
fof(f1985,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF77)
| apply(sK66,X0) = sK49(sK66,sK65,X0,X1)
| ~ relation(sK65) ),
inference(forward_subsumption_resolution,[],[f1979,f814]) ).
fof(f1986,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF77)
| apply(sK66,X0) = sK49(sK66,sK65,X0,X1) ),
inference(forward_subsumption_resolution,[],[f1985,f813]) ).
fof(f1994,plain,
! [X0] :
( apply(sK66,X0) = sK49(sK66,sK65,X0,sK36(sF77,X0))
| ~ in(X0,relation_dom(sF77))
| ~ relation(sF77) ),
inference(resolution,[],[f1986,f1103]) ).
fof(f2003,plain,
! [X0] :
( apply(sK66,X0) = sK49(sK66,sK65,X0,sK36(sF77,X0))
| ~ in(X0,relation_dom(sF77)) ),
inference(forward_subsumption_resolution,[],[f1994,f1183]) ).
fof(f2005,plain,
! [X0] :
( ~ in(X0,sF78)
| apply(sK66,X0) = sK49(sK66,sK65,X0,sK36(sF77,X0)) ),
inference(forward_demodulation,[],[f2003,f1133]) ).
fof(f2016,plain,
( apply(sK66,sK64) = sK49(sK66,sK65,sK64,sK36(sF77,sK64))
| ~ spl79_1 ),
inference(resolution,[],[f2005,f1143]) ).
fof(f2017,plain,
( sF75 = sK49(sK66,sK65,sK64,sK36(sF77,sK64))
| ~ spl79_1 ),
inference(forward_demodulation,[],[f2016,f1127]) ).
fof(f2020,plain,
( in(unordered_pair(unordered_pair(sF75,sK36(sF77,sK64)),unordered_pair(sF75,sF75)),sK65)
| ~ in(unordered_pair(unordered_pair(sK64,sK36(sF77,sK64)),unordered_pair(sK64,sK64)),relation_composition(sK66,sK65))
| ~ relation(sK65)
| ~ relation(sK66)
| ~ spl79_1 ),
inference(superposition,[],[f1159,f2017]) ).
fof(f2022,plain,
( in(unordered_pair(unordered_pair(sF75,sK36(sF77,sK64)),unordered_pair(sF75,sF75)),sK65)
| ~ in(unordered_pair(unordered_pair(sK64,sK36(sF77,sK64)),unordered_pair(sK64,sK64)),relation_composition(sK66,sK65))
| ~ relation(sK66)
| ~ spl79_1 ),
inference(forward_subsumption_resolution,[],[f2020,f813]) ).
fof(f2025,plain,
( in(unordered_pair(unordered_pair(sF75,sK36(sF77,sK64)),unordered_pair(sF75,sF75)),sK65)
| ~ in(unordered_pair(unordered_pair(sK64,sK36(sF77,sK64)),unordered_pair(sK64,sK64)),relation_composition(sK66,sK65))
| ~ spl79_1 ),
inference(forward_subsumption_resolution,[],[f2022,f815]) ).
fof(f2028,plain,
( ~ in(unordered_pair(unordered_pair(sK64,sK36(sF77,sK64)),unordered_pair(sK64,sK64)),sF77)
| in(unordered_pair(unordered_pair(sF75,sK36(sF77,sK64)),unordered_pair(sF75,sF75)),sK65)
| ~ spl79_1 ),
inference(forward_demodulation,[],[f2025,f1131]) ).
fof(f2032,definition,
( spl79_18
<=> in(unordered_pair(unordered_pair(sF75,sK36(sF77,sK64)),unordered_pair(sF75,sF75)),sK65) ),
introduced(definition,[new_symbols(definition,[spl79_18])],[avatar_definition]) ).
fof(f2034,plain,
( in(unordered_pair(unordered_pair(sF75,sK36(sF77,sK64)),unordered_pair(sF75,sF75)),sK65)
| ~ spl79_18 ),
inference(avatar_component_clause,[],[f2032]) ).
fof(f2036,definition,
( spl79_19
<=> in(unordered_pair(unordered_pair(sK64,sK36(sF77,sK64)),unordered_pair(sK64,sK64)),sF77) ),
introduced(definition,[new_symbols(definition,[spl79_19])],[avatar_definition]) ).
fof(f2038,plain,
( ~ in(unordered_pair(unordered_pair(sK64,sK36(sF77,sK64)),unordered_pair(sK64,sK64)),sF77)
| spl79_19 ),
inference(avatar_component_clause,[],[f2036]) ).
fof(f2039,plain,
( spl79_18
| ~ spl79_19
| ~ spl79_1 ),
inference(avatar_split_clause,[],[f2028,f1141,f2036,f2032]) ).
fof(f2060,plain,
( ~ in(sK64,relation_dom(sF77))
| ~ relation(sF77)
| spl79_19 ),
inference(resolution,[],[f2038,f1103]) ).
fof(f2063,plain,
( ~ in(sK64,relation_dom(sF77))
| spl79_19 ),
inference(forward_subsumption_resolution,[],[f2060,f1183]) ).
fof(f2064,plain,
( ~ in(sK64,sF78)
| spl79_19 ),
inference(forward_demodulation,[],[f2063,f1133]) ).
fof(f2065,plain,
( $false
| ~ spl79_1
| spl79_19 ),
inference(forward_subsumption_resolution,[],[f2064,f1143]) ).
fof(f2066,plain,
( ~ spl79_1
| spl79_19 ),
inference(avatar_contradiction_clause,[],[f2065]) ).
fof(f2116,plain,
( in(sF75,relation_dom(sK65))
| ~ relation(sK65)
| ~ spl79_18 ),
inference(resolution,[],[f2034,f1020]) ).
fof(f2119,plain,
( in(sF75,relation_dom(sK65))
| ~ spl79_18 ),
inference(forward_subsumption_resolution,[],[f2116,f813]) ).
fof(f2123,plain,
( in(sF75,sF76)
| ~ spl79_18 ),
inference(forward_demodulation,[],[f2119,f1129]) ).
fof(f2126,plain,
( $false
| spl79_2
| ~ spl79_18 ),
inference(forward_subsumption_resolution,[],[f2123,f1146]) ).
fof(f2127,plain,
( spl79_2
| ~ spl79_18 ),
inference(avatar_contradiction_clause,[],[f2126]) ).
cnf(s1,plain,
( spl79_1
| spl79_2 ),
inference(sat_conversion,[],[f1148]) ).
cnf(s2,plain,
( spl79_1
| spl79_3 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s3,plain,
( ~ spl79_1
| ~ spl79_2
| ~ spl79_3 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s14,plain,
( spl79_1
| ~ spl79_2
| ~ spl79_3 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s15,plain,
( ~ spl79_1
| spl79_3 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s16,plain,
( ~ spl79_1
| spl79_18
| ~ spl79_19 ),
inference(sat_conversion,[],[f2039]) ).
cnf(s19,plain,
( ~ spl79_1
| spl79_19 ),
inference(sat_conversion,[],[f2066]) ).
cnf(s20,plain,
( spl79_2
| ~ spl79_18 ),
inference(sat_conversion,[],[f2127]) ).
cnf(s22,plain,
spl79_1,
inference(rat,[],[s14,s1,s2]) ).
cnf(s23,plain,
spl79_19,
inference(rat,[],[s19,s22]) ).
cnf(s24,plain,
spl79_3,
inference(rat,[],[s15,s22]) ).
cnf(s27,plain,
spl79_18,
inference(rat,[],[s16,s22,s23]) ).
cnf(s28,plain,
~ spl79_2,
inference(rat,[],[s3,s22,s24]) ).
cnf(s29,plain,
$false,
inference(rat,[],[s20,s27,s28]) ).
fof(f2132,plain,
$false,
inference(avatar_sat_refutation,[],[s29]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU213+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 % Computer : n011.cluster.edu
% 0.12/0.42 % Model : x86_64 x86_64
% 0.12/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.42 % Memory : 8046.5625MB
% 0.12/0.42 % OS : Linux 6.8.0-71-generic
% 0.12/0.42 % CPULimit : 300
% 0.12/0.42 % WCLimit : 300
% 0.12/0.42 % DateTime : Mon Sep 28 04:04:46 UTC 2026
% 0.12/0.42 % CPUTime :
% 0.12/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.46 Running first-order theorem proving
% 0.12/0.46 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
% 5.22/2.13 % (3009685)Detected formulas, will run a generic FOF schedule.
% 5.22/2.13 % (3009692)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=646004109:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.22/2.13 % (3009696)dis-21_1_sil=8000:lcm=predicate:random_seed=2110825330: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)
% 5.22/2.13 % (3009694)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=318464422:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.22/2.13 % (3009695)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3163526693:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.22/2.13 % (3009693)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1477081651:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.22/2.13 % (3009690)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=652351635:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.22/2.13 % (3009691)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=3066110226:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.22/2.13 % (3009693)Instruction limit reached!
% 5.22/2.13 % (3009693)------------------------------
% 5.22/2.13 % (3009693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009693)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009693)Termination reason: Instruction limit
% 5.22/2.13 % (3009693)Termination phase: Saturation
% 5.22/2.13 % (3009693)Time elapsed: 0.071 s
% 5.22/2.13 % (3009693)Peak memory usage: 90 MB
% 5.22/2.13 % (3009693)Instructions burned: 110 (million)
% 5.22/2.13 % (3009696)Instruction limit reached!
% 5.22/2.13 % (3009696)------------------------------
% 5.22/2.13 % (3009696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009696)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009696)Termination reason: Instruction limit
% 5.22/2.13 % (3009696)Termination phase: Saturation
% 5.22/2.13 % (3009696)Time elapsed: 0.074 s
% 5.22/2.13 % (3009696)Peak memory usage: 91 MB
% 5.22/2.13 % (3009696)Instructions burned: 129 (million)
% 5.22/2.13 % (3009694)Instruction limit reached!
% 5.22/2.13 % (3009694)------------------------------
% 5.22/2.13 % (3009694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009694)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009694)Termination reason: Instruction limit
% 5.22/2.13 % (3009694)Termination phase: Saturation
% 5.22/2.13 % (3009694)Time elapsed: 0.078 s
% 5.22/2.13 % (3009694)Peak memory usage: 89 MB
% 5.22/2.13 % (3009694)Instructions burned: 119 (million)
% 5.22/2.13 % (3009695)Instruction limit reached!
% 5.22/2.13 % (3009695)------------------------------
% 5.22/2.13 % (3009695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009695)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009695)Termination reason: Instruction limit
% 5.22/2.13 % (3009695)Termination phase: Saturation
% 5.22/2.13 % (3009695)Time elapsed: 0.094 s
% 5.22/2.13 % (3009695)Peak memory usage: 90 MB
% 5.22/2.13 % (3009695)Instructions burned: 140 (million)
% 5.22/2.13 % (3009706)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1263556999:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.22/2.13 % (3009705)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3057495502:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.22/2.13 % (3009704)lrs+10_1_sil=8000:sp=occurrence:random_seed=1229578874:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.22/2.13 % (3009707)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=2451984377:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.22/2.13 % (3009705)Instruction limit reached!
% 5.22/2.13 % (3009705)------------------------------
% 5.22/2.13 % (3009705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009705)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009705)Termination reason: Instruction limit
% 5.22/2.13 % (3009705)Termination phase: Saturation
% 5.22/2.13 % (3009705)Time elapsed: 0.077 s
% 5.22/2.13 % (3009705)Peak memory usage: 91 MB
% 5.22/2.13 % (3009705)Instructions burned: 159 (million)
% 5.22/2.13 % (3009707)Instruction limit reached!
% 5.22/2.13 % (3009707)------------------------------
% 5.22/2.13 % (3009707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009707)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009707)Termination reason: Instruction limit
% 5.22/2.13 % (3009707)Termination phase: Saturation
% 5.22/2.13 % (3009707)Time elapsed: 0.136 s
% 5.22/2.13 % (3009707)Peak memory usage: 94 MB
% 5.22/2.13 % (3009707)Instructions burned: 249 (million)
% 5.22/2.13 % (3009712)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1606787562:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 5.22/2.13 % (3009704)Instruction limit reached!
% 5.22/2.13 % (3009704)------------------------------
% 5.22/2.13 % (3009704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009704)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009704)Termination reason: Instruction limit
% 5.22/2.13 % (3009704)Termination phase: Saturation
% 5.22/2.13 % (3009704)Time elapsed: 0.211 s
% 5.22/2.13 % (3009704)Peak memory usage: 93 MB
% 5.22/2.13 % (3009704)Instructions burned: 286 (million)
% 5.22/2.13 % (3009706)Instruction limit reached!
% 5.22/2.13 % (3009706)------------------------------
% 5.22/2.13 % (3009706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009706)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009706)Termination reason: Instruction limit
% 5.22/2.13 % (3009706)Termination phase: Saturation
% 5.22/2.13 % (3009706)Time elapsed: 0.215 s
% 5.22/2.13 % (3009706)Peak memory usage: 93 MB
% 5.22/2.13 % (3009706)Instructions burned: 325 (million)
% 5.22/2.13 % (3009713)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2145394287:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.22/2.13 % (3009715)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3684855814:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 5.22/2.13 % (3009716)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3218088690:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 5.22/2.13 % (3009712)Instruction limit reached!
% 5.22/2.13 % (3009712)------------------------------
% 5.22/2.13 % (3009712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009712)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009712)Termination reason: Instruction limit
% 5.22/2.13 % (3009712)Termination phase: Saturation
% 5.22/2.13 % (3009712)Time elapsed: 0.185 s
% 5.22/2.13 % (3009712)Peak memory usage: 90 MB
% 5.22/2.13 % (3009712)Instructions burned: 294 (million)
% 5.22/2.13 % (3009716)Instruction limit reached!
% 5.22/2.13 % (3009716)------------------------------
% 5.22/2.13 % (3009716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009716)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009716)Termination reason: Instruction limit
% 5.22/2.13 % (3009716)Termination phase: Saturation
% 5.22/2.13 % (3009716)Time elapsed: 0.066 s
% 5.22/2.13 % (3009716)Peak memory usage: 89 MB
% 5.22/2.13 % (3009716)Instructions burned: 128 (million)
% 5.22/2.13 % (3009715)Instruction limit reached!
% 5.22/2.13 % (3009715)------------------------------
% 5.22/2.13 % (3009715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009715)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009715)Termination reason: Instruction limit
% 5.22/2.13 % (3009715)Termination phase: Saturation
% 5.22/2.13 % (3009715)Time elapsed: 0.069 s
% 5.22/2.13 % (3009715)Peak memory usage: 90 MB
% 5.22/2.13 % (3009715)Instructions burned: 114 (million)
% 5.22/2.13 % (3009720)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1405744066:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 5.22/2.13 % (3009722)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=550635432:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 5.22/2.13 % (3009721)lrs+10_1_sil=8000:sp=occurrence:random_seed=2134453024:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 5.22/2.13 % (3009720)Instruction limit reached!
% 5.22/2.13 % (3009720)------------------------------
% 5.22/2.13 % (3009720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009720)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009720)Termination reason: Instruction limit
% 5.22/2.13 % (3009720)Termination phase: Saturation
% 5.22/2.13 % (3009720)Time elapsed: 0.068 s
% 5.22/2.13 % (3009720)Peak memory usage: 89 MB
% 5.22/2.13 % (3009720)Instructions burned: 114 (million)
% 5.22/2.13 % (3009690)First to succeed.
% 5.22/2.13 % (3009690)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3009685"
% 5.22/2.13 % (3009726)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3899456573:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 5.22/2.13 % (3009691)Also succeeded, but the first one will report.
% 5.22/2.13 % (3009722)Instruction limit reached!
% 5.22/2.13 % (3009722)------------------------------
% 5.22/2.13 % (3009722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/2.13 % (3009722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/2.13 % (3009722)CaDiCaL version: 2.1.3
% 5.22/2.13 % (3009722)Termination reason: Instruction limit
% 5.22/2.13 % (3009722)Termination phase: Saturation
% 5.22/2.13 % (3009722)Time elapsed: 0.283 s
% 5.22/2.13 % (3009722)Peak memory usage: 93 MB
% 5.22/2.13 % (3009722)Instructions burned: 437 (million)
% 5.22/2.13 % (3009690)Refutation found. Thanks to Tanya!
% 5.22/2.13 % SZS status Theorem for theBenchmark
% 5.22/2.13 % SZS output start Proof for theBenchmark
% See solution above
% 9.29/2.32 % (3009690)------------------------------
% 9.29/2.32 % (3009690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.29/2.32 % (3009690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/2.32 % (3009690)CaDiCaL version: 2.1.3
% 9.29/2.32 % (3009690)Termination reason: Refutation
% 9.29/2.32 % (3009690)Time elapsed: 0.808 s
% 9.29/2.32 % (3009690)Peak memory usage: 133 MB
% 9.29/2.32 % (3009690)Instructions burned: 1245 (million)
% 9.29/2.32 % (3009690)------------------------------
% 9.29/2.32 % (3009690)------------------------------
% 9.29/2.32 % (3009685)Success in time 1.235 s
% 9.29/2.32 % Vampire exiting
%------------------------------------------------------------------------------