%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET998+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:42:30 PM UTC 2026
% Result : Theorem 15.93s 3.25s
% Output : Refutation 16.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 46
% Syntax : Number of formulae : 372 ( 57 unt; 40 def)
% Number of atoms : 1498 ( 144 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 2016 ( 890 ~; 949 |; 96 &)
% ( 59 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 41 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 4 con; 0-4 aty)
% Number of variables : 384 ( 0 sgn 354 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f5,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( ( in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) )
& ( ~ in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> X2 = empty_set ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f6,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_relat_1) ).
fof(f7,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f8,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/sandbox2/benchmark/theBenchmark.p',d8_relat_1) ).
fof(f33,conjecture,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( ( ! [X3] :
( in(X3,relation_dom(X2))
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),relation_dom(X1)) ) )
& ! [X3] :
( in(X3,relation_dom(X2))
=> apply(X2,X3) = apply(X1,apply(X0,X3)) ) )
=> X2 = relation_composition(X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_funct_1) ).
fof(f34,negated_conjecture,
~ ! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( ( ! [X3] :
( in(X3,relation_dom(X2))
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),relation_dom(X1)) ) )
& ! [X3] :
( in(X3,relation_dom(X2))
=> apply(X2,X3) = apply(X1,apply(X0,X3)) ) )
=> X2 = relation_composition(X0,X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f43,plain,
~ ! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( ( ! [X3] :
( in(X3,relation_dom(X2))
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),relation_dom(X1)) ) )
& ! [X4] :
( in(X4,relation_dom(X2))
=> apply(X2,X4) = apply(X1,apply(X0,X4)) ) )
=> X2 = relation_composition(X0,X1) ) ) ) ),
inference(rectify,[],[f34]) ).
fof(f50,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f51,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f50]) ).
fof(f52,plain,
! [X0] :
( ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f53,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,[],[f8]) ).
fof(f67,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( relation_composition(X0,X1) != X2
& ! [X3] :
( in(X3,relation_dom(X2))
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),relation_dom(X1)) ) )
& ! [X4] :
( apply(X2,X4) = apply(X1,apply(X0,X4))
| ~ in(X4,relation_dom(X2)) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) )
& relation(X0)
& function(X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f68,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( relation_composition(X0,X1) != X2
& ! [X3] :
( in(X3,relation_dom(X2))
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),relation_dom(X1)) ) )
& ! [X4] :
( apply(X2,X4) = apply(X1,apply(X0,X4))
| ~ in(X4,relation_dom(X2)) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) )
& relation(X0)
& function(X0) ),
inference(flattening,[],[f67]) ).
fof(f78,plain,
! [X0] :
( ! [X1,X2] :
( ( ( ( X2 = apply(X0,X1)
| ~ in(ordered_pair(X1,X2),X0) )
& ( in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2 ) )
| ~ in(X1,relation_dom(X0)) )
& ( ( ( X2 = apply(X0,X1)
| empty_set != X2 )
& ( X2 = empty_set
| apply(X0,X1) != X2 ) )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f51]) ).
fof(f79,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,[],[f52]) ).
fof(f80,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,[],[f79]) ).
fof(f81,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ( ( ! [X3] : ~ in(ordered_pair(sK0(X0,X1),X3),X0)
| ~ in(sK0(X0,X1),X1) )
& ( in(ordered_pair(sK0(X0,X1),sK1(X0,X1)),X0)
| in(sK0(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( in(ordered_pair(X5,sK2(X0,X5)),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X2,sK0(X0,X1)),skolemize(X4,sK1(X0,X1)),skolemize(X7,sK2(X0,X5))],[f80]) ).
fof(f82,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,[],[f53]) ).
fof(f83,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,[],[f82]) ).
fof(f84,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = relation_composition(X0,X1)
| ( ( ! [X5] :
( ~ in(ordered_pair(sK3(X0,X1,X2),X5),X0)
| ~ in(ordered_pair(X5,sK4(X0,X1,X2)),X1) )
| ~ in(ordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),X2) )
& ( ( in(ordered_pair(sK3(X0,X1,X2),sK5(X0,X1,X2)),X0)
& in(ordered_pair(sK5(X0,X1,X2),sK4(X0,X1,X2)),X1) )
| in(ordered_pair(sK3(X0,X1,X2),sK4(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,sK6(X0,X1,X7,X8)),X0)
& in(ordered_pair(sK6(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,[sK3,sK4,sK5,sK6]),skolemize(X3,sK3(X0,X1,X2)),skolemize(X4,sK4(X0,X1,X2)),skolemize(X6,sK5(X0,X1,X2)),skolemize(X10,sK6(X0,X1,X7,X8))],[f83]) ).
fof(f94,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( relation_composition(X0,X1) != X2
& ! [X3] :
( ( in(X3,relation_dom(X2))
| ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),relation_dom(X1)) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),relation_dom(X1)) )
| ~ in(X3,relation_dom(X2)) ) )
& ! [X4] :
( apply(X2,X4) = apply(X1,apply(X0,X4))
| ~ in(X4,relation_dom(X2)) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) )
& relation(X0)
& function(X0) ),
inference(nnf_transformation,[],[f68]) ).
fof(f95,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( relation_composition(X0,X1) != X2
& ! [X3] :
( ( in(X3,relation_dom(X2))
| ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),relation_dom(X1)) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),relation_dom(X1)) )
| ~ in(X3,relation_dom(X2)) ) )
& ! [X4] :
( apply(X2,X4) = apply(X1,apply(X0,X4))
| ~ in(X4,relation_dom(X2)) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) )
& relation(X0)
& function(X0) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
( sK18 != relation_composition(sK16,sK17)
& ! [X3] :
( ( in(X3,relation_dom(sK18))
| ~ in(X3,relation_dom(sK16))
| ~ in(apply(sK16,X3),relation_dom(sK17)) )
& ( ( in(X3,relation_dom(sK16))
& in(apply(sK16,X3),relation_dom(sK17)) )
| ~ in(X3,relation_dom(sK18)) ) )
& ! [X4] :
( apply(sK18,X4) = apply(sK17,apply(sK16,X4))
| ~ in(X4,relation_dom(sK18)) )
& relation(sK18)
& function(sK18)
& relation(sK17)
& function(sK17)
& relation(sK16)
& function(sK16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X2,sK18)],[f95]) ).
fof(f100,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f101,plain,
! [X2,X0,X1] :
( empty_set = X2
| apply(X0,X1) != X2
| in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f102,plain,
! [X2,X0,X1] :
( apply(X0,X1) = X2
| empty_set != X2
| in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f103,plain,
! [X2,X0,X1] :
( in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f104,plain,
! [X2,X0,X1] :
( apply(X0,X1) = X2
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f106,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(ordered_pair(X5,X6),X0)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f109,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f7]) ).
fof(f113,plain,
! [X2,X0,X1] :
( relation_composition(X0,X1) = X2
| in(ordered_pair(sK5(X0,X1,X2),sK4(X0,X1,X2)),X1)
| in(ordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f84]) ).
fof(f114,plain,
! [X2,X0,X1] :
( relation_composition(X0,X1) = X2
| in(ordered_pair(sK3(X0,X1,X2),sK5(X0,X1,X2)),X0)
| in(ordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f84]) ).
fof(f115,plain,
! [X2,X0,X1,X5] :
( relation_composition(X0,X1) = X2
| ~ in(ordered_pair(sK3(X0,X1,X2),X5),X0)
| ~ in(ordered_pair(X5,sK4(X0,X1,X2)),X1)
| ~ in(ordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f84]) ).
fof(f151,plain,
function(sK16),
inference(cnf_transformation,[],[f96]) ).
fof(f152,plain,
relation(sK16),
inference(cnf_transformation,[],[f96]) ).
fof(f153,plain,
function(sK17),
inference(cnf_transformation,[],[f96]) ).
fof(f154,plain,
relation(sK17),
inference(cnf_transformation,[],[f96]) ).
fof(f155,plain,
function(sK18),
inference(cnf_transformation,[],[f96]) ).
fof(f156,plain,
relation(sK18),
inference(cnf_transformation,[],[f96]) ).
fof(f157,plain,
! [X4] :
( apply(sK18,X4) = apply(sK17,apply(sK16,X4))
| ~ in(X4,relation_dom(sK18)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f158,plain,
! [X3] :
( in(apply(sK16,X3),relation_dom(sK17))
| ~ in(X3,relation_dom(sK18)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f159,plain,
! [X3] :
( in(X3,relation_dom(sK16))
| ~ in(X3,relation_dom(sK18)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f160,plain,
! [X3] :
( in(X3,relation_dom(sK18))
| ~ in(X3,relation_dom(sK16))
| ~ in(apply(sK16,X3),relation_dom(sK17)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f161,plain,
sK18 != relation_composition(sK16,sK17),
inference(cnf_transformation,[],[f96]) ).
fof(f169,plain,
! [X2,X0,X1] :
( apply(X0,X1) = X2
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(definition_unfolding,[],[f104,f109]) ).
fof(f170,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| apply(X0,X1) != X2
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(definition_unfolding,[],[f103,f109]) ).
fof(f173,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(unordered_pair(unordered_pair(X5,X6),singleton(X5)),X0)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(definition_unfolding,[],[f106,f109]) ).
fof(f175,plain,
! [X2,X0,X1,X5] :
( relation_composition(X0,X1) = X2
| ~ in(unordered_pair(unordered_pair(sK3(X0,X1,X2),X5),singleton(sK3(X0,X1,X2))),X0)
| ~ in(unordered_pair(unordered_pair(X5,sK4(X0,X1,X2)),singleton(X5)),X1)
| ~ in(unordered_pair(unordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),singleton(sK3(X0,X1,X2))),X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f115,f109,f109,f109]) ).
fof(f176,plain,
! [X2,X0,X1] :
( relation_composition(X0,X1) = X2
| in(unordered_pair(unordered_pair(sK3(X0,X1,X2),sK5(X0,X1,X2)),singleton(sK3(X0,X1,X2))),X0)
| in(unordered_pair(unordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),singleton(sK3(X0,X1,X2))),X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f114,f109,f109]) ).
fof(f177,plain,
! [X2,X0,X1] :
( relation_composition(X0,X1) = X2
| in(unordered_pair(unordered_pair(sK5(X0,X1,X2),sK4(X0,X1,X2)),singleton(sK5(X0,X1,X2))),X1)
| in(unordered_pair(unordered_pair(sK3(X0,X1,X2),sK4(X0,X1,X2)),singleton(sK3(X0,X1,X2))),X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f113,f109,f109]) ).
fof(f182,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X1,apply(X0,X1)),singleton(X1)),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f170]) ).
fof(f183,plain,
! [X0,X1] :
( apply(X0,X1) = empty_set
| in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f102]) ).
fof(f184,plain,
! [X0,X1] :
( apply(X0,X1) = empty_set
| in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f101]) ).
fof(f185,plain,
! [X0,X6,X5] :
( in(X5,relation_dom(X0))
| ~ in(unordered_pair(unordered_pair(X5,X6),singleton(X5)),X0)
| ~ relation(X0) ),
inference(equality_resolution,[],[f173]) ).
fof(f193,definition,
( spl20_1
<=> ! [X3] :
( in(X3,relation_dom(sK16))
| ~ in(X3,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f194,plain,
( ! [X3] :
( ~ in(X3,relation_dom(sK18))
| in(X3,relation_dom(sK16)) )
| ~ spl20_1 ),
inference(avatar_component_clause,[],[f193]) ).
fof(f195,plain,
spl20_1,
inference(avatar_split_clause,[],[f159,f193]) ).
fof(f205,plain,
( ! [X0,X1] :
( in(X0,relation_dom(sK16))
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK18)
| ~ relation(sK18) )
| ~ spl20_1 ),
inference(resolution,[],[f194,f185]) ).
fof(f217,plain,
( ! [X0,X1] :
( in(X0,relation_dom(sK16))
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK18) )
| ~ spl20_1 ),
inference(forward_subsumption_resolution,[],[f205,f156]) ).
fof(f231,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| in(X0,relation_dom(sK16)) )
| ~ spl20_1 ),
inference(forward_demodulation,[],[f217,f100]) ).
fof(f244,definition,
( spl20_2
<=> relation(sK16) ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
fof(f246,plain,
( relation(sK16)
| ~ spl20_2 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f247,plain,
spl20_2,
inference(avatar_split_clause,[],[f152,f244]) ).
fof(f249,definition,
( spl20_3
<=> relation(sK17) ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
fof(f251,plain,
( relation(sK17)
| ~ spl20_3 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f252,plain,
spl20_3,
inference(avatar_split_clause,[],[f154,f249]) ).
fof(f254,definition,
( spl20_4
<=> function(sK16) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f256,plain,
( function(sK16)
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f257,plain,
spl20_4,
inference(avatar_split_clause,[],[f151,f254]) ).
fof(f259,definition,
( spl20_5
<=> function(sK17) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f261,plain,
( function(sK17)
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f262,plain,
spl20_5,
inference(avatar_split_clause,[],[f153,f259]) ).
fof(f264,definition,
( spl20_6
<=> ! [X3] :
( in(X3,relation_dom(sK18))
| ~ in(X3,relation_dom(sK16))
| ~ in(apply(sK16,X3),relation_dom(sK17)) ) ),
introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition]) ).
fof(f265,plain,
( ! [X3] :
( ~ in(apply(sK16,X3),relation_dom(sK17))
| ~ in(X3,relation_dom(sK16))
| in(X3,relation_dom(sK18)) )
| ~ spl20_6 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
spl20_6,
inference(avatar_split_clause,[],[f160,f264]) ).
fof(f267,plain,
( ! [X0,X1] :
( ~ in(X0,relation_dom(sK16))
| in(X0,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(apply(sK16,X0),X1),singleton(apply(sK16,X0))),sK17)
| ~ relation(sK17) )
| ~ spl20_6 ),
inference(resolution,[],[f265,f185]) ).
fof(f273,plain,
( ! [X0,X1] :
( ~ in(X0,relation_dom(sK17))
| ~ in(X1,relation_dom(sK16))
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ in(X1,relation_dom(sK16))
| ~ relation(sK16)
| ~ function(sK16) )
| ~ spl20_6 ),
inference(superposition,[],[f265,f169]) ).
fof(f276,plain,
( ! [X0,X1] :
( ~ in(X0,relation_dom(sK17))
| ~ in(X1,relation_dom(sK16))
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ relation(sK16)
| ~ function(sK16) )
| ~ spl20_6 ),
inference(duplicate_literal_removal,[],[f273]) ).
fof(f279,plain,
( ! [X0,X1] :
( ~ in(X0,relation_dom(sK17))
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ relation(sK16)
| ~ function(sK16) )
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f276,f185]) ).
fof(f282,plain,
( ! [X0,X1] :
( ~ in(X0,relation_dom(sK16))
| in(X0,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(apply(sK16,X0),X1),singleton(apply(sK16,X0))),sK17) )
| ~ spl20_3
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f267,f251]) ).
fof(f285,plain,
( ! [X0,X1] :
( ~ in(X0,relation_dom(sK17))
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ function(sK16) )
| ~ spl20_2
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f279,f246]) ).
fof(f288,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(apply(sK16,X0)),unordered_pair(apply(sK16,X0),X1)),sK17)
| ~ in(X0,relation_dom(sK16))
| in(X0,relation_dom(sK18)) )
| ~ spl20_3
| ~ spl20_6 ),
inference(forward_demodulation,[],[f282,f100]) ).
fof(f289,plain,
( ! [X0,X1] :
( ~ in(X0,relation_dom(sK17))
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16) )
| ~ spl20_2
| ~ spl20_4
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f285,f256]) ).
fof(f290,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| ~ in(X0,relation_dom(sK17))
| in(X1,relation_dom(sK18)) )
| ~ spl20_2
| ~ spl20_4
| ~ spl20_6 ),
inference(forward_demodulation,[],[f289,f100]) ).
fof(f295,plain,
( ! [X0,X1] :
( apply(sK17,X0) = X1
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK17)
| ~ in(X0,relation_dom(sK17))
| ~ relation(sK17) )
| ~ spl20_5 ),
inference(resolution,[],[f261,f169]) ).
fof(f302,plain,
( ! [X0,X1] :
( apply(sK17,X0) = X1
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK17)
| ~ relation(sK17) )
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f295,f185]) ).
fof(f306,plain,
( ! [X0,X1] :
( apply(sK17,X0) = X1
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK17) )
| ~ spl20_3
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f302,f251]) ).
fof(f307,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK17)
| apply(sK17,X0) = X1 )
| ~ spl20_3
| ~ spl20_5 ),
inference(forward_demodulation,[],[f306,f100]) ).
fof(f309,definition,
( spl20_7
<=> relation(sK18) ),
introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition]) ).
fof(f311,plain,
( relation(sK18)
| ~ spl20_7 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
spl20_7,
inference(avatar_split_clause,[],[f156,f309]) ).
fof(f317,plain,
( ! [X0,X1] :
( apply(sK16,X0) = X1
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK16)
| ~ in(X0,relation_dom(sK16))
| ~ relation(sK16) )
| ~ spl20_4 ),
inference(resolution,[],[f256,f169]) ).
fof(f318,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sK16,X0)),singleton(X0)),sK16)
| ~ in(X0,relation_dom(sK16))
| ~ relation(sK16) )
| ~ spl20_4 ),
inference(resolution,[],[f256,f182]) ).
fof(f323,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sK16,X0)),singleton(X0)),sK16)
| ~ in(X0,relation_dom(sK16)) )
| ~ spl20_2
| ~ spl20_4 ),
inference(forward_subsumption_resolution,[],[f318,f246]) ).
fof(f324,plain,
( ! [X0,X1] :
( apply(sK16,X0) = X1
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK16)
| ~ relation(sK16) )
| ~ spl20_4 ),
inference(forward_subsumption_resolution,[],[f317,f185]) ).
fof(f327,plain,
( ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK16,X0))),sK16)
| ~ in(X0,relation_dom(sK16)) )
| ~ spl20_2
| ~ spl20_4 ),
inference(forward_demodulation,[],[f323,f100]) ).
fof(f328,plain,
( ! [X0,X1] :
( apply(sK16,X0) = X1
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK16) )
| ~ spl20_2
| ~ spl20_4 ),
inference(forward_subsumption_resolution,[],[f324,f246]) ).
fof(f329,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK16)
| apply(sK16,X0) = X1 )
| ~ spl20_2
| ~ spl20_4 ),
inference(forward_demodulation,[],[f328,f100]) ).
fof(f331,definition,
( spl20_8
<=> sK18 = relation_composition(sK16,sK17) ),
introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition]) ).
fof(f333,plain,
( sK18 != relation_composition(sK16,sK17)
| spl20_8 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f334,plain,
~ spl20_8,
inference(avatar_split_clause,[],[f161,f331]) ).
fof(f335,plain,
( ! [X0] :
( sK18 != X0
| in(unordered_pair(unordered_pair(sK5(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK5(sK16,sK17,X0))),sK17)
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0)
| ~ relation(sK17)
| ~ relation(sK16) )
| spl20_8 ),
inference(superposition,[],[f333,f177]) ).
fof(f336,plain,
( ! [X0] :
( sK18 != X0
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK5(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),sK16)
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0)
| ~ relation(sK17)
| ~ relation(sK16) )
| spl20_8 ),
inference(superposition,[],[f333,f176]) ).
fof(f337,plain,
( ! [X0,X1] :
( sK18 != X0
| ~ in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),X1),singleton(sK3(sK16,sK17,X0))),sK16)
| ~ in(unordered_pair(unordered_pair(X1,sK4(sK16,sK17,X0)),singleton(X1)),sK17)
| ~ in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0)
| ~ relation(sK17)
| ~ relation(sK16) )
| spl20_8 ),
inference(superposition,[],[f333,f175]) ).
fof(f338,plain,
( ! [X0,X1] :
( sK18 != X0
| ~ in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),X1),singleton(sK3(sK16,sK17,X0))),sK16)
| ~ in(unordered_pair(unordered_pair(X1,sK4(sK16,sK17,X0)),singleton(X1)),sK17)
| ~ in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0)
| ~ relation(sK16) )
| ~ spl20_3
| spl20_8 ),
inference(forward_subsumption_resolution,[],[f337,f251]) ).
fof(f339,plain,
( ! [X0] :
( sK18 != X0
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK5(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),sK16)
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0)
| ~ relation(sK16) )
| ~ spl20_3
| spl20_8 ),
inference(forward_subsumption_resolution,[],[f336,f251]) ).
fof(f340,plain,
( ! [X0] :
( sK18 != X0
| in(unordered_pair(unordered_pair(sK5(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK5(sK16,sK17,X0))),sK17)
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0)
| ~ relation(sK16) )
| ~ spl20_3
| spl20_8 ),
inference(forward_subsumption_resolution,[],[f335,f251]) ).
fof(f341,plain,
( ! [X0,X1] :
( sK18 != X0
| ~ in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),X1),singleton(sK3(sK16,sK17,X0))),sK16)
| ~ in(unordered_pair(unordered_pair(X1,sK4(sK16,sK17,X0)),singleton(X1)),sK17)
| ~ in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_subsumption_resolution,[],[f338,f246]) ).
fof(f342,plain,
( ! [X0] :
( sK18 != X0
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK5(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),sK16)
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_subsumption_resolution,[],[f339,f246]) ).
fof(f343,plain,
( ! [X0] :
( sK18 != X0
| in(unordered_pair(unordered_pair(sK5(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK5(sK16,sK17,X0))),sK17)
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_subsumption_resolution,[],[f340,f246]) ).
fof(f344,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),X1)),sK16)
| sK18 != X0
| ~ in(unordered_pair(unordered_pair(X1,sK4(sK16,sK17,X0)),singleton(X1)),sK17)
| ~ in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_demodulation,[],[f341,f100]) ).
fof(f345,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK5(sK16,sK17,X0))),sK16)
| sK18 != X0
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_demodulation,[],[f342,f100]) ).
fof(f346,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK5(sK16,sK17,X0)),unordered_pair(sK5(sK16,sK17,X0),sK4(sK16,sK17,X0))),sK17)
| sK18 != X0
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_demodulation,[],[f343,f100]) ).
fof(f347,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK4(sK16,sK17,X0))),sK17)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),X1)),sK16)
| sK18 != X0
| ~ in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_demodulation,[],[f344,f100]) ).
fof(f348,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK5(sK16,sK17,X0))),sK16)
| sK18 != X0
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_demodulation,[],[f345,f100]) ).
fof(f349,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK5(sK16,sK17,X0)),unordered_pair(sK4(sK16,sK17,X0),sK5(sK16,sK17,X0))),sK17)
| sK18 != X0
| in(unordered_pair(unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0)),singleton(sK3(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_demodulation,[],[f346,f100]) ).
fof(f350,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK4(sK16,sK17,X0))),sK17)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),X1)),sK16)
| sK18 != X0
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_demodulation,[],[f347,f100]) ).
fof(f351,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| in(unordered_pair(singleton(sK5(sK16,sK17,X0)),unordered_pair(sK4(sK16,sK17,X0),sK5(sK16,sK17,X0))),sK17)
| sK18 != X0
| ~ relation(X0) )
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(forward_demodulation,[],[f349,f100]) ).
fof(f468,plain,
( ! [X0,X1] :
( in(X0,relation_dom(sK16))
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK16) )
| ~ spl20_2 ),
inference(resolution,[],[f246,f185]) ).
fof(f483,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK16)
| in(X0,relation_dom(sK16)) )
| ~ spl20_2 ),
inference(forward_demodulation,[],[f468,f100]) ).
fof(f533,definition,
( spl20_9
<=> function(sK18) ),
introduced(definition,[new_symbols(definition,[spl20_9])],[avatar_definition]) ).
fof(f535,plain,
( function(sK18)
| ~ spl20_9 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f536,plain,
spl20_9,
inference(avatar_split_clause,[],[f155,f533]) ).
fof(f538,definition,
( spl20_10
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK16)
| apply(sK16,X0) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl20_10])],[avatar_definition]) ).
fof(f539,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK16)
| apply(sK16,X0) = X1 )
| ~ spl20_10 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( spl20_10
| ~ spl20_2
| ~ spl20_4 ),
inference(avatar_split_clause,[],[f329,f254,f244,f538]) ).
fof(f545,definition,
( spl20_11
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK17)
| apply(sK17,X0) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl20_11])],[avatar_definition]) ).
fof(f546,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK17)
| apply(sK17,X0) = X1 )
| ~ spl20_11 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f547,plain,
( spl20_11
| ~ spl20_3
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f307,f259,f249,f545]) ).
fof(f550,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X0,X1)),sK17)
| apply(sK17,X1) = X0 )
| ~ spl20_11 ),
inference(superposition,[],[f546,f100]) ).
fof(f552,definition,
( spl20_12
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| in(X0,relation_dom(sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
fof(f553,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| in(X0,relation_dom(sK16)) )
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f554,plain,
( spl20_12
| ~ spl20_1 ),
inference(avatar_split_clause,[],[f231,f193,f552]) ).
fof(f559,definition,
( spl20_13
<=> ! [X3] :
( in(apply(sK16,X3),relation_dom(sK17))
| ~ in(X3,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
fof(f560,plain,
( ! [X3] :
( in(apply(sK16,X3),relation_dom(sK17))
| ~ in(X3,relation_dom(sK18)) )
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f561,plain,
spl20_13,
inference(avatar_split_clause,[],[f158,f559]) ).
fof(f604,plain,
( ! [X0,X1] :
( apply(sK18,X0) = X1
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK18)
| ~ in(X0,relation_dom(sK18))
| ~ function(sK18) )
| ~ spl20_7 ),
inference(resolution,[],[f311,f169]) ).
fof(f616,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sK18,X0)),singleton(X0)),sK18)
| ~ in(X0,relation_dom(sK18))
| ~ function(sK18) )
| ~ spl20_7 ),
inference(resolution,[],[f311,f182]) ).
fof(f619,plain,
( ! [X0,X1] :
( in(X0,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK18) )
| ~ spl20_7 ),
inference(resolution,[],[f311,f185]) ).
fof(f634,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| in(X0,relation_dom(sK18)) )
| ~ spl20_7 ),
inference(forward_demodulation,[],[f619,f100]) ).
fof(f637,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(X0,apply(sK18,X0)),singleton(X0)),sK18)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_7
| ~ spl20_9 ),
inference(forward_subsumption_resolution,[],[f616,f535]) ).
fof(f649,plain,
( ! [X0,X1] :
( apply(sK18,X0) = X1
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK18)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_7
| ~ spl20_9 ),
inference(forward_subsumption_resolution,[],[f604,f535]) ).
fof(f660,plain,
( ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK18,X0))),sK18)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_7
| ~ spl20_9 ),
inference(forward_demodulation,[],[f637,f100]) ).
fof(f670,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| apply(sK18,X0) = X1
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_7
| ~ spl20_9 ),
inference(forward_demodulation,[],[f649,f100]) ).
fof(f683,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| apply(sK18,X0) = X1 )
| ~ spl20_7
| ~ spl20_9 ),
inference(forward_subsumption_resolution,[],[f670,f634]) ).
fof(f689,definition,
( spl20_14
<=> ! [X4] :
( apply(sK18,X4) = apply(sK17,apply(sK16,X4))
| ~ in(X4,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
fof(f690,plain,
( ! [X4] :
( apply(sK18,X4) = apply(sK17,apply(sK16,X4))
| ~ in(X4,relation_dom(sK18)) )
| ~ spl20_14 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f691,plain,
spl20_14,
inference(avatar_split_clause,[],[f157,f689]) ).
fof(f706,definition,
( spl20_15
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| apply(sK18,X0) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl20_15])],[avatar_definition]) ).
fof(f707,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| apply(sK18,X0) = X1 )
| ~ spl20_15 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f708,plain,
( spl20_15
| ~ spl20_7
| ~ spl20_9 ),
inference(avatar_split_clause,[],[f683,f533,f309,f706]) ).
fof(f714,plain,
( ! [X0,X1] :
( apply(sK17,X0) = apply(sK18,X1)
| ~ in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ in(X1,relation_dom(sK16))
| ~ relation(sK16)
| ~ function(sK16) )
| ~ spl20_14 ),
inference(superposition,[],[f690,f169]) ).
fof(f720,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(apply(sK16,X0),apply(sK18,X0)),singleton(apply(sK16,X0))),sK17)
| ~ in(apply(sK16,X0),relation_dom(sK17))
| ~ relation(sK17)
| ~ function(sK17)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_14 ),
inference(superposition,[],[f182,f690]) ).
fof(f723,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(apply(sK16,X0),apply(sK18,X0)),singleton(apply(sK16,X0))),sK17)
| ~ relation(sK17)
| ~ function(sK17)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_13
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f720,f560]) ).
fof(f729,plain,
( ! [X0,X1] :
( apply(sK17,X0) = apply(sK18,X1)
| ~ in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ relation(sK16)
| ~ function(sK16) )
| ~ spl20_1
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f714,f194]) ).
fof(f731,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(apply(sK16,X0),apply(sK18,X0)),singleton(apply(sK16,X0))),sK17)
| ~ function(sK17)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_3
| ~ spl20_13
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f723,f251]) ).
fof(f737,plain,
( ! [X0,X1] :
( apply(sK17,X0) = apply(sK18,X1)
| ~ in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ function(sK16) )
| ~ spl20_1
| ~ spl20_2
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f729,f246]) ).
fof(f739,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(apply(sK16,X0),apply(sK18,X0)),singleton(apply(sK16,X0))),sK17)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_3
| ~ spl20_5
| ~ spl20_13
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f731,f261]) ).
fof(f745,plain,
( ! [X0,X1] :
( apply(sK17,X0) = apply(sK18,X1)
| ~ in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16) )
| ~ spl20_1
| ~ spl20_2
| ~ spl20_4
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f737,f256]) ).
fof(f747,plain,
( ! [X0] :
( in(unordered_pair(singleton(apply(sK16,X0)),unordered_pair(apply(sK16,X0),apply(sK18,X0))),sK17)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_3
| ~ spl20_5
| ~ spl20_13
| ~ spl20_14 ),
inference(forward_demodulation,[],[f739,f100]) ).
fof(f749,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| apply(sK17,X0) = apply(sK18,X1)
| ~ in(X1,relation_dom(sK18)) )
| ~ spl20_1
| ~ spl20_2
| ~ spl20_4
| ~ spl20_14 ),
inference(forward_demodulation,[],[f745,f100]) ).
fof(f755,definition,
( spl20_17
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(apply(sK16,X0)),unordered_pair(apply(sK16,X0),X1)),sK17)
| ~ in(X0,relation_dom(sK16))
| in(X0,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_17])],[avatar_definition]) ).
fof(f756,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(apply(sK16,X0)),unordered_pair(apply(sK16,X0),X1)),sK17)
| ~ in(X0,relation_dom(sK16))
| in(X0,relation_dom(sK18)) )
| ~ spl20_17 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f757,plain,
( spl20_17
| ~ spl20_3
| ~ spl20_6 ),
inference(avatar_split_clause,[],[f288,f264,f249,f755]) ).
fof(f761,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK17)
| ~ in(X1,relation_dom(sK16))
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ in(X1,relation_dom(sK16))
| ~ relation(sK16)
| ~ function(sK16) )
| ~ spl20_17 ),
inference(superposition,[],[f756,f169]) ).
fof(f764,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK17)
| ~ in(X1,relation_dom(sK16))
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ relation(sK16)
| ~ function(sK16) )
| ~ spl20_17 ),
inference(duplicate_literal_removal,[],[f761]) ).
fof(f765,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK17)
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ relation(sK16)
| ~ function(sK16) )
| ~ spl20_17 ),
inference(forward_subsumption_resolution,[],[f764,f185]) ).
fof(f766,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK17)
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16)
| ~ function(sK16) )
| ~ spl20_2
| ~ spl20_17 ),
inference(forward_subsumption_resolution,[],[f765,f246]) ).
fof(f767,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK17)
| in(X1,relation_dom(sK18))
| ~ in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sK16) )
| ~ spl20_2
| ~ spl20_4
| ~ spl20_17 ),
inference(forward_subsumption_resolution,[],[f766,f256]) ).
fof(f768,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK17)
| in(X1,relation_dom(sK18)) )
| ~ spl20_2
| ~ spl20_4
| ~ spl20_17 ),
inference(forward_demodulation,[],[f767,f100]) ).
fof(f770,definition,
( spl20_18
<=> ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK17)
| in(X1,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_18])],[avatar_definition]) ).
fof(f771,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK17)
| in(X1,relation_dom(sK18)) )
| ~ spl20_18 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f772,plain,
( spl20_18
| ~ spl20_2
| ~ spl20_4
| ~ spl20_17 ),
inference(avatar_split_clause,[],[f768,f755,f254,f244,f770]) ).
fof(f774,definition,
( spl20_19
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| in(X0,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
fof(f775,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK18)
| in(X0,relation_dom(sK18)) )
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f776,plain,
( spl20_19
| ~ spl20_7 ),
inference(avatar_split_clause,[],[f634,f309,f774]) ).
fof(f793,definition,
( spl20_21
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK16)
| in(X0,relation_dom(sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl20_21])],[avatar_definition]) ).
fof(f794,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK16)
| in(X0,relation_dom(sK16)) )
| ~ spl20_21 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f795,plain,
( spl20_21
| ~ spl20_2 ),
inference(avatar_split_clause,[],[f483,f244,f793]) ).
fof(f797,definition,
( spl20_22
<=> ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK18,X0))),sK18)
| ~ in(X0,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_22])],[avatar_definition]) ).
fof(f798,plain,
( ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK18,X0))),sK18)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_22 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f799,plain,
( spl20_22
| ~ spl20_7
| ~ spl20_9 ),
inference(avatar_split_clause,[],[f660,f533,f309,f797]) ).
fof(f842,definition,
( spl20_24
<=> ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK16,X0))),sK16)
| ~ in(X0,relation_dom(sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl20_24])],[avatar_definition]) ).
fof(f843,plain,
( ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK16,X0))),sK16)
| ~ in(X0,relation_dom(sK16)) )
| ~ spl20_24 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f844,plain,
( spl20_24
| ~ spl20_2
| ~ spl20_4 ),
inference(avatar_split_clause,[],[f327,f254,f244,f842]) ).
fof(f952,definition,
( spl20_29
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| ~ in(X0,relation_dom(sK17))
| in(X1,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_29])],[avatar_definition]) ).
fof(f953,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| ~ in(X0,relation_dom(sK17))
| in(X1,relation_dom(sK18)) )
| ~ spl20_29 ),
inference(avatar_component_clause,[],[f952]) ).
fof(f954,plain,
( spl20_29
| ~ spl20_2
| ~ spl20_4
| ~ spl20_6 ),
inference(avatar_split_clause,[],[f290,f264,f254,f244,f952]) ).
fof(f964,definition,
( spl20_30
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| apply(sK17,X0) = apply(sK18,X1)
| ~ in(X1,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_30])],[avatar_definition]) ).
fof(f965,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X0)),sK16)
| apply(sK17,X0) = apply(sK18,X1)
| ~ in(X1,relation_dom(sK18)) )
| ~ spl20_30 ),
inference(avatar_component_clause,[],[f964]) ).
fof(f966,plain,
( spl20_30
| ~ spl20_1
| ~ spl20_2
| ~ spl20_4
| ~ spl20_14 ),
inference(avatar_split_clause,[],[f749,f689,f254,f244,f193,f964]) ).
fof(f968,definition,
( spl20_31
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK4(sK16,sK17,X0))),sK17)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),X1)),sK16)
| sK18 != X0
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_31])],[avatar_definition]) ).
fof(f969,plain,
( ! [X0,X1] :
( sK18 != X0
| ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK4(sK16,sK17,X0))),sK17)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),X1)),sK16)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_31 ),
inference(avatar_component_clause,[],[f968]) ).
fof(f970,plain,
( spl20_31
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(avatar_split_clause,[],[f350,f331,f249,f244,f968]) ).
fof(f971,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK16,sK17,sK18))),sK17)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),X0)),sK16)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18)
| ~ relation(sK18) )
| ~ spl20_31 ),
inference(equality_resolution,[],[f969]) ).
fof(f972,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK16,sK17,sK18))),sK17)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),X0)),sK16)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18) )
| ~ spl20_7
| ~ spl20_31 ),
inference(forward_subsumption_resolution,[],[f971,f311]) ).
fof(f974,definition,
( spl20_32
<=> in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18) ),
introduced(definition,[new_symbols(definition,[spl20_32])],[avatar_definition]) ).
fof(f975,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18)
| ~ spl20_32 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f976,plain,
( ~ in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18)
| spl20_32 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f978,definition,
( spl20_33
<=> ! [X0] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK16,sK17,sK18))),sK17)
| ~ in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),X0)),sK16) ) ),
introduced(definition,[new_symbols(definition,[spl20_33])],[avatar_definition]) ).
fof(f979,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),X0)),sK16)
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK16,sK17,sK18))),sK17) )
| ~ spl20_33 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f980,plain,
( ~ spl20_32
| spl20_33
| ~ spl20_7
| ~ spl20_31 ),
inference(avatar_split_clause,[],[f972,f968,f309,f978,f974]) ).
fof(f991,definition,
( spl20_35
<=> ! [X0] :
( in(unordered_pair(singleton(apply(sK16,X0)),unordered_pair(apply(sK16,X0),apply(sK18,X0))),sK17)
| ~ in(X0,relation_dom(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl20_35])],[avatar_definition]) ).
fof(f992,plain,
( ! [X0] :
( in(unordered_pair(singleton(apply(sK16,X0)),unordered_pair(apply(sK16,X0),apply(sK18,X0))),sK17)
| ~ in(X0,relation_dom(sK18)) )
| ~ spl20_35 ),
inference(avatar_component_clause,[],[f991]) ).
fof(f993,plain,
( spl20_35
| ~ spl20_3
| ~ spl20_5
| ~ spl20_13
| ~ spl20_14 ),
inference(avatar_split_clause,[],[f747,f689,f559,f259,f249,f991]) ).
fof(f1107,definition,
( spl20_45
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X0,X1)),sK17)
| apply(sK17,X1) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl20_45])],[avatar_definition]) ).
fof(f1108,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X0,X1)),sK17)
| apply(sK17,X1) = X0 )
| ~ spl20_45 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1109,plain,
( spl20_45
| ~ spl20_11 ),
inference(avatar_split_clause,[],[f550,f545,f1107]) ).
fof(f1370,definition,
( spl20_56
<=> ! [X0] :
( in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK5(sK16,sK17,X0))),sK16)
| sK18 != X0
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_56])],[avatar_definition]) ).
fof(f1371,plain,
( ! [X0] :
( sK18 != X0
| in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK5(sK16,sK17,X0))),sK16)
| in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_56 ),
inference(avatar_component_clause,[],[f1370]) ).
fof(f1372,plain,
( spl20_56
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(avatar_split_clause,[],[f348,f331,f249,f244,f1370]) ).
fof(f1373,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK16)
| in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18)
| ~ relation(sK18)
| ~ spl20_56 ),
inference(equality_resolution,[],[f1371]) ).
fof(f1374,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK16)
| ~ relation(sK18)
| spl20_32
| ~ spl20_56 ),
inference(forward_subsumption_resolution,[],[f1373,f976]) ).
fof(f1375,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK16)
| ~ spl20_7
| spl20_32
| ~ spl20_56 ),
inference(forward_subsumption_resolution,[],[f1374,f311]) ).
fof(f1377,definition,
( spl20_57
<=> in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK16) ),
introduced(definition,[new_symbols(definition,[spl20_57])],[avatar_definition]) ).
fof(f1379,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK16)
| ~ spl20_57 ),
inference(avatar_component_clause,[],[f1377]) ).
fof(f1380,plain,
( spl20_57
| ~ spl20_7
| spl20_32
| ~ spl20_56 ),
inference(avatar_split_clause,[],[f1375,f1370,f974,f309,f1377]) ).
fof(f1385,plain,
( in(sK3(sK16,sK17,sK18),relation_dom(sK16))
| ~ spl20_21
| ~ spl20_57 ),
inference(resolution,[],[f1379,f794]) ).
fof(f1386,plain,
( sK5(sK16,sK17,sK18) = apply(sK16,sK3(sK16,sK17,sK18))
| ~ spl20_10
| ~ spl20_57 ),
inference(resolution,[],[f1379,f539]) ).
fof(f1402,definition,
( spl20_58
<=> in(sK3(sK16,sK17,sK18),relation_dom(sK16)) ),
introduced(definition,[new_symbols(definition,[spl20_58])],[avatar_definition]) ).
fof(f1403,plain,
( ~ in(sK3(sK16,sK17,sK18),relation_dom(sK16))
| spl20_58 ),
inference(avatar_component_clause,[],[f1402]) ).
fof(f1404,plain,
( in(sK3(sK16,sK17,sK18),relation_dom(sK16))
| ~ spl20_58 ),
inference(avatar_component_clause,[],[f1402]) ).
fof(f1405,plain,
( spl20_58
| ~ spl20_21
| ~ spl20_57 ),
inference(avatar_split_clause,[],[f1385,f1377,f793,f1402]) ).
fof(f1468,plain,
( in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| ~ spl20_19
| ~ spl20_32 ),
inference(resolution,[],[f975,f775]) ).
fof(f1469,plain,
( sK4(sK16,sK17,sK18) = apply(sK18,sK3(sK16,sK17,sK18))
| ~ spl20_15
| ~ spl20_32 ),
inference(resolution,[],[f975,f707]) ).
fof(f1470,plain,
( in(sK3(sK16,sK17,sK18),relation_dom(sK16))
| ~ spl20_12
| ~ spl20_32 ),
inference(resolution,[],[f975,f553]) ).
fof(f1482,plain,
( $false
| ~ spl20_12
| ~ spl20_32
| spl20_58 ),
inference(forward_subsumption_resolution,[],[f1470,f1403]) ).
fof(f1483,plain,
( ~ spl20_12
| ~ spl20_32
| spl20_58 ),
inference(avatar_contradiction_clause,[],[f1482]) ).
fof(f1497,plain,
( ~ in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(apply(sK16,sK3(sK16,sK17,sK18)),sK4(sK16,sK17,sK18))),sK17)
| ~ in(sK3(sK16,sK17,sK18),relation_dom(sK16))
| ~ spl20_24
| ~ spl20_33 ),
inference(resolution,[],[f979,f843]) ).
fof(f1504,plain,
( ~ in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(apply(sK16,sK3(sK16,sK17,sK18)),sK4(sK16,sK17,sK18))),sK17)
| ~ spl20_24
| ~ spl20_33
| ~ spl20_58 ),
inference(forward_subsumption_resolution,[],[f1497,f1404]) ).
fof(f1506,plain,
( ~ in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(sK4(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18)))),sK17)
| ~ spl20_24
| ~ spl20_33
| ~ spl20_58 ),
inference(forward_demodulation,[],[f1504,f100]) ).
fof(f1511,definition,
( spl20_62
<=> in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(sK4(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK17) ),
introduced(definition,[new_symbols(definition,[spl20_62])],[avatar_definition]) ).
fof(f1512,plain,
( in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(sK4(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK17)
| ~ spl20_62 ),
inference(avatar_component_clause,[],[f1511]) ).
fof(f1513,plain,
( ~ in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(sK4(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK17)
| spl20_62 ),
inference(avatar_component_clause,[],[f1511]) ).
fof(f1541,plain,
( in(unordered_pair(unordered_pair(sK3(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18))),singleton(sK3(sK16,sK17,sK18))),sK16)
| ~ relation(sK16)
| ~ function(sK16)
| ~ spl20_58 ),
inference(resolution,[],[f1404,f182]) ).
fof(f1554,plain,
( in(unordered_pair(unordered_pair(sK3(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18))),singleton(sK3(sK16,sK17,sK18))),sK16)
| ~ function(sK16)
| ~ spl20_2
| ~ spl20_58 ),
inference(forward_subsumption_resolution,[],[f1541,f246]) ).
fof(f1559,plain,
( in(unordered_pair(unordered_pair(sK3(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18))),singleton(sK3(sK16,sK17,sK18))),sK16)
| ~ spl20_2
| ~ spl20_4
| ~ spl20_58 ),
inference(forward_subsumption_resolution,[],[f1554,f256]) ).
fof(f1562,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18)))),sK16)
| ~ spl20_2
| ~ spl20_4
| ~ spl20_58 ),
inference(forward_demodulation,[],[f1559,f100]) ).
fof(f1569,definition,
( spl20_64
<=> in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(sK4(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18)))),sK17) ),
introduced(definition,[new_symbols(definition,[spl20_64])],[avatar_definition]) ).
fof(f1571,plain,
( ~ in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(sK4(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18)))),sK17)
| spl20_64 ),
inference(avatar_component_clause,[],[f1569]) ).
fof(f1572,plain,
( ~ spl20_64
| ~ spl20_24
| ~ spl20_33
| ~ spl20_58 ),
inference(avatar_split_clause,[],[f1506,f1402,f978,f842,f1569]) ).
fof(f1574,definition,
( spl20_65
<=> in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18)))),sK16) ),
introduced(definition,[new_symbols(definition,[spl20_65])],[avatar_definition]) ).
fof(f1576,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18)))),sK16)
| ~ spl20_65 ),
inference(avatar_component_clause,[],[f1574]) ).
fof(f1577,plain,
( spl20_65
| ~ spl20_2
| ~ spl20_4
| ~ spl20_58 ),
inference(avatar_split_clause,[],[f1562,f1402,f254,f244,f1574]) ).
fof(f1585,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(apply(sK16,sK3(sK16,sK17,sK18)),X0)),sK17)
| in(sK3(sK16,sK17,sK18),relation_dom(sK18)) )
| ~ spl20_18
| ~ spl20_65 ),
inference(resolution,[],[f1576,f771]) ).
fof(f1618,definition,
( spl20_67
<=> sK4(sK16,sK17,sK18) = apply(sK18,sK3(sK16,sK17,sK18)) ),
introduced(definition,[new_symbols(definition,[spl20_67])],[avatar_definition]) ).
fof(f1619,plain,
( sK4(sK16,sK17,sK18) != apply(sK18,sK3(sK16,sK17,sK18))
| spl20_67 ),
inference(avatar_component_clause,[],[f1618]) ).
fof(f1620,plain,
( sK4(sK16,sK17,sK18) = apply(sK18,sK3(sK16,sK17,sK18))
| ~ spl20_67 ),
inference(avatar_component_clause,[],[f1618]) ).
fof(f1621,plain,
( spl20_67
| ~ spl20_15
| ~ spl20_32 ),
inference(avatar_split_clause,[],[f1469,f974,f706,f1618]) ).
fof(f1626,plain,
( in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(apply(sK16,sK3(sK16,sK17,sK18)),sK4(sK16,sK17,sK18))),sK17)
| ~ in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| ~ spl20_35
| ~ spl20_67 ),
inference(superposition,[],[f992,f1620]) ).
fof(f1628,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18)
| ~ in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| ~ spl20_22
| ~ spl20_67 ),
inference(superposition,[],[f798,f1620]) ).
fof(f1635,plain,
( in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(apply(sK16,sK3(sK16,sK17,sK18)),sK4(sK16,sK17,sK18))),sK17)
| ~ spl20_19
| ~ spl20_32
| ~ spl20_35
| ~ spl20_67 ),
inference(forward_subsumption_resolution,[],[f1626,f1468]) ).
fof(f1639,plain,
( in(unordered_pair(singleton(apply(sK16,sK3(sK16,sK17,sK18))),unordered_pair(sK4(sK16,sK17,sK18),apply(sK16,sK3(sK16,sK17,sK18)))),sK17)
| ~ spl20_19
| ~ spl20_32
| ~ spl20_35
| ~ spl20_67 ),
inference(forward_demodulation,[],[f1635,f100]) ).
fof(f1643,plain,
( $false
| ~ spl20_19
| ~ spl20_32
| ~ spl20_35
| spl20_64
| ~ spl20_67 ),
inference(forward_subsumption_resolution,[],[f1639,f1571]) ).
fof(f1644,plain,
( ~ spl20_19
| ~ spl20_32
| ~ spl20_35
| spl20_64
| ~ spl20_67 ),
inference(avatar_contradiction_clause,[],[f1643]) ).
fof(f1653,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(sK5(sK16,sK17,sK18),X0)),sK17)
| in(sK3(sK16,sK17,sK18),relation_dom(sK18)) )
| ~ spl20_10
| ~ spl20_18
| ~ spl20_57
| ~ spl20_65 ),
inference(forward_demodulation,[],[f1585,f1386]) ).
fof(f1657,plain,
( ~ in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| ~ spl20_22
| spl20_32
| ~ spl20_67 ),
inference(forward_subsumption_resolution,[],[f1628,f976]) ).
fof(f1667,plain,
( ! [X0] : ~ in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(sK5(sK16,sK17,sK18),X0)),sK17)
| ~ spl20_10
| ~ spl20_18
| ~ spl20_22
| spl20_32
| ~ spl20_57
| ~ spl20_65
| ~ spl20_67 ),
inference(backward_subsumption_resolution,[],[f1653,f1657]) ).
fof(f1681,plain,
( apply(sK17,sK5(sK16,sK17,sK18)) = apply(sK18,sK3(sK16,sK17,sK18))
| ~ in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| ~ spl20_30
| ~ spl20_57 ),
inference(resolution,[],[f1379,f965]) ).
fof(f1683,plain,
( ~ in(sK5(sK16,sK17,sK18),relation_dom(sK17))
| in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| ~ spl20_29
| ~ spl20_57 ),
inference(resolution,[],[f1379,f953]) ).
fof(f1696,definition,
( spl20_68
<=> in(sK5(sK16,sK17,sK18),relation_dom(sK17)) ),
introduced(definition,[new_symbols(definition,[spl20_68])],[avatar_definition]) ).
fof(f1697,plain,
( in(sK5(sK16,sK17,sK18),relation_dom(sK17))
| ~ spl20_68 ),
inference(avatar_component_clause,[],[f1696]) ).
fof(f1698,plain,
( ~ in(sK5(sK16,sK17,sK18),relation_dom(sK17))
| spl20_68 ),
inference(avatar_component_clause,[],[f1696]) ).
fof(f1701,definition,
( spl20_69
<=> ! [X0] : ~ in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(sK5(sK16,sK17,sK18),X0)),sK17) ),
introduced(definition,[new_symbols(definition,[spl20_69])],[avatar_definition]) ).
fof(f1702,plain,
( ! [X0] : ~ in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(sK5(sK16,sK17,sK18),X0)),sK17)
| ~ spl20_69 ),
inference(avatar_component_clause,[],[f1701]) ).
fof(f1703,plain,
( spl20_69
| ~ spl20_10
| ~ spl20_18
| ~ spl20_22
| spl20_32
| ~ spl20_57
| ~ spl20_65
| ~ spl20_67 ),
inference(avatar_split_clause,[],[f1667,f1618,f1574,f1377,f974,f797,f770,f538,f1701]) ).
fof(f1705,definition,
( spl20_70
<=> empty_set = sK4(sK16,sK17,sK18) ),
introduced(definition,[new_symbols(definition,[spl20_70])],[avatar_definition]) ).
fof(f1706,plain,
( empty_set != sK4(sK16,sK17,sK18)
| spl20_70 ),
inference(avatar_component_clause,[],[f1705]) ).
fof(f1707,plain,
( empty_set = sK4(sK16,sK17,sK18)
| ~ spl20_70 ),
inference(avatar_component_clause,[],[f1705]) ).
fof(f1710,definition,
( spl20_71
<=> in(sK3(sK16,sK17,sK18),relation_dom(sK18)) ),
introduced(definition,[new_symbols(definition,[spl20_71])],[avatar_definition]) ).
fof(f1711,plain,
( in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| ~ spl20_71 ),
inference(avatar_component_clause,[],[f1710]) ).
fof(f1712,plain,
( ~ in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| spl20_71 ),
inference(avatar_component_clause,[],[f1710]) ).
fof(f1721,plain,
( empty_set = apply(sK17,sK5(sK16,sK17,sK18))
| ~ relation(sK17)
| ~ function(sK17)
| spl20_68 ),
inference(resolution,[],[f1698,f183]) ).
fof(f1727,plain,
( empty_set = apply(sK17,sK5(sK16,sK17,sK18))
| ~ function(sK17)
| ~ spl20_3
| spl20_68 ),
inference(forward_subsumption_resolution,[],[f1721,f251]) ).
fof(f1732,plain,
( empty_set = apply(sK17,sK5(sK16,sK17,sK18))
| ~ spl20_3
| ~ spl20_5
| spl20_68 ),
inference(forward_subsumption_resolution,[],[f1727,f261]) ).
fof(f1909,definition,
( spl20_84
<=> ! [X0] :
( in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| in(unordered_pair(singleton(sK5(sK16,sK17,X0)),unordered_pair(sK4(sK16,sK17,X0),sK5(sK16,sK17,X0))),sK17)
| sK18 != X0
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_84])],[avatar_definition]) ).
fof(f1910,plain,
( ! [X0] :
( sK18 != X0
| in(unordered_pair(singleton(sK5(sK16,sK17,X0)),unordered_pair(sK4(sK16,sK17,X0),sK5(sK16,sK17,X0))),sK17)
| in(unordered_pair(singleton(sK3(sK16,sK17,X0)),unordered_pair(sK3(sK16,sK17,X0),sK4(sK16,sK17,X0))),X0)
| ~ relation(X0) )
| ~ spl20_84 ),
inference(avatar_component_clause,[],[f1909]) ).
fof(f1911,plain,
( spl20_84
| ~ spl20_2
| ~ spl20_3
| spl20_8 ),
inference(avatar_split_clause,[],[f351,f331,f249,f244,f1909]) ).
fof(f1912,plain,
( in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(sK4(sK16,sK17,sK18),sK5(sK16,sK17,sK18))),sK17)
| in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18)
| ~ relation(sK18)
| ~ spl20_84 ),
inference(equality_resolution,[],[f1910]) ).
fof(f1913,plain,
( in(unordered_pair(singleton(sK3(sK16,sK17,sK18)),unordered_pair(sK3(sK16,sK17,sK18),sK4(sK16,sK17,sK18))),sK18)
| ~ relation(sK18)
| spl20_62
| ~ spl20_84 ),
inference(forward_subsumption_resolution,[],[f1912,f1513]) ).
fof(f1917,plain,
( empty_set != apply(sK18,sK3(sK16,sK17,sK18))
| spl20_67
| ~ spl20_70 ),
inference(forward_demodulation,[],[f1619,f1707]) ).
fof(f1918,plain,
( ~ relation(sK18)
| spl20_32
| spl20_62
| ~ spl20_84 ),
inference(forward_subsumption_resolution,[],[f1913,f976]) ).
fof(f1923,plain,
( $false
| ~ spl20_7
| spl20_32
| spl20_62
| ~ spl20_84 ),
inference(forward_subsumption_resolution,[],[f1918,f311]) ).
fof(f1924,plain,
( ~ spl20_7
| spl20_32
| spl20_62
| ~ spl20_84 ),
inference(avatar_contradiction_clause,[],[f1923]) ).
fof(f1940,plain,
( empty_set = apply(sK18,sK3(sK16,sK17,sK18))
| ~ relation(sK18)
| ~ function(sK18)
| spl20_71 ),
inference(resolution,[],[f1712,f184]) ).
fof(f1948,plain,
( ~ relation(sK18)
| ~ function(sK18)
| spl20_67
| ~ spl20_70
| spl20_71 ),
inference(forward_subsumption_resolution,[],[f1940,f1917]) ).
fof(f1953,plain,
( ~ function(sK18)
| ~ spl20_7
| spl20_67
| ~ spl20_70
| spl20_71 ),
inference(forward_subsumption_resolution,[],[f1948,f311]) ).
fof(f1957,plain,
( $false
| ~ spl20_7
| ~ spl20_9
| spl20_67
| ~ spl20_70
| spl20_71 ),
inference(forward_subsumption_resolution,[],[f1953,f535]) ).
fof(f1958,plain,
( ~ spl20_7
| ~ spl20_9
| spl20_67
| ~ spl20_70
| spl20_71 ),
inference(avatar_contradiction_clause,[],[f1957]) ).
fof(f1963,plain,
( sK4(sK16,sK17,sK18) = apply(sK17,sK5(sK16,sK17,sK18))
| ~ spl20_45
| ~ spl20_62 ),
inference(resolution,[],[f1512,f1108]) ).
fof(f1977,plain,
( empty_set = sK4(sK16,sK17,sK18)
| ~ spl20_3
| ~ spl20_5
| ~ spl20_45
| ~ spl20_62
| spl20_68 ),
inference(forward_demodulation,[],[f1963,f1732]) ).
fof(f1981,plain,
( $false
| ~ spl20_3
| ~ spl20_5
| ~ spl20_45
| ~ spl20_62
| spl20_68
| spl20_70 ),
inference(forward_subsumption_resolution,[],[f1977,f1706]) ).
fof(f1982,plain,
( ~ spl20_3
| ~ spl20_5
| ~ spl20_45
| ~ spl20_62
| spl20_68
| spl20_70 ),
inference(avatar_contradiction_clause,[],[f1981]) ).
fof(f1989,plain,
( in(sK3(sK16,sK17,sK18),relation_dom(sK18))
| ~ spl20_29
| ~ spl20_57
| ~ spl20_68 ),
inference(forward_subsumption_resolution,[],[f1683,f1697]) ).
fof(f1996,plain,
( $false
| ~ spl20_29
| ~ spl20_57
| ~ spl20_68
| spl20_71 ),
inference(forward_subsumption_resolution,[],[f1989,f1712]) ).
fof(f1997,plain,
( ~ spl20_29
| ~ spl20_57
| ~ spl20_68
| spl20_71 ),
inference(avatar_contradiction_clause,[],[f1996]) ).
fof(f2003,plain,
( apply(sK17,sK5(sK16,sK17,sK18)) = apply(sK18,sK3(sK16,sK17,sK18))
| ~ spl20_30
| ~ spl20_57
| ~ spl20_71 ),
inference(forward_subsumption_resolution,[],[f1681,f1711]) ).
fof(f2006,plain,
( sK4(sK16,sK17,sK18) = apply(sK18,sK3(sK16,sK17,sK18))
| ~ spl20_30
| ~ spl20_45
| ~ spl20_57
| ~ spl20_62
| ~ spl20_71 ),
inference(forward_demodulation,[],[f2003,f1963]) ).
fof(f2007,plain,
( $false
| ~ spl20_30
| ~ spl20_45
| ~ spl20_57
| ~ spl20_62
| spl20_67
| ~ spl20_71 ),
inference(forward_subsumption_resolution,[],[f2006,f1619]) ).
fof(f2008,plain,
( ~ spl20_30
| ~ spl20_45
| ~ spl20_57
| ~ spl20_62
| spl20_67
| ~ spl20_71 ),
inference(avatar_contradiction_clause,[],[f2007]) ).
fof(f2123,plain,
( ! [X0] : ~ in(unordered_pair(singleton(sK5(sK16,sK17,sK18)),unordered_pair(X0,sK5(sK16,sK17,sK18))),sK17)
| ~ spl20_69 ),
inference(superposition,[],[f1702,f100]) ).
fof(f2124,plain,
( $false
| ~ spl20_62
| ~ spl20_69 ),
inference(backward_subsumption_resolution,[],[f1512,f2123]) ).
fof(f2126,plain,
( ~ spl20_62
| ~ spl20_69 ),
inference(avatar_contradiction_clause,[],[f2124]) ).
cnf(s1,plain,
spl20_1,
inference(sat_conversion,[],[f195]) ).
cnf(s2,plain,
spl20_2,
inference(sat_conversion,[],[f247]) ).
cnf(s3,plain,
spl20_3,
inference(sat_conversion,[],[f252]) ).
cnf(s4,plain,
spl20_4,
inference(sat_conversion,[],[f257]) ).
cnf(s5,plain,
spl20_5,
inference(sat_conversion,[],[f262]) ).
cnf(s6,plain,
spl20_6,
inference(sat_conversion,[],[f266]) ).
cnf(s7,plain,
spl20_7,
inference(sat_conversion,[],[f312]) ).
cnf(s8,plain,
~ spl20_8,
inference(sat_conversion,[],[f334]) ).
cnf(s9,plain,
spl20_9,
inference(sat_conversion,[],[f536]) ).
cnf(s10,plain,
( ~ spl20_2
| ~ spl20_4
| spl20_10 ),
inference(sat_conversion,[],[f540]) ).
cnf(s11,plain,
( ~ spl20_3
| ~ spl20_5
| spl20_11 ),
inference(sat_conversion,[],[f547]) ).
cnf(s12,plain,
( ~ spl20_1
| spl20_12 ),
inference(sat_conversion,[],[f554]) ).
cnf(s13,plain,
spl20_13,
inference(sat_conversion,[],[f561]) ).
cnf(s14,plain,
spl20_14,
inference(sat_conversion,[],[f691]) ).
cnf(s15,plain,
( ~ spl20_7
| ~ spl20_9
| spl20_15 ),
inference(sat_conversion,[],[f708]) ).
cnf(s17,plain,
( ~ spl20_3
| ~ spl20_6
| spl20_17 ),
inference(sat_conversion,[],[f757]) ).
cnf(s18,plain,
( ~ spl20_2
| ~ spl20_4
| ~ spl20_17
| spl20_18 ),
inference(sat_conversion,[],[f772]) ).
cnf(s19,plain,
( ~ spl20_7
| spl20_19 ),
inference(sat_conversion,[],[f776]) ).
cnf(s21,plain,
( ~ spl20_2
| spl20_21 ),
inference(sat_conversion,[],[f795]) ).
cnf(s22,plain,
( ~ spl20_7
| ~ spl20_9
| spl20_22 ),
inference(sat_conversion,[],[f799]) ).
cnf(s24,plain,
( ~ spl20_2
| ~ spl20_4
| spl20_24 ),
inference(sat_conversion,[],[f844]) ).
cnf(s29,plain,
( ~ spl20_2
| ~ spl20_4
| ~ spl20_6
| spl20_29 ),
inference(sat_conversion,[],[f954]) ).
cnf(s30,plain,
( ~ spl20_1
| ~ spl20_2
| ~ spl20_4
| ~ spl20_14
| spl20_30 ),
inference(sat_conversion,[],[f966]) ).
cnf(s31,plain,
( ~ spl20_2
| ~ spl20_3
| spl20_8
| spl20_31 ),
inference(sat_conversion,[],[f970]) ).
cnf(s32,plain,
( ~ spl20_7
| ~ spl20_31
| ~ spl20_32
| spl20_33 ),
inference(sat_conversion,[],[f980]) ).
cnf(s34,plain,
( ~ spl20_3
| ~ spl20_5
| ~ spl20_13
| ~ spl20_14
| spl20_35 ),
inference(sat_conversion,[],[f993]) ).
cnf(s44,plain,
( ~ spl20_11
| spl20_45 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s55,plain,
( ~ spl20_2
| ~ spl20_3
| spl20_8
| spl20_56 ),
inference(sat_conversion,[],[f1372]) ).
cnf(s56,plain,
( ~ spl20_7
| spl20_32
| ~ spl20_56
| spl20_57 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s57,plain,
( ~ spl20_21
| ~ spl20_57
| spl20_58 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s61,plain,
( ~ spl20_12
| ~ spl20_32
| spl20_58 ),
inference(sat_conversion,[],[f1483]) ).
cnf(s65,plain,
( ~ spl20_24
| ~ spl20_33
| ~ spl20_58
| ~ spl20_64 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s66,plain,
( ~ spl20_2
| ~ spl20_4
| ~ spl20_58
| spl20_65 ),
inference(sat_conversion,[],[f1577]) ).
cnf(s68,plain,
( ~ spl20_15
| ~ spl20_32
| spl20_67 ),
inference(sat_conversion,[],[f1621]) ).
cnf(s69,plain,
( ~ spl20_19
| ~ spl20_32
| ~ spl20_35
| spl20_64
| ~ spl20_67 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s72,plain,
( ~ spl20_10
| ~ spl20_18
| ~ spl20_22
| spl20_32
| ~ spl20_57
| ~ spl20_65
| ~ spl20_67
| spl20_69 ),
inference(sat_conversion,[],[f1703]) ).
cnf(s88,plain,
( ~ spl20_2
| ~ spl20_3
| spl20_8
| spl20_84 ),
inference(sat_conversion,[],[f1911]) ).
cnf(s90,plain,
( ~ spl20_7
| spl20_32
| spl20_62
| ~ spl20_84 ),
inference(sat_conversion,[],[f1924]) ).
cnf(s95,plain,
( ~ spl20_7
| ~ spl20_9
| spl20_67
| ~ spl20_70
| spl20_71 ),
inference(sat_conversion,[],[f1958]) ).
cnf(s96,plain,
( ~ spl20_3
| ~ spl20_5
| ~ spl20_45
| ~ spl20_62
| spl20_68
| spl20_70 ),
inference(sat_conversion,[],[f1982]) ).
cnf(s101,plain,
( ~ spl20_29
| ~ spl20_57
| ~ spl20_68
| spl20_71 ),
inference(sat_conversion,[],[f1997]) ).
cnf(s105,plain,
( ~ spl20_30
| ~ spl20_45
| ~ spl20_57
| ~ spl20_62
| spl20_67
| ~ spl20_71 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s112,plain,
( ~ spl20_62
| ~ spl20_69 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s118,plain,
spl20_22,
inference(rat,[],[s22,s9,s7]) ).
cnf(s119,plain,
spl20_19,
inference(rat,[],[s19,s7]) ).
cnf(s120,plain,
spl20_15,
inference(rat,[],[s15,s9,s7]) ).
cnf(s131,plain,
spl20_35,
inference(rat,[],[s34,s5,s14,s13,s3]) ).
cnf(s136,plain,
spl20_17,
inference(rat,[],[s17,s6,s3]) ).
cnf(s138,plain,
spl20_11,
inference(rat,[],[s11,s5,s3]) ).
cnf(s141,plain,
spl20_45,
inference(rat,[],[s44,s138]) ).
cnf(s142,plain,
spl20_84,
inference(rat,[],[s88,s3,s8,s2]) ).
cnf(s145,plain,
spl20_56,
inference(rat,[],[s55,s3,s8,s2]) ).
cnf(s151,plain,
spl20_31,
inference(rat,[],[s31,s3,s8,s2]) ).
cnf(s152,plain,
spl20_29,
inference(rat,[],[s29,s4,s6,s2]) ).
cnf(s153,plain,
spl20_24,
inference(rat,[],[s24,s4,s2]) ).
cnf(s154,plain,
spl20_21,
inference(rat,[],[s21,s2]) ).
cnf(s155,plain,
spl20_18,
inference(rat,[],[s18,s136,s4,s2]) ).
cnf(s156,plain,
spl20_10,
inference(rat,[],[s10,s4,s2]) ).
cnf(s164,plain,
spl20_30,
inference(rat,[],[s30,s2,s14,s4,s1]) ).
cnf(s166,plain,
spl20_12,
inference(rat,[],[s12,s1]) ).
cnf(s169,plain,
( spl20_67
| ~ spl20_57
| ~ spl20_62 ),
inference(rat,[],[s96,s101,s95,s105,s164,s7,s9,s152,s141,s3,s5]) ).
cnf(s170,plain,
spl20_32,
inference(rat,[],[s169,s72,s66,s57,s112,s56,s90,s118,s155,s156,s4,s2,s154,s7,s145,s142]) ).
cnf(s171,plain,
spl20_67,
inference(rat,[],[s68,s120,s170]) ).
cnf(s172,plain,
spl20_58,
inference(rat,[],[s61,s166,s170]) ).
cnf(s173,plain,
spl20_33,
inference(rat,[],[s32,s151,s7,s170]) ).
cnf(s174,plain,
spl20_64,
inference(rat,[],[s69,s171,s131,s119,s170]) ).
cnf(s178,plain,
$false,
inference(rat,[],[s65,s174,s153,s172,s173]) ).
fof(f2129,plain,
$false,
inference(avatar_sat_refutation,[],[s178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET998+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 % Computer : n015.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 28 03:24:46 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.49 Running first-order theorem proving
% 0.21/0.49 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.93/3.25 % (2228199)Detected formulas, will run a generic FOF schedule.
% 15.93/3.25 % (2228204)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=3119097310:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 15.93/3.25 % (2228208)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2992635224:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 15.93/3.25 % (2228207)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3184893543:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 15.93/3.25 % (2228205)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=1634003469:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 15.93/3.25 % (2228206)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=1920314601:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 15.93/3.25 % (2228207)Refutation not found, incomplete strategy
% 15.93/3.25 % (2228207)------------------------------
% 15.93/3.25 % (2228207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228207)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228207)Termination reason: Refutation not found, incomplete strategy
% 15.93/3.25 % (2228207)Time elapsed: 0.006 s
% 15.93/3.25 % (2228207)Peak memory usage: 88 MB
% 15.93/3.25 % (2228207)Instructions burned: 4 (million)
% 15.93/3.25 % (2228210)dis-21_1_sil=8000:lcm=predicate:random_seed=1394771077: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)
% 15.93/3.25 % (2228209)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2637449508:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 15.93/3.25 % (2228208)Instruction limit reached!
% 15.93/3.25 % (2228208)------------------------------
% 15.93/3.25 % (2228208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228208)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228208)Termination reason: Instruction limit
% 15.93/3.25 % (2228208)Termination phase: Saturation
% 15.93/3.25 % (2228208)Time elapsed: 0.109 s
% 15.93/3.25 % (2228208)Peak memory usage: 88 MB
% 15.93/3.25 % (2228208)Instructions burned: 119 (million)
% 15.93/3.25 % (2228209)Instruction limit reached!
% 15.93/3.25 % (2228209)------------------------------
% 15.93/3.25 % (2228209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228209)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228209)Termination reason: Instruction limit
% 15.93/3.25 % (2228209)Termination phase: Saturation
% 15.93/3.25 % (2228209)Time elapsed: 0.140 s
% 15.93/3.25 % (2228209)Peak memory usage: 90 MB
% 15.93/3.25 % (2228209)Instructions burned: 139 (million)
% 15.93/3.25 % (2228210)Instruction limit reached!
% 15.93/3.25 % (2228210)------------------------------
% 15.93/3.25 % (2228210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228210)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228210)Termination reason: Instruction limit
% 15.93/3.25 % (2228210)Termination phase: Saturation
% 15.93/3.25 % (2228210)Time elapsed: 0.143 s
% 15.93/3.25 % (2228210)Peak memory usage: 90 MB
% 15.93/3.25 % (2228210)Instructions burned: 129 (million)
% 15.93/3.25 % (2228218)lrs+10_1_sil=8000:sp=occurrence:random_seed=650430272:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 15.93/3.25 % (2228207)------------------------------
% 15.93/3.25 % (2228207)------------------------------
% 15.93/3.25 % (2228219)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1364600554:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 15.93/3.25 % (2228220)lrs+1011_1_sil=32000:sp=occurrence:random_seed=444025294:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 15.93/3.25 % (2228218)Instruction limit reached!
% 15.93/3.25 % (2228218)------------------------------
% 15.93/3.25 % (2228218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228218)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228218)Termination reason: Instruction limit
% 15.93/3.25 % (2228218)Termination phase: Saturation
% 15.93/3.25 % (2228218)Time elapsed: 0.251 s
% 15.93/3.25 % (2228218)Peak memory usage: 91 MB
% 15.93/3.25 % (2228218)Instructions burned: 285 (million)
% 15.93/3.25 % (2228222)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=582650407:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 15.93/3.25 % (2228219)Instruction limit reached!
% 15.93/3.25 % (2228219)------------------------------
% 15.93/3.25 % (2228219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228219)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228219)Termination reason: Instruction limit
% 15.93/3.25 % (2228219)Termination phase: Saturation
% 15.93/3.25 % (2228219)Time elapsed: 0.138 s
% 15.93/3.25 % (2228219)Peak memory usage: 90 MB
% 15.93/3.25 % (2228219)Instructions burned: 157 (million)
% 15.93/3.25 % (2228220)Instruction limit reached!
% 15.93/3.25 % (2228220)------------------------------
% 15.93/3.25 % (2228220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228220)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228220)Termination reason: Instruction limit
% 15.93/3.25 % (2228220)Termination phase: Saturation
% 15.93/3.25 % (2228220)Time elapsed: 0.314 s
% 15.93/3.25 % (2228220)Peak memory usage: 92 MB
% 15.93/3.25 % (2228220)Instructions burned: 325 (million)
% 15.93/3.25 % (2228222)Instruction limit reached!
% 15.93/3.25 % (2228222)------------------------------
% 15.93/3.25 % (2228222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228222)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228222)Termination reason: Instruction limit
% 15.93/3.25 % (2228222)Termination phase: Saturation
% 15.93/3.25 % (2228222)Time elapsed: 0.223 s
% 15.93/3.25 % (2228222)Peak memory usage: 93 MB
% 15.93/3.25 % (2228222)Instructions burned: 248 (million)
% 15.93/3.25 % (2228225)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=584220661:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 15.93/3.25 % (2228225)Refutation not found, incomplete strategy
% 15.93/3.25 % (2228225)------------------------------
% 15.93/3.25 % (2228225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228225)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228225)Termination reason: Refutation not found, incomplete strategy
% 15.93/3.25 % (2228225)Time elapsed: 0.008 s
% 15.93/3.25 % (2228225)Peak memory usage: 89 MB
% 15.93/3.25 % (2228225)Instructions burned: 6 (million)
% 15.93/3.25 % (2228227)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3709523826:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 15.93/3.25 % (2228229)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1113281163:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 15.93/3.25 % (2228231)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=323222282:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 15.93/3.25 % (2228229)Instruction limit reached!
% 15.93/3.25 % (2228229)------------------------------
% 15.93/3.25 % (2228229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228229)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228229)Termination reason: Instruction limit
% 15.93/3.25 % (2228229)Termination phase: Saturation
% 15.93/3.25 % (2228229)Time elapsed: 0.120 s
% 15.93/3.25 % (2228229)Peak memory usage: 90 MB
% 15.93/3.25 % (2228229)Instructions burned: 113 (million)
% 15.93/3.25 % (2228231)Instruction limit reached!
% 15.93/3.25 % (2228231)------------------------------
% 15.93/3.25 % (2228231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228231)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228231)Termination reason: Instruction limit
% 15.93/3.25 % (2228231)Termination phase: Saturation
% 15.93/3.25 % (2228231)Time elapsed: 0.114 s
% 15.93/3.25 % (2228231)Peak memory usage: 89 MB
% 15.93/3.25 % (2228231)Instructions burned: 128 (million)
% 15.93/3.25 % (2228225)------------------------------
% 15.93/3.25 % (2228225)------------------------------
% 15.93/3.25 % (2228237)lrs+10_1_sil=8000:sp=occurrence:random_seed=1709721146:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 15.93/3.25 % (2228236)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3812051510:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 15.93/3.25 % (2228206)First to succeed.
% 15.93/3.25 % (2228206)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2228199"
% 15.93/3.25 % (2228236)Instruction limit reached!
% 15.93/3.25 % (2228236)------------------------------
% 15.93/3.25 % (2228236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228236)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228236)Termination reason: Instruction limit
% 15.93/3.25 % (2228236)Termination phase: Saturation
% 15.93/3.25 % (2228236)Time elapsed: 0.108 s
% 15.93/3.25 % (2228236)Peak memory usage: 89 MB
% 15.93/3.25 % (2228236)Instructions burned: 114 (million)
% 15.93/3.25 % (2228238)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=592140114:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 15.93/3.25 % (2228238)Refutation not found, incomplete strategy
% 15.93/3.25 % (2228238)------------------------------
% 15.93/3.25 % (2228238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.93/3.25 % (2228238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.93/3.25 % (2228238)CaDiCaL version: 2.1.3
% 15.93/3.25 % (2228238)Termination reason: Refutation not found, incomplete strategy
% 15.93/3.25 % (2228238)Time elapsed: 0.011 s
% 15.93/3.25 % (2228238)Peak memory usage: 89 MB
% 15.93/3.25 % (2228238)Instructions burned: 8 (million)
% 15.93/3.25 % (2228241)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1197418922:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 15.93/3.25 % (2228206)Refutation found. Thanks to Tanya!
% 15.93/3.25 % SZS status Theorem for theBenchmark
% 15.93/3.25 % SZS output start Proof for theBenchmark
% See solution above
% 16.52/3.56 % (2228206)------------------------------
% 16.52/3.56 % (2228206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.52/3.56 % (2228206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.52/3.56 % (2228206)CaDiCaL version: 2.1.3
% 16.52/3.56 % (2228206)Termination reason: Refutation
% 16.52/3.56 % (2228206)Time elapsed: 1.482 s
% 16.52/3.56 % (2228206)Peak memory usage: 133 MB
% 16.52/3.56 % (2228206)Instructions burned: 1326 (million)
% 16.52/3.56 % (2228206)------------------------------
% 16.52/3.56 % (2228206)------------------------------
% 16.52/3.56 % (2228199)Success in time 2.24 s
% 16.52/3.56 % Vampire exiting
%------------------------------------------------------------------------------