%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET738+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:41:47 PM UTC 2026
% Result : Theorem 29.07s 4.96s
% Output : Refutation 30.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 75
% Syntax : Number of formulae : 499 ( 78 unt; 69 def)
% Number of atoms : 2033 ( 112 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 2878 (1344 ~;1338 |; 99 &)
% ( 80 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 77 ( 75 usr; 67 prp; 0-5 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-5 aty)
% Number of variables : 759 ( 0 sgn 725 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [X0,X1,X2] :
( maps(X0,X1,X2)
<=> ( ! [X3] :
( member(X3,X1)
=> ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) ) )
& ! [X3,X5,X6] :
( ( member(X3,X1)
& member(X5,X2)
& member(X6,X2) )
=> ( ( apply(X0,X3,X5)
& apply(X0,X3,X6) )
=> X5 = X6 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maps) ).
fof(f14,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( member(X5,X2)
& member(X6,X4) )
=> ( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
<=> ? [X7] :
( member(X7,X3)
& apply(X1,X5,X7)
& apply(X0,X7,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compose_function) ).
fof(f17,axiom,
! [X0,X1,X2] :
( injective(X0,X1,X2)
<=> ! [X3,X4,X5] :
( ( member(X3,X1)
& member(X4,X1)
& member(X5,X2) )
=> ( ( apply(X0,X3,X5)
& apply(X0,X4,X5) )
=> X3 = X4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',injective) ).
fof(f18,axiom,
! [X0,X1,X2] :
( surjective(X0,X1,X2)
<=> ! [X3] :
( member(X3,X2)
=> ? [X4] :
( member(X4,X1)
& apply(X0,X4,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',surjective) ).
fof(f19,axiom,
! [X0,X1,X2] :
( one_to_one(X0,X1,X2)
<=> ( injective(X0,X1,X2)
& surjective(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',one_to_one) ).
fof(f29,conjecture,
! [X0,X1,X2,X3,X4,X5] :
( ( maps(X0,X3,X4)
& maps(X1,X4,X5)
& maps(X2,X5,X3)
& injective(compose_function(X2,compose_function(X1,X0,X3,X4,X5),X3,X5,X3),X3,X3)
& injective(compose_function(X0,compose_function(X2,X1,X4,X5,X3),X4,X3,X4),X4,X4)
& surjective(compose_function(X1,compose_function(X0,X2,X5,X3,X4),X5,X4,X5),X5,X5) )
=> one_to_one(X2,X5,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thII29) ).
fof(f30,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5] :
( ( maps(X0,X3,X4)
& maps(X1,X4,X5)
& maps(X2,X5,X3)
& injective(compose_function(X2,compose_function(X1,X0,X3,X4,X5),X3,X5,X3),X3,X3)
& injective(compose_function(X0,compose_function(X2,X1,X4,X5,X3),X4,X3,X4),X4,X4)
& surjective(compose_function(X1,compose_function(X0,X2,X5,X3,X4),X5,X4,X5),X5,X5) )
=> one_to_one(X2,X5,X3) ),
inference(negated_conjecture,[status(cth)],[f29]) ).
fof(f31,plain,
! [X0,X1,X2] :
( maps(X0,X1,X2)
<=> ( ! [X3] :
( member(X3,X1)
=> ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) ) )
& ! [X5,X6,X7] :
( ( member(X5,X1)
& member(X6,X2)
& member(X7,X2) )
=> ( ( apply(X0,X5,X6)
& apply(X0,X5,X7) )
=> X6 = X7 ) ) ) ),
inference(rectify,[],[f12]) ).
fof(f32,plain,
! [X0,X1,X2] :
( ( injective(X0,X1,X2)
& surjective(X0,X1,X2) )
=> one_to_one(X0,X1,X2) ),
inference(unused_predicate_definition_removal,[],[f19]) ).
fof(f33,plain,
! [X0,X1,X2] :
( maps(X0,X1,X2)
=> ( ! [X3] :
( member(X3,X1)
=> ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) ) )
& ! [X5,X6,X7] :
( ( member(X5,X1)
& member(X6,X2)
& member(X7,X2) )
=> ( ( apply(X0,X5,X6)
& apply(X0,X5,X7) )
=> X6 = X7 ) ) ) ),
inference(unused_predicate_definition_removal,[],[f31]) ).
fof(f34,plain,
? [X0,X1,X2,X3,X4,X5] :
( ~ one_to_one(X2,X5,X3)
& maps(X0,X3,X4)
& maps(X1,X4,X5)
& maps(X2,X5,X3)
& injective(compose_function(X2,compose_function(X1,X0,X3,X4,X5),X3,X5,X3),X3,X3)
& injective(compose_function(X0,compose_function(X2,X1,X4,X5,X3),X4,X3,X4),X4,X4)
& surjective(compose_function(X1,compose_function(X0,X2,X5,X3,X4),X5,X4,X5),X5,X5) ),
inference(ennf_transformation,[],[f30]) ).
fof(f35,plain,
? [X0,X1,X2,X3,X4,X5] :
( ~ one_to_one(X2,X5,X3)
& maps(X0,X3,X4)
& maps(X1,X4,X5)
& maps(X2,X5,X3)
& injective(compose_function(X2,compose_function(X1,X0,X3,X4,X5),X3,X5,X3),X3,X3)
& injective(compose_function(X0,compose_function(X2,X1,X4,X5,X3),X4,X3,X4),X4,X4)
& surjective(compose_function(X1,compose_function(X0,X2,X5,X3,X4),X5,X4,X5),X5,X5) ),
inference(flattening,[],[f34]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ( ! [X3] :
( ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) )
| ~ member(X3,X1) )
& ! [X5,X6,X7] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X5,X1)
| ~ member(X6,X2)
| ~ member(X7,X2) ) )
| ~ maps(X0,X1,X2) ),
inference(ennf_transformation,[],[f33]) ).
fof(f37,plain,
! [X0,X1,X2] :
( ( ! [X3] :
( ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) )
| ~ member(X3,X1) )
& ! [X5,X6,X7] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X5,X1)
| ~ member(X6,X2)
| ~ member(X7,X2) ) )
| ~ maps(X0,X1,X2) ),
inference(flattening,[],[f36]) ).
fof(f38,plain,
! [X0,X1,X2] :
( one_to_one(X0,X1,X2)
| ~ injective(X0,X1,X2)
| ~ surjective(X0,X1,X2) ),
inference(ennf_transformation,[],[f32]) ).
fof(f39,plain,
! [X0,X1,X2] :
( one_to_one(X0,X1,X2)
| ~ injective(X0,X1,X2)
| ~ surjective(X0,X1,X2) ),
inference(flattening,[],[f38]) ).
fof(f40,plain,
! [X0,X1,X2] :
( injective(X0,X1,X2)
<=> ! [X3,X4,X5] :
( X3 = X4
| ~ apply(X0,X3,X5)
| ~ apply(X0,X4,X5)
| ~ member(X3,X1)
| ~ member(X4,X1)
| ~ member(X5,X2) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f41,plain,
! [X0,X1,X2] :
( injective(X0,X1,X2)
<=> ! [X3,X4,X5] :
( X3 = X4
| ~ apply(X0,X3,X5)
| ~ apply(X0,X4,X5)
| ~ member(X3,X1)
| ~ member(X4,X1)
| ~ member(X5,X2) ) ),
inference(flattening,[],[f40]) ).
fof(f42,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
<=> ? [X7] :
( member(X7,X3)
& apply(X1,X5,X7)
& apply(X0,X7,X6) ) )
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(ennf_transformation,[],[f14]) ).
fof(f43,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
<=> ? [X7] :
( member(X7,X3)
& apply(X1,X5,X7)
& apply(X0,X7,X6) ) )
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(flattening,[],[f42]) ).
fof(f44,plain,
! [X0,X1,X2] :
( surjective(X0,X1,X2)
<=> ! [X3] :
( ? [X4] :
( member(X4,X1)
& apply(X0,X4,X3) )
| ~ member(X3,X2) ) ),
inference(ennf_transformation,[],[f18]) ).
fof(f45,plain,
( ~ one_to_one(sK2,sK5,sK3)
& maps(sK0,sK3,sK4)
& maps(sK1,sK4,sK5)
& maps(sK2,sK5,sK3)
& injective(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),sK3,sK3)
& injective(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK4)
& surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5)],[f35]) ).
fof(f46,plain,
! [X0,X1,X2] :
( ( ! [X3] :
( ( member(sK6(X0,X2,X3),X2)
& apply(X0,X3,sK6(X0,X2,X3)) )
| ~ member(X3,X1) )
& ! [X5,X6,X7] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X5,X1)
| ~ member(X6,X2)
| ~ member(X7,X2) ) )
| ~ maps(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X4,sK6(X0,X2,X3))],[f37]) ).
fof(f47,plain,
! [X0,X1,X2] :
( ( injective(X0,X1,X2)
| ? [X3,X4,X5] :
( X3 != X4
& apply(X0,X3,X5)
& apply(X0,X4,X5)
& member(X3,X1)
& member(X4,X1)
& member(X5,X2) ) )
& ( ! [X3,X4,X5] :
( X3 = X4
| ~ apply(X0,X3,X5)
| ~ apply(X0,X4,X5)
| ~ member(X3,X1)
| ~ member(X4,X1)
| ~ member(X5,X2) )
| ~ injective(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f48,plain,
! [X0,X1,X2] :
( ( injective(X0,X1,X2)
| ? [X3,X4,X5] :
( X3 != X4
& apply(X0,X3,X5)
& apply(X0,X4,X5)
& member(X3,X1)
& member(X4,X1)
& member(X5,X2) ) )
& ( ! [X6,X7,X8] :
( X6 = X7
| ~ apply(X0,X6,X8)
| ~ apply(X0,X7,X8)
| ~ member(X6,X1)
| ~ member(X7,X1)
| ~ member(X8,X2) )
| ~ injective(X0,X1,X2) ) ),
inference(rectify,[],[f47]) ).
fof(f49,plain,
! [X0,X1,X2] :
( ( injective(X0,X1,X2)
| ( sK7(X0,X1,X2) != sK8(X0,X1,X2)
& apply(X0,sK7(X0,X1,X2),sK9(X0,X1,X2))
& apply(X0,sK8(X0,X1,X2),sK9(X0,X1,X2))
& member(sK7(X0,X1,X2),X1)
& member(sK8(X0,X1,X2),X1)
& member(sK9(X0,X1,X2),X2) ) )
& ( ! [X6,X7,X8] :
( X6 = X7
| ~ apply(X0,X6,X8)
| ~ apply(X0,X7,X8)
| ~ member(X6,X1)
| ~ member(X7,X1)
| ~ member(X8,X2) )
| ~ injective(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9]),skolemize(X3,sK7(X0,X1,X2)),skolemize(X4,sK8(X0,X1,X2)),skolemize(X5,sK9(X0,X1,X2))],[f48]) ).
fof(f50,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( ( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ! [X7] :
( ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6) ) )
& ( ? [X7] :
( member(X7,X3)
& apply(X1,X5,X7)
& apply(X0,X7,X6) )
| ~ apply(compose_function(X0,X1,X2,X3,X4),X5,X6) ) )
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(nnf_transformation,[],[f43]) ).
fof(f51,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( ( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ! [X7] :
( ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6) ) )
& ( ? [X8] :
( member(X8,X3)
& apply(X1,X5,X8)
& apply(X0,X8,X6) )
| ~ apply(compose_function(X0,X1,X2,X3,X4),X5,X6) ) )
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(rectify,[],[f50]) ).
fof(f52,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( ( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ! [X7] :
( ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6) ) )
& ( ( member(sK10(X0,X1,X3,X5,X6),X3)
& apply(X1,X5,sK10(X0,X1,X3,X5,X6))
& apply(X0,sK10(X0,X1,X3,X5,X6),X6) )
| ~ apply(compose_function(X0,X1,X2,X3,X4),X5,X6) ) )
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X8,sK10(X0,X1,X3,X5,X6))],[f51]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ( surjective(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ member(X4,X1)
| ~ apply(X0,X4,X3) )
& member(X3,X2) ) )
& ( ! [X3] :
( ? [X4] :
( member(X4,X1)
& apply(X0,X4,X3) )
| ~ member(X3,X2) )
| ~ surjective(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ( surjective(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ member(X4,X1)
| ~ apply(X0,X4,X3) )
& member(X3,X2) ) )
& ( ! [X5] :
( ? [X6] :
( member(X6,X1)
& apply(X0,X6,X5) )
| ~ member(X5,X2) )
| ~ surjective(X0,X1,X2) ) ),
inference(rectify,[],[f53]) ).
fof(f55,plain,
! [X0,X1,X2] :
( ( surjective(X0,X1,X2)
| ( ! [X4] :
( ~ member(X4,X1)
| ~ apply(X0,X4,sK11(X0,X1,X2)) )
& member(sK11(X0,X1,X2),X2) ) )
& ( ! [X5] :
( ( member(sK12(X0,X1,X5),X1)
& apply(X0,sK12(X0,X1,X5),X5) )
| ~ member(X5,X2) )
| ~ surjective(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X0,X1,X2)),skolemize(X6,sK12(X0,X1,X5))],[f54]) ).
fof(f56,plain,
surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5),
inference(cnf_transformation,[],[f45]) ).
fof(f57,plain,
injective(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK4),
inference(cnf_transformation,[],[f45]) ).
fof(f58,plain,
injective(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),sK3,sK3),
inference(cnf_transformation,[],[f45]) ).
fof(f59,plain,
maps(sK2,sK5,sK3),
inference(cnf_transformation,[],[f45]) ).
fof(f60,plain,
maps(sK1,sK4,sK5),
inference(cnf_transformation,[],[f45]) ).
fof(f61,plain,
maps(sK0,sK3,sK4),
inference(cnf_transformation,[],[f45]) ).
fof(f62,plain,
~ one_to_one(sK2,sK5,sK3),
inference(cnf_transformation,[],[f45]) ).
fof(f63,plain,
! [X2,X0,X1,X6,X7,X5] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X5,X1)
| ~ member(X6,X2)
| ~ member(X7,X2)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f46]) ).
fof(f64,plain,
! [X2,X3,X0,X1] :
( apply(X0,X3,sK6(X0,X2,X3))
| ~ member(X3,X1)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f46]) ).
fof(f65,plain,
! [X2,X3,X0,X1] :
( member(sK6(X0,X2,X3),X2)
| ~ member(X3,X1)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f46]) ).
fof(f66,plain,
! [X2,X0,X1] :
( one_to_one(X0,X1,X2)
| ~ injective(X0,X1,X2)
| ~ surjective(X0,X1,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f67,plain,
! [X2,X0,X1,X8,X6,X7] :
( X6 = X7
| ~ apply(X0,X6,X8)
| ~ apply(X0,X7,X8)
| ~ member(X6,X1)
| ~ member(X7,X1)
| ~ member(X8,X2)
| ~ injective(X0,X1,X2) ),
inference(cnf_transformation,[],[f49]) ).
fof(f68,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| member(sK9(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f49]) ).
fof(f69,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| member(sK8(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f70,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| member(sK7(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f71,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| apply(X0,sK8(X0,X1,X2),sK9(X0,X1,X2)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f72,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| apply(X0,sK7(X0,X1,X2),sK9(X0,X1,X2)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f73,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| sK7(X0,X1,X2) != sK8(X0,X1,X2) ),
inference(cnf_transformation,[],[f49]) ).
fof(f74,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( apply(X0,sK10(X0,X1,X3,X5,X6),X6)
| ~ apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(cnf_transformation,[],[f52]) ).
fof(f75,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( apply(X1,X5,sK10(X0,X1,X3,X5,X6))
| ~ apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(cnf_transformation,[],[f52]) ).
fof(f76,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( member(sK10(X0,X1,X3,X5,X6),X3)
| ~ apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(cnf_transformation,[],[f52]) ).
fof(f77,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6)
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(cnf_transformation,[],[f52]) ).
fof(f78,plain,
! [X2,X0,X1,X5] :
( apply(X0,sK12(X0,X1,X5),X5)
| ~ member(X5,X2)
| ~ surjective(X0,X1,X2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f79,plain,
! [X2,X0,X1,X5] :
( member(sK12(X0,X1,X5),X1)
| ~ member(X5,X2)
| ~ surjective(X0,X1,X2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f80,plain,
! [X2,X0,X1] :
( surjective(X0,X1,X2)
| member(sK11(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f81,plain,
! [X2,X0,X1,X4] :
( surjective(X0,X1,X2)
| ~ member(X4,X1)
| ~ apply(X0,X4,sK11(X0,X1,X2)) ),
inference(cnf_transformation,[],[f55]) ).
fof(f82,plain,
! [X2,X0,X1,X5] :
( ~ member(X5,X1)
| ~ maps(X0,X1,X2)
| sP13(X5,X2,X0) ),
inference(cnf_transformation,[],[f82_D]) ).
fof(f82_D,definition,
! [X0,X2,X5] :
( ! [X1] :
( ~ member(X5,X1)
| ~ maps(X0,X1,X2) )
<=> ~ sP13(X5,X2,X0) ),
introduced(definition,[new_symbols(definition,[sP13])],[general_splitting_component_introduction]) ).
fof(f83,plain,
! [X2,X0,X6,X7,X5] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X6,X2)
| ~ member(X7,X2)
| ~ sP13(X5,X2,X0) ),
inference(general_splitting,[],[f63,f82_D]) ).
fof(f84,plain,
! [X2,X0,X1,X8] :
( ~ member(X8,X2)
| ~ injective(X0,X1,X2)
| sP14(X1,X0,X8) ),
inference(cnf_transformation,[],[f84_D]) ).
fof(f84_D,definition,
! [X8,X0,X1] :
( ! [X2] :
( ~ member(X8,X2)
| ~ injective(X0,X1,X2) )
<=> ~ sP14(X1,X0,X8) ),
introduced(definition,[new_symbols(definition,[sP14])],[general_splitting_component_introduction]) ).
fof(f85,plain,
! [X0,X1,X8,X6,X7] :
( X6 = X7
| ~ apply(X0,X6,X8)
| ~ apply(X0,X7,X8)
| ~ member(X6,X1)
| ~ member(X7,X1)
| ~ sP14(X1,X0,X8) ),
inference(general_splitting,[],[f67,f84_D]) ).
fof(f86,plain,
! [X3,X0,X1,X6,X7,X5] :
( ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6)
| sP15(X5,X6,X0,X3,X1) ),
inference(cnf_transformation,[],[f86_D]) ).
fof(f86_D,definition,
! [X1,X3,X0,X6,X5] :
( ! [X7] :
( ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6) )
<=> ~ sP15(X5,X6,X0,X3,X1) ),
introduced(definition,[new_symbols(definition,[sP15])],[general_splitting_component_introduction]) ).
fof(f87,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X5,X2)
| ~ member(X6,X4)
| ~ sP15(X5,X6,X0,X3,X1) ),
inference(general_splitting,[],[f77,f86_D]) ).
fof(f89,definition,
( spl16_1
<=> one_to_one(sK2,sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f91,plain,
( ~ one_to_one(sK2,sK5,sK3)
| spl16_1 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f92,plain,
~ spl16_1,
inference(avatar_split_clause,[],[f62,f89]) ).
fof(f93,plain,
( ~ injective(sK2,sK5,sK3)
| ~ surjective(sK2,sK5,sK3)
| spl16_1 ),
inference(resolution,[],[f91,f66]) ).
fof(f95,definition,
( spl16_2
<=> injective(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),sK3,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f97,plain,
( injective(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),sK3,sK3)
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f95]) ).
fof(f98,plain,
spl16_2,
inference(avatar_split_clause,[],[f58,f95]) ).
fof(f100,plain,
( ! [X0] :
( ~ member(X0,sK3)
| sP14(sK3,compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X0) )
| ~ spl16_2 ),
inference(resolution,[],[f97,f84]) ).
fof(f102,definition,
( spl16_3
<=> maps(sK2,sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition]) ).
fof(f104,plain,
( maps(sK2,sK5,sK3)
| ~ spl16_3 ),
inference(avatar_component_clause,[],[f102]) ).
fof(f105,plain,
spl16_3,
inference(avatar_split_clause,[],[f59,f102]) ).
fof(f106,plain,
( ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) )
| ~ spl16_3 ),
inference(resolution,[],[f104,f64]) ).
fof(f107,plain,
( ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) )
| ~ spl16_3 ),
inference(resolution,[],[f104,f65]) ).
fof(f110,definition,
( spl16_4
<=> ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition]) ).
fof(f111,plain,
( ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) )
| ~ spl16_4 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f112,plain,
( spl16_4
| ~ spl16_3 ),
inference(avatar_split_clause,[],[f106,f102,f110]) ).
fof(f117,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK5)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| sP15(X3,sK6(sK2,sK3,X0),sK2,X1,X2) )
| ~ spl16_4 ),
inference(resolution,[],[f111,f86]) ).
fof(f120,definition,
( spl16_5
<=> ! [X0] :
( ~ member(X0,sK3)
| sP14(sK3,compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition]) ).
fof(f121,plain,
( ! [X0] :
( sP14(sK3,compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X0)
| ~ member(X0,sK3) )
| ~ spl16_5 ),
inference(avatar_component_clause,[],[f120]) ).
fof(f122,plain,
( spl16_5
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f100,f95,f120]) ).
fof(f124,definition,
( spl16_6
<=> injective(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_6])],[avatar_definition]) ).
fof(f126,plain,
( injective(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK4)
| ~ spl16_6 ),
inference(avatar_component_clause,[],[f124]) ).
fof(f127,plain,
spl16_6,
inference(avatar_split_clause,[],[f57,f124]) ).
fof(f129,definition,
( spl16_7
<=> maps(sK0,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_7])],[avatar_definition]) ).
fof(f131,plain,
( maps(sK0,sK3,sK4)
| ~ spl16_7 ),
inference(avatar_component_clause,[],[f129]) ).
fof(f132,plain,
spl16_7,
inference(avatar_split_clause,[],[f61,f129]) ).
fof(f133,plain,
( ! [X0] :
( apply(sK0,X0,sK6(sK0,sK4,X0))
| ~ member(X0,sK3) )
| ~ spl16_7 ),
inference(resolution,[],[f131,f64]) ).
fof(f134,plain,
( ! [X0] :
( member(sK6(sK0,sK4,X0),sK4)
| ~ member(X0,sK3) )
| ~ spl16_7 ),
inference(resolution,[],[f131,f65]) ).
fof(f137,definition,
( spl16_8
<=> ! [X0] :
( apply(sK0,X0,sK6(sK0,sK4,X0))
| ~ member(X0,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_8])],[avatar_definition]) ).
fof(f138,plain,
( ! [X0] :
( apply(sK0,X0,sK6(sK0,sK4,X0))
| ~ member(X0,sK3) )
| ~ spl16_8 ),
inference(avatar_component_clause,[],[f137]) ).
fof(f139,plain,
( spl16_8
| ~ spl16_7 ),
inference(avatar_split_clause,[],[f133,f129,f137]) ).
fof(f144,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK3)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| sP15(X3,sK6(sK0,sK4,X0),sK0,X1,X2) )
| ~ spl16_8 ),
inference(resolution,[],[f138,f86]) ).
fof(f151,definition,
( spl16_10
<=> maps(sK1,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_10])],[avatar_definition]) ).
fof(f153,plain,
( maps(sK1,sK4,sK5)
| ~ spl16_10 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,plain,
spl16_10,
inference(avatar_split_clause,[],[f60,f151]) ).
fof(f155,plain,
( ! [X0] :
( apply(sK1,X0,sK6(sK1,sK5,X0))
| ~ member(X0,sK4) )
| ~ spl16_10 ),
inference(resolution,[],[f153,f64]) ).
fof(f156,plain,
( ! [X0] :
( member(sK6(sK1,sK5,X0),sK5)
| ~ member(X0,sK4) )
| ~ spl16_10 ),
inference(resolution,[],[f153,f65]) ).
fof(f157,plain,
( ! [X0] :
( ~ member(X0,sK4)
| sP13(X0,sK5,sK1) )
| ~ spl16_10 ),
inference(resolution,[],[f153,f82]) ).
fof(f159,definition,
( spl16_11
<=> ! [X0] :
( apply(sK1,X0,sK6(sK1,sK5,X0))
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_11])],[avatar_definition]) ).
fof(f160,plain,
( ! [X0] :
( apply(sK1,X0,sK6(sK1,sK5,X0))
| ~ member(X0,sK4) )
| ~ spl16_11 ),
inference(avatar_component_clause,[],[f159]) ).
fof(f161,plain,
( spl16_11
| ~ spl16_10 ),
inference(avatar_split_clause,[],[f155,f151,f159]) ).
fof(f166,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK4)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| sP15(X3,sK6(sK1,sK5,X0),sK1,X1,X2) )
| ~ spl16_11 ),
inference(resolution,[],[f160,f86]) ).
fof(f169,definition,
( spl16_12
<=> surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_12])],[avatar_definition]) ).
fof(f171,plain,
( surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5)
| ~ spl16_12 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f172,plain,
spl16_12,
inference(avatar_split_clause,[],[f56,f169]) ).
fof(f174,plain,
( ! [X0] :
( ~ member(X0,sK4)
| sP14(sK4,compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X0) )
| ~ spl16_6 ),
inference(resolution,[],[f126,f84]) ).
fof(f176,definition,
( spl16_13
<=> ! [X0] :
( ~ member(X0,sK4)
| sP14(sK4,compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_13])],[avatar_definition]) ).
fof(f177,plain,
( ! [X0] :
( sP14(sK4,compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X0)
| ~ member(X0,sK4) )
| ~ spl16_13 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f178,plain,
( spl16_13
| ~ spl16_6 ),
inference(avatar_split_clause,[],[f174,f124,f176]) ).
fof(f179,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK3)
| X1 = X2
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X1,X0)
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,X0)
| ~ member(X1,sK3)
| ~ member(X2,sK3) )
| ~ spl16_5 ),
inference(resolution,[],[f121,f85]) ).
fof(f180,plain,
( ! [X0] :
( apply(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)
| ~ member(X0,sK5) )
| ~ spl16_12 ),
inference(resolution,[],[f171,f78]) ).
fof(f181,plain,
( ! [X0] :
( member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) )
| ~ spl16_12 ),
inference(resolution,[],[f171,f79]) ).
fof(f188,definition,
( spl16_15
<=> ! [X0] :
( ~ member(X0,sK4)
| sP13(X0,sK5,sK1) ) ),
introduced(definition,[new_symbols(definition,[spl16_15])],[avatar_definition]) ).
fof(f189,plain,
( ! [X0] :
( sP13(X0,sK5,sK1)
| ~ member(X0,sK4) )
| ~ spl16_15 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f190,plain,
( spl16_15
| ~ spl16_10 ),
inference(avatar_split_clause,[],[f157,f151,f188]) ).
fof(f191,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK4)
| X1 = X2
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X1,X0)
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X2,X0)
| ~ member(X1,sK4)
| ~ member(X2,sK4) )
| ~ spl16_13 ),
inference(resolution,[],[f177,f85]) ).
fof(f194,definition,
( spl16_16
<=> ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_16])],[avatar_definition]) ).
fof(f195,plain,
( ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) )
| ~ spl16_16 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f196,plain,
( spl16_16
| ~ spl16_3 ),
inference(avatar_split_clause,[],[f107,f102,f194]) ).
fof(f198,definition,
( spl16_17
<=> ! [X0] :
( member(sK6(sK1,sK5,X0),sK5)
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_17])],[avatar_definition]) ).
fof(f199,plain,
( ! [X0] :
( member(sK6(sK1,sK5,X0),sK5)
| ~ member(X0,sK4) )
| ~ spl16_17 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f200,plain,
( spl16_17
| ~ spl16_10 ),
inference(avatar_split_clause,[],[f156,f151,f198]) ).
fof(f203,definition,
( spl16_18
<=> ! [X0] :
( member(sK6(sK0,sK4,X0),sK4)
| ~ member(X0,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_18])],[avatar_definition]) ).
fof(f204,plain,
( ! [X0] :
( member(sK6(sK0,sK4,X0),sK4)
| ~ member(X0,sK3) )
| ~ spl16_18 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f205,plain,
( spl16_18
| ~ spl16_7 ),
inference(avatar_split_clause,[],[f134,f129,f203]) ).
fof(f206,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK4)
| X1 = X2
| ~ apply(sK1,X0,X1)
| ~ apply(sK1,X0,X2)
| ~ member(X1,sK5)
| ~ member(X2,sK5) )
| ~ spl16_15 ),
inference(resolution,[],[f189,f83]) ).
fof(f208,definition,
( spl16_19
<=> ! [X0] :
( member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_19])],[avatar_definition]) ).
fof(f209,plain,
( ! [X0] :
( member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) )
| ~ spl16_19 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f210,plain,
( spl16_19
| ~ spl16_12 ),
inference(avatar_split_clause,[],[f181,f169,f208]) ).
fof(f260,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK4)
| member(sK12(X1,X2,sK6(sK1,sK5,X0)),X2)
| ~ surjective(X1,X2,sK5) )
| ~ spl16_17 ),
inference(resolution,[],[f199,f79]) ).
fof(f292,definition,
( spl16_20
<=> ! [X0] :
( apply(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)
| ~ member(X0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_20])],[avatar_definition]) ).
fof(f293,plain,
( ! [X0] :
( apply(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)
| ~ member(X0,sK5) )
| ~ spl16_20 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f294,plain,
( spl16_20
| ~ spl16_12 ),
inference(avatar_split_clause,[],[f180,f169,f292]) ).
fof(f295,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),X0)
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) )
| ~ spl16_20 ),
inference(resolution,[],[f293,f74]) ).
fof(f296,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(compose_function(sK0,sK2,sK5,sK3,sK4),sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0))
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) )
| ~ spl16_20 ),
inference(resolution,[],[f293,f75]) ).
fof(f297,plain,
( ! [X0] :
( ~ member(X0,sK5)
| member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4)
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) )
| ~ spl16_20 ),
inference(resolution,[],[f293,f76]) ).
fof(f305,plain,
( ! [X0] :
( ~ member(X0,sK5)
| member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4)
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5) )
| ~ spl16_20 ),
inference(duplicate_literal_removal,[],[f297]) ).
fof(f306,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(compose_function(sK0,sK2,sK5,sK3,sK4),sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0))
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5) )
| ~ spl16_20 ),
inference(duplicate_literal_removal,[],[f296]) ).
fof(f307,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),X0)
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5) )
| ~ spl16_20 ),
inference(duplicate_literal_removal,[],[f295]) ).
fof(f308,plain,
( ! [X0] :
( ~ member(X0,sK5)
| member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4) )
| ~ spl16_19
| ~ spl16_20 ),
inference(forward_subsumption_resolution,[],[f305,f209]) ).
fof(f309,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(compose_function(sK0,sK2,sK5,sK3,sK4),sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)) )
| ~ spl16_19
| ~ spl16_20 ),
inference(forward_subsumption_resolution,[],[f306,f209]) ).
fof(f310,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),X0) )
| ~ spl16_19
| ~ spl16_20 ),
inference(forward_subsumption_resolution,[],[f307,f209]) ).
fof(f312,definition,
( spl16_21
<=> ! [X0] :
( ~ member(X0,sK5)
| apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_21])],[avatar_definition]) ).
fof(f313,plain,
( ! [X0] :
( apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),X0)
| ~ member(X0,sK5) )
| ~ spl16_21 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f314,plain,
( spl16_21
| ~ spl16_19
| ~ spl16_20 ),
inference(avatar_split_clause,[],[f310,f292,f208,f312]) ).
fof(f323,definition,
( spl16_22
<=> ! [X0] :
( ~ member(X0,sK5)
| member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_22])],[avatar_definition]) ).
fof(f324,plain,
( ! [X0] :
( member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4)
| ~ member(X0,sK5) )
| ~ spl16_22 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f325,plain,
( spl16_22
| ~ spl16_19
| ~ spl16_20 ),
inference(avatar_split_clause,[],[f308,f292,f208,f323]) ).
fof(f360,definition,
( spl16_24
<=> ! [X2,X0,X1] :
( ~ member(X0,sK4)
| X1 = X2
| ~ apply(sK1,X0,X1)
| ~ apply(sK1,X0,X2)
| ~ member(X1,sK5)
| ~ member(X2,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_24])],[avatar_definition]) ).
fof(f361,plain,
( ! [X2,X0,X1] :
( ~ apply(sK1,X0,X2)
| X1 = X2
| ~ apply(sK1,X0,X1)
| ~ member(X0,sK4)
| ~ member(X1,sK5)
| ~ member(X2,sK5) )
| ~ spl16_24 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f362,plain,
( spl16_24
| ~ spl16_15 ),
inference(avatar_split_clause,[],[f206,f188,f360]) ).
fof(f364,plain,
( ! [X0,X1] :
( X0 = X1
| ~ apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X1),X1),X0)
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X1),X1),sK4)
| ~ member(X0,sK5)
| ~ member(X1,sK5)
| ~ member(X1,sK5) )
| ~ spl16_21
| ~ spl16_24 ),
inference(resolution,[],[f361,f313]) ).
fof(f371,plain,
( ! [X0,X1] :
( X0 = X1
| ~ apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X1),X1),X0)
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X1),X1),sK4)
| ~ member(X0,sK5)
| ~ member(X1,sK5) )
| ~ spl16_21
| ~ spl16_24 ),
inference(duplicate_literal_removal,[],[f364]) ).
fof(f373,plain,
( ! [X0,X1] :
( X0 = X1
| ~ apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X1),X1),X0)
| ~ member(X0,sK5)
| ~ member(X1,sK5) )
| ~ spl16_21
| ~ spl16_22
| ~ spl16_24 ),
inference(forward_subsumption_resolution,[],[f371,f324]) ).
fof(f389,definition,
( spl16_26
<=> ! [X0] :
( ~ member(X0,sK5)
| apply(compose_function(sK0,sK2,sK5,sK3,sK4),sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl16_26])],[avatar_definition]) ).
fof(f390,plain,
( ! [X0] :
( apply(compose_function(sK0,sK2,sK5,sK3,sK4),sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0))
| ~ member(X0,sK5) )
| ~ spl16_26 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f391,plain,
( spl16_26
| ~ spl16_19
| ~ spl16_20 ),
inference(avatar_split_clause,[],[f309,f292,f208,f389]) ).
fof(f392,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0))
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4) )
| ~ spl16_26 ),
inference(resolution,[],[f390,f74]) ).
fof(f393,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)))
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4) )
| ~ spl16_26 ),
inference(resolution,[],[f390,f75]) ).
fof(f394,plain,
( ! [X0] :
( ~ member(X0,sK5)
| member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK3)
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4) )
| ~ spl16_26 ),
inference(resolution,[],[f390,f76]) ).
fof(f401,plain,
( ! [X0] :
( ~ member(X0,sK5)
| member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK3)
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4) )
| ~ spl16_19
| ~ spl16_26 ),
inference(forward_subsumption_resolution,[],[f394,f209]) ).
fof(f402,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)))
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4) )
| ~ spl16_19
| ~ spl16_26 ),
inference(forward_subsumption_resolution,[],[f393,f209]) ).
fof(f403,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0))
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0),sK4) )
| ~ spl16_19
| ~ spl16_26 ),
inference(forward_subsumption_resolution,[],[f392,f209]) ).
fof(f404,plain,
( ! [X0] :
( ~ member(X0,sK5)
| member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK3) )
| ~ spl16_19
| ~ spl16_22
| ~ spl16_26 ),
inference(forward_subsumption_resolution,[],[f401,f324]) ).
fof(f405,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0))) )
| ~ spl16_19
| ~ spl16_22
| ~ spl16_26 ),
inference(forward_subsumption_resolution,[],[f402,f324]) ).
fof(f406,plain,
( ! [X0] :
( ~ member(X0,sK5)
| apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)) )
| ~ spl16_19
| ~ spl16_22
| ~ spl16_26 ),
inference(forward_subsumption_resolution,[],[f403,f324]) ).
fof(f408,definition,
( spl16_27
<=> ! [X0] :
( ~ member(X0,sK5)
| member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_27])],[avatar_definition]) ).
fof(f409,plain,
( ! [X0] :
( member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK3)
| ~ member(X0,sK5) )
| ~ spl16_27 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f410,plain,
( spl16_27
| ~ spl16_19
| ~ spl16_22
| ~ spl16_26 ),
inference(avatar_split_clause,[],[f404,f389,f323,f208,f408]) ).
fof(f432,definition,
( spl16_28
<=> ! [X0] :
( ~ member(X0,sK5)
| apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0))) ) ),
introduced(definition,[new_symbols(definition,[spl16_28])],[avatar_definition]) ).
fof(f433,plain,
( ! [X0] :
( apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)))
| ~ member(X0,sK5) )
| ~ spl16_28 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f434,plain,
( spl16_28
| ~ spl16_19
| ~ spl16_22
| ~ spl16_26 ),
inference(avatar_split_clause,[],[f405,f389,f323,f208,f432]) ).
fof(f457,definition,
( spl16_30
<=> ! [X0] :
( ~ member(X0,sK5)
| apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl16_30])],[avatar_definition]) ).
fof(f458,plain,
( ! [X0] :
( apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),X0))
| ~ member(X0,sK5) )
| ~ spl16_30 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f459,plain,
( spl16_30
| ~ spl16_19
| ~ spl16_22
| ~ spl16_26 ),
inference(avatar_split_clause,[],[f406,f389,f323,f208,f457]) ).
fof(f470,definition,
( spl16_31
<=> ! [X0,X3,X2,X1] :
( ~ member(X0,sK5)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| sP15(X3,sK6(sK2,sK3,X0),sK2,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_31])],[avatar_definition]) ).
fof(f471,plain,
( ! [X2,X3,X0,X1] :
( sP15(X3,sK6(sK2,sK3,X0),sK2,X1,X2)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| ~ member(X0,sK5) )
| ~ spl16_31 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f472,plain,
( spl16_31
| ~ spl16_4 ),
inference(avatar_split_clause,[],[f117,f110,f470]) ).
fof(f473,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| ~ member(X0,sK5)
| apply(compose_function(sK2,X2,X4,X1,X5),X3,sK6(sK2,sK3,X0))
| ~ member(X3,X4)
| ~ member(sK6(sK2,sK3,X0),X5) )
| ~ spl16_31 ),
inference(resolution,[],[f471,f87]) ).
fof(f648,definition,
( spl16_44
<=> ! [X2,X0,X1] :
( ~ member(X0,sK4)
| member(sK12(X1,X2,sK6(sK1,sK5,X0)),X2)
| ~ surjective(X1,X2,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_44])],[avatar_definition]) ).
fof(f649,plain,
( ! [X2,X0,X1] :
( member(sK12(X1,X2,sK6(sK1,sK5,X0)),X2)
| ~ member(X0,sK4)
| ~ surjective(X1,X2,sK5) )
| ~ spl16_44 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f650,plain,
( spl16_44
| ~ spl16_17 ),
inference(avatar_split_clause,[],[f260,f198,f648]) ).
fof(f674,definition,
( spl16_45
<=> ! [X0,X3,X2,X1] :
( ~ member(X0,sK3)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| sP15(X3,sK6(sK0,sK4,X0),sK0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_45])],[avatar_definition]) ).
fof(f675,plain,
( ! [X2,X3,X0,X1] :
( sP15(X3,sK6(sK0,sK4,X0),sK0,X1,X2)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| ~ member(X0,sK3) )
| ~ spl16_45 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f676,plain,
( spl16_45
| ~ spl16_8 ),
inference(avatar_split_clause,[],[f144,f137,f674]) ).
fof(f677,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| ~ member(X0,sK3)
| apply(compose_function(sK0,X2,X4,X1,X5),X3,sK6(sK0,sK4,X0))
| ~ member(X3,X4)
| ~ member(sK6(sK0,sK4,X0),X5) )
| ~ spl16_45 ),
inference(resolution,[],[f675,f87]) ).
fof(f681,definition,
( spl16_46
<=> ! [X0,X3,X2,X1] :
( ~ member(X0,sK4)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| sP15(X3,sK6(sK1,sK5,X0),sK1,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_46])],[avatar_definition]) ).
fof(f682,plain,
( ! [X2,X3,X0,X1] :
( sP15(X3,sK6(sK1,sK5,X0),sK1,X1,X2)
| ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| ~ member(X0,sK4) )
| ~ spl16_46 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f683,plain,
( spl16_46
| ~ spl16_11 ),
inference(avatar_split_clause,[],[f166,f159,f681]) ).
fof(f834,definition,
( spl16_61
<=> surjective(sK2,sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_61])],[avatar_definition]) ).
fof(f836,plain,
( ~ surjective(sK2,sK5,sK3)
| spl16_61 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f838,definition,
( spl16_62
<=> injective(sK2,sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_62])],[avatar_definition]) ).
fof(f840,plain,
( ~ injective(sK2,sK5,sK3)
| spl16_62 ),
inference(avatar_component_clause,[],[f838]) ).
fof(f841,plain,
( ~ spl16_61
| ~ spl16_62
| spl16_1 ),
inference(avatar_split_clause,[],[f93,f89,f838,f834]) ).
fof(f842,plain,
( member(sK11(sK2,sK5,sK3),sK3)
| spl16_61 ),
inference(resolution,[],[f836,f80]) ).
fof(f843,plain,
( ! [X0] :
( ~ member(X0,sK5)
| ~ apply(sK2,X0,sK11(sK2,sK5,sK3)) )
| spl16_61 ),
inference(resolution,[],[f836,f81]) ).
fof(f845,definition,
( spl16_63
<=> ! [X0] :
( ~ member(X0,sK5)
| ~ apply(sK2,X0,sK11(sK2,sK5,sK3)) ) ),
introduced(definition,[new_symbols(definition,[spl16_63])],[avatar_definition]) ).
fof(f846,plain,
( ! [X0] :
( ~ apply(sK2,X0,sK11(sK2,sK5,sK3))
| ~ member(X0,sK5) )
| ~ spl16_63 ),
inference(avatar_component_clause,[],[f845]) ).
fof(f847,plain,
( spl16_63
| spl16_61 ),
inference(avatar_split_clause,[],[f843,f834,f845]) ).
fof(f851,definition,
( spl16_64
<=> member(sK11(sK2,sK5,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl16_64])],[avatar_definition]) ).
fof(f853,plain,
( member(sK11(sK2,sK5,sK3),sK3)
| ~ spl16_64 ),
inference(avatar_component_clause,[],[f851]) ).
fof(f854,plain,
( spl16_64
| spl16_61 ),
inference(avatar_split_clause,[],[f842,f834,f851]) ).
fof(f1044,definition,
( spl16_75
<=> ! [X2,X0,X1] :
( ~ member(X0,sK3)
| X1 = X2
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X1,X0)
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,X0)
| ~ member(X1,sK3)
| ~ member(X2,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_75])],[avatar_definition]) ).
fof(f1045,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,X0)
| X1 = X2
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X1,X0)
| ~ member(X0,sK3)
| ~ member(X1,sK3)
| ~ member(X2,sK3) )
| ~ spl16_75 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1046,plain,
( spl16_75
| ~ spl16_5 ),
inference(avatar_split_clause,[],[f179,f120,f1044]) ).
fof(f1342,definition,
( spl16_93
<=> ! [X2,X0,X1] :
( ~ member(X0,sK4)
| X1 = X2
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X1,X0)
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X2,X0)
| ~ member(X1,sK4)
| ~ member(X2,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_93])],[avatar_definition]) ).
fof(f1343,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X2,X0)
| X1 = X2
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X1,X0)
| ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X2,sK4) )
| ~ spl16_93 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1344,plain,
( spl16_93
| ~ spl16_13 ),
inference(avatar_split_clause,[],[f191,f176,f1342]) ).
fof(f2446,definition,
( spl16_150
<=> ! [X5,X4,X0,X3,X2,X1] :
( ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| ~ member(X0,sK5)
| apply(compose_function(sK2,X2,X4,X1,X5),X3,sK6(sK2,sK3,X0))
| ~ member(X3,X4)
| ~ member(sK6(sK2,sK3,X0),X5) ) ),
introduced(definition,[new_symbols(definition,[spl16_150])],[avatar_definition]) ).
fof(f2447,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( apply(compose_function(sK2,X2,X4,X1,X5),X3,sK6(sK2,sK3,X0))
| ~ apply(X2,X3,X0)
| ~ member(X0,sK5)
| ~ member(X0,X1)
| ~ member(X3,X4)
| ~ member(sK6(sK2,sK3,X0),X5) )
| ~ spl16_150 ),
inference(avatar_component_clause,[],[f2446]) ).
fof(f2448,plain,
( spl16_150
| ~ spl16_31 ),
inference(avatar_split_clause,[],[f473,f470,f2446]) ).
fof(f2450,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X1)
| ~ member(X1,sK5)
| ~ member(X1,sK5)
| ~ member(X0,sK3)
| ~ member(sK6(sK2,sK3,X1),sK3)
| X0 = X2
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,sK6(sK2,sK3,X1))
| ~ member(sK6(sK2,sK3,X1),sK3)
| ~ member(X2,sK3)
| ~ member(X0,sK3) )
| ~ spl16_75
| ~ spl16_150 ),
inference(resolution,[],[f2447,f1045]) ).
fof(f2479,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X1)
| ~ member(X1,sK5)
| ~ member(X0,sK3)
| ~ member(sK6(sK2,sK3,X1),sK3)
| X0 = X2
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,sK6(sK2,sK3,X1))
| ~ member(X2,sK3) )
| ~ spl16_75
| ~ spl16_150 ),
inference(duplicate_literal_removal,[],[f2450]) ).
fof(f2482,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X1)
| ~ member(X1,sK5)
| ~ member(X0,sK3)
| X0 = X2
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,sK6(sK2,sK3,X1))
| ~ member(X2,sK3) )
| ~ spl16_16
| ~ spl16_75
| ~ spl16_150 ),
inference(forward_subsumption_resolution,[],[f2479,f195]) ).
fof(f2485,definition,
( spl16_151
<=> ! [X2,X0,X1] :
( ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X1)
| ~ member(X1,sK5)
| ~ member(X0,sK3)
| X0 = X2
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,sK6(sK2,sK3,X1))
| ~ member(X2,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_151])],[avatar_definition]) ).
fof(f2486,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,sK6(sK2,sK3,X1))
| ~ member(X1,sK5)
| ~ member(X0,sK3)
| X0 = X2
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X1)
| ~ member(X2,sK3) )
| ~ spl16_151 ),
inference(avatar_component_clause,[],[f2485]) ).
fof(f2487,plain,
( spl16_151
| ~ spl16_16
| ~ spl16_75
| ~ spl16_150 ),
inference(avatar_split_clause,[],[f2482,f2446,f1044,f194,f2485]) ).
fof(f2489,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK5)
| ~ member(X1,sK3)
| X1 = X2
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X1,X0)
| ~ member(X2,sK3)
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X2,X0)
| ~ member(X0,sK5)
| ~ member(X0,sK5)
| ~ member(X2,sK3)
| ~ member(sK6(sK2,sK3,X0),sK3) )
| ~ spl16_150
| ~ spl16_151 ),
inference(resolution,[],[f2486,f2447]) ).
fof(f2496,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK5)
| ~ member(X1,sK3)
| X1 = X2
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X1,X0)
| ~ member(X2,sK3)
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X2,X0)
| ~ member(sK6(sK2,sK3,X0),sK3) )
| ~ spl16_150
| ~ spl16_151 ),
inference(duplicate_literal_removal,[],[f2489]) ).
fof(f2498,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK5)
| ~ member(X1,sK3)
| X1 = X2
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X1,X0)
| ~ member(X2,sK3)
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X2,X0) )
| ~ spl16_16
| ~ spl16_150
| ~ spl16_151 ),
inference(forward_subsumption_resolution,[],[f2496,f195]) ).
fof(f2500,definition,
( spl16_152
<=> ! [X2,X0,X1] :
( ~ member(X0,sK5)
| ~ member(X1,sK3)
| X1 = X2
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X1,X0)
| ~ member(X2,sK3)
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_152])],[avatar_definition]) ).
fof(f2501,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X2,X0)
| ~ member(X1,sK3)
| X1 = X2
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X1,X0)
| ~ member(X2,sK3)
| ~ member(X0,sK5) )
| ~ spl16_152 ),
inference(avatar_component_clause,[],[f2500]) ).
fof(f2502,plain,
( spl16_152
| ~ spl16_16
| ~ spl16_150
| ~ spl16_151 ),
inference(avatar_split_clause,[],[f2498,f2485,f2446,f194,f2500]) ).
fof(f2503,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK3)
| X0 = X1
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X2)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| ~ sP15(X1,X2,sK1,sK4,sK0) )
| ~ spl16_152 ),
inference(resolution,[],[f2501,f87]) ).
fof(f2518,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK3)
| X0 = X1
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X2)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| ~ sP15(X1,X2,sK1,sK4,sK0) )
| ~ spl16_152 ),
inference(duplicate_literal_removal,[],[f2503]) ).
fof(f2523,definition,
( spl16_153
<=> ! [X2,X0,X1] :
( ~ member(X0,sK3)
| X0 = X1
| ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X2)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| ~ sP15(X1,X2,sK1,sK4,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl16_153])],[avatar_definition]) ).
fof(f2524,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK1,sK0,sK3,sK4,sK5),X0,X2)
| X0 = X1
| ~ member(X0,sK3)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| ~ sP15(X1,X2,sK1,sK4,sK0) )
| ~ spl16_153 ),
inference(avatar_component_clause,[],[f2523]) ).
fof(f2525,plain,
( spl16_153
| ~ spl16_152 ),
inference(avatar_split_clause,[],[f2518,f2500,f2523]) ).
fof(f2526,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X0,sK3)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| ~ sP15(X1,X2,sK1,sK4,sK0)
| ~ member(X0,sK3)
| ~ member(X2,sK5)
| ~ sP15(X0,X2,sK1,sK4,sK0) )
| ~ spl16_153 ),
inference(resolution,[],[f2524,f87]) ).
fof(f2541,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X0,sK3)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| ~ sP15(X1,X2,sK1,sK4,sK0)
| ~ sP15(X0,X2,sK1,sK4,sK0) )
| ~ spl16_153 ),
inference(duplicate_literal_removal,[],[f2526]) ).
fof(f2546,definition,
( spl16_154
<=> ! [X2,X0,X1] :
( X0 = X1
| ~ member(X0,sK3)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| ~ sP15(X1,X2,sK1,sK4,sK0)
| ~ sP15(X0,X2,sK1,sK4,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl16_154])],[avatar_definition]) ).
fof(f2547,plain,
( ! [X2,X0,X1] :
( ~ sP15(X1,X2,sK1,sK4,sK0)
| ~ member(X0,sK3)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| X0 = X1
| ~ sP15(X0,X2,sK1,sK4,sK0) )
| ~ spl16_154 ),
inference(avatar_component_clause,[],[f2546]) ).
fof(f2548,plain,
( spl16_154
| ~ spl16_153 ),
inference(avatar_split_clause,[],[f2541,f2523,f2546]) ).
fof(f2549,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK3)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| X0 = X1
| ~ sP15(X0,X2,sK1,sK4,sK0)
| ~ member(X3,sK4)
| ~ apply(sK0,X1,X3)
| ~ apply(sK1,X3,X2) )
| ~ spl16_154 ),
inference(resolution,[],[f2547,f86]) ).
fof(f2558,definition,
( spl16_155
<=> ! [X0,X3,X2,X1] :
( ~ member(X0,sK3)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| X0 = X1
| ~ sP15(X0,X2,sK1,sK4,sK0)
| ~ member(X3,sK4)
| ~ apply(sK0,X1,X3)
| ~ apply(sK1,X3,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_155])],[avatar_definition]) ).
fof(f2559,plain,
( ! [X2,X3,X0,X1] :
( ~ sP15(X0,X2,sK1,sK4,sK0)
| ~ member(X1,sK3)
| ~ member(X2,sK5)
| X0 = X1
| ~ member(X0,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X1,X3)
| ~ apply(sK1,X3,X2) )
| ~ spl16_155 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2560,plain,
( spl16_155
| ~ spl16_154 ),
inference(avatar_split_clause,[],[f2549,f2546,f2558]) ).
fof(f2562,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK3)
| ~ member(sK6(sK1,sK5,X1),sK5)
| X0 = X2
| ~ member(X2,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X0,X3)
| ~ apply(sK1,X3,sK6(sK1,sK5,X1))
| ~ member(X1,sK4)
| ~ apply(sK0,X2,X1)
| ~ member(X1,sK4) )
| ~ spl16_46
| ~ spl16_155 ),
inference(resolution,[],[f2559,f682]) ).
fof(f2565,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK3)
| ~ member(sK6(sK1,sK5,X1),sK5)
| X0 = X2
| ~ member(X2,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X0,X3)
| ~ apply(sK1,X3,sK6(sK1,sK5,X1))
| ~ member(X1,sK4)
| ~ apply(sK0,X2,X1) )
| ~ spl16_46
| ~ spl16_155 ),
inference(duplicate_literal_removal,[],[f2562]) ).
fof(f2567,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK3)
| X0 = X2
| ~ member(X2,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X0,X3)
| ~ apply(sK1,X3,sK6(sK1,sK5,X1))
| ~ member(X1,sK4)
| ~ apply(sK0,X2,X1) )
| ~ spl16_17
| ~ spl16_46
| ~ spl16_155 ),
inference(forward_subsumption_resolution,[],[f2565,f199]) ).
fof(f2598,definition,
( spl16_157
<=> ! [X0,X3,X2,X1] :
( ~ member(X0,sK3)
| X0 = X2
| ~ member(X2,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X0,X3)
| ~ apply(sK1,X3,sK6(sK1,sK5,X1))
| ~ member(X1,sK4)
| ~ apply(sK0,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl16_157])],[avatar_definition]) ).
fof(f2599,plain,
( ! [X2,X3,X0,X1] :
( ~ apply(sK1,X3,sK6(sK1,sK5,X1))
| X0 = X2
| ~ member(X2,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X0,X3)
| ~ member(X0,sK3)
| ~ member(X1,sK4)
| ~ apply(sK0,X2,X1) )
| ~ spl16_157 ),
inference(avatar_component_clause,[],[f2598]) ).
fof(f2600,plain,
( spl16_157
| ~ spl16_17
| ~ spl16_46
| ~ spl16_155 ),
inference(avatar_split_clause,[],[f2567,f2558,f681,f198,f2598]) ).
fof(f2602,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X2)),sK6(sK1,sK5,X2)),sK4)
| ~ apply(sK0,X0,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X2)),sK6(sK1,sK5,X2)))
| ~ member(X0,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X1,X2)
| ~ member(sK6(sK1,sK5,X2),sK5) )
| ~ spl16_21
| ~ spl16_157 ),
inference(resolution,[],[f2599,f313]) ).
fof(f2621,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ apply(sK0,X0,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X2)),sK6(sK1,sK5,X2)))
| ~ member(X0,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X1,X2)
| ~ member(sK6(sK1,sK5,X2),sK5) )
| ~ spl16_21
| ~ spl16_22
| ~ spl16_157 ),
inference(forward_subsumption_resolution,[],[f2602,f324]) ).
fof(f2622,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ apply(sK0,X0,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X2)),sK6(sK1,sK5,X2)))
| ~ member(X0,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X1,X2) )
| ~ spl16_17
| ~ spl16_21
| ~ spl16_22
| ~ spl16_157 ),
inference(forward_subsumption_resolution,[],[f2621,f199]) ).
fof(f2965,definition,
( spl16_178
<=> ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ apply(sK0,X0,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X2)),sK6(sK1,sK5,X2)))
| ~ member(X0,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_178])],[avatar_definition]) ).
fof(f2966,plain,
( ! [X2,X0,X1] :
( ~ apply(sK0,X0,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X2)),sK6(sK1,sK5,X2)))
| ~ member(X1,sK3)
| X0 = X1
| ~ member(X0,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X1,X2) )
| ~ spl16_178 ),
inference(avatar_component_clause,[],[f2965]) ).
fof(f2967,plain,
( spl16_178
| ~ spl16_17
| ~ spl16_21
| ~ spl16_22
| ~ spl16_157 ),
inference(avatar_split_clause,[],[f2622,f2598,f323,f312,f198,f2965]) ).
fof(f2968,plain,
( ! [X0,X1] :
( ~ member(X0,sK3)
| sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK6(sK1,sK5,X1))) = X0
| ~ member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK6(sK1,sK5,X1))),sK3)
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1)
| ~ member(sK6(sK1,sK5,X1),sK5) )
| ~ spl16_30
| ~ spl16_178 ),
inference(resolution,[],[f2966,f458]) ).
fof(f2977,plain,
( ! [X0,X1] :
( ~ member(X0,sK3)
| sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK6(sK1,sK5,X1))) = X0
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1)
| ~ member(sK6(sK1,sK5,X1),sK5) )
| ~ spl16_27
| ~ spl16_30
| ~ spl16_178 ),
inference(forward_subsumption_resolution,[],[f2968,f409]) ).
fof(f2978,plain,
( ! [X0,X1] :
( ~ member(X0,sK3)
| sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK6(sK1,sK5,X1))) = X0
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1) )
| ~ spl16_17
| ~ spl16_27
| ~ spl16_30
| ~ spl16_178 ),
inference(forward_subsumption_resolution,[],[f2977,f199]) ).
fof(f2980,definition,
( spl16_179
<=> ! [X0,X1] :
( ~ member(X0,sK3)
| sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK6(sK1,sK5,X1))) = X0
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl16_179])],[avatar_definition]) ).
fof(f2981,plain,
( ! [X0,X1] :
( sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),sK6(sK1,sK5,X1))) = X0
| ~ member(X0,sK3)
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1) )
| ~ spl16_179 ),
inference(avatar_component_clause,[],[f2980]) ).
fof(f2982,plain,
( spl16_179
| ~ spl16_17
| ~ spl16_27
| ~ spl16_30
| ~ spl16_178 ),
inference(avatar_split_clause,[],[f2978,f2965,f457,f408,f198,f2980]) ).
fof(f2987,plain,
( ! [X0,X1] :
( apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),X0)
| ~ member(sK6(sK1,sK5,X1),sK5)
| ~ member(X0,sK3)
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1) )
| ~ spl16_28
| ~ spl16_179 ),
inference(superposition,[],[f433,f2981]) ).
fof(f2994,plain,
( ! [X0,X1] :
( apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),X0)
| ~ member(X0,sK3)
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1) )
| ~ spl16_17
| ~ spl16_28
| ~ spl16_179 ),
inference(forward_subsumption_resolution,[],[f2987,f199]) ).
fof(f2998,definition,
( spl16_180
<=> ! [X0,X1] :
( apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),X0)
| ~ member(X0,sK3)
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl16_180])],[avatar_definition]) ).
fof(f2999,plain,
( ! [X0,X1] :
( apply(sK2,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X1)),X0)
| ~ member(X0,sK3)
| ~ member(X1,sK4)
| ~ apply(sK0,X0,X1) )
| ~ spl16_180 ),
inference(avatar_component_clause,[],[f2998]) ).
fof(f3000,plain,
( spl16_180
| ~ spl16_17
| ~ spl16_28
| ~ spl16_179 ),
inference(avatar_split_clause,[],[f2994,f2980,f432,f198,f2998]) ).
fof(f3003,plain,
( ! [X0] :
( ~ member(sK11(sK2,sK5,sK3),sK3)
| ~ member(X0,sK4)
| ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),sK5) )
| ~ spl16_63
| ~ spl16_180 ),
inference(resolution,[],[f2999,f846]) ).
fof(f3022,plain,
( ! [X0] :
( ~ member(X0,sK4)
| ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),sK5) )
| ~ spl16_63
| ~ spl16_64
| ~ spl16_180 ),
inference(forward_subsumption_resolution,[],[f3003,f853]) ).
fof(f3025,definition,
( spl16_181
<=> ! [X0] :
( ~ member(X0,sK4)
| ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_181])],[avatar_definition]) ).
fof(f3026,plain,
( ! [X0] :
( ~ member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),sK5)
| ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(X0,sK4) )
| ~ spl16_181 ),
inference(avatar_component_clause,[],[f3025]) ).
fof(f3027,plain,
( spl16_181
| ~ spl16_63
| ~ spl16_64
| ~ spl16_180 ),
inference(avatar_split_clause,[],[f3022,f2998,f851,f845,f3025]) ).
fof(f3029,plain,
( ! [X0] :
( ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(X0,sK4)
| ~ member(X0,sK4)
| ~ surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5) )
| ~ spl16_44
| ~ spl16_181 ),
inference(resolution,[],[f3026,f649]) ).
fof(f3038,plain,
( ! [X0] :
( ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(X0,sK4)
| ~ surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5) )
| ~ spl16_44
| ~ spl16_181 ),
inference(duplicate_literal_removal,[],[f3029]) ).
fof(f3043,plain,
( ! [X0] :
( ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(X0,sK4) )
| ~ spl16_12
| ~ spl16_44
| ~ spl16_181 ),
inference(forward_subsumption_resolution,[],[f3038,f171]) ).
fof(f3047,definition,
( spl16_182
<=> ! [X0] :
( ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_182])],[avatar_definition]) ).
fof(f3048,plain,
( ! [X0] :
( ~ apply(sK0,sK11(sK2,sK5,sK3),X0)
| ~ member(X0,sK4) )
| ~ spl16_182 ),
inference(avatar_component_clause,[],[f3047]) ).
fof(f3049,plain,
( spl16_182
| ~ spl16_12
| ~ spl16_44
| ~ spl16_181 ),
inference(avatar_split_clause,[],[f3043,f3025,f648,f169,f3047]) ).
fof(f3050,plain,
( ~ member(sK6(sK0,sK4,sK11(sK2,sK5,sK3)),sK4)
| ~ member(sK11(sK2,sK5,sK3),sK3)
| ~ spl16_8
| ~ spl16_182 ),
inference(resolution,[],[f3048,f138]) ).
fof(f3054,plain,
( ~ member(sK11(sK2,sK5,sK3),sK3)
| ~ spl16_8
| ~ spl16_18
| ~ spl16_182 ),
inference(forward_subsumption_resolution,[],[f3050,f204]) ).
fof(f3055,plain,
( $false
| ~ spl16_8
| ~ spl16_18
| ~ spl16_64
| ~ spl16_182 ),
inference(forward_subsumption_resolution,[],[f3054,f853]) ).
fof(f3056,plain,
( ~ spl16_8
| ~ spl16_18
| ~ spl16_64
| ~ spl16_182 ),
inference(avatar_contradiction_clause,[],[f3055]) ).
fof(f3064,plain,
( member(sK9(sK2,sK5,sK3),sK3)
| spl16_62 ),
inference(resolution,[],[f840,f68]) ).
fof(f3065,plain,
( member(sK8(sK2,sK5,sK3),sK5)
| spl16_62 ),
inference(resolution,[],[f840,f69]) ).
fof(f3066,plain,
( member(sK7(sK2,sK5,sK3),sK5)
| spl16_62 ),
inference(resolution,[],[f840,f70]) ).
fof(f3067,plain,
( apply(sK2,sK8(sK2,sK5,sK3),sK9(sK2,sK5,sK3))
| spl16_62 ),
inference(resolution,[],[f840,f71]) ).
fof(f3068,plain,
( apply(sK2,sK7(sK2,sK5,sK3),sK9(sK2,sK5,sK3))
| spl16_62 ),
inference(resolution,[],[f840,f72]) ).
fof(f3069,plain,
( sK8(sK2,sK5,sK3) != sK7(sK2,sK5,sK3)
| spl16_62 ),
inference(resolution,[],[f840,f73]) ).
fof(f3071,definition,
( spl16_183
<=> apply(sK2,sK8(sK2,sK5,sK3),sK9(sK2,sK5,sK3)) ),
introduced(definition,[new_symbols(definition,[spl16_183])],[avatar_definition]) ).
fof(f3073,plain,
( apply(sK2,sK8(sK2,sK5,sK3),sK9(sK2,sK5,sK3))
| ~ spl16_183 ),
inference(avatar_component_clause,[],[f3071]) ).
fof(f3074,plain,
( spl16_183
| spl16_62 ),
inference(avatar_split_clause,[],[f3067,f838,f3071]) ).
fof(f3085,definition,
( spl16_184
<=> apply(sK2,sK7(sK2,sK5,sK3),sK9(sK2,sK5,sK3)) ),
introduced(definition,[new_symbols(definition,[spl16_184])],[avatar_definition]) ).
fof(f3087,plain,
( apply(sK2,sK7(sK2,sK5,sK3),sK9(sK2,sK5,sK3))
| ~ spl16_184 ),
inference(avatar_component_clause,[],[f3085]) ).
fof(f3088,plain,
( spl16_184
| spl16_62 ),
inference(avatar_split_clause,[],[f3068,f838,f3085]) ).
fof(f3099,definition,
( spl16_185
<=> member(sK8(sK2,sK5,sK3),sK5) ),
introduced(definition,[new_symbols(definition,[spl16_185])],[avatar_definition]) ).
fof(f3101,plain,
( member(sK8(sK2,sK5,sK3),sK5)
| ~ spl16_185 ),
inference(avatar_component_clause,[],[f3099]) ).
fof(f3102,plain,
( spl16_185
| spl16_62 ),
inference(avatar_split_clause,[],[f3065,f838,f3099]) ).
fof(f3104,definition,
( spl16_186
<=> member(sK7(sK2,sK5,sK3),sK5) ),
introduced(definition,[new_symbols(definition,[spl16_186])],[avatar_definition]) ).
fof(f3106,plain,
( member(sK7(sK2,sK5,sK3),sK5)
| ~ spl16_186 ),
inference(avatar_component_clause,[],[f3104]) ).
fof(f3107,plain,
( spl16_186
| spl16_62 ),
inference(avatar_split_clause,[],[f3066,f838,f3104]) ).
fof(f3129,definition,
( spl16_187
<=> sK8(sK2,sK5,sK3) = sK7(sK2,sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_187])],[avatar_definition]) ).
fof(f3131,plain,
( sK8(sK2,sK5,sK3) != sK7(sK2,sK5,sK3)
| spl16_187 ),
inference(avatar_component_clause,[],[f3129]) ).
fof(f3132,plain,
( ~ spl16_187
| spl16_62 ),
inference(avatar_split_clause,[],[f3069,f838,f3129]) ).
fof(f3177,definition,
( spl16_190
<=> member(sK9(sK2,sK5,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl16_190])],[avatar_definition]) ).
fof(f3179,plain,
( member(sK9(sK2,sK5,sK3),sK3)
| ~ spl16_190 ),
inference(avatar_component_clause,[],[f3177]) ).
fof(f3180,plain,
( spl16_190
| spl16_62 ),
inference(avatar_split_clause,[],[f3064,f838,f3177]) ).
fof(f6196,definition,
( spl16_314
<=> ! [X0,X1] :
( X0 = X1
| ~ apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X1),X1),X0)
| ~ member(X0,sK5)
| ~ member(X1,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_314])],[avatar_definition]) ).
fof(f6197,plain,
( ! [X0,X1] :
( ~ apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X1),X1),X0)
| X0 = X1
| ~ member(X0,sK5)
| ~ member(X1,sK5) )
| ~ spl16_314 ),
inference(avatar_component_clause,[],[f6196]) ).
fof(f6198,plain,
( spl16_314
| ~ spl16_21
| ~ spl16_22
| ~ spl16_24 ),
inference(avatar_split_clause,[],[f373,f360,f323,f312,f6196]) ).
fof(f10067,definition,
( spl16_444
<=> ! [X5,X4,X0,X3,X2,X1] :
( ~ member(X0,X1)
| ~ apply(X2,X3,X0)
| ~ member(X0,sK3)
| apply(compose_function(sK0,X2,X4,X1,X5),X3,sK6(sK0,sK4,X0))
| ~ member(X3,X4)
| ~ member(sK6(sK0,sK4,X0),X5) ) ),
introduced(definition,[new_symbols(definition,[spl16_444])],[avatar_definition]) ).
fof(f10068,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( apply(compose_function(sK0,X2,X4,X1,X5),X3,sK6(sK0,sK4,X0))
| ~ apply(X2,X3,X0)
| ~ member(X0,sK3)
| ~ member(X0,X1)
| ~ member(X3,X4)
| ~ member(sK6(sK0,sK4,X0),X5) )
| ~ spl16_444 ),
inference(avatar_component_clause,[],[f10067]) ).
fof(f10069,plain,
( spl16_444
| ~ spl16_45 ),
inference(avatar_split_clause,[],[f677,f674,f10067]) ).
fof(f10071,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X1)
| ~ member(X1,sK3)
| ~ member(X1,sK3)
| ~ member(X0,sK4)
| ~ member(sK6(sK0,sK4,X1),sK4)
| X0 = X2
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X2,sK6(sK0,sK4,X1))
| ~ member(sK6(sK0,sK4,X1),sK4)
| ~ member(X2,sK4)
| ~ member(X0,sK4) )
| ~ spl16_93
| ~ spl16_444 ),
inference(resolution,[],[f10068,f1343]) ).
fof(f10109,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X1)
| ~ member(X1,sK3)
| ~ member(X0,sK4)
| ~ member(sK6(sK0,sK4,X1),sK4)
| X0 = X2
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X2,sK6(sK0,sK4,X1))
| ~ member(X2,sK4) )
| ~ spl16_93
| ~ spl16_444 ),
inference(duplicate_literal_removal,[],[f10071]) ).
fof(f10116,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X1)
| ~ member(X1,sK3)
| ~ member(X0,sK4)
| X0 = X2
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X2,sK6(sK0,sK4,X1))
| ~ member(X2,sK4) )
| ~ spl16_18
| ~ spl16_93
| ~ spl16_444 ),
inference(forward_subsumption_resolution,[],[f10109,f204]) ).
fof(f10119,definition,
( spl16_445
<=> ! [X2,X0,X1] :
( ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X1)
| ~ member(X1,sK3)
| ~ member(X0,sK4)
| X0 = X2
| ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X2,sK6(sK0,sK4,X1))
| ~ member(X2,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_445])],[avatar_definition]) ).
fof(f10120,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X2,sK6(sK0,sK4,X1))
| ~ member(X1,sK3)
| ~ member(X0,sK4)
| X0 = X2
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X1)
| ~ member(X2,sK4) )
| ~ spl16_445 ),
inference(avatar_component_clause,[],[f10119]) ).
fof(f10121,plain,
( spl16_445
| ~ spl16_18
| ~ spl16_93
| ~ spl16_444 ),
inference(avatar_split_clause,[],[f10116,f10067,f1342,f203,f10119]) ).
fof(f10122,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK3)
| ~ member(X1,sK4)
| X1 = X2
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X1,X0)
| ~ member(X2,sK4)
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X2,X0)
| ~ member(X0,sK3)
| ~ member(X0,sK3)
| ~ member(X2,sK4)
| ~ member(sK6(sK0,sK4,X0),sK4) )
| ~ spl16_444
| ~ spl16_445 ),
inference(resolution,[],[f10120,f10068]) ).
fof(f10136,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK3)
| ~ member(X1,sK4)
| X1 = X2
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X1,X0)
| ~ member(X2,sK4)
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X2,X0)
| ~ member(sK6(sK0,sK4,X0),sK4) )
| ~ spl16_444
| ~ spl16_445 ),
inference(duplicate_literal_removal,[],[f10122]) ).
fof(f10139,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK3)
| ~ member(X1,sK4)
| X1 = X2
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X1,X0)
| ~ member(X2,sK4)
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X2,X0) )
| ~ spl16_18
| ~ spl16_444
| ~ spl16_445 ),
inference(forward_subsumption_resolution,[],[f10136,f204]) ).
fof(f10142,definition,
( spl16_446
<=> ! [X2,X0,X1] :
( ~ member(X0,sK3)
| ~ member(X1,sK4)
| X1 = X2
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X1,X0)
| ~ member(X2,sK4)
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_446])],[avatar_definition]) ).
fof(f10143,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X2,X0)
| ~ member(X1,sK4)
| X1 = X2
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X1,X0)
| ~ member(X2,sK4)
| ~ member(X0,sK3) )
| ~ spl16_446 ),
inference(avatar_component_clause,[],[f10142]) ).
fof(f10144,plain,
( spl16_446
| ~ spl16_18
| ~ spl16_444
| ~ spl16_445 ),
inference(avatar_split_clause,[],[f10139,f10119,f10067,f203,f10142]) ).
fof(f10147,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK4)
| X0 = X1
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X2)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| ~ sP15(X1,X2,sK2,sK5,sK1) )
| ~ spl16_446 ),
inference(resolution,[],[f10143,f87]) ).
fof(f10175,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK4)
| X0 = X1
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X2)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| ~ sP15(X1,X2,sK2,sK5,sK1) )
| ~ spl16_446 ),
inference(duplicate_literal_removal,[],[f10147]) ).
fof(f10185,definition,
( spl16_447
<=> ! [X2,X0,X1] :
( ~ member(X0,sK4)
| X0 = X1
| ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X2)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| ~ sP15(X1,X2,sK2,sK5,sK1) ) ),
introduced(definition,[new_symbols(definition,[spl16_447])],[avatar_definition]) ).
fof(f10186,plain,
( ! [X2,X0,X1] :
( ~ apply(compose_function(sK2,sK1,sK4,sK5,sK3),X0,X2)
| X0 = X1
| ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| ~ sP15(X1,X2,sK2,sK5,sK1) )
| ~ spl16_447 ),
inference(avatar_component_clause,[],[f10185]) ).
fof(f10187,plain,
( spl16_447
| ~ spl16_446 ),
inference(avatar_split_clause,[],[f10175,f10142,f10185]) ).
fof(f10190,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| ~ sP15(X1,X2,sK2,sK5,sK1)
| ~ member(X0,sK4)
| ~ member(X2,sK3)
| ~ sP15(X0,X2,sK2,sK5,sK1) )
| ~ spl16_447 ),
inference(resolution,[],[f10186,f87]) ).
fof(f10218,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| ~ sP15(X1,X2,sK2,sK5,sK1)
| ~ sP15(X0,X2,sK2,sK5,sK1) )
| ~ spl16_447 ),
inference(duplicate_literal_removal,[],[f10190]) ).
fof(f10287,definition,
( spl16_449
<=> ! [X2,X0,X1] :
( X0 = X1
| ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| ~ sP15(X1,X2,sK2,sK5,sK1)
| ~ sP15(X0,X2,sK2,sK5,sK1) ) ),
introduced(definition,[new_symbols(definition,[spl16_449])],[avatar_definition]) ).
fof(f10288,plain,
( ! [X2,X0,X1] :
( ~ sP15(X1,X2,sK2,sK5,sK1)
| ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| X0 = X1
| ~ sP15(X0,X2,sK2,sK5,sK1) )
| ~ spl16_449 ),
inference(avatar_component_clause,[],[f10287]) ).
fof(f10289,plain,
( spl16_449
| ~ spl16_447 ),
inference(avatar_split_clause,[],[f10218,f10185,f10287]) ).
fof(f10290,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| X0 = X1
| ~ sP15(X0,X2,sK2,sK5,sK1)
| ~ member(X3,sK5)
| ~ apply(sK1,X1,X3)
| ~ apply(sK2,X3,X2) )
| ~ spl16_449 ),
inference(resolution,[],[f10288,f86]) ).
fof(f10299,definition,
( spl16_450
<=> ! [X0,X3,X2,X1] :
( ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| X0 = X1
| ~ sP15(X0,X2,sK2,sK5,sK1)
| ~ member(X3,sK5)
| ~ apply(sK1,X1,X3)
| ~ apply(sK2,X3,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_450])],[avatar_definition]) ).
fof(f10300,plain,
( ! [X2,X3,X0,X1] :
( ~ sP15(X0,X2,sK2,sK5,sK1)
| ~ member(X1,sK4)
| ~ member(X2,sK3)
| X0 = X1
| ~ member(X0,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X1,X3)
| ~ apply(sK2,X3,X2) )
| ~ spl16_450 ),
inference(avatar_component_clause,[],[f10299]) ).
fof(f10301,plain,
( spl16_450
| ~ spl16_449 ),
inference(avatar_split_clause,[],[f10290,f10287,f10299]) ).
fof(f10302,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ member(X0,sK4)
| ~ member(X1,sK3)
| X0 = X2
| ~ member(X2,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X0,X3)
| ~ apply(sK2,X3,X1)
| ~ member(X4,sK5)
| ~ apply(sK1,X2,X4)
| ~ apply(sK2,X4,X1) )
| ~ spl16_450 ),
inference(resolution,[],[f10300,f86]) ).
fof(f10312,definition,
( spl16_451
<=> ! [X4,X0,X3,X2,X1] :
( ~ member(X0,sK4)
| ~ member(X1,sK3)
| X0 = X2
| ~ member(X2,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X0,X3)
| ~ apply(sK2,X3,X1)
| ~ member(X4,sK5)
| ~ apply(sK1,X2,X4)
| ~ apply(sK2,X4,X1) ) ),
introduced(definition,[new_symbols(definition,[spl16_451])],[avatar_definition]) ).
fof(f10313,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ apply(sK2,X4,X1)
| ~ member(X1,sK3)
| X0 = X2
| ~ member(X2,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X0,X3)
| ~ apply(sK2,X3,X1)
| ~ member(X4,sK5)
| ~ apply(sK1,X2,X4)
| ~ member(X0,sK4) )
| ~ spl16_451 ),
inference(avatar_component_clause,[],[f10312]) ).
fof(f10314,plain,
( spl16_451
| ~ spl16_450 ),
inference(avatar_split_clause,[],[f10302,f10299,f10312]) ).
fof(f10318,plain,
( ! [X2,X0,X1] :
( ~ member(sK9(sK2,sK5,sK3),sK3)
| X0 = X1
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| ~ apply(sK2,X2,sK9(sK2,sK5,sK3))
| ~ member(sK8(sK2,sK5,sK3),sK5)
| ~ apply(sK1,X1,sK8(sK2,sK5,sK3))
| ~ member(X0,sK4) )
| ~ spl16_183
| ~ spl16_451 ),
inference(resolution,[],[f10313,f3073]) ).
fof(f10375,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| ~ apply(sK2,X2,sK9(sK2,sK5,sK3))
| ~ member(sK8(sK2,sK5,sK3),sK5)
| ~ apply(sK1,X1,sK8(sK2,sK5,sK3))
| ~ member(X0,sK4) )
| ~ spl16_183
| ~ spl16_190
| ~ spl16_451 ),
inference(forward_subsumption_resolution,[],[f10318,f3179]) ).
fof(f10383,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| ~ apply(sK2,X2,sK9(sK2,sK5,sK3))
| ~ apply(sK1,X1,sK8(sK2,sK5,sK3))
| ~ member(X0,sK4) )
| ~ spl16_183
| ~ spl16_185
| ~ spl16_190
| ~ spl16_451 ),
inference(forward_subsumption_resolution,[],[f10375,f3101]) ).
fof(f10613,definition,
( spl16_459
<=> ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| ~ apply(sK2,X2,sK9(sK2,sK5,sK3))
| ~ apply(sK1,X1,sK8(sK2,sK5,sK3))
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_459])],[avatar_definition]) ).
fof(f10614,plain,
( ! [X2,X0,X1] :
( ~ apply(sK2,X2,sK9(sK2,sK5,sK3))
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| X0 = X1
| ~ apply(sK1,X1,sK8(sK2,sK5,sK3))
| ~ member(X0,sK4) )
| ~ spl16_459 ),
inference(avatar_component_clause,[],[f10613]) ).
fof(f10615,plain,
( spl16_459
| ~ spl16_183
| ~ spl16_185
| ~ spl16_190
| ~ spl16_451 ),
inference(avatar_split_clause,[],[f10383,f10312,f3177,f3099,f3071,f10613]) ).
fof(f10616,plain,
( ! [X0,X1] :
( ~ member(X0,sK4)
| ~ member(sK7(sK2,sK5,sK3),sK5)
| ~ apply(sK1,X1,sK7(sK2,sK5,sK3))
| X0 = X1
| ~ apply(sK1,X0,sK8(sK2,sK5,sK3))
| ~ member(X1,sK4) )
| ~ spl16_184
| ~ spl16_459 ),
inference(resolution,[],[f10614,f3087]) ).
fof(f11875,definition,
( spl16_506
<=> ! [X0,X1] :
( ~ apply(sK1,X0,sK7(sK2,sK5,sK3))
| ~ member(X1,sK4)
| X0 = X1
| ~ member(X0,sK4)
| ~ apply(sK1,X1,sK8(sK2,sK5,sK3)) ) ),
introduced(definition,[new_symbols(definition,[spl16_506])],[avatar_definition]) ).
fof(f11876,plain,
( ! [X0,X1] :
( ~ apply(sK1,X1,sK8(sK2,sK5,sK3))
| ~ member(X1,sK4)
| X0 = X1
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3)) )
| ~ spl16_506 ),
inference(avatar_component_clause,[],[f11875]) ).
fof(f11878,plain,
( ! [X0] :
( ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK8(sK2,sK5,sK3)),sK8(sK2,sK5,sK3)),sK4)
| sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK8(sK2,sK5,sK3)),sK8(sK2,sK5,sK3)) = X0
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3))
| ~ member(sK8(sK2,sK5,sK3),sK5) )
| ~ spl16_21
| ~ spl16_506 ),
inference(resolution,[],[f11876,f313]) ).
fof(f11884,plain,
( ! [X0] :
( sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK8(sK2,sK5,sK3)),sK8(sK2,sK5,sK3)) = X0
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3))
| ~ member(sK8(sK2,sK5,sK3),sK5) )
| ~ spl16_21
| ~ spl16_22
| ~ spl16_506 ),
inference(forward_subsumption_resolution,[],[f11878,f324]) ).
fof(f11886,plain,
( ! [X0] :
( sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK8(sK2,sK5,sK3)),sK8(sK2,sK5,sK3)) = X0
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3)) )
| ~ spl16_21
| ~ spl16_22
| ~ spl16_185
| ~ spl16_506 ),
inference(forward_subsumption_resolution,[],[f11884,f3101]) ).
fof(f11888,definition,
( spl16_507
<=> ! [X0] :
( sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK8(sK2,sK5,sK3)),sK8(sK2,sK5,sK3)) = X0
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3)) ) ),
introduced(definition,[new_symbols(definition,[spl16_507])],[avatar_definition]) ).
fof(f11889,plain,
( ! [X0] :
( sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK8(sK2,sK5,sK3)),sK8(sK2,sK5,sK3)) = X0
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3)) )
| ~ spl16_507 ),
inference(avatar_component_clause,[],[f11888]) ).
fof(f11890,plain,
( spl16_507
| ~ spl16_21
| ~ spl16_22
| ~ spl16_185
| ~ spl16_506 ),
inference(avatar_split_clause,[],[f11886,f11875,f3099,f323,f312,f11888]) ).
fof(f11894,plain,
( ! [X0] :
( apply(sK1,X0,sK8(sK2,sK5,sK3))
| ~ member(sK8(sK2,sK5,sK3),sK5)
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3)) )
| ~ spl16_21
| ~ spl16_507 ),
inference(superposition,[],[f313,f11889]) ).
fof(f11916,plain,
( ! [X0] :
( apply(sK1,X0,sK8(sK2,sK5,sK3))
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3)) )
| ~ spl16_21
| ~ spl16_185
| ~ spl16_507 ),
inference(forward_subsumption_resolution,[],[f11894,f3101]) ).
fof(f11919,definition,
( spl16_508
<=> ! [X0] :
( apply(sK1,X0,sK8(sK2,sK5,sK3))
| ~ member(X0,sK4)
| ~ apply(sK1,X0,sK7(sK2,sK5,sK3)) ) ),
introduced(definition,[new_symbols(definition,[spl16_508])],[avatar_definition]) ).
fof(f11920,plain,
( ! [X0] :
( ~ apply(sK1,X0,sK7(sK2,sK5,sK3))
| ~ member(X0,sK4)
| apply(sK1,X0,sK8(sK2,sK5,sK3)) )
| ~ spl16_508 ),
inference(avatar_component_clause,[],[f11919]) ).
fof(f11921,plain,
( spl16_508
| ~ spl16_21
| ~ spl16_185
| ~ spl16_507 ),
inference(avatar_split_clause,[],[f11916,f11888,f3099,f312,f11919]) ).
fof(f11922,plain,
( ~ member(sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK7(sK2,sK5,sK3)),sK7(sK2,sK5,sK3)),sK4)
| apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK7(sK2,sK5,sK3)),sK7(sK2,sK5,sK3)),sK8(sK2,sK5,sK3))
| ~ member(sK7(sK2,sK5,sK3),sK5)
| ~ spl16_21
| ~ spl16_508 ),
inference(resolution,[],[f11920,f313]) ).
fof(f11928,plain,
( apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK7(sK2,sK5,sK3)),sK7(sK2,sK5,sK3)),sK8(sK2,sK5,sK3))
| ~ member(sK7(sK2,sK5,sK3),sK5)
| ~ spl16_21
| ~ spl16_22
| ~ spl16_508 ),
inference(forward_subsumption_resolution,[],[f11922,f324]) ).
fof(f11930,plain,
( apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK7(sK2,sK5,sK3)),sK7(sK2,sK5,sK3)),sK8(sK2,sK5,sK3))
| ~ spl16_21
| ~ spl16_22
| ~ spl16_186
| ~ spl16_508 ),
inference(forward_subsumption_resolution,[],[f11928,f3106]) ).
fof(f11932,definition,
( spl16_509
<=> apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK7(sK2,sK5,sK3)),sK7(sK2,sK5,sK3)),sK8(sK2,sK5,sK3)) ),
introduced(definition,[new_symbols(definition,[spl16_509])],[avatar_definition]) ).
fof(f11934,plain,
( apply(sK1,sK10(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK4,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK7(sK2,sK5,sK3)),sK7(sK2,sK5,sK3)),sK8(sK2,sK5,sK3))
| ~ spl16_509 ),
inference(avatar_component_clause,[],[f11932]) ).
fof(f11935,plain,
( spl16_509
| ~ spl16_21
| ~ spl16_22
| ~ spl16_186
| ~ spl16_508 ),
inference(avatar_split_clause,[],[f11930,f11919,f3104,f323,f312,f11932]) ).
fof(f11936,plain,
( sK8(sK2,sK5,sK3) = sK7(sK2,sK5,sK3)
| ~ member(sK8(sK2,sK5,sK3),sK5)
| ~ member(sK7(sK2,sK5,sK3),sK5)
| ~ spl16_314
| ~ spl16_509 ),
inference(resolution,[],[f11934,f6197]) ).
fof(f11954,plain,
( ~ member(sK8(sK2,sK5,sK3),sK5)
| ~ member(sK7(sK2,sK5,sK3),sK5)
| spl16_187
| ~ spl16_314
| ~ spl16_509 ),
inference(forward_subsumption_resolution,[],[f11936,f3131]) ).
fof(f11955,plain,
( ~ member(sK7(sK2,sK5,sK3),sK5)
| ~ spl16_185
| spl16_187
| ~ spl16_314
| ~ spl16_509 ),
inference(forward_subsumption_resolution,[],[f11954,f3101]) ).
fof(f11956,plain,
( $false
| ~ spl16_185
| ~ spl16_186
| spl16_187
| ~ spl16_314
| ~ spl16_509 ),
inference(forward_subsumption_resolution,[],[f11955,f3106]) ).
fof(f11957,plain,
( ~ spl16_185
| ~ spl16_186
| spl16_187
| ~ spl16_314
| ~ spl16_509 ),
inference(avatar_contradiction_clause,[],[f11956]) ).
fof(f11963,plain,
( ! [X0,X1] :
( ~ member(X0,sK4)
| ~ apply(sK1,X1,sK7(sK2,sK5,sK3))
| X0 = X1
| ~ apply(sK1,X0,sK8(sK2,sK5,sK3))
| ~ member(X1,sK4) )
| ~ spl16_184
| ~ spl16_186
| ~ spl16_459 ),
inference(forward_subsumption_resolution,[],[f10616,f3106]) ).
fof(f11967,plain,
( spl16_506
| ~ spl16_184
| ~ spl16_186
| ~ spl16_459 ),
inference(avatar_split_clause,[],[f11963,f10613,f3104,f3085,f11875]) ).
cnf(s1,plain,
~ spl16_1,
inference(sat_conversion,[],[f92]) ).
cnf(s2,plain,
spl16_2,
inference(sat_conversion,[],[f98]) ).
cnf(s3,plain,
spl16_3,
inference(sat_conversion,[],[f105]) ).
cnf(s4,plain,
( ~ spl16_3
| spl16_4 ),
inference(sat_conversion,[],[f112]) ).
cnf(s5,plain,
( ~ spl16_2
| spl16_5 ),
inference(sat_conversion,[],[f122]) ).
cnf(s6,plain,
spl16_6,
inference(sat_conversion,[],[f127]) ).
cnf(s7,plain,
spl16_7,
inference(sat_conversion,[],[f132]) ).
cnf(s8,plain,
( ~ spl16_7
| spl16_8 ),
inference(sat_conversion,[],[f139]) ).
cnf(s10,plain,
spl16_10,
inference(sat_conversion,[],[f154]) ).
cnf(s11,plain,
( ~ spl16_10
| spl16_11 ),
inference(sat_conversion,[],[f161]) ).
cnf(s12,plain,
spl16_12,
inference(sat_conversion,[],[f172]) ).
cnf(s13,plain,
( ~ spl16_6
| spl16_13 ),
inference(sat_conversion,[],[f178]) ).
cnf(s15,plain,
( ~ spl16_10
| spl16_15 ),
inference(sat_conversion,[],[f190]) ).
cnf(s16,plain,
( ~ spl16_3
| spl16_16 ),
inference(sat_conversion,[],[f196]) ).
cnf(s17,plain,
( ~ spl16_10
| spl16_17 ),
inference(sat_conversion,[],[f200]) ).
cnf(s18,plain,
( ~ spl16_7
| spl16_18 ),
inference(sat_conversion,[],[f205]) ).
cnf(s19,plain,
( ~ spl16_12
| spl16_19 ),
inference(sat_conversion,[],[f210]) ).
cnf(s20,plain,
( ~ spl16_12
| spl16_20 ),
inference(sat_conversion,[],[f294]) ).
cnf(s21,plain,
( ~ spl16_19
| ~ spl16_20
| spl16_21 ),
inference(sat_conversion,[],[f314]) ).
cnf(s22,plain,
( ~ spl16_19
| ~ spl16_20
| spl16_22 ),
inference(sat_conversion,[],[f325]) ).
cnf(s24,plain,
( ~ spl16_15
| spl16_24 ),
inference(sat_conversion,[],[f362]) ).
cnf(s26,plain,
( ~ spl16_19
| ~ spl16_20
| spl16_26 ),
inference(sat_conversion,[],[f391]) ).
cnf(s27,plain,
( ~ spl16_19
| ~ spl16_22
| ~ spl16_26
| spl16_27 ),
inference(sat_conversion,[],[f410]) ).
cnf(s28,plain,
( ~ spl16_19
| ~ spl16_22
| ~ spl16_26
| spl16_28 ),
inference(sat_conversion,[],[f434]) ).
cnf(s30,plain,
( ~ spl16_19
| ~ spl16_22
| ~ spl16_26
| spl16_30 ),
inference(sat_conversion,[],[f459]) ).
cnf(s31,plain,
( ~ spl16_4
| spl16_31 ),
inference(sat_conversion,[],[f472]) ).
cnf(s44,plain,
( ~ spl16_17
| spl16_44 ),
inference(sat_conversion,[],[f650]) ).
cnf(s45,plain,
( ~ spl16_8
| spl16_45 ),
inference(sat_conversion,[],[f676]) ).
cnf(s46,plain,
( ~ spl16_11
| spl16_46 ),
inference(sat_conversion,[],[f683]) ).
cnf(s59,plain,
( spl16_1
| ~ spl16_61
| ~ spl16_62 ),
inference(sat_conversion,[],[f841]) ).
cnf(s60,plain,
( spl16_61
| spl16_63 ),
inference(sat_conversion,[],[f847]) ).
cnf(s61,plain,
( spl16_61
| spl16_64 ),
inference(sat_conversion,[],[f854]) ).
cnf(s73,plain,
( ~ spl16_5
| spl16_75 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s91,plain,
( ~ spl16_13
| spl16_93 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s151,plain,
( ~ spl16_31
| spl16_150 ),
inference(sat_conversion,[],[f2448]) ).
cnf(s152,plain,
( ~ spl16_16
| ~ spl16_75
| ~ spl16_150
| spl16_151 ),
inference(sat_conversion,[],[f2487]) ).
cnf(s153,plain,
( ~ spl16_16
| ~ spl16_150
| ~ spl16_151
| spl16_152 ),
inference(sat_conversion,[],[f2502]) ).
cnf(s154,plain,
( ~ spl16_152
| spl16_153 ),
inference(sat_conversion,[],[f2525]) ).
cnf(s155,plain,
( ~ spl16_153
| spl16_154 ),
inference(sat_conversion,[],[f2548]) ).
cnf(s156,plain,
( ~ spl16_154
| spl16_155 ),
inference(sat_conversion,[],[f2560]) ).
cnf(s158,plain,
( ~ spl16_17
| ~ spl16_46
| ~ spl16_155
| spl16_157 ),
inference(sat_conversion,[],[f2600]) ).
cnf(s177,plain,
( ~ spl16_17
| ~ spl16_21
| ~ spl16_22
| ~ spl16_157
| spl16_178 ),
inference(sat_conversion,[],[f2967]) ).
cnf(s178,plain,
( ~ spl16_17
| ~ spl16_27
| ~ spl16_30
| ~ spl16_178
| spl16_179 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s179,plain,
( ~ spl16_17
| ~ spl16_28
| ~ spl16_179
| spl16_180 ),
inference(sat_conversion,[],[f3000]) ).
cnf(s180,plain,
( ~ spl16_63
| ~ spl16_64
| ~ spl16_180
| spl16_181 ),
inference(sat_conversion,[],[f3027]) ).
cnf(s181,plain,
( ~ spl16_12
| ~ spl16_44
| ~ spl16_181
| spl16_182 ),
inference(sat_conversion,[],[f3049]) ).
cnf(s182,plain,
( ~ spl16_8
| ~ spl16_18
| ~ spl16_64
| ~ spl16_182 ),
inference(sat_conversion,[],[f3056]) ).
cnf(s184,plain,
( spl16_62
| spl16_183 ),
inference(sat_conversion,[],[f3074]) ).
cnf(s185,plain,
( spl16_62
| spl16_184 ),
inference(sat_conversion,[],[f3088]) ).
cnf(s186,plain,
( spl16_62
| spl16_185 ),
inference(sat_conversion,[],[f3102]) ).
cnf(s187,plain,
( spl16_62
| spl16_186 ),
inference(sat_conversion,[],[f3107]) ).
cnf(s188,plain,
( spl16_62
| ~ spl16_187 ),
inference(sat_conversion,[],[f3132]) ).
cnf(s191,plain,
( spl16_62
| spl16_190 ),
inference(sat_conversion,[],[f3180]) ).
cnf(s313,plain,
( ~ spl16_21
| ~ spl16_22
| ~ spl16_24
| spl16_314 ),
inference(sat_conversion,[],[f6198]) ).
cnf(s447,plain,
( ~ spl16_45
| spl16_444 ),
inference(sat_conversion,[],[f10069]) ).
cnf(s448,plain,
( ~ spl16_18
| ~ spl16_93
| ~ spl16_444
| spl16_445 ),
inference(sat_conversion,[],[f10121]) ).
cnf(s449,plain,
( ~ spl16_18
| ~ spl16_444
| ~ spl16_445
| spl16_446 ),
inference(sat_conversion,[],[f10144]) ).
cnf(s450,plain,
( ~ spl16_446
| spl16_447 ),
inference(sat_conversion,[],[f10187]) ).
cnf(s452,plain,
( ~ spl16_447
| spl16_449 ),
inference(sat_conversion,[],[f10289]) ).
cnf(s453,plain,
( ~ spl16_449
| spl16_450 ),
inference(sat_conversion,[],[f10301]) ).
cnf(s454,plain,
( ~ spl16_450
| spl16_451 ),
inference(sat_conversion,[],[f10314]) ).
cnf(s462,plain,
( ~ spl16_183
| ~ spl16_185
| ~ spl16_190
| ~ spl16_451
| spl16_459 ),
inference(sat_conversion,[],[f10615]) ).
cnf(s514,plain,
( ~ spl16_21
| ~ spl16_22
| ~ spl16_185
| ~ spl16_506
| spl16_507 ),
inference(sat_conversion,[],[f11890]) ).
cnf(s515,plain,
( ~ spl16_21
| ~ spl16_185
| ~ spl16_507
| spl16_508 ),
inference(sat_conversion,[],[f11921]) ).
cnf(s516,plain,
( ~ spl16_21
| ~ spl16_22
| ~ spl16_186
| ~ spl16_508
| spl16_509 ),
inference(sat_conversion,[],[f11935]) ).
cnf(s517,plain,
( ~ spl16_185
| ~ spl16_186
| spl16_187
| ~ spl16_314
| ~ spl16_509 ),
inference(sat_conversion,[],[f11957]) ).
cnf(s518,plain,
( ~ spl16_184
| ~ spl16_186
| ~ spl16_459
| spl16_506 ),
inference(sat_conversion,[],[f11967]) ).
cnf(s519,plain,
spl16_20,
inference(rat,[],[s20,s12]) ).
cnf(s520,plain,
spl16_19,
inference(rat,[],[s19,s12]) ).
cnf(s528,plain,
spl16_26,
inference(rat,[],[s26,s519,s520]) ).
cnf(s529,plain,
spl16_22,
inference(rat,[],[s22,s519,s520]) ).
cnf(s530,plain,
spl16_21,
inference(rat,[],[s21,s519,s520]) ).
cnf(s536,plain,
spl16_30,
inference(rat,[],[s30,s528,s520,s529]) ).
cnf(s537,plain,
spl16_28,
inference(rat,[],[s28,s528,s520,s529]) ).
cnf(s538,plain,
spl16_27,
inference(rat,[],[s27,s528,s520,s529]) ).
cnf(s544,plain,
spl16_17,
inference(rat,[],[s17,s10]) ).
cnf(s545,plain,
spl16_15,
inference(rat,[],[s15,s10]) ).
cnf(s546,plain,
spl16_11,
inference(rat,[],[s11,s10]) ).
cnf(s559,plain,
spl16_44,
inference(rat,[],[s44,s544]) ).
cnf(s560,plain,
spl16_24,
inference(rat,[],[s24,s545]) ).
cnf(s564,plain,
spl16_46,
inference(rat,[],[s46,s546]) ).
cnf(s571,plain,
spl16_314,
inference(rat,[],[s313,s530,s529,s560]) ).
cnf(s581,plain,
spl16_18,
inference(rat,[],[s18,s7]) ).
cnf(s583,plain,
spl16_8,
inference(rat,[],[s8,s7]) ).
cnf(s601,plain,
spl16_45,
inference(rat,[],[s45,s583]) ).
cnf(s612,plain,
spl16_444,
inference(rat,[],[s447,s601]) ).
cnf(s616,plain,
spl16_13,
inference(rat,[],[s13,s6]) ).
cnf(s617,plain,
spl16_93,
inference(rat,[],[s91,s616]) ).
cnf(s618,plain,
spl16_445,
inference(rat,[],[s448,s612,s581,s617]) ).
cnf(s620,plain,
spl16_446,
inference(rat,[],[s449,s612,s581,s618]) ).
cnf(s621,plain,
spl16_447,
inference(rat,[],[s450,s620]) ).
cnf(s622,plain,
spl16_449,
inference(rat,[],[s452,s621]) ).
cnf(s623,plain,
spl16_450,
inference(rat,[],[s453,s622]) ).
cnf(s624,plain,
spl16_451,
inference(rat,[],[s454,s623]) ).
cnf(s625,plain,
spl16_16,
inference(rat,[],[s16,s3]) ).
cnf(s627,plain,
spl16_4,
inference(rat,[],[s4,s3]) ).
cnf(s649,plain,
spl16_31,
inference(rat,[],[s31,s627]) ).
cnf(s663,plain,
spl16_150,
inference(rat,[],[s151,s649]) ).
cnf(s686,plain,
spl16_5,
inference(rat,[],[s5,s2]) ).
cnf(s687,plain,
spl16_75,
inference(rat,[],[s73,s686]) ).
cnf(s688,plain,
spl16_151,
inference(rat,[],[s152,s663,s625,s687]) ).
cnf(s690,plain,
spl16_152,
inference(rat,[],[s153,s663,s625,s688]) ).
cnf(s694,plain,
spl16_153,
inference(rat,[],[s154,s690]) ).
cnf(s698,plain,
spl16_154,
inference(rat,[],[s155,s694]) ).
cnf(s702,plain,
spl16_155,
inference(rat,[],[s156,s698]) ).
cnf(s708,plain,
spl16_157,
inference(rat,[],[s158,s564,s544,s702]) ).
cnf(s718,plain,
spl16_178,
inference(rat,[],[s177,s544,s530,s529,s708]) ).
cnf(s723,plain,
spl16_179,
inference(rat,[],[s178,s544,s538,s536,s718]) ).
cnf(s728,plain,
spl16_180,
inference(rat,[],[s179,s544,s537,s723]) ).
cnf(s730,plain,
spl16_61,
inference(rat,[],[s181,s180,s182,s60,s61,s12,s559,s728,s581,s583]) ).
cnf(s733,plain,
~ spl16_62,
inference(rat,[],[s59,s1,s730]) ).
cnf(s748,plain,
spl16_190,
inference(rat,[],[s191,s733]) ).
cnf(s749,plain,
~ spl16_187,
inference(rat,[],[s188,s733]) ).
cnf(s750,plain,
spl16_186,
inference(rat,[],[s187,s733]) ).
cnf(s751,plain,
spl16_185,
inference(rat,[],[s186,s733]) ).
cnf(s752,plain,
spl16_184,
inference(rat,[],[s185,s733]) ).
cnf(s753,plain,
spl16_183,
inference(rat,[],[s184,s733]) ).
cnf(s770,plain,
~ spl16_509,
inference(rat,[],[s517,s750,s571,s749,s751]) ).
cnf(s778,plain,
spl16_459,
inference(rat,[],[s462,s751,s624,s748,s753]) ).
cnf(s792,plain,
~ spl16_508,
inference(rat,[],[s516,s750,s530,s529,s770]) ).
cnf(s800,plain,
spl16_506,
inference(rat,[],[s518,s752,s750,s778]) ).
cnf(s813,plain,
~ spl16_507,
inference(rat,[],[s515,s751,s530,s792]) ).
cnf(s823,plain,
$false,
inference(rat,[],[s514,s751,s530,s529,s800,s813]) ).
fof(f11968,plain,
$false,
inference(avatar_sat_refutation,[],[s823]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET738+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n014.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 28 02:40:02 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.45 Running first-order theorem proving
% 0.12/0.45 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
% 18.72/3.45 % (1383933)Detected formulas, will run a generic FOF schedule.
% 18.72/3.45 % (1383950)dis-21_1_sil=8000:lcm=predicate:random_seed=2235667107: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)
% 18.72/3.45 % (1383950)Instruction limit reached!
% 18.72/3.45 % (1383950)------------------------------
% 18.72/3.45 % (1383950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.72/3.45 % (1383950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.72/3.45 % (1383950)CaDiCaL version: 2.1.3
% 18.72/3.45 % (1383950)Termination reason: Instruction limit
% 18.72/3.45 % (1383950)Termination phase: Saturation
% 18.72/3.45 % (1383950)Time elapsed: 0.044 s
% 18.72/3.45 % (1383950)Peak memory usage: 89 MB
% 18.72/3.45 % (1383950)Instructions burned: 131 (million)
% 18.72/3.45 % (1383948)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=587244550:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 18.72/3.45 % (1383945)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=3407000680:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 18.72/3.45 % (1383944)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=3387336192:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 18.72/3.45 % (1383946)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=17079979:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 18.72/3.45 % (1383947)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=179344539:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 18.72/3.45 % (1383949)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3085666592:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 18.72/3.45 % (1383948)Instruction limit reached!
% 18.72/3.45 % (1383948)------------------------------
% 18.72/3.45 % (1383948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.72/3.45 % (1383948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.72/3.45 % (1383948)CaDiCaL version: 2.1.3
% 18.72/3.45 % (1383948)Termination reason: Instruction limit
% 18.72/3.45 % (1383948)Termination phase: Saturation
% 18.72/3.45 % (1383948)Time elapsed: 0.103 s
% 18.72/3.45 % (1383948)Peak memory usage: 89 MB
% 18.72/3.45 % (1383948)Instructions burned: 119 (million)
% 18.72/3.45 % (1383947)Instruction limit reached!
% 18.72/3.45 % (1383947)------------------------------
% 18.72/3.45 % (1383947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.72/3.45 % (1383947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.72/3.45 % (1383947)CaDiCaL version: 2.1.3
% 18.72/3.45 % (1383947)Termination reason: Instruction limit
% 18.72/3.45 % (1383947)Termination phase: Saturation
% 18.72/3.45 % (1383947)Time elapsed: 0.090 s
% 18.72/3.45 % (1383947)Peak memory usage: 89 MB
% 18.72/3.45 % (1383947)Instructions burned: 109 (million)
% 18.72/3.45 % (1383954)lrs+10_1_sil=8000:sp=occurrence:random_seed=1448900874:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 18.72/3.45 % (1383949)Instruction limit reached!
% 18.72/3.45 % (1383949)------------------------------
% 18.72/3.45 % (1383949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.72/3.45 % (1383949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.72/3.45 % (1383949)CaDiCaL version: 2.1.3
% 18.72/3.45 % (1383949)Termination reason: Instruction limit
% 18.72/3.45 % (1383949)Termination phase: Saturation
% 18.72/3.45 % (1383949)Time elapsed: 0.137 s
% 18.72/3.45 % (1383949)Peak memory usage: 89 MB
% 18.72/3.45 % (1383949)Instructions burned: 139 (million)
% 18.72/3.45 % (1383954)Instruction limit reached!
% 18.72/3.45 % (1383954)------------------------------
% 18.72/3.45 % (1383954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.72/3.45 % (1383954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.72/3.45 % (1383954)CaDiCaL version: 2.1.3
% 18.72/3.45 % (1383954)Termination reason: Instruction limit
% 18.72/3.45 % (1383954)Termination phase: Saturation
% 18.72/3.45 % (1383954)Time elapsed: 0.130 s
% 18.72/3.45 % (1383954)Peak memory usage: 93 MB
% 18.72/3.45 % (1383954)Instructions burned: 287 (million)
% 25.37/4.35 % (1383963)lrs+10_1_sil=32000:urr=on:br=off:random_seed=335991794:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 25.37/4.35 % (1383963)Refutation not found, incomplete strategy
% 25.37/4.35 % (1383963)------------------------------
% 25.37/4.35 % (1383963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.35 % (1383963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.35 % (1383963)CaDiCaL version: 2.1.3
% 25.37/4.35 % (1383963)Termination reason: Refutation not found, incomplete strategy
% 25.37/4.35 % (1383963)Time elapsed: 0.002 s
% 25.37/4.35 % (1383963)Peak memory usage: 88 MB
% 25.37/4.35 % (1383963)Instructions burned: 2 (million)
% 25.37/4.35 % (1383965)lrs+1011_1_sil=32000:sp=occurrence:random_seed=887819873:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 25.37/4.35 % (1383967)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=3875276109:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 25.37/4.35 % (1383969)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=81469401:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 25.37/4.35 % (1383963)------------------------------
% 25.37/4.35 % (1383963)------------------------------
% 25.37/4.35 % (1383967)Instruction limit reached!
% 25.37/4.35 % (1383967)------------------------------
% 25.37/4.35 % (1383967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.35 % (1383967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.35 % (1383967)CaDiCaL version: 2.1.3
% 25.37/4.35 % (1383967)Termination reason: Instruction limit
% 25.37/4.35 % (1383967)Termination phase: Saturation
% 25.37/4.35 % (1383967)Time elapsed: 0.220 s
% 25.37/4.35 % (1383967)Peak memory usage: 92 MB
% 25.37/4.35 % (1383967)Instructions burned: 249 (million)
% 25.37/4.35 % (1383965)Instruction limit reached!
% 25.37/4.35 % (1383965)------------------------------
% 25.37/4.35 % (1383965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.35 % (1383965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.35 % (1383965)CaDiCaL version: 2.1.3
% 25.37/4.35 % (1383965)Termination reason: Instruction limit
% 25.37/4.35 % (1383965)Termination phase: Saturation
% 25.37/4.35 % (1383965)Time elapsed: 0.292 s
% 25.37/4.35 % (1383965)Peak memory usage: 93 MB
% 25.37/4.35 % (1383965)Instructions burned: 325 (million)
% 25.37/4.35 % (1383978)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2598801301:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 25.37/4.35 % (1383969)Instruction limit reached!
% 25.37/4.35 % (1383969)------------------------------
% 25.37/4.35 % (1383969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.35 % (1383969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.35 % (1383969)CaDiCaL version: 2.1.3
% 25.37/4.35 % (1383969)Termination reason: Instruction limit
% 25.37/4.35 % (1383969)Termination phase: Saturation
% 25.37/4.35 % (1383969)Time elapsed: 0.267 s
% 25.37/4.35 % (1383969)Peak memory usage: 89 MB
% 25.37/4.35 % (1383969)Instructions burned: 294 (million)
% 25.37/4.35 % (1383982)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=249418549:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 25.37/4.35 % (1383981)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=639396336:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 25.37/4.35 % (1383982)Instruction limit reached!
% 25.37/4.35 % (1383982)------------------------------
% 25.37/4.35 % (1383982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.35 % (1383982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.35 % (1383982)CaDiCaL version: 2.1.3
% 25.37/4.35 % (1383982)Termination reason: Instruction limit
% 25.37/4.35 % (1383982)Termination phase: Saturation
% 25.37/4.35 % (1383982)Time elapsed: 0.080 s
% 25.37/4.35 % (1383982)Peak memory usage: 89 MB
% 25.37/4.35 % (1383982)Instructions burned: 127 (million)
% 25.37/4.35 % (1383986)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2354821279:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 25.37/4.35 % (1383981)Instruction limit reached!
% 25.37/4.35 % (1383981)------------------------------
% 25.37/4.35 % (1383981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1383981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1383981)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1383981)Termination reason: Instruction limit
% 29.07/4.96 % (1383981)Termination phase: Saturation
% 29.07/4.96 % (1383981)Time elapsed: 0.122 s
% 29.07/4.96 % (1383981)Peak memory usage: 89 MB
% 29.07/4.96 % (1383981)Instructions burned: 114 (million)
% 29.07/4.96 % (1383989)lrs+10_1_sil=8000:sp=occurrence:random_seed=308346280:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 29.07/4.96 % (1383986)Instruction limit reached!
% 29.07/4.96 % (1383986)------------------------------
% 29.07/4.96 % (1383986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1383986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1383986)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1383986)Termination reason: Instruction limit
% 29.07/4.96 % (1383986)Termination phase: Saturation
% 29.07/4.96 % (1383986)Time elapsed: 0.117 s
% 29.07/4.96 % (1383986)Peak memory usage: 89 MB
% 29.07/4.96 % (1383986)Instructions burned: 114 (million)
% 29.07/4.96 % (1383991)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=385087740:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 29.07/4.96 % (1383995)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2343247118:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 29.07/4.96 % (1383991)Instruction limit reached!
% 29.07/4.96 % (1383991)------------------------------
% 29.07/4.96 % (1383991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1383991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1383991)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1383991)Termination reason: Instruction limit
% 29.07/4.96 % (1383991)Termination phase: Saturation
% 29.07/4.96 % (1383991)Time elapsed: 0.356 s
% 29.07/4.96 % (1383991)Peak memory usage: 91 MB
% 29.07/4.96 % (1383991)Instructions burned: 437 (million)
% 29.07/4.96 % (1383989)Instruction limit reached!
% 29.07/4.96 % (1383989)------------------------------
% 29.07/4.96 % (1383989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1383989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1383989)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1383989)Termination reason: Instruction limit
% 29.07/4.96 % (1383989)Termination phase: Saturation
% 29.07/4.96 % (1383989)Time elapsed: 0.689 s
% 29.07/4.96 % (1383989)Peak memory usage: 102 MB
% 29.07/4.96 % (1383989)Instructions burned: 907 (million)
% 29.07/4.96 % (1384000)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2523072851:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 29.07/4.96 % (1384000)Refutation not found, incomplete strategy
% 29.07/4.96 % (1384000)------------------------------
% 29.07/4.96 % (1384000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384000)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384000)Termination reason: Refutation not found, incomplete strategy
% 29.07/4.96 % (1384000)Time elapsed: 0.004 s
% 29.07/4.96 % (1384000)Peak memory usage: 88 MB
% 29.07/4.96 % (1384000)Instructions burned: 2 (million)
% 29.07/4.96 % (1384002)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4051962155:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 29.07/4.96 % (1384000)------------------------------
% 29.07/4.96 % (1384000)------------------------------
% 29.07/4.96 % (1384002)Instruction limit reached!
% 29.07/4.96 % (1384002)------------------------------
% 29.07/4.96 % (1384002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384002)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384002)Termination reason: Instruction limit
% 29.07/4.96 % (1384002)Termination phase: Saturation
% 29.07/4.96 % (1384002)Time elapsed: 0.510 s
% 29.07/4.96 % (1384002)Peak memory usage: 97 MB
% 29.07/4.96 % (1384002)Instructions burned: 592 (million)
% 29.07/4.96 % (1384008)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3577698479:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi)
% 29.07/4.96 % (1384009)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=866541582:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/125Mi)
% 29.07/4.96 % (1384009)Instruction limit reached!
% 29.07/4.96 % (1384009)------------------------------
% 29.07/4.96 % (1384009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384009)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384009)Termination reason: Instruction limit
% 29.07/4.96 % (1384009)Termination phase: Saturation
% 29.07/4.96 % (1384009)Time elapsed: 0.086 s
% 29.07/4.96 % (1384009)Peak memory usage: 90 MB
% 29.07/4.96 % (1384009)Instructions burned: 125 (million)
% 29.07/4.96 % (1383978)Instruction limit reached!
% 29.07/4.96 % (1383978)------------------------------
% 29.07/4.96 % (1383978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1383978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1383978)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1383978)Termination reason: Instruction limit
% 29.07/4.96 % (1383978)Termination phase: Saturation
% 29.07/4.96 % (1383978)Time elapsed: 2.090 s
% 29.07/4.96 % (1383978)Peak memory usage: 139 MB
% 29.07/4.96 % (1383978)Instructions burned: 2351 (million)
% 29.07/4.96 % (1384015)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1736805270:i=134:gtgl=5:slsql=off:gtg=exists_sym_2971 on theBenchmark for (2971ds/134Mi)
% 29.07/4.96 % (1384015)Instruction limit reached!
% 29.07/4.96 % (1384015)------------------------------
% 29.07/4.96 % (1384015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384015)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384015)Termination reason: Instruction limit
% 29.07/4.96 % (1384015)Termination phase: Saturation
% 29.07/4.96 % (1384015)Time elapsed: 0.071 s
% 29.07/4.96 % (1384015)Peak memory usage: 89 MB
% 29.07/4.96 % (1384015)Instructions burned: 136 (million)
% 29.07/4.96 % (1384016)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=534930277:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/141Mi)
% 29.07/4.96 % (1384016)Instruction limit reached!
% 29.07/4.96 % (1384016)------------------------------
% 29.07/4.96 % (1384016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384016)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384016)Termination reason: Instruction limit
% 29.07/4.96 % (1384016)Termination phase: Saturation
% 29.07/4.96 % (1384016)Time elapsed: 0.067 s
% 29.07/4.96 % (1384016)Peak memory usage: 92 MB
% 29.07/4.96 % (1384016)Instructions burned: 142 (million)
% 29.07/4.96 % (1384018)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2780270446:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2969 on theBenchmark for (2969ds/431Mi)
% 29.07/4.96 % (1384018)Refutation not found, incomplete strategy
% 29.07/4.96 % (1384018)------------------------------
% 29.07/4.96 % (1384018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384018)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384018)Termination reason: Refutation not found, incomplete strategy
% 29.07/4.96 % (1384018)Time elapsed: 0.004 s
% 29.07/4.96 % (1384018)Peak memory usage: 88 MB
% 29.07/4.96 % (1384018)Instructions burned: 4 (million)
% 29.07/4.96 % (1384021)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2637771536:i=6060:aac=none:ins=25_2968 on theBenchmark for (2968ds/6060Mi)
% 29.07/4.96 % (1384018)------------------------------
% 29.07/4.96 % (1384018)------------------------------
% 29.07/4.96 % (1384063)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2600988013:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 29.07/4.96 % (1384063)Instruction limit reached!
% 29.07/4.96 % (1384063)------------------------------
% 29.07/4.96 % (1384063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384063)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384063)Termination reason: Instruction limit
% 29.07/4.96 % (1384063)Termination phase: Saturation
% 29.07/4.96 % (1384063)Time elapsed: 0.085 s
% 29.07/4.96 % (1384063)Peak memory usage: 90 MB
% 29.07/4.96 % (1384063)Instructions burned: 151 (million)
% 29.07/4.96 % (1383995)Instruction limit reached!
% 29.07/4.96 % (1383995)------------------------------
% 29.07/4.96 % (1383995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1383995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1383995)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1383995)Termination reason: Instruction limit
% 29.07/4.96 % (1383995)Termination phase: Saturation
% 29.07/4.96 % (1383995)Time elapsed: 2.279 s
% 29.07/4.96 % (1383995)Peak memory usage: 161 MB
% 29.07/4.96 % (1383995)Instructions burned: 5206 (million)
% 29.07/4.96 % (1384065)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2636946824:i=14155:bd=all_2963 on theBenchmark for (2963ds/14155Mi)
% 29.07/4.96 % (1384066)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1582073223:i=667:av=off:fsr=off_2962 on theBenchmark for (2962ds/667Mi)
% 29.07/4.96 % (1383946)First to succeed.
% 29.07/4.96 % (1383946)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1383933"
% 29.07/4.96 % (1384066)Instruction limit reached!
% 29.07/4.96 % (1384066)------------------------------
% 29.07/4.96 % (1384066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384066)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384066)Termination reason: Instruction limit
% 29.07/4.96 % (1384066)Termination phase: Saturation
% 29.07/4.96 % (1384066)Time elapsed: 0.202 s
% 29.07/4.96 % (1384066)Peak memory usage: 92 MB
% 29.07/4.96 % (1384066)Instructions burned: 669 (million)
% 29.07/4.96 % (1384069)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=389598373:s2a=on:i=185:s2at=1.8:fdi=4_2959 on theBenchmark for (2959ds/185Mi)
% 29.07/4.96 % (1384069)Instruction limit reached!
% 29.07/4.96 % (1384069)------------------------------
% 29.07/4.96 % (1384069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1384069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1384069)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1384069)Termination reason: Instruction limit
% 29.07/4.96 % (1384069)Termination phase: Saturation
% 29.07/4.96 % (1384069)Time elapsed: 0.078 s
% 29.07/4.96 % (1384069)Peak memory usage: 92 MB
% 29.07/4.96 % (1384069)Instructions burned: 188 (million)
% 29.07/4.96 % (1383946)Refutation found. Thanks to Tanya!
% 29.07/4.96 % SZS status Theorem for theBenchmark
% 29.07/4.96 % SZS output start Proof for theBenchmark
% See solution above
% 30.33/5.06 % (1383946)------------------------------
% 30.33/5.06 % (1383946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.33/5.06 % (1383946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.33/5.06 % (1383946)CaDiCaL version: 2.1.3
% 30.33/5.06 % (1383946)Termination reason: Refutation
% 30.33/5.06 % (1383946)Time elapsed: 3.751 s
% 30.33/5.06 % (1383946)Peak memory usage: 156 MB
% 30.33/5.06 % (1383946)Instructions burned: 4116 (million)
% 30.33/5.06 % (1383946)------------------------------
% 30.33/5.06 % (1383946)------------------------------
% 30.33/5.06 % (1383933)Success in time 4.252 s
% 30.33/5.06 % Vampire exiting
%------------------------------------------------------------------------------