%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET736+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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:46 PM UTC 2026
% Result : Theorem 20.39s 4.24s
% Output : Refutation 24.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 64
% Syntax : Number of formulae : 429 ( 70 unt; 58 def)
% Number of atoms : 1731 ( 104 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 2410 (1108 ~;1117 |; 99 &)
% ( 69 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 66 ( 64 usr; 57 prp; 0-5 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-5 aty)
% Number of variables : 687 ( 0 sgn 653 !; 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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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(X0,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thII27) ).
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(X0,X3,X4) ),
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(X0,X3,X4)
& 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(X0,X3,X4)
& 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(sK0,sK3,sK4)
& 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(sK0,sK3,sK4),
inference(cnf_transformation,[],[f45]) ).
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(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(sK0,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f91,plain,
( ~ one_to_one(sK0,sK3,sK4)
| spl16_1 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f92,plain,
~ spl16_1,
inference(avatar_split_clause,[],[f62,f89]) ).
fof(f93,plain,
( ~ injective(sK0,sK3,sK4)
| ~ surjective(sK0,sK3,sK4)
| spl16_1 ),
inference(resolution,[],[f91,f66]) ).
fof(f95,definition,
( spl16_2
<=> injective(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f97,plain,
( injective(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK4)
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f95]) ).
fof(f98,plain,
spl16_2,
inference(avatar_split_clause,[],[f57,f95]) ).
fof(f100,plain,
( ! [X0] :
( ~ member(X0,sK4)
| sP14(sK4,compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X0) )
| ~ spl16_2 ),
inference(resolution,[],[f97,f84]) ).
fof(f102,definition,
( spl16_3
<=> injective(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),sK3,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition]) ).
fof(f104,plain,
( injective(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),sK3,sK3)
| ~ spl16_3 ),
inference(avatar_component_clause,[],[f102]) ).
fof(f105,plain,
spl16_3,
inference(avatar_split_clause,[],[f58,f102]) ).
fof(f107,plain,
( ! [X0] :
( ~ member(X0,sK3)
| sP14(sK3,compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X0) )
| ~ spl16_3 ),
inference(resolution,[],[f104,f84]) ).
fof(f109,definition,
( spl16_4
<=> ! [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_4])],[avatar_definition]) ).
fof(f110,plain,
( ! [X0] :
( sP14(sK3,compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X0)
| ~ member(X0,sK3) )
| ~ spl16_4 ),
inference(avatar_component_clause,[],[f109]) ).
fof(f111,plain,
( spl16_4
| ~ spl16_3 ),
inference(avatar_split_clause,[],[f107,f102,f109]) ).
fof(f113,definition,
( spl16_5
<=> maps(sK0,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition]) ).
fof(f115,plain,
( maps(sK0,sK3,sK4)
| ~ spl16_5 ),
inference(avatar_component_clause,[],[f113]) ).
fof(f116,plain,
spl16_5,
inference(avatar_split_clause,[],[f61,f113]) ).
fof(f117,plain,
( ! [X0] :
( apply(sK0,X0,sK6(sK0,sK4,X0))
| ~ member(X0,sK3) )
| ~ spl16_5 ),
inference(resolution,[],[f115,f64]) ).
fof(f118,plain,
( ! [X0] :
( member(sK6(sK0,sK4,X0),sK4)
| ~ member(X0,sK3) )
| ~ spl16_5 ),
inference(resolution,[],[f115,f65]) ).
fof(f121,definition,
( spl16_6
<=> ! [X0] :
( apply(sK0,X0,sK6(sK0,sK4,X0))
| ~ member(X0,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_6])],[avatar_definition]) ).
fof(f122,plain,
( ! [X0] :
( apply(sK0,X0,sK6(sK0,sK4,X0))
| ~ member(X0,sK3) )
| ~ spl16_6 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f123,plain,
( spl16_6
| ~ spl16_5 ),
inference(avatar_split_clause,[],[f117,f113,f121]) ).
fof(f128,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_6 ),
inference(resolution,[],[f122,f86]) ).
fof(f131,definition,
( spl16_7
<=> ! [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_7])],[avatar_definition]) ).
fof(f132,plain,
( ! [X0] :
( sP14(sK4,compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),X0)
| ~ member(X0,sK4) )
| ~ spl16_7 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f133,plain,
( spl16_7
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f100,f95,f131]) ).
fof(f135,definition,
( spl16_8
<=> maps(sK2,sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_8])],[avatar_definition]) ).
fof(f137,plain,
( maps(sK2,sK5,sK3)
| ~ spl16_8 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f138,plain,
spl16_8,
inference(avatar_split_clause,[],[f59,f135]) ).
fof(f139,plain,
( ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) )
| ~ spl16_8 ),
inference(resolution,[],[f137,f64]) ).
fof(f140,plain,
( ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) )
| ~ spl16_8 ),
inference(resolution,[],[f137,f65]) ).
fof(f143,definition,
( spl16_9
<=> ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_9])],[avatar_definition]) ).
fof(f144,plain,
( ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) )
| ~ spl16_9 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f145,plain,
( spl16_9
| ~ spl16_8 ),
inference(avatar_split_clause,[],[f139,f135,f143]) ).
fof(f150,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_9 ),
inference(resolution,[],[f144,f86]) ).
fof(f157,definition,
( spl16_11
<=> maps(sK1,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_11])],[avatar_definition]) ).
fof(f159,plain,
( maps(sK1,sK4,sK5)
| ~ spl16_11 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f160,plain,
spl16_11,
inference(avatar_split_clause,[],[f60,f157]) ).
fof(f161,plain,
( ! [X0] :
( apply(sK1,X0,sK6(sK1,sK5,X0))
| ~ member(X0,sK4) )
| ~ spl16_11 ),
inference(resolution,[],[f159,f64]) ).
fof(f162,plain,
( ! [X0] :
( member(sK6(sK1,sK5,X0),sK5)
| ~ member(X0,sK4) )
| ~ spl16_11 ),
inference(resolution,[],[f159,f65]) ).
fof(f165,definition,
( spl16_12
<=> ! [X0] :
( apply(sK1,X0,sK6(sK1,sK5,X0))
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_12])],[avatar_definition]) ).
fof(f166,plain,
( ! [X0] :
( apply(sK1,X0,sK6(sK1,sK5,X0))
| ~ member(X0,sK4) )
| ~ spl16_12 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f167,plain,
( spl16_12
| ~ spl16_11 ),
inference(avatar_split_clause,[],[f161,f157,f165]) ).
fof(f172,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_12 ),
inference(resolution,[],[f166,f86]) ).
fof(f174,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_4 ),
inference(resolution,[],[f110,f85]) ).
fof(f176,definition,
( spl16_13
<=> surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_13])],[avatar_definition]) ).
fof(f178,plain,
( surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5)
| ~ spl16_13 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f179,plain,
spl16_13,
inference(avatar_split_clause,[],[f56,f176]) ).
fof(f180,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_7 ),
inference(resolution,[],[f132,f85]) ).
fof(f189,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_13 ),
inference(resolution,[],[f178,f78]) ).
fof(f190,plain,
( ! [X0] :
( member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) )
| ~ spl16_13 ),
inference(resolution,[],[f178,f79]) ).
fof(f194,definition,
( spl16_16
<=> ! [X0] :
( member(sK6(sK0,sK4,X0),sK4)
| ~ member(X0,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_16])],[avatar_definition]) ).
fof(f195,plain,
( ! [X0] :
( member(sK6(sK0,sK4,X0),sK4)
| ~ member(X0,sK3) )
| ~ spl16_16 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f196,plain,
( spl16_16
| ~ spl16_5 ),
inference(avatar_split_clause,[],[f118,f113,f194]) ).
fof(f198,definition,
( spl16_17
<=> ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_17])],[avatar_definition]) ).
fof(f199,plain,
( ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) )
| ~ spl16_17 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f200,plain,
( spl16_17
| ~ spl16_8 ),
inference(avatar_split_clause,[],[f140,f135,f198]) ).
fof(f203,definition,
( spl16_18
<=> ! [X0] :
( member(sK6(sK1,sK5,X0),sK5)
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_18])],[avatar_definition]) ).
fof(f204,plain,
( ! [X0] :
( member(sK6(sK1,sK5,X0),sK5)
| ~ member(X0,sK4) )
| ~ spl16_18 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f205,plain,
( spl16_18
| ~ spl16_11 ),
inference(avatar_split_clause,[],[f162,f157,f203]) ).
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_13 ),
inference(avatar_split_clause,[],[f190,f176,f208]) ).
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_13 ),
inference(avatar_split_clause,[],[f189,f176,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(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(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(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(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(f445,definition,
( spl16_29
<=> ! [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_29])],[avatar_definition]) ).
fof(f446,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_29 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f447,plain,
( spl16_29
| ~ spl16_19
| ~ spl16_22
| ~ spl16_26 ),
inference(avatar_split_clause,[],[f406,f389,f323,f208,f445]) ).
fof(f470,definition,
( spl16_31
<=> ! [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_31])],[avatar_definition]) ).
fof(f471,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_31 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f472,plain,
( spl16_31
| ~ spl16_6 ),
inference(avatar_split_clause,[],[f128,f121,f470]) ).
fof(f473,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_31 ),
inference(resolution,[],[f471,f87]) ).
fof(f730,definition,
( spl16_50
<=> ! [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_50])],[avatar_definition]) ).
fof(f731,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_50 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f732,plain,
( spl16_50
| ~ spl16_12 ),
inference(avatar_split_clause,[],[f172,f165,f730]) ).
fof(f737,definition,
( spl16_51
<=> ! [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_51])],[avatar_definition]) ).
fof(f738,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_51 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f739,plain,
( spl16_51
| ~ spl16_9 ),
inference(avatar_split_clause,[],[f150,f143,f737]) ).
fof(f740,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_51 ),
inference(resolution,[],[f738,f87]) ).
fof(f778,definition,
( spl16_56
<=> surjective(sK0,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_56])],[avatar_definition]) ).
fof(f780,plain,
( ~ surjective(sK0,sK3,sK4)
| spl16_56 ),
inference(avatar_component_clause,[],[f778]) ).
fof(f782,definition,
( spl16_57
<=> injective(sK0,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_57])],[avatar_definition]) ).
fof(f784,plain,
( ~ injective(sK0,sK3,sK4)
| spl16_57 ),
inference(avatar_component_clause,[],[f782]) ).
fof(f785,plain,
( ~ spl16_56
| ~ spl16_57
| spl16_1 ),
inference(avatar_split_clause,[],[f93,f89,f782,f778]) ).
fof(f787,plain,
( ! [X0] :
( ~ member(X0,sK3)
| ~ apply(sK0,X0,sK11(sK0,sK3,sK4)) )
| spl16_56 ),
inference(resolution,[],[f780,f81]) ).
fof(f789,definition,
( spl16_58
<=> ! [X0] :
( ~ member(X0,sK3)
| ~ apply(sK0,X0,sK11(sK0,sK3,sK4)) ) ),
introduced(definition,[new_symbols(definition,[spl16_58])],[avatar_definition]) ).
fof(f790,plain,
( ! [X0] :
( ~ apply(sK0,X0,sK11(sK0,sK3,sK4))
| ~ member(X0,sK3) )
| ~ spl16_58 ),
inference(avatar_component_clause,[],[f789]) ).
fof(f791,plain,
( spl16_58
| spl16_56 ),
inference(avatar_split_clause,[],[f787,f778,f789]) ).
fof(f795,plain,
( member(sK9(sK0,sK3,sK4),sK4)
| spl16_57 ),
inference(resolution,[],[f784,f68]) ).
fof(f796,plain,
( member(sK8(sK0,sK3,sK4),sK3)
| spl16_57 ),
inference(resolution,[],[f784,f69]) ).
fof(f798,plain,
( apply(sK0,sK8(sK0,sK3,sK4),sK9(sK0,sK3,sK4))
| spl16_57 ),
inference(resolution,[],[f784,f71]) ).
fof(f800,plain,
( sK8(sK0,sK3,sK4) != sK7(sK0,sK3,sK4)
| spl16_57 ),
inference(resolution,[],[f784,f73]) ).
fof(f802,definition,
( spl16_59
<=> apply(sK0,sK8(sK0,sK3,sK4),sK9(sK0,sK3,sK4)) ),
introduced(definition,[new_symbols(definition,[spl16_59])],[avatar_definition]) ).
fof(f804,plain,
( apply(sK0,sK8(sK0,sK3,sK4),sK9(sK0,sK3,sK4))
| ~ spl16_59 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f805,plain,
( spl16_59
| spl16_57 ),
inference(avatar_split_clause,[],[f798,f782,f802]) ).
fof(f830,definition,
( spl16_61
<=> member(sK8(sK0,sK3,sK4),sK3) ),
introduced(definition,[new_symbols(definition,[spl16_61])],[avatar_definition]) ).
fof(f832,plain,
( member(sK8(sK0,sK3,sK4),sK3)
| ~ spl16_61 ),
inference(avatar_component_clause,[],[f830]) ).
fof(f833,plain,
( spl16_61
| spl16_57 ),
inference(avatar_split_clause,[],[f796,f782,f830]) ).
fof(f880,definition,
( spl16_63
<=> sK8(sK0,sK3,sK4) = sK7(sK0,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_63])],[avatar_definition]) ).
fof(f882,plain,
( sK8(sK0,sK3,sK4) != sK7(sK0,sK3,sK4)
| spl16_63 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f883,plain,
( ~ spl16_63
| spl16_57 ),
inference(avatar_split_clause,[],[f800,f782,f880]) ).
fof(f923,definition,
( spl16_67
<=> member(sK9(sK0,sK3,sK4),sK4) ),
introduced(definition,[new_symbols(definition,[spl16_67])],[avatar_definition]) ).
fof(f925,plain,
( member(sK9(sK0,sK3,sK4),sK4)
| ~ spl16_67 ),
inference(avatar_component_clause,[],[f923]) ).
fof(f926,plain,
( spl16_67
| spl16_57 ),
inference(avatar_split_clause,[],[f795,f782,f923]) ).
fof(f1180,definition,
( spl16_80
<=> ! [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_80])],[avatar_definition]) ).
fof(f1181,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_80 ),
inference(avatar_component_clause,[],[f1180]) ).
fof(f1182,plain,
( spl16_80
| ~ spl16_7 ),
inference(avatar_split_clause,[],[f180,f131,f1180]) ).
fof(f1975,definition,
( spl16_123
<=> ! [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_123])],[avatar_definition]) ).
fof(f1976,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_123 ),
inference(avatar_component_clause,[],[f1975]) ).
fof(f1977,plain,
( spl16_123
| ~ spl16_4 ),
inference(avatar_split_clause,[],[f174,f109,f1975]) ).
fof(f3358,definition,
( spl16_187
<=> ! [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_187])],[avatar_definition]) ).
fof(f3359,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_187 ),
inference(avatar_component_clause,[],[f3358]) ).
fof(f3360,plain,
( spl16_187
| ~ spl16_31 ),
inference(avatar_split_clause,[],[f473,f470,f3358]) ).
fof(f3365,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_80
| ~ spl16_187 ),
inference(resolution,[],[f3359,f1181]) ).
fof(f3391,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_80
| ~ spl16_187 ),
inference(duplicate_literal_removal,[],[f3365]) ).
fof(f3403,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_16
| ~ spl16_80
| ~ spl16_187 ),
inference(forward_subsumption_resolution,[],[f3391,f195]) ).
fof(f3410,definition,
( spl16_188
<=> ! [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_188])],[avatar_definition]) ).
fof(f3411,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_188 ),
inference(avatar_component_clause,[],[f3410]) ).
fof(f3412,plain,
( spl16_188
| ~ spl16_16
| ~ spl16_80
| ~ spl16_187 ),
inference(avatar_split_clause,[],[f3403,f3358,f1180,f194,f3410]) ).
fof(f3413,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_187
| ~ spl16_188 ),
inference(resolution,[],[f3411,f3359]) ).
fof(f3429,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_187
| ~ spl16_188 ),
inference(duplicate_literal_removal,[],[f3413]) ).
fof(f3437,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_16
| ~ spl16_187
| ~ spl16_188 ),
inference(forward_subsumption_resolution,[],[f3429,f195]) ).
fof(f3443,definition,
( spl16_189
<=> ! [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_189])],[avatar_definition]) ).
fof(f3444,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_189 ),
inference(avatar_component_clause,[],[f3443]) ).
fof(f3445,plain,
( spl16_189
| ~ spl16_16
| ~ spl16_187
| ~ spl16_188 ),
inference(avatar_split_clause,[],[f3437,f3410,f3358,f194,f3443]) ).
fof(f3446,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_189 ),
inference(resolution,[],[f3444,f87]) ).
fof(f3463,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_189 ),
inference(duplicate_literal_removal,[],[f3446]) ).
fof(f3469,definition,
( spl16_190
<=> ! [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_190])],[avatar_definition]) ).
fof(f3470,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_190 ),
inference(avatar_component_clause,[],[f3469]) ).
fof(f3471,plain,
( spl16_190
| ~ spl16_189 ),
inference(avatar_split_clause,[],[f3463,f3443,f3469]) ).
fof(f3472,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_190 ),
inference(resolution,[],[f3470,f87]) ).
fof(f3489,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_190 ),
inference(duplicate_literal_removal,[],[f3472]) ).
fof(f3495,definition,
( spl16_191
<=> ! [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_191])],[avatar_definition]) ).
fof(f3496,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_191 ),
inference(avatar_component_clause,[],[f3495]) ).
fof(f3497,plain,
( spl16_191
| ~ spl16_190 ),
inference(avatar_split_clause,[],[f3489,f3469,f3495]) ).
fof(f3498,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_191 ),
inference(resolution,[],[f3496,f86]) ).
fof(f3507,definition,
( spl16_192
<=> ! [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_192])],[avatar_definition]) ).
fof(f3508,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_192 ),
inference(avatar_component_clause,[],[f3507]) ).
fof(f3509,plain,
( spl16_192
| ~ spl16_191 ),
inference(avatar_split_clause,[],[f3498,f3495,f3507]) ).
fof(f3511,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK4)
| ~ member(sK6(sK2,sK3,X1),sK3)
| X0 = X2
| ~ member(X2,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X0,X3)
| ~ apply(sK2,X3,sK6(sK2,sK3,X1))
| ~ member(X1,sK5)
| ~ apply(sK1,X2,X1)
| ~ member(X1,sK5) )
| ~ spl16_51
| ~ spl16_192 ),
inference(resolution,[],[f3508,f738]) ).
fof(f3514,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK4)
| ~ member(sK6(sK2,sK3,X1),sK3)
| X0 = X2
| ~ member(X2,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X0,X3)
| ~ apply(sK2,X3,sK6(sK2,sK3,X1))
| ~ member(X1,sK5)
| ~ apply(sK1,X2,X1) )
| ~ spl16_51
| ~ spl16_192 ),
inference(duplicate_literal_removal,[],[f3511]) ).
fof(f3516,plain,
( ! [X2,X3,X0,X1] :
( ~ member(X0,sK4)
| X0 = X2
| ~ member(X2,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X0,X3)
| ~ apply(sK2,X3,sK6(sK2,sK3,X1))
| ~ member(X1,sK5)
| ~ apply(sK1,X2,X1) )
| ~ spl16_17
| ~ spl16_51
| ~ spl16_192 ),
inference(forward_subsumption_resolution,[],[f3514,f199]) ).
fof(f3557,definition,
( spl16_194
<=> ! [X0,X3,X2,X1] :
( ~ member(X0,sK4)
| X0 = X2
| ~ member(X2,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X0,X3)
| ~ apply(sK2,X3,sK6(sK2,sK3,X1))
| ~ member(X1,sK5)
| ~ apply(sK1,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl16_194])],[avatar_definition]) ).
fof(f3558,plain,
( ! [X2,X3,X0,X1] :
( ~ apply(sK2,X3,sK6(sK2,sK3,X1))
| X0 = X2
| ~ member(X2,sK4)
| ~ member(X3,sK5)
| ~ apply(sK1,X0,X3)
| ~ member(X0,sK4)
| ~ member(X1,sK5)
| ~ apply(sK1,X2,X1) )
| ~ spl16_194 ),
inference(avatar_component_clause,[],[f3557]) ).
fof(f3559,plain,
( spl16_194
| ~ spl16_17
| ~ spl16_51
| ~ spl16_192 ),
inference(avatar_split_clause,[],[f3516,f3507,f737,f198,f3557]) ).
fof(f3560,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| ~ member(X0,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X1,X2)
| ~ member(X2,sK5) )
| ~ spl16_9
| ~ spl16_194 ),
inference(resolution,[],[f3558,f144]) ).
fof(f3580,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| ~ member(X0,sK4)
| ~ apply(sK1,X1,X2) )
| ~ spl16_9
| ~ spl16_194 ),
inference(duplicate_literal_removal,[],[f3560]) ).
fof(f3585,definition,
( spl16_195
<=> ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| ~ member(X0,sK4)
| ~ apply(sK1,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_195])],[avatar_definition]) ).
fof(f3586,plain,
( ! [X2,X0,X1] :
( ~ apply(sK1,X1,X2)
| ~ member(X1,sK4)
| ~ member(X2,sK5)
| ~ apply(sK1,X0,X2)
| ~ member(X0,sK4)
| X0 = X1 )
| ~ spl16_195 ),
inference(avatar_component_clause,[],[f3585]) ).
fof(f3587,plain,
( spl16_195
| ~ spl16_9
| ~ spl16_194 ),
inference(avatar_split_clause,[],[f3580,f3557,f143,f3585]) ).
fof(f3588,plain,
( ! [X0,X1] :
( ~ member(X0,sK4)
| ~ member(sK6(sK1,sK5,X0),sK5)
| ~ apply(sK1,X1,sK6(sK1,sK5,X0))
| ~ member(X1,sK4)
| X0 = X1
| ~ member(X0,sK4) )
| ~ spl16_12
| ~ spl16_195 ),
inference(resolution,[],[f3586,f166]) ).
fof(f3610,plain,
( ! [X0,X1] :
( ~ member(X0,sK4)
| ~ member(sK6(sK1,sK5,X0),sK5)
| ~ apply(sK1,X1,sK6(sK1,sK5,X0))
| ~ member(X1,sK4)
| X0 = X1 )
| ~ spl16_12
| ~ spl16_195 ),
inference(duplicate_literal_removal,[],[f3588]) ).
fof(f3617,plain,
( ! [X0,X1] :
( ~ member(X0,sK4)
| ~ apply(sK1,X1,sK6(sK1,sK5,X0))
| ~ member(X1,sK4)
| X0 = X1 )
| ~ spl16_12
| ~ spl16_18
| ~ spl16_195 ),
inference(forward_subsumption_resolution,[],[f3610,f204]) ).
fof(f3637,definition,
( spl16_198
<=> ! [X0,X1] :
( ~ member(X0,sK4)
| ~ apply(sK1,X1,sK6(sK1,sK5,X0))
| ~ member(X1,sK4)
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl16_198])],[avatar_definition]) ).
fof(f3638,plain,
( ! [X0,X1] :
( ~ apply(sK1,X1,sK6(sK1,sK5,X0))
| ~ member(X0,sK4)
| ~ member(X1,sK4)
| X0 = X1 )
| ~ spl16_198 ),
inference(avatar_component_clause,[],[f3637]) ).
fof(f3639,plain,
( spl16_198
| ~ spl16_12
| ~ spl16_18
| ~ spl16_195 ),
inference(avatar_split_clause,[],[f3617,f3585,f203,f165,f3637]) ).
fof(f3641,plain,
( ! [X0] :
( ~ member(X0,sK4)
| ~ 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,X0)),sK6(sK1,sK5,X0)),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,sK6(sK1,sK5,X0)),sK6(sK1,sK5,X0)) = X0
| ~ member(sK6(sK1,sK5,X0),sK5) )
| ~ spl16_21
| ~ spl16_198 ),
inference(resolution,[],[f3638,f313]) ).
fof(f3661,plain,
( ! [X0] :
( ~ member(X0,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,sK6(sK1,sK5,X0)),sK6(sK1,sK5,X0)) = X0
| ~ member(sK6(sK1,sK5,X0),sK5) )
| ~ spl16_21
| ~ spl16_22
| ~ spl16_198 ),
inference(forward_subsumption_resolution,[],[f3641,f324]) ).
fof(f3662,plain,
( ! [X0] :
( ~ member(X0,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,sK6(sK1,sK5,X0)),sK6(sK1,sK5,X0)) = X0 )
| ~ spl16_18
| ~ spl16_21
| ~ spl16_22
| ~ spl16_198 ),
inference(forward_subsumption_resolution,[],[f3661,f204]) ).
fof(f3683,definition,
( spl16_200
<=> ! [X0] :
( ~ member(X0,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,sK6(sK1,sK5,X0)),sK6(sK1,sK5,X0)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl16_200])],[avatar_definition]) ).
fof(f3684,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,sK6(sK1,sK5,X0)),sK6(sK1,sK5,X0)) = X0
| ~ member(X0,sK4) )
| ~ spl16_200 ),
inference(avatar_component_clause,[],[f3683]) ).
fof(f3685,plain,
( spl16_200
| ~ spl16_18
| ~ spl16_21
| ~ spl16_22
| ~ spl16_198 ),
inference(avatar_split_clause,[],[f3662,f3637,f323,f312,f203,f3683]) ).
fof(f3690,plain,
( ! [X0] :
( member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),X0),sK3)
| ~ member(sK6(sK1,sK5,X0),sK5)
| ~ member(X0,sK4) )
| ~ spl16_27
| ~ spl16_200 ),
inference(superposition,[],[f409,f3684]) ).
fof(f3692,plain,
( ! [X0] :
( apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),X0),X0)
| ~ member(sK6(sK1,sK5,X0),sK5)
| ~ member(X0,sK4) )
| ~ spl16_29
| ~ spl16_200 ),
inference(superposition,[],[f446,f3684]) ).
fof(f3699,plain,
( ! [X0] :
( apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),X0),X0)
| ~ member(X0,sK4) )
| ~ spl16_18
| ~ spl16_29
| ~ spl16_200 ),
inference(forward_subsumption_resolution,[],[f3692,f204]) ).
fof(f3701,plain,
( ! [X0] :
( member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),X0),sK3)
| ~ member(X0,sK4) )
| ~ spl16_18
| ~ spl16_27
| ~ spl16_200 ),
inference(forward_subsumption_resolution,[],[f3690,f204]) ).
fof(f3717,definition,
( spl16_202
<=> ! [X0] :
( apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),X0),X0)
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_202])],[avatar_definition]) ).
fof(f3718,plain,
( ! [X0] :
( apply(sK0,sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),X0),X0)
| ~ member(X0,sK4) )
| ~ spl16_202 ),
inference(avatar_component_clause,[],[f3717]) ).
fof(f3719,plain,
( spl16_202
| ~ spl16_18
| ~ spl16_29
| ~ spl16_200 ),
inference(avatar_split_clause,[],[f3699,f3683,f445,f203,f3717]) ).
fof(f3764,definition,
( spl16_204
<=> ! [X0] :
( member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),X0),sK3)
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_204])],[avatar_definition]) ).
fof(f3765,plain,
( ! [X0] :
( member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,X0)),X0),sK3)
| ~ member(X0,sK4) )
| ~ spl16_204 ),
inference(avatar_component_clause,[],[f3764]) ).
fof(f3766,plain,
( spl16_204
| ~ spl16_18
| ~ spl16_27
| ~ spl16_200 ),
inference(avatar_split_clause,[],[f3701,f3683,f408,f203,f3764]) ).
fof(f6331,definition,
( spl16_328
<=> ! [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_328])],[avatar_definition]) ).
fof(f6332,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_328 ),
inference(avatar_component_clause,[],[f6331]) ).
fof(f6333,plain,
( spl16_328
| ~ spl16_51 ),
inference(avatar_split_clause,[],[f740,f737,f6331]) ).
fof(f6335,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_123
| ~ spl16_328 ),
inference(resolution,[],[f6332,f1976]) ).
fof(f6379,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_123
| ~ spl16_328 ),
inference(duplicate_literal_removal,[],[f6335]) ).
fof(f6387,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_17
| ~ spl16_123
| ~ spl16_328 ),
inference(forward_subsumption_resolution,[],[f6379,f199]) ).
fof(f6408,definition,
( spl16_330
<=> ! [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_330])],[avatar_definition]) ).
fof(f6409,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_330 ),
inference(avatar_component_clause,[],[f6408]) ).
fof(f6410,plain,
( spl16_330
| ~ spl16_17
| ~ spl16_123
| ~ spl16_328 ),
inference(avatar_split_clause,[],[f6387,f6331,f1975,f198,f6408]) ).
fof(f6411,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_328
| ~ spl16_330 ),
inference(resolution,[],[f6409,f6332]) ).
fof(f6425,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_328
| ~ spl16_330 ),
inference(duplicate_literal_removal,[],[f6411]) ).
fof(f6427,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_17
| ~ spl16_328
| ~ spl16_330 ),
inference(forward_subsumption_resolution,[],[f6425,f199]) ).
fof(f6430,definition,
( spl16_331
<=> ! [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_331])],[avatar_definition]) ).
fof(f6431,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_331 ),
inference(avatar_component_clause,[],[f6430]) ).
fof(f6432,plain,
( spl16_331
| ~ spl16_17
| ~ spl16_328
| ~ spl16_330 ),
inference(avatar_split_clause,[],[f6427,f6408,f6331,f198,f6430]) ).
fof(f6433,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_331 ),
inference(resolution,[],[f6431,f87]) ).
fof(f6455,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_331 ),
inference(duplicate_literal_removal,[],[f6433]) ).
fof(f6464,definition,
( spl16_332
<=> ! [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_332])],[avatar_definition]) ).
fof(f6465,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_332 ),
inference(avatar_component_clause,[],[f6464]) ).
fof(f6466,plain,
( spl16_332
| ~ spl16_331 ),
inference(avatar_split_clause,[],[f6455,f6430,f6464]) ).
fof(f6467,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_332 ),
inference(resolution,[],[f6465,f87]) ).
fof(f6489,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_332 ),
inference(duplicate_literal_removal,[],[f6467]) ).
fof(f6498,definition,
( spl16_333
<=> ! [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_333])],[avatar_definition]) ).
fof(f6499,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_333 ),
inference(avatar_component_clause,[],[f6498]) ).
fof(f6500,plain,
( spl16_333
| ~ spl16_332 ),
inference(avatar_split_clause,[],[f6489,f6464,f6498]) ).
fof(f6501,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_333 ),
inference(resolution,[],[f6499,f86]) ).
fof(f6514,definition,
( spl16_334
<=> ! [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_334])],[avatar_definition]) ).
fof(f6515,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_334 ),
inference(avatar_component_clause,[],[f6514]) ).
fof(f6516,plain,
( spl16_334
| ~ spl16_333 ),
inference(avatar_split_clause,[],[f6501,f6498,f6514]) ).
fof(f6520,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_50
| ~ spl16_334 ),
inference(resolution,[],[f6515,f731]) ).
fof(f6523,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_50
| ~ spl16_334 ),
inference(duplicate_literal_removal,[],[f6520]) ).
fof(f6526,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_18
| ~ spl16_50
| ~ spl16_334 ),
inference(forward_subsumption_resolution,[],[f6523,f204]) ).
fof(f6576,definition,
( spl16_336
<=> ! [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_336])],[avatar_definition]) ).
fof(f6577,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_336 ),
inference(avatar_component_clause,[],[f6576]) ).
fof(f6578,plain,
( spl16_336
| ~ spl16_18
| ~ spl16_50
| ~ spl16_334 ),
inference(avatar_split_clause,[],[f6526,f6514,f730,f203,f6576]) ).
fof(f6579,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| ~ member(X0,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X1,X2)
| ~ member(X2,sK4) )
| ~ spl16_12
| ~ spl16_336 ),
inference(resolution,[],[f6577,f166]) ).
fof(f6605,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| ~ member(X0,sK3)
| ~ apply(sK0,X1,X2) )
| ~ spl16_12
| ~ spl16_336 ),
inference(duplicate_literal_removal,[],[f6579]) ).
fof(f6616,definition,
( spl16_337
<=> ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| ~ member(X0,sK3)
| ~ apply(sK0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_337])],[avatar_definition]) ).
fof(f6617,plain,
( ! [X2,X0,X1] :
( ~ apply(sK0,X1,X2)
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| ~ member(X0,sK3)
| X0 = X1 )
| ~ spl16_337 ),
inference(avatar_component_clause,[],[f6616]) ).
fof(f6618,plain,
( spl16_337
| ~ spl16_12
| ~ spl16_336 ),
inference(avatar_split_clause,[],[f6605,f6576,f165,f6616]) ).
fof(f6621,plain,
( ! [X0] :
( ~ member(sK8(sK0,sK3,sK4),sK3)
| ~ member(sK9(sK0,sK3,sK4),sK4)
| ~ apply(sK0,X0,sK9(sK0,sK3,sK4))
| ~ member(X0,sK3)
| sK8(sK0,sK3,sK4) = X0 )
| ~ spl16_59
| ~ spl16_337 ),
inference(resolution,[],[f6617,f804]) ).
fof(f6662,plain,
( ! [X0] :
( ~ member(sK9(sK0,sK3,sK4),sK4)
| ~ apply(sK0,X0,sK9(sK0,sK3,sK4))
| ~ member(X0,sK3)
| sK8(sK0,sK3,sK4) = X0 )
| ~ spl16_59
| ~ spl16_61
| ~ spl16_337 ),
inference(forward_subsumption_resolution,[],[f6621,f832]) ).
fof(f6669,plain,
( ! [X0] :
( ~ apply(sK0,X0,sK9(sK0,sK3,sK4))
| ~ member(X0,sK3)
| sK8(sK0,sK3,sK4) = X0 )
| ~ spl16_59
| ~ spl16_61
| ~ spl16_67
| ~ spl16_337 ),
inference(forward_subsumption_resolution,[],[f6662,f925]) ).
fof(f6676,definition,
( spl16_338
<=> ! [X0] :
( ~ apply(sK0,X0,sK9(sK0,sK3,sK4))
| ~ member(X0,sK3)
| sK8(sK0,sK3,sK4) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl16_338])],[avatar_definition]) ).
fof(f6677,plain,
( ! [X0] :
( ~ apply(sK0,X0,sK9(sK0,sK3,sK4))
| ~ member(X0,sK3)
| sK8(sK0,sK3,sK4) = X0 )
| ~ spl16_338 ),
inference(avatar_component_clause,[],[f6676]) ).
fof(f6678,plain,
( spl16_338
| ~ spl16_59
| ~ spl16_61
| ~ spl16_67
| ~ spl16_337 ),
inference(avatar_split_clause,[],[f6669,f6616,f923,f830,f802,f6676]) ).
fof(f6683,plain,
( ~ member(sK7(sK0,sK3,sK4),sK3)
| sK8(sK0,sK3,sK4) = sK7(sK0,sK3,sK4)
| injective(sK0,sK3,sK4)
| ~ spl16_338 ),
inference(resolution,[],[f6677,f72]) ).
fof(f6688,plain,
( sK8(sK0,sK3,sK4) = sK7(sK0,sK3,sK4)
| injective(sK0,sK3,sK4)
| ~ spl16_338 ),
inference(forward_subsumption_resolution,[],[f6683,f70]) ).
fof(f6691,plain,
( injective(sK0,sK3,sK4)
| spl16_63
| ~ spl16_338 ),
inference(forward_subsumption_resolution,[],[f6688,f882]) ).
fof(f6695,plain,
( $false
| spl16_57
| spl16_63
| ~ spl16_338 ),
inference(forward_subsumption_resolution,[],[f6691,f784]) ).
fof(f6696,plain,
( spl16_57
| spl16_63
| ~ spl16_338 ),
inference(avatar_contradiction_clause,[],[f6695]) ).
fof(f6787,plain,
( ~ member(sK10(sK0,sK2,sK3,sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK6(sK1,sK5,sK11(sK0,sK3,sK4))),sK11(sK0,sK3,sK4)),sK3)
| ~ member(sK11(sK0,sK3,sK4),sK4)
| ~ spl16_58
| ~ spl16_202 ),
inference(resolution,[],[f790,f3718]) ).
fof(f6790,plain,
( ~ member(sK11(sK0,sK3,sK4),sK4)
| ~ spl16_58
| ~ spl16_202
| ~ spl16_204 ),
inference(forward_subsumption_resolution,[],[f6787,f3765]) ).
fof(f6808,definition,
( spl16_341
<=> member(sK11(sK0,sK3,sK4),sK4) ),
introduced(definition,[new_symbols(definition,[spl16_341])],[avatar_definition]) ).
fof(f6810,plain,
( ~ member(sK11(sK0,sK3,sK4),sK4)
| spl16_341 ),
inference(avatar_component_clause,[],[f6808]) ).
fof(f6811,plain,
( ~ spl16_341
| ~ spl16_58
| ~ spl16_202
| ~ spl16_204 ),
inference(avatar_split_clause,[],[f6790,f3764,f3717,f789,f6808]) ).
fof(f6812,plain,
( surjective(sK0,sK3,sK4)
| spl16_341 ),
inference(resolution,[],[f6810,f80]) ).
fof(f6813,plain,
( $false
| spl16_56
| spl16_341 ),
inference(forward_subsumption_resolution,[],[f6812,f780]) ).
fof(f6814,plain,
( spl16_56
| spl16_341 ),
inference(avatar_contradiction_clause,[],[f6813]) ).
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,[],[f111]) ).
cnf(s5,plain,
spl16_5,
inference(sat_conversion,[],[f116]) ).
cnf(s6,plain,
( ~ spl16_5
| spl16_6 ),
inference(sat_conversion,[],[f123]) ).
cnf(s7,plain,
( ~ spl16_2
| spl16_7 ),
inference(sat_conversion,[],[f133]) ).
cnf(s8,plain,
spl16_8,
inference(sat_conversion,[],[f138]) ).
cnf(s9,plain,
( ~ spl16_8
| spl16_9 ),
inference(sat_conversion,[],[f145]) ).
cnf(s11,plain,
spl16_11,
inference(sat_conversion,[],[f160]) ).
cnf(s12,plain,
( ~ spl16_11
| spl16_12 ),
inference(sat_conversion,[],[f167]) ).
cnf(s13,plain,
spl16_13,
inference(sat_conversion,[],[f179]) ).
cnf(s16,plain,
( ~ spl16_5
| spl16_16 ),
inference(sat_conversion,[],[f196]) ).
cnf(s17,plain,
( ~ spl16_8
| spl16_17 ),
inference(sat_conversion,[],[f200]) ).
cnf(s18,plain,
( ~ spl16_11
| spl16_18 ),
inference(sat_conversion,[],[f205]) ).
cnf(s19,plain,
( ~ spl16_13
| spl16_19 ),
inference(sat_conversion,[],[f210]) ).
cnf(s20,plain,
( ~ spl16_13
| 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(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(s29,plain,
( ~ spl16_19
| ~ spl16_22
| ~ spl16_26
| spl16_29 ),
inference(sat_conversion,[],[f447]) ).
cnf(s31,plain,
( ~ spl16_6
| spl16_31 ),
inference(sat_conversion,[],[f472]) ).
cnf(s49,plain,
( ~ spl16_12
| spl16_50 ),
inference(sat_conversion,[],[f732]) ).
cnf(s50,plain,
( ~ spl16_9
| spl16_51 ),
inference(sat_conversion,[],[f739]) ).
cnf(s55,plain,
( spl16_1
| ~ spl16_56
| ~ spl16_57 ),
inference(sat_conversion,[],[f785]) ).
cnf(s56,plain,
( spl16_56
| spl16_58 ),
inference(sat_conversion,[],[f791]) ).
cnf(s57,plain,
( spl16_57
| spl16_59 ),
inference(sat_conversion,[],[f805]) ).
cnf(s59,plain,
( spl16_57
| spl16_61 ),
inference(sat_conversion,[],[f833]) ).
cnf(s61,plain,
( spl16_57
| ~ spl16_63 ),
inference(sat_conversion,[],[f883]) ).
cnf(s65,plain,
( spl16_57
| spl16_67 ),
inference(sat_conversion,[],[f926]) ).
cnf(s78,plain,
( ~ spl16_7
| spl16_80 ),
inference(sat_conversion,[],[f1182]) ).
cnf(s120,plain,
( ~ spl16_4
| spl16_123 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s185,plain,
( ~ spl16_31
| spl16_187 ),
inference(sat_conversion,[],[f3360]) ).
cnf(s186,plain,
( ~ spl16_16
| ~ spl16_80
| ~ spl16_187
| spl16_188 ),
inference(sat_conversion,[],[f3412]) ).
cnf(s187,plain,
( ~ spl16_16
| ~ spl16_187
| ~ spl16_188
| spl16_189 ),
inference(sat_conversion,[],[f3445]) ).
cnf(s188,plain,
( ~ spl16_189
| spl16_190 ),
inference(sat_conversion,[],[f3471]) ).
cnf(s189,plain,
( ~ spl16_190
| spl16_191 ),
inference(sat_conversion,[],[f3497]) ).
cnf(s190,plain,
( ~ spl16_191
| spl16_192 ),
inference(sat_conversion,[],[f3509]) ).
cnf(s192,plain,
( ~ spl16_17
| ~ spl16_51
| ~ spl16_192
| spl16_194 ),
inference(sat_conversion,[],[f3559]) ).
cnf(s193,plain,
( ~ spl16_9
| ~ spl16_194
| spl16_195 ),
inference(sat_conversion,[],[f3587]) ).
cnf(s196,plain,
( ~ spl16_12
| ~ spl16_18
| ~ spl16_195
| spl16_198 ),
inference(sat_conversion,[],[f3639]) ).
cnf(s198,plain,
( ~ spl16_18
| ~ spl16_21
| ~ spl16_22
| ~ spl16_198
| spl16_200 ),
inference(sat_conversion,[],[f3685]) ).
cnf(s200,plain,
( ~ spl16_18
| ~ spl16_29
| ~ spl16_200
| spl16_202 ),
inference(sat_conversion,[],[f3719]) ).
cnf(s202,plain,
( ~ spl16_18
| ~ spl16_27
| ~ spl16_200
| spl16_204 ),
inference(sat_conversion,[],[f3766]) ).
cnf(s318,plain,
( ~ spl16_51
| spl16_328 ),
inference(sat_conversion,[],[f6333]) ).
cnf(s320,plain,
( ~ spl16_17
| ~ spl16_123
| ~ spl16_328
| spl16_330 ),
inference(sat_conversion,[],[f6410]) ).
cnf(s321,plain,
( ~ spl16_17
| ~ spl16_328
| ~ spl16_330
| spl16_331 ),
inference(sat_conversion,[],[f6432]) ).
cnf(s322,plain,
( ~ spl16_331
| spl16_332 ),
inference(sat_conversion,[],[f6466]) ).
cnf(s323,plain,
( ~ spl16_332
| spl16_333 ),
inference(sat_conversion,[],[f6500]) ).
cnf(s324,plain,
( ~ spl16_333
| spl16_334 ),
inference(sat_conversion,[],[f6516]) ).
cnf(s326,plain,
( ~ spl16_18
| ~ spl16_50
| ~ spl16_334
| spl16_336 ),
inference(sat_conversion,[],[f6578]) ).
cnf(s327,plain,
( ~ spl16_12
| ~ spl16_336
| spl16_337 ),
inference(sat_conversion,[],[f6618]) ).
cnf(s328,plain,
( ~ spl16_59
| ~ spl16_61
| ~ spl16_67
| ~ spl16_337
| spl16_338 ),
inference(sat_conversion,[],[f6678]) ).
cnf(s330,plain,
( spl16_57
| spl16_63
| ~ spl16_338 ),
inference(sat_conversion,[],[f6696]) ).
cnf(s340,plain,
( ~ spl16_58
| ~ spl16_202
| ~ spl16_204
| ~ spl16_341 ),
inference(sat_conversion,[],[f6811]) ).
cnf(s341,plain,
( spl16_56
| spl16_341 ),
inference(sat_conversion,[],[f6814]) ).
cnf(s342,plain,
spl16_20,
inference(rat,[],[s20,s13]) ).
cnf(s343,plain,
spl16_19,
inference(rat,[],[s19,s13]) ).
cnf(s351,plain,
spl16_26,
inference(rat,[],[s26,s342,s343]) ).
cnf(s352,plain,
spl16_22,
inference(rat,[],[s22,s342,s343]) ).
cnf(s353,plain,
spl16_21,
inference(rat,[],[s21,s342,s343]) ).
cnf(s357,plain,
spl16_29,
inference(rat,[],[s29,s351,s343,s352]) ).
cnf(s359,plain,
spl16_27,
inference(rat,[],[s27,s351,s343,s352]) ).
cnf(s362,plain,
spl16_18,
inference(rat,[],[s18,s11]) ).
cnf(s364,plain,
spl16_12,
inference(rat,[],[s12,s11]) ).
cnf(s381,plain,
spl16_50,
inference(rat,[],[s49,s364]) ).
cnf(s393,plain,
spl16_17,
inference(rat,[],[s17,s8]) ).
cnf(s395,plain,
spl16_9,
inference(rat,[],[s9,s8]) ).
cnf(s415,plain,
spl16_51,
inference(rat,[],[s50,s395]) ).
cnf(s422,plain,
spl16_328,
inference(rat,[],[s318,s415]) ).
cnf(s424,plain,
spl16_16,
inference(rat,[],[s16,s5]) ).
cnf(s426,plain,
spl16_6,
inference(rat,[],[s6,s5]) ).
cnf(s446,plain,
spl16_31,
inference(rat,[],[s31,s426]) ).
cnf(s455,plain,
spl16_187,
inference(rat,[],[s185,s446]) ).
cnf(s458,plain,
spl16_4,
inference(rat,[],[s4,s3]) ).
cnf(s459,plain,
spl16_123,
inference(rat,[],[s120,s458]) ).
cnf(s460,plain,
spl16_330,
inference(rat,[],[s320,s422,s393,s459]) ).
cnf(s462,plain,
spl16_331,
inference(rat,[],[s321,s422,s393,s460]) ).
cnf(s463,plain,
spl16_332,
inference(rat,[],[s322,s462]) ).
cnf(s464,plain,
spl16_333,
inference(rat,[],[s323,s463]) ).
cnf(s465,plain,
spl16_334,
inference(rat,[],[s324,s464]) ).
cnf(s467,plain,
spl16_336,
inference(rat,[],[s326,s381,s362,s465]) ).
cnf(s468,plain,
spl16_337,
inference(rat,[],[s327,s364,s467]) ).
cnf(s469,plain,
spl16_7,
inference(rat,[],[s7,s2]) ).
cnf(s470,plain,
spl16_80,
inference(rat,[],[s78,s469]) ).
cnf(s471,plain,
spl16_188,
inference(rat,[],[s186,s455,s424,s470]) ).
cnf(s473,plain,
spl16_189,
inference(rat,[],[s187,s455,s424,s471]) ).
cnf(s476,plain,
spl16_190,
inference(rat,[],[s188,s473]) ).
cnf(s478,plain,
spl16_191,
inference(rat,[],[s189,s476]) ).
cnf(s480,plain,
spl16_192,
inference(rat,[],[s190,s478]) ).
cnf(s486,plain,
spl16_194,
inference(rat,[],[s192,s415,s393,s480]) ).
cnf(s491,plain,
spl16_195,
inference(rat,[],[s193,s395,s486]) ).
cnf(s495,plain,
spl16_198,
inference(rat,[],[s196,s364,s362,s491]) ).
cnf(s499,plain,
spl16_200,
inference(rat,[],[s198,s362,s353,s352,s495]) ).
cnf(s501,plain,
spl16_202,
inference(rat,[],[s200,s362,s357,s499]) ).
cnf(s502,plain,
spl16_204,
inference(rat,[],[s202,s362,s359,s499]) ).
cnf(s503,plain,
spl16_56,
inference(rat,[],[s340,s56,s341,s502,s501]) ).
cnf(s506,plain,
~ spl16_57,
inference(rat,[],[s55,s1,s503]) ).
cnf(s516,plain,
spl16_67,
inference(rat,[],[s65,s506]) ).
cnf(s517,plain,
~ spl16_63,
inference(rat,[],[s61,s506]) ).
cnf(s519,plain,
spl16_61,
inference(rat,[],[s59,s506]) ).
cnf(s521,plain,
spl16_59,
inference(rat,[],[s57,s506]) ).
cnf(s529,plain,
~ spl16_338,
inference(rat,[],[s330,s506,s517]) ).
cnf(s535,plain,
$false,
inference(rat,[],[s328,s529,s468,s516,s519,s521]) ).
fof(f6815,plain,
$false,
inference(avatar_sat_refutation,[],[s535]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET736+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n014.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 28 02:40:01 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.90/3.80 % (1383804)Detected formulas, will run a generic FOF schedule.
% 19.90/3.80 % (1383911)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1018271056:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 19.90/3.80 % (1383912)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3278045785:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 19.90/3.80 % (1383913)dis-21_1_sil=8000:lcm=predicate:random_seed=3347916976: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)
% 19.90/3.80 % (1383909)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=2259585459:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 19.90/3.80 % (1383908)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=233107638:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 19.90/3.80 % (1383907)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=960490813:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 19.90/3.80 % (1383911)Instruction limit reached!
% 19.90/3.80 % (1383911)------------------------------
% 19.90/3.80 % (1383911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.80 % (1383911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.80 % (1383911)CaDiCaL version: 2.1.3
% 19.90/3.80 % (1383911)Termination reason: Instruction limit
% 19.90/3.80 % (1383911)Termination phase: Saturation
% 19.90/3.80 % (1383911)Time elapsed: 0.041 s
% 19.90/3.80 % (1383911)Peak memory usage: 89 MB
% 19.90/3.80 % (1383911)Instructions burned: 122 (million)
% 19.90/3.80 % (1383910)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4183055272:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 19.90/3.80 % (1383913)Instruction limit reached!
% 19.90/3.80 % (1383913)------------------------------
% 19.90/3.80 % (1383913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.80 % (1383913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.80 % (1383913)CaDiCaL version: 2.1.3
% 19.90/3.80 % (1383913)Termination reason: Instruction limit
% 19.90/3.80 % (1383913)Termination phase: Saturation
% 19.90/3.80 % (1383913)Time elapsed: 0.058 s
% 19.90/3.80 % (1383913)Peak memory usage: 89 MB
% 19.90/3.80 % (1383913)Instructions burned: 131 (million)
% 19.90/3.80 % (1383910)Instruction limit reached!
% 19.90/3.80 % (1383910)------------------------------
% 19.90/3.80 % (1383910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.80 % (1383910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.80 % (1383910)CaDiCaL version: 2.1.3
% 19.90/3.80 % (1383910)Termination reason: Instruction limit
% 19.90/3.80 % (1383910)Termination phase: Saturation
% 19.90/3.80 % (1383910)Time elapsed: 0.063 s
% 19.90/3.80 % (1383910)Peak memory usage: 89 MB
% 19.90/3.80 % (1383910)Instructions burned: 110 (million)
% 19.90/3.80 % (1383912)Instruction limit reached!
% 19.90/3.80 % (1383912)------------------------------
% 19.90/3.80 % (1383912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.80 % (1383912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.80 % (1383912)CaDiCaL version: 2.1.3
% 19.90/3.80 % (1383912)Termination reason: Instruction limit
% 19.90/3.80 % (1383912)Termination phase: Saturation
% 19.90/3.80 % (1383912)Time elapsed: 0.126 s
% 19.90/3.80 % (1383912)Peak memory usage: 89 MB
% 19.90/3.80 % (1383912)Instructions burned: 139 (million)
% 19.90/3.80 % (1383920)lrs+10_1_sil=8000:sp=occurrence:random_seed=264861488:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 19.90/3.80 % (1383926)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2314776091:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 19.90/3.80 % (1383926)Refutation not found, incomplete strategy
% 19.90/3.80 % (1383926)------------------------------
% 19.90/3.80 % (1383926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.80 % (1383926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.80 % (1383926)CaDiCaL version: 2.1.3
% 19.90/3.80 % (1383926)Termination reason: Refutation not found, incomplete strategy
% 20.39/4.24 % (1383926)Time elapsed: 0.003 s
% 20.39/4.24 % (1383926)Peak memory usage: 88 MB
% 20.39/4.24 % (1383926)Instructions burned: 2 (million)
% 20.39/4.24 % (1383930)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3038487716:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 20.39/4.24 % (1383937)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=2116592985:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 20.39/4.24 % (1383920)Instruction limit reached!
% 20.39/4.24 % (1383920)------------------------------
% 20.39/4.24 % (1383920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383920)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383920)Termination reason: Instruction limit
% 20.39/4.24 % (1383920)Termination phase: Saturation
% 20.39/4.24 % (1383920)Time elapsed: 0.159 s
% 20.39/4.24 % (1383920)Peak memory usage: 93 MB
% 20.39/4.24 % (1383920)Instructions burned: 286 (million)
% 20.39/4.24 % (1383937)Instruction limit reached!
% 20.39/4.24 % (1383937)------------------------------
% 20.39/4.24 % (1383937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383937)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383937)Termination reason: Instruction limit
% 20.39/4.24 % (1383937)Termination phase: Saturation
% 20.39/4.24 % (1383937)Time elapsed: 0.164 s
% 20.39/4.24 % (1383937)Peak memory usage: 92 MB
% 20.39/4.24 % (1383937)Instructions burned: 249 (million)
% 20.39/4.24 % (1383930)Instruction limit reached!
% 20.39/4.24 % (1383930)------------------------------
% 20.39/4.24 % (1383930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383930)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383930)Termination reason: Instruction limit
% 20.39/4.24 % (1383930)Termination phase: Saturation
% 20.39/4.24 % (1383930)Time elapsed: 0.262 s
% 20.39/4.24 % (1383930)Peak memory usage: 93 MB
% 20.39/4.24 % (1383930)Instructions burned: 325 (million)
% 20.39/4.24 % (1383926)------------------------------
% 20.39/4.24 % (1383926)------------------------------
% 20.39/4.24 % (1383942)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2549682089:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.39/4.24 % (1383952)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=305606417:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 20.39/4.24 % (1383953)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=889456234:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 20.39/4.24 % (1383955)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3395965250:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 20.39/4.24 % (1383942)Instruction limit reached!
% 20.39/4.24 % (1383942)------------------------------
% 20.39/4.24 % (1383942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383942)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383942)Termination reason: Instruction limit
% 20.39/4.24 % (1383942)Termination phase: Saturation
% 20.39/4.24 % (1383942)Time elapsed: 0.254 s
% 20.39/4.24 % (1383942)Peak memory usage: 89 MB
% 20.39/4.24 % (1383942)Instructions burned: 295 (million)
% 20.39/4.24 % (1383953)Instruction limit reached!
% 20.39/4.24 % (1383953)------------------------------
% 20.39/4.24 % (1383953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383953)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383953)Termination reason: Instruction limit
% 20.39/4.24 % (1383953)Termination phase: Saturation
% 20.39/4.24 % (1383953)Time elapsed: 0.123 s
% 20.39/4.24 % (1383953)Peak memory usage: 89 MB
% 20.39/4.24 % (1383953)Instructions burned: 113 (million)
% 20.39/4.24 % (1383955)Instruction limit reached!
% 20.39/4.24 % (1383955)------------------------------
% 20.39/4.24 % (1383955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383955)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383955)Termination reason: Instruction limit
% 20.39/4.24 % (1383955)Termination phase: Saturation
% 20.39/4.24 % (1383955)Time elapsed: 0.116 s
% 20.39/4.24 % (1383955)Peak memory usage: 89 MB
% 20.39/4.24 % (1383955)Instructions burned: 127 (million)
% 20.39/4.24 % (1383972)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2415060268:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 20.39/4.24 % (1383974)lrs+10_1_sil=8000:sp=occurrence:random_seed=3855704254:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 20.39/4.24 % (1383975)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=760489701:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 20.39/4.24 % (1383972)Instruction limit reached!
% 20.39/4.24 % (1383972)------------------------------
% 20.39/4.24 % (1383972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383972)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383972)Termination reason: Instruction limit
% 20.39/4.24 % (1383972)Termination phase: Saturation
% 20.39/4.24 % (1383972)Time elapsed: 0.115 s
% 20.39/4.24 % (1383972)Peak memory usage: 89 MB
% 20.39/4.24 % (1383972)Instructions burned: 114 (million)
% 20.39/4.24 % (1383985)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3236422711:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 20.39/4.24 % (1383975)Instruction limit reached!
% 20.39/4.24 % (1383975)------------------------------
% 20.39/4.24 % (1383975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383975)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383975)Termination reason: Instruction limit
% 20.39/4.24 % (1383975)Termination phase: Saturation
% 20.39/4.24 % (1383975)Time elapsed: 0.354 s
% 20.39/4.24 % (1383975)Peak memory usage: 91 MB
% 20.39/4.24 % (1383975)Instructions burned: 438 (million)
% 20.39/4.24 % (1383974)Instruction limit reached!
% 20.39/4.24 % (1383974)------------------------------
% 20.39/4.24 % (1383974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383974)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383974)Termination reason: Instruction limit
% 20.39/4.24 % (1383974)Termination phase: Saturation
% 20.39/4.24 % (1383974)Time elapsed: 0.682 s
% 20.39/4.24 % (1383974)Peak memory usage: 101 MB
% 20.39/4.24 % (1383974)Instructions burned: 907 (million)
% 20.39/4.24 % (1383994)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3695166909:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 20.39/4.24 % (1383994)Refutation not found, incomplete strategy
% 20.39/4.24 % (1383994)------------------------------
% 20.39/4.24 % (1383994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383994)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383994)Termination reason: Refutation not found, incomplete strategy
% 20.39/4.24 % (1383994)Time elapsed: 0.004 s
% 20.39/4.24 % (1383994)Peak memory usage: 88 MB
% 20.39/4.24 % (1383994)Instructions burned: 2 (million)
% 20.39/4.24 % (1383999)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=659535668:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 20.39/4.24 % (1383994)------------------------------
% 20.39/4.24 % (1383994)------------------------------
% 20.39/4.24 % (1384003)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2104455892:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 20.39/4.24 % (1383999)Instruction limit reached!
% 20.39/4.24 % (1383999)------------------------------
% 20.39/4.24 % (1383999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383999)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383999)Termination reason: Instruction limit
% 20.39/4.24 % (1383999)Termination phase: Saturation
% 20.39/4.24 % (1383999)Time elapsed: 0.517 s
% 20.39/4.24 % (1383999)Peak memory usage: 97 MB
% 20.39/4.24 % (1383999)Instructions burned: 593 (million)
% 20.39/4.24 % (1383909)First to succeed.
% 20.39/4.24 % (1383909)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1383804"
% 20.39/4.24 % (1384007)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=1348220265:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/125Mi)
% 20.39/4.24 % (1384007)Instruction limit reached!
% 20.39/4.24 % (1384007)------------------------------
% 20.39/4.24 % (1384007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1384007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1384007)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1384007)Termination reason: Instruction limit
% 20.39/4.24 % (1384007)Termination phase: Saturation
% 20.39/4.24 % (1384007)Time elapsed: 0.124 s
% 20.39/4.24 % (1384007)Peak memory usage: 90 MB
% 20.39/4.24 % (1384007)Instructions burned: 125 (million)
% 20.39/4.24 % (1383952)Instruction limit reached!
% 20.39/4.24 % (1383952)------------------------------
% 20.39/4.24 % (1383952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.39/4.24 % (1383952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.39/4.24 % (1383952)CaDiCaL version: 2.1.3
% 20.39/4.24 % (1383952)Termination reason: Instruction limit
% 20.39/4.24 % (1383952)Termination phase: Saturation
% 20.39/4.24 % (1383952)Time elapsed: 2.376 s
% 20.39/4.24 % (1383952)Peak memory usage: 139 MB
% 20.39/4.24 % (1383952)Instructions burned: 2351 (million)
% 20.39/4.24 % (1383909)Refutation found. Thanks to Tanya!
% 20.39/4.24 % SZS status Theorem for theBenchmark
% 20.39/4.24 % SZS output start Proof for theBenchmark
% See solution above
% 24.26/4.47 % (1383909)------------------------------
% 24.26/4.47 % (1383909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.26/4.47 % (1383909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.26/4.47 % (1383909)CaDiCaL version: 2.1.3
% 24.26/4.47 % (1383909)Termination reason: Refutation
% 24.26/4.47 % (1383909)Time elapsed: 2.759 s
% 24.26/4.47 % (1383909)Peak memory usage: 146 MB
% 24.26/4.47 % (1383909)Instructions burned: 2751 (million)
% 24.26/4.47 % (1383909)------------------------------
% 24.26/4.47 % (1383909)------------------------------
% 24.26/4.47 % (1383804)Success in time 3.357 s
% 24.26/4.47 % Vampire exiting
%------------------------------------------------------------------------------