%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET740+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:41:47 PM UTC 2026
% Result : Theorem 10.51s 2.05s
% Output : Refutation 10.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 53
% Syntax : Number of formulae : 352 ( 58 unt; 47 def)
% Number of atoms : 1354 ( 73 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 1824 ( 822 ~; 828 |; 99 &)
% ( 58 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 55 ( 53 usr; 45 prp; 0-5 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-5 aty)
% Number of variables : 552 ( 0 sgn 518 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [X0,X1,X2] :
( maps(X0,X1,X2)
<=> ( ! [X3] :
( member(X3,X1)
=> ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) ) )
& ! [X3,X5,X6] :
( ( member(X3,X1)
& member(X5,X2)
& member(X6,X2) )
=> ( ( apply(X0,X3,X5)
& apply(X0,X3,X6) )
=> X5 = X6 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maps) ).
fof(f14,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( member(X5,X2)
& member(X6,X4) )
=> ( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
<=> ? [X7] :
( member(X7,X3)
& apply(X1,X5,X7)
& apply(X0,X7,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compose_function) ).
fof(f17,axiom,
! [X0,X1,X2] :
( injective(X0,X1,X2)
<=> ! [X3,X4,X5] :
( ( member(X3,X1)
& member(X4,X1)
& member(X5,X2) )
=> ( ( apply(X0,X3,X5)
& apply(X0,X4,X5) )
=> X3 = X4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',injective) ).
fof(f18,axiom,
! [X0,X1,X2] :
( surjective(X0,X1,X2)
<=> ! [X3] :
( member(X3,X2)
=> ? [X4] :
( member(X4,X1)
& apply(X0,X4,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',surjective) ).
fof(f19,axiom,
! [X0,X1,X2] :
( one_to_one(X0,X1,X2)
<=> ( injective(X0,X1,X2)
& surjective(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',one_to_one) ).
fof(f29,conjecture,
! [X0,X1,X2,X3,X4,X5] :
( ( maps(X0,X3,X4)
& maps(X1,X4,X5)
& maps(X2,X5,X3)
& injective(compose_function(X2,compose_function(X1,X0,X3,X4,X5),X3,X5,X3),X3,X3)
& surjective(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(X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thII31) ).
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)
& surjective(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(X1,X4,X5) ),
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(X1,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)
& surjective(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(X1,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)
& surjective(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(sK1,sK4,sK5)
& 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)
& surjective(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,
surjective(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(f61,plain,
maps(sK0,sK3,sK4),
inference(cnf_transformation,[],[f45]) ).
fof(f62,plain,
~ one_to_one(sK1,sK4,sK5),
inference(cnf_transformation,[],[f45]) ).
fof(f63,plain,
! [X2,X0,X1,X6,X7,X5] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X5,X1)
| ~ member(X6,X2)
| ~ member(X7,X2)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f46]) ).
fof(f64,plain,
! [X2,X3,X0,X1] :
( apply(X0,X3,sK6(X0,X2,X3))
| ~ member(X3,X1)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f46]) ).
fof(f65,plain,
! [X2,X3,X0,X1] :
( member(sK6(X0,X2,X3),X2)
| ~ member(X3,X1)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f46]) ).
fof(f66,plain,
! [X2,X0,X1] :
( one_to_one(X0,X1,X2)
| ~ injective(X0,X1,X2)
| ~ surjective(X0,X1,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f67,plain,
! [X2,X0,X1,X8,X6,X7] :
( X6 = X7
| ~ apply(X0,X6,X8)
| ~ apply(X0,X7,X8)
| ~ member(X6,X1)
| ~ member(X7,X1)
| ~ member(X8,X2)
| ~ injective(X0,X1,X2) ),
inference(cnf_transformation,[],[f49]) ).
fof(f68,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| member(sK9(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f49]) ).
fof(f69,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| member(sK8(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f70,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| member(sK7(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f71,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| apply(X0,sK8(X0,X1,X2),sK9(X0,X1,X2)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f72,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| apply(X0,sK7(X0,X1,X2),sK9(X0,X1,X2)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f73,plain,
! [X2,X0,X1] :
( injective(X0,X1,X2)
| sK7(X0,X1,X2) != sK8(X0,X1,X2) ),
inference(cnf_transformation,[],[f49]) ).
fof(f74,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( apply(X0,sK10(X0,X1,X3,X5,X6),X6)
| ~ apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(cnf_transformation,[],[f52]) ).
fof(f76,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( member(sK10(X0,X1,X3,X5,X6),X3)
| ~ apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(cnf_transformation,[],[f52]) ).
fof(f77,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6)
| ~ member(X5,X2)
| ~ member(X6,X4) ),
inference(cnf_transformation,[],[f52]) ).
fof(f78,plain,
! [X2,X0,X1,X5] :
( apply(X0,sK12(X0,X1,X5),X5)
| ~ member(X5,X2)
| ~ surjective(X0,X1,X2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f79,plain,
! [X2,X0,X1,X5] :
( member(sK12(X0,X1,X5),X1)
| ~ member(X5,X2)
| ~ surjective(X0,X1,X2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f80,plain,
! [X2,X0,X1] :
( surjective(X0,X1,X2)
| member(sK11(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f81,plain,
! [X2,X0,X1,X4] :
( surjective(X0,X1,X2)
| ~ member(X4,X1)
| ~ apply(X0,X4,sK11(X0,X1,X2)) ),
inference(cnf_transformation,[],[f55]) ).
fof(f82,plain,
! [X2,X0,X1,X5] :
( ~ member(X5,X1)
| ~ maps(X0,X1,X2)
| sP13(X5,X2,X0) ),
inference(cnf_transformation,[],[f82_D]) ).
fof(f82_D,definition,
! [X0,X2,X5] :
( ! [X1] :
( ~ member(X5,X1)
| ~ maps(X0,X1,X2) )
<=> ~ sP13(X5,X2,X0) ),
introduced(definition,[new_symbols(definition,[sP13])],[general_splitting_component_introduction]) ).
fof(f83,plain,
! [X2,X0,X6,X7,X5] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X6,X2)
| ~ member(X7,X2)
| ~ sP13(X5,X2,X0) ),
inference(general_splitting,[],[f63,f82_D]) ).
fof(f84,plain,
! [X2,X0,X1,X8] :
( ~ member(X8,X2)
| ~ injective(X0,X1,X2)
| sP14(X1,X0,X8) ),
inference(cnf_transformation,[],[f84_D]) ).
fof(f84_D,definition,
! [X8,X0,X1] :
( ! [X2] :
( ~ member(X8,X2)
| ~ injective(X0,X1,X2) )
<=> ~ sP14(X1,X0,X8) ),
introduced(definition,[new_symbols(definition,[sP14])],[general_splitting_component_introduction]) ).
fof(f85,plain,
! [X0,X1,X8,X6,X7] :
( X6 = X7
| ~ apply(X0,X6,X8)
| ~ apply(X0,X7,X8)
| ~ member(X6,X1)
| ~ member(X7,X1)
| ~ sP14(X1,X0,X8) ),
inference(general_splitting,[],[f67,f84_D]) ).
fof(f86,plain,
! [X3,X0,X1,X6,X7,X5] :
( ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6)
| sP15(X5,X6,X0,X3,X1) ),
inference(cnf_transformation,[],[f86_D]) ).
fof(f86_D,definition,
! [X1,X3,X0,X6,X5] :
( ! [X7] :
( ~ member(X7,X3)
| ~ apply(X1,X5,X7)
| ~ apply(X0,X7,X6) )
<=> ~ sP15(X5,X6,X0,X3,X1) ),
introduced(definition,[new_symbols(definition,[sP15])],[general_splitting_component_introduction]) ).
fof(f87,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( apply(compose_function(X0,X1,X2,X3,X4),X5,X6)
| ~ member(X5,X2)
| ~ member(X6,X4)
| ~ sP15(X5,X6,X0,X3,X1) ),
inference(general_splitting,[],[f77,f86_D]) ).
fof(f89,definition,
( spl16_1
<=> one_to_one(sK1,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f91,plain,
( ~ one_to_one(sK1,sK4,sK5)
| spl16_1 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f92,plain,
~ spl16_1,
inference(avatar_split_clause,[],[f62,f89]) ).
fof(f93,plain,
( ~ injective(sK1,sK4,sK5)
| ~ surjective(sK1,sK4,sK5)
| spl16_1 ),
inference(resolution,[],[f91,f66]) ).
fof(f95,definition,
( spl16_2
<=> injective(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),sK3,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f97,plain,
( injective(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),sK3,sK3)
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f95]) ).
fof(f98,plain,
spl16_2,
inference(avatar_split_clause,[],[f58,f95]) ).
fof(f100,definition,
( spl16_3
<=> surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition]) ).
fof(f102,plain,
( surjective(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,sK5)
| ~ spl16_3 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,plain,
spl16_3,
inference(avatar_split_clause,[],[f56,f100]) ).
fof(f104,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_3 ),
inference(resolution,[],[f102,f78]) ).
fof(f105,plain,
( ! [X0] :
( member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) )
| ~ spl16_3 ),
inference(resolution,[],[f102,f79]) ).
fof(f108,plain,
( ! [X0] :
( ~ member(X0,sK3)
| sP14(sK3,compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X0) )
| ~ spl16_2 ),
inference(resolution,[],[f97,f84]) ).
fof(f110,definition,
( spl16_4
<=> surjective(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition]) ).
fof(f112,plain,
( surjective(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK4)
| ~ spl16_4 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f113,plain,
spl16_4,
inference(avatar_split_clause,[],[f57,f110]) ).
fof(f115,definition,
( spl16_5
<=> ! [X0] :
( ~ member(X0,sK3)
| sP14(sK3,compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition]) ).
fof(f116,plain,
( ! [X0] :
( sP14(sK3,compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X0)
| ~ member(X0,sK3) )
| ~ spl16_5 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f117,plain,
( spl16_5
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f108,f95,f115]) ).
fof(f123,plain,
( ! [X0] :
( apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0)
| ~ member(X0,sK4) )
| ~ spl16_4 ),
inference(resolution,[],[f112,f78]) ).
fof(f124,plain,
( ! [X0] :
( member(sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),sK4)
| ~ member(X0,sK4) )
| ~ spl16_4 ),
inference(resolution,[],[f112,f79]) ).
fof(f127,definition,
( spl16_7
<=> maps(sK0,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl16_7])],[avatar_definition]) ).
fof(f129,plain,
( maps(sK0,sK3,sK4)
| ~ spl16_7 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f130,plain,
spl16_7,
inference(avatar_split_clause,[],[f61,f127]) ).
fof(f133,plain,
( ! [X0] :
( ~ member(X0,sK3)
| sP13(X0,sK4,sK0) )
| ~ spl16_7 ),
inference(resolution,[],[f129,f82]) ).
fof(f145,definition,
( spl16_9
<=> maps(sK2,sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl16_9])],[avatar_definition]) ).
fof(f147,plain,
( maps(sK2,sK5,sK3)
| ~ spl16_9 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f148,plain,
spl16_9,
inference(avatar_split_clause,[],[f59,f145]) ).
fof(f149,plain,
( ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) )
| ~ spl16_9 ),
inference(resolution,[],[f147,f64]) ).
fof(f150,plain,
( ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) )
| ~ spl16_9 ),
inference(resolution,[],[f147,f65]) ).
fof(f153,definition,
( spl16_10
<=> ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_10])],[avatar_definition]) ).
fof(f154,plain,
( ! [X0] :
( apply(sK2,X0,sK6(sK2,sK3,X0))
| ~ member(X0,sK5) )
| ~ spl16_10 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f155,plain,
( spl16_10
| ~ spl16_9 ),
inference(avatar_split_clause,[],[f149,f145,f153]) ).
fof(f160,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_10 ),
inference(resolution,[],[f154,f86]) ).
fof(f184,definition,
( spl16_14
<=> ! [X0] :
( ~ member(X0,sK3)
| sP13(X0,sK4,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl16_14])],[avatar_definition]) ).
fof(f185,plain,
( ! [X0] :
( sP13(X0,sK4,sK0)
| ~ member(X0,sK3) )
| ~ spl16_14 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f186,plain,
( spl16_14
| ~ spl16_7 ),
inference(avatar_split_clause,[],[f133,f127,f184]) ).
fof(f188,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK3)
| X1 = X2
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X1,X0)
| ~ apply(compose_function(sK2,compose_function(sK1,sK0,sK3,sK4,sK5),sK3,sK5,sK3),X2,X0)
| ~ member(X1,sK3)
| ~ member(X2,sK3) )
| ~ spl16_5 ),
inference(resolution,[],[f116,f85]) ).
fof(f198,definition,
( spl16_17
<=> ! [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_17])],[avatar_definition]) ).
fof(f199,plain,
( ! [X0] :
( member(sK12(compose_function(sK1,compose_function(sK0,sK2,sK5,sK3,sK4),sK5,sK4,sK5),sK5,X0),sK5)
| ~ member(X0,sK5) )
| ~ spl16_17 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f200,plain,
( spl16_17
| ~ spl16_3 ),
inference(avatar_split_clause,[],[f105,f100,f198]) ).
fof(f222,definition,
( spl16_18
<=> ! [X0] :
( member(sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),sK4)
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_18])],[avatar_definition]) ).
fof(f223,plain,
( ! [X0] :
( member(sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),sK4)
| ~ member(X0,sK4) )
| ~ spl16_18 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f224,plain,
( spl16_18
| ~ spl16_4 ),
inference(avatar_split_clause,[],[f124,f110,f222]) ).
fof(f246,definition,
( spl16_19
<=> ! [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_19])],[avatar_definition]) ).
fof(f247,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_19 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f248,plain,
( spl16_19
| ~ spl16_3 ),
inference(avatar_split_clause,[],[f104,f100,f246]) ).
fof(f249,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_19 ),
inference(resolution,[],[f247,f74]) ).
fof(f251,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_19 ),
inference(resolution,[],[f247,f76]) ).
fof(f259,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_19 ),
inference(duplicate_literal_removal,[],[f251]) ).
fof(f261,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_19 ),
inference(duplicate_literal_removal,[],[f249]) ).
fof(f262,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_17
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f259,f199]) ).
fof(f264,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_17
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f261,f199]) ).
fof(f266,definition,
( spl16_20
<=> ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_20])],[avatar_definition]) ).
fof(f267,plain,
( ! [X0] :
( member(sK6(sK2,sK3,X0),sK3)
| ~ member(X0,sK5) )
| ~ spl16_20 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f268,plain,
( spl16_20
| ~ spl16_9 ),
inference(avatar_split_clause,[],[f150,f145,f266]) ).
fof(f270,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sK3)
| X1 = X2
| ~ apply(sK0,X0,X1)
| ~ apply(sK0,X0,X2)
| ~ member(X1,sK4)
| ~ member(X2,sK4) )
| ~ spl16_14 ),
inference(resolution,[],[f185,f83]) ).
fof(f332,definition,
( spl16_21
<=> ! [X0] :
( apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0)
| ~ member(X0,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_21])],[avatar_definition]) ).
fof(f333,plain,
( ! [X0] :
( apply(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0)
| ~ member(X0,sK4) )
| ~ spl16_21 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f334,plain,
( spl16_21
| ~ spl16_4 ),
inference(avatar_split_clause,[],[f123,f110,f332]) ).
fof(f335,plain,
( ! [X0] :
( ~ member(X0,sK4)
| apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),X0)
| ~ member(sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),sK4)
| ~ member(X0,sK4) )
| ~ spl16_21 ),
inference(resolution,[],[f333,f74]) ).
fof(f337,plain,
( ! [X0] :
( ~ member(X0,sK4)
| member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),sK3)
| ~ member(sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),sK4)
| ~ member(X0,sK4) )
| ~ spl16_21 ),
inference(resolution,[],[f333,f76]) ).
fof(f345,plain,
( ! [X0] :
( ~ member(X0,sK4)
| member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),sK3)
| ~ member(sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),sK4) )
| ~ spl16_21 ),
inference(duplicate_literal_removal,[],[f337]) ).
fof(f347,plain,
( ! [X0] :
( ~ member(X0,sK4)
| apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),X0)
| ~ member(sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),sK4) )
| ~ spl16_21 ),
inference(duplicate_literal_removal,[],[f335]) ).
fof(f348,plain,
( ! [X0] :
( ~ member(X0,sK4)
| member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),sK3) )
| ~ spl16_18
| ~ spl16_21 ),
inference(forward_subsumption_resolution,[],[f345,f223]) ).
fof(f350,plain,
( ! [X0] :
( ~ member(X0,sK4)
| apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),X0) )
| ~ spl16_18
| ~ spl16_21 ),
inference(forward_subsumption_resolution,[],[f347,f223]) ).
fof(f352,definition,
( spl16_22
<=> ! [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_22])],[avatar_definition]) ).
fof(f353,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_22 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f354,plain,
( spl16_22
| ~ spl16_17
| ~ spl16_19 ),
inference(avatar_split_clause,[],[f264,f246,f198,f352]) ).
fof(f361,plain,
( ! [X0,X1] :
( ~ member(sK11(sK1,X0,X1),sK5)
| surjective(sK1,X0,X1)
| ~ 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,sK11(sK1,X0,X1)),sK11(sK1,X0,X1)),X0) )
| ~ spl16_22 ),
inference(resolution,[],[f353,f81]) ).
fof(f363,definition,
( spl16_23
<=> ! [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_23])],[avatar_definition]) ).
fof(f364,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_23 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f365,plain,
( spl16_23
| ~ spl16_17
| ~ spl16_19 ),
inference(avatar_split_clause,[],[f262,f246,f198,f363]) ).
fof(f387,definition,
( spl16_24
<=> ! [X0] :
( ~ member(X0,sK4)
| apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_24])],[avatar_definition]) ).
fof(f388,plain,
( ! [X0] :
( apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),X0)
| ~ member(X0,sK4) )
| ~ spl16_24 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f389,plain,
( spl16_24
| ~ spl16_18
| ~ spl16_21 ),
inference(avatar_split_clause,[],[f350,f332,f222,f387]) ).
fof(f398,definition,
( spl16_25
<=> ! [X0] :
( ~ member(X0,sK4)
| member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_25])],[avatar_definition]) ).
fof(f399,plain,
( ! [X0] :
( member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X0),X0),sK3)
| ~ member(X0,sK4) )
| ~ spl16_25 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f400,plain,
( spl16_25
| ~ spl16_18
| ~ spl16_21 ),
inference(avatar_split_clause,[],[f348,f332,f222,f398]) ).
fof(f438,definition,
( spl16_27
<=> ! [X2,X0,X1] :
( ~ member(X0,sK3)
| X1 = X2
| ~ apply(sK0,X0,X1)
| ~ apply(sK0,X0,X2)
| ~ member(X1,sK4)
| ~ member(X2,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_27])],[avatar_definition]) ).
fof(f439,plain,
( ! [X2,X0,X1] :
( ~ apply(sK0,X0,X2)
| X1 = X2
| ~ apply(sK0,X0,X1)
| ~ member(X0,sK3)
| ~ member(X1,sK4)
| ~ member(X2,sK4) )
| ~ spl16_27 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f440,plain,
( spl16_27
| ~ spl16_14 ),
inference(avatar_split_clause,[],[f270,f184,f438]) ).
fof(f442,plain,
( ! [X0,X1] :
( X0 = X1
| ~ apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X1),X1),X0)
| ~ member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X1),X1),sK3)
| ~ member(X0,sK4)
| ~ member(X1,sK4)
| ~ member(X1,sK4) )
| ~ spl16_24
| ~ spl16_27 ),
inference(resolution,[],[f439,f388]) ).
fof(f449,plain,
( ! [X0,X1] :
( X0 = X1
| ~ apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X1),X1),X0)
| ~ member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X1),X1),sK3)
| ~ member(X0,sK4)
| ~ member(X1,sK4) )
| ~ spl16_24
| ~ spl16_27 ),
inference(duplicate_literal_removal,[],[f442]) ).
fof(f451,plain,
( ! [X0,X1] :
( X0 = X1
| ~ apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X1),X1),X0)
| ~ member(X0,sK4)
| ~ member(X1,sK4) )
| ~ spl16_24
| ~ spl16_25
| ~ spl16_27 ),
inference(forward_subsumption_resolution,[],[f449,f399]) ).
fof(f953,definition,
( spl16_61
<=> surjective(sK1,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_61])],[avatar_definition]) ).
fof(f955,plain,
( ~ surjective(sK1,sK4,sK5)
| spl16_61 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f957,definition,
( spl16_62
<=> injective(sK1,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_62])],[avatar_definition]) ).
fof(f959,plain,
( ~ injective(sK1,sK4,sK5)
| spl16_62 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f960,plain,
( ~ spl16_61
| ~ spl16_62
| spl16_1 ),
inference(avatar_split_clause,[],[f93,f89,f957,f953]) ).
fof(f970,plain,
( member(sK9(sK1,sK4,sK5),sK5)
| spl16_62 ),
inference(resolution,[],[f959,f68]) ).
fof(f971,plain,
( member(sK8(sK1,sK4,sK5),sK4)
| spl16_62 ),
inference(resolution,[],[f959,f69]) ).
fof(f972,plain,
( member(sK7(sK1,sK4,sK5),sK4)
| spl16_62 ),
inference(resolution,[],[f959,f70]) ).
fof(f973,plain,
( apply(sK1,sK8(sK1,sK4,sK5),sK9(sK1,sK4,sK5))
| spl16_62 ),
inference(resolution,[],[f959,f71]) ).
fof(f974,plain,
( apply(sK1,sK7(sK1,sK4,sK5),sK9(sK1,sK4,sK5))
| spl16_62 ),
inference(resolution,[],[f959,f72]) ).
fof(f975,plain,
( sK8(sK1,sK4,sK5) != sK7(sK1,sK4,sK5)
| spl16_62 ),
inference(resolution,[],[f959,f73]) ).
fof(f977,definition,
( spl16_64
<=> apply(sK1,sK8(sK1,sK4,sK5),sK9(sK1,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl16_64])],[avatar_definition]) ).
fof(f979,plain,
( apply(sK1,sK8(sK1,sK4,sK5),sK9(sK1,sK4,sK5))
| ~ spl16_64 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f980,plain,
( spl16_64
| spl16_62 ),
inference(avatar_split_clause,[],[f973,f957,f977]) ).
fof(f991,definition,
( spl16_65
<=> apply(sK1,sK7(sK1,sK4,sK5),sK9(sK1,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl16_65])],[avatar_definition]) ).
fof(f993,plain,
( apply(sK1,sK7(sK1,sK4,sK5),sK9(sK1,sK4,sK5))
| ~ spl16_65 ),
inference(avatar_component_clause,[],[f991]) ).
fof(f994,plain,
( spl16_65
| spl16_62 ),
inference(avatar_split_clause,[],[f974,f957,f991]) ).
fof(f996,definition,
( spl16_66
<=> member(sK8(sK1,sK4,sK5),sK4) ),
introduced(definition,[new_symbols(definition,[spl16_66])],[avatar_definition]) ).
fof(f998,plain,
( member(sK8(sK1,sK4,sK5),sK4)
| ~ spl16_66 ),
inference(avatar_component_clause,[],[f996]) ).
fof(f999,plain,
( spl16_66
| spl16_62 ),
inference(avatar_split_clause,[],[f971,f957,f996]) ).
fof(f1010,definition,
( spl16_67
<=> member(sK7(sK1,sK4,sK5),sK4) ),
introduced(definition,[new_symbols(definition,[spl16_67])],[avatar_definition]) ).
fof(f1012,plain,
( member(sK7(sK1,sK4,sK5),sK4)
| ~ spl16_67 ),
inference(avatar_component_clause,[],[f1010]) ).
fof(f1013,plain,
( spl16_67
| spl16_62 ),
inference(avatar_split_clause,[],[f972,f957,f1010]) ).
fof(f1055,definition,
( spl16_68
<=> sK8(sK1,sK4,sK5) = sK7(sK1,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl16_68])],[avatar_definition]) ).
fof(f1057,plain,
( sK8(sK1,sK4,sK5) != sK7(sK1,sK4,sK5)
| spl16_68 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1058,plain,
( ~ spl16_68
| spl16_62 ),
inference(avatar_split_clause,[],[f975,f957,f1055]) ).
fof(f1082,definition,
( spl16_71
<=> member(sK9(sK1,sK4,sK5),sK5) ),
introduced(definition,[new_symbols(definition,[spl16_71])],[avatar_definition]) ).
fof(f1084,plain,
( member(sK9(sK1,sK4,sK5),sK5)
| ~ spl16_71 ),
inference(avatar_component_clause,[],[f1082]) ).
fof(f1085,plain,
( spl16_71
| spl16_62 ),
inference(avatar_split_clause,[],[f970,f957,f1082]) ).
fof(f1251,definition,
( spl16_81
<=> ! [X0] :
( surjective(sK1,sK4,X0)
| ~ member(sK11(sK1,sK4,X0),sK5) ) ),
introduced(definition,[new_symbols(definition,[spl16_81])],[avatar_definition]) ).
fof(f1252,plain,
( ! [X0] :
( ~ member(sK11(sK1,sK4,X0),sK5)
| surjective(sK1,sK4,X0) )
| ~ spl16_81 ),
inference(avatar_component_clause,[],[f1251]) ).
fof(f1254,plain,
( surjective(sK1,sK4,sK5)
| surjective(sK1,sK4,sK5)
| ~ spl16_81 ),
inference(resolution,[],[f1252,f80]) ).
fof(f1255,plain,
( surjective(sK1,sK4,sK5)
| ~ spl16_81 ),
inference(duplicate_literal_removal,[],[f1254]) ).
fof(f1257,definition,
( spl16_82
<=> ! [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_82])],[avatar_definition]) ).
fof(f1258,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_82 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1259,plain,
( spl16_82
| ~ spl16_10 ),
inference(avatar_split_clause,[],[f160,f153,f1257]) ).
fof(f1260,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_82 ),
inference(resolution,[],[f1258,f87]) ).
fof(f1505,definition,
( spl16_99
<=> ! [X0,X1] :
( ~ member(sK11(sK1,X0,X1),sK5)
| surjective(sK1,X0,X1)
| ~ 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,sK11(sK1,X0,X1)),sK11(sK1,X0,X1)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_99])],[avatar_definition]) ).
fof(f1506,plain,
( ! [X0,X1] :
( ~ 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,sK11(sK1,X0,X1)),sK11(sK1,X0,X1)),X0)
| surjective(sK1,X0,X1)
| ~ member(sK11(sK1,X0,X1),sK5) )
| ~ spl16_99 ),
inference(avatar_component_clause,[],[f1505]) ).
fof(f1507,plain,
( spl16_99
| ~ spl16_22 ),
inference(avatar_split_clause,[],[f361,f352,f1505]) ).
fof(f1509,plain,
( ! [X0] :
( surjective(sK1,sK4,X0)
| ~ member(sK11(sK1,sK4,X0),sK5)
| ~ member(sK11(sK1,sK4,X0),sK5) )
| ~ spl16_23
| ~ spl16_99 ),
inference(resolution,[],[f1506,f364]) ).
fof(f1510,plain,
( ! [X0] :
( surjective(sK1,sK4,X0)
| ~ member(sK11(sK1,sK4,X0),sK5) )
| ~ spl16_23
| ~ spl16_99 ),
inference(duplicate_literal_removal,[],[f1509]) ).
fof(f1847,definition,
( spl16_118
<=> ! [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_118])],[avatar_definition]) ).
fof(f1848,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_118 ),
inference(avatar_component_clause,[],[f1847]) ).
fof(f1849,plain,
( spl16_118
| ~ spl16_5 ),
inference(avatar_split_clause,[],[f188,f115,f1847]) ).
fof(f5151,definition,
( spl16_253
<=> ! [X0,X1] :
( X0 = X1
| ~ apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X1),X1),X0)
| ~ member(X0,sK4)
| ~ member(X1,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl16_253])],[avatar_definition]) ).
fof(f5152,plain,
( ! [X0,X1] :
( ~ apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,X1),X1),X0)
| X0 = X1
| ~ member(X0,sK4)
| ~ member(X1,sK4) )
| ~ spl16_253 ),
inference(avatar_component_clause,[],[f5151]) ).
fof(f5153,plain,
( spl16_253
| ~ spl16_24
| ~ spl16_25
| ~ spl16_27 ),
inference(avatar_split_clause,[],[f451,f438,f398,f387,f5151]) ).
fof(f5683,plain,
( $false
| spl16_61
| ~ spl16_81 ),
inference(forward_subsumption_resolution,[],[f1255,f955]) ).
fof(f5684,plain,
( spl16_61
| ~ spl16_81 ),
inference(avatar_contradiction_clause,[],[f5683]) ).
fof(f5817,plain,
( spl16_81
| ~ spl16_23
| ~ spl16_99 ),
inference(avatar_split_clause,[],[f1510,f1505,f363,f1251]) ).
fof(f7631,definition,
( spl16_344
<=> ! [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_344])],[avatar_definition]) ).
fof(f7632,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_344 ),
inference(avatar_component_clause,[],[f7631]) ).
fof(f7633,plain,
( spl16_344
| ~ spl16_82 ),
inference(avatar_split_clause,[],[f1260,f1257,f7631]) ).
fof(f7634,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_118
| ~ spl16_344 ),
inference(resolution,[],[f7632,f1848]) ).
fof(f7669,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_118
| ~ spl16_344 ),
inference(duplicate_literal_removal,[],[f7634]) ).
fof(f7674,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_20
| ~ spl16_118
| ~ spl16_344 ),
inference(forward_subsumption_resolution,[],[f7669,f267]) ).
fof(f7678,definition,
( spl16_345
<=> ! [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_345])],[avatar_definition]) ).
fof(f7679,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_345 ),
inference(avatar_component_clause,[],[f7678]) ).
fof(f7680,plain,
( spl16_345
| ~ spl16_20
| ~ spl16_118
| ~ spl16_344 ),
inference(avatar_split_clause,[],[f7674,f7631,f1847,f266,f7678]) ).
fof(f7681,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_344
| ~ spl16_345 ),
inference(resolution,[],[f7679,f7632]) ).
fof(f7691,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_344
| ~ spl16_345 ),
inference(duplicate_literal_removal,[],[f7681]) ).
fof(f7694,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_20
| ~ spl16_344
| ~ spl16_345 ),
inference(forward_subsumption_resolution,[],[f7691,f267]) ).
fof(f7697,definition,
( spl16_346
<=> ! [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_346])],[avatar_definition]) ).
fof(f7698,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_346 ),
inference(avatar_component_clause,[],[f7697]) ).
fof(f7699,plain,
( spl16_346
| ~ spl16_20
| ~ spl16_344
| ~ spl16_345 ),
inference(avatar_split_clause,[],[f7694,f7678,f7631,f266,f7697]) ).
fof(f7702,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_346 ),
inference(resolution,[],[f7698,f87]) ).
fof(f7721,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_346 ),
inference(duplicate_literal_removal,[],[f7702]) ).
fof(f7729,definition,
( spl16_347
<=> ! [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_347])],[avatar_definition]) ).
fof(f7730,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_347 ),
inference(avatar_component_clause,[],[f7729]) ).
fof(f7731,plain,
( spl16_347
| ~ spl16_346 ),
inference(avatar_split_clause,[],[f7721,f7697,f7729]) ).
fof(f7734,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_347 ),
inference(resolution,[],[f7730,f87]) ).
fof(f7753,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_347 ),
inference(duplicate_literal_removal,[],[f7734]) ).
fof(f7761,definition,
( spl16_348
<=> ! [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_348])],[avatar_definition]) ).
fof(f7762,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_348 ),
inference(avatar_component_clause,[],[f7761]) ).
fof(f7763,plain,
( spl16_348
| ~ spl16_347 ),
inference(avatar_split_clause,[],[f7753,f7729,f7761]) ).
fof(f7764,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_348 ),
inference(resolution,[],[f7762,f86]) ).
fof(f7773,definition,
( spl16_349
<=> ! [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_349])],[avatar_definition]) ).
fof(f7774,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_349 ),
inference(avatar_component_clause,[],[f7773]) ).
fof(f7775,plain,
( spl16_349
| ~ spl16_348 ),
inference(avatar_split_clause,[],[f7764,f7761,f7773]) ).
fof(f7776,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ member(X0,sK3)
| ~ member(X1,sK5)
| X0 = X2
| ~ member(X2,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X0,X3)
| ~ apply(sK1,X3,X1)
| ~ member(X4,sK4)
| ~ apply(sK0,X2,X4)
| ~ apply(sK1,X4,X1) )
| ~ spl16_349 ),
inference(resolution,[],[f7774,f86]) ).
fof(f7786,definition,
( spl16_350
<=> ! [X4,X0,X3,X2,X1] :
( ~ member(X0,sK3)
| ~ member(X1,sK5)
| X0 = X2
| ~ member(X2,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X0,X3)
| ~ apply(sK1,X3,X1)
| ~ member(X4,sK4)
| ~ apply(sK0,X2,X4)
| ~ apply(sK1,X4,X1) ) ),
introduced(definition,[new_symbols(definition,[spl16_350])],[avatar_definition]) ).
fof(f7787,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ apply(sK1,X4,X1)
| ~ member(X1,sK5)
| X0 = X2
| ~ member(X2,sK3)
| ~ member(X3,sK4)
| ~ apply(sK0,X0,X3)
| ~ apply(sK1,X3,X1)
| ~ member(X4,sK4)
| ~ apply(sK0,X2,X4)
| ~ member(X0,sK3) )
| ~ spl16_350 ),
inference(avatar_component_clause,[],[f7786]) ).
fof(f7788,plain,
( spl16_350
| ~ spl16_349 ),
inference(avatar_split_clause,[],[f7776,f7773,f7786]) ).
fof(f7793,plain,
( ! [X2,X0,X1] :
( ~ member(sK9(sK1,sK4,sK5),sK5)
| X0 = X1
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| ~ apply(sK1,X2,sK9(sK1,sK4,sK5))
| ~ member(sK8(sK1,sK4,sK5),sK4)
| ~ apply(sK0,X1,sK8(sK1,sK4,sK5))
| ~ member(X0,sK3) )
| ~ spl16_64
| ~ spl16_350 ),
inference(resolution,[],[f7787,f979]) ).
fof(f7832,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| ~ apply(sK1,X2,sK9(sK1,sK4,sK5))
| ~ member(sK8(sK1,sK4,sK5),sK4)
| ~ apply(sK0,X1,sK8(sK1,sK4,sK5))
| ~ member(X0,sK3) )
| ~ spl16_64
| ~ spl16_71
| ~ spl16_350 ),
inference(forward_subsumption_resolution,[],[f7793,f1084]) ).
fof(f7839,plain,
( ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| ~ apply(sK1,X2,sK9(sK1,sK4,sK5))
| ~ apply(sK0,X1,sK8(sK1,sK4,sK5))
| ~ member(X0,sK3) )
| ~ spl16_64
| ~ spl16_66
| ~ spl16_71
| ~ spl16_350 ),
inference(forward_subsumption_resolution,[],[f7832,f998]) ).
fof(f8061,definition,
( spl16_359
<=> ! [X2,X0,X1] :
( X0 = X1
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| ~ apply(sK1,X2,sK9(sK1,sK4,sK5))
| ~ apply(sK0,X1,sK8(sK1,sK4,sK5))
| ~ member(X0,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_359])],[avatar_definition]) ).
fof(f8062,plain,
( ! [X2,X0,X1] :
( ~ apply(sK1,X2,sK9(sK1,sK4,sK5))
| ~ member(X1,sK3)
| ~ member(X2,sK4)
| ~ apply(sK0,X0,X2)
| X0 = X1
| ~ apply(sK0,X1,sK8(sK1,sK4,sK5))
| ~ member(X0,sK3) )
| ~ spl16_359 ),
inference(avatar_component_clause,[],[f8061]) ).
fof(f8063,plain,
( spl16_359
| ~ spl16_64
| ~ spl16_66
| ~ spl16_71
| ~ spl16_350 ),
inference(avatar_split_clause,[],[f7839,f7786,f1082,f996,f977,f8061]) ).
fof(f8064,plain,
( ! [X0,X1] :
( ~ member(X0,sK3)
| ~ member(sK7(sK1,sK4,sK5),sK4)
| ~ apply(sK0,X1,sK7(sK1,sK4,sK5))
| X0 = X1
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5))
| ~ member(X1,sK3) )
| ~ spl16_65
| ~ spl16_359 ),
inference(resolution,[],[f8062,f993]) ).
fof(f8079,plain,
( ! [X0,X1] :
( ~ member(X0,sK3)
| ~ apply(sK0,X1,sK7(sK1,sK4,sK5))
| X0 = X1
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5))
| ~ member(X1,sK3) )
| ~ spl16_65
| ~ spl16_67
| ~ spl16_359 ),
inference(forward_subsumption_resolution,[],[f8064,f1012]) ).
fof(f8121,definition,
( spl16_362
<=> ! [X0,X1] :
( ~ member(X0,sK3)
| ~ apply(sK0,X1,sK7(sK1,sK4,sK5))
| X0 = X1
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5))
| ~ member(X1,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl16_362])],[avatar_definition]) ).
fof(f8122,plain,
( ! [X0,X1] :
( ~ apply(sK0,X1,sK7(sK1,sK4,sK5))
| ~ member(X0,sK3)
| X0 = X1
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5))
| ~ member(X1,sK3) )
| ~ spl16_362 ),
inference(avatar_component_clause,[],[f8121]) ).
fof(f8123,plain,
( spl16_362
| ~ spl16_65
| ~ spl16_67
| ~ spl16_359 ),
inference(avatar_split_clause,[],[f8079,f8061,f1010,f991,f8121]) ).
fof(f8124,plain,
( ! [X0] :
( ~ member(X0,sK3)
| sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK7(sK1,sK4,sK5)),sK7(sK1,sK4,sK5)) = X0
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5))
| ~ member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK7(sK1,sK4,sK5)),sK7(sK1,sK4,sK5)),sK3)
| ~ member(sK7(sK1,sK4,sK5),sK4) )
| ~ spl16_24
| ~ spl16_362 ),
inference(resolution,[],[f8122,f388]) ).
fof(f8128,plain,
( ! [X0] :
( ~ member(X0,sK3)
| sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK7(sK1,sK4,sK5)),sK7(sK1,sK4,sK5)) = X0
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5))
| ~ member(sK7(sK1,sK4,sK5),sK4) )
| ~ spl16_24
| ~ spl16_25
| ~ spl16_362 ),
inference(forward_subsumption_resolution,[],[f8124,f399]) ).
fof(f8129,plain,
( ! [X0] :
( ~ member(X0,sK3)
| sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK7(sK1,sK4,sK5)),sK7(sK1,sK4,sK5)) = X0
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5)) )
| ~ spl16_24
| ~ spl16_25
| ~ spl16_67
| ~ spl16_362 ),
inference(forward_subsumption_resolution,[],[f8128,f1012]) ).
fof(f8568,definition,
( spl16_378
<=> ! [X0] :
( ~ member(X0,sK3)
| sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK7(sK1,sK4,sK5)),sK7(sK1,sK4,sK5)) = X0
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5)) ) ),
introduced(definition,[new_symbols(definition,[spl16_378])],[avatar_definition]) ).
fof(f8569,plain,
( ! [X0] :
( sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK7(sK1,sK4,sK5)),sK7(sK1,sK4,sK5)) = X0
| ~ member(X0,sK3)
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5)) )
| ~ spl16_378 ),
inference(avatar_component_clause,[],[f8568]) ).
fof(f8570,plain,
( spl16_378
| ~ spl16_24
| ~ spl16_25
| ~ spl16_67
| ~ spl16_362 ),
inference(avatar_split_clause,[],[f8129,f8121,f1010,f398,f387,f8568]) ).
fof(f8574,plain,
( ! [X0] :
( apply(sK0,X0,sK7(sK1,sK4,sK5))
| ~ member(sK7(sK1,sK4,sK5),sK4)
| ~ member(X0,sK3)
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5)) )
| ~ spl16_24
| ~ spl16_378 ),
inference(superposition,[],[f388,f8569]) ).
fof(f8594,plain,
( ! [X0] :
( apply(sK0,X0,sK7(sK1,sK4,sK5))
| ~ member(X0,sK3)
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5)) )
| ~ spl16_24
| ~ spl16_67
| ~ spl16_378 ),
inference(forward_subsumption_resolution,[],[f8574,f1012]) ).
fof(f8597,definition,
( spl16_379
<=> ! [X0] :
( apply(sK0,X0,sK7(sK1,sK4,sK5))
| ~ member(X0,sK3)
| ~ apply(sK0,X0,sK8(sK1,sK4,sK5)) ) ),
introduced(definition,[new_symbols(definition,[spl16_379])],[avatar_definition]) ).
fof(f8598,plain,
( ! [X0] :
( ~ apply(sK0,X0,sK8(sK1,sK4,sK5))
| ~ member(X0,sK3)
| apply(sK0,X0,sK7(sK1,sK4,sK5)) )
| ~ spl16_379 ),
inference(avatar_component_clause,[],[f8597]) ).
fof(f8599,plain,
( spl16_379
| ~ spl16_24
| ~ spl16_67
| ~ spl16_378 ),
inference(avatar_split_clause,[],[f8594,f8568,f1010,f387,f8597]) ).
fof(f8600,plain,
( ~ member(sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK8(sK1,sK4,sK5)),sK8(sK1,sK4,sK5)),sK3)
| apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK8(sK1,sK4,sK5)),sK8(sK1,sK4,sK5)),sK7(sK1,sK4,sK5))
| ~ member(sK8(sK1,sK4,sK5),sK4)
| ~ spl16_24
| ~ spl16_379 ),
inference(resolution,[],[f8598,f388]) ).
fof(f8604,plain,
( apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK8(sK1,sK4,sK5)),sK8(sK1,sK4,sK5)),sK7(sK1,sK4,sK5))
| ~ member(sK8(sK1,sK4,sK5),sK4)
| ~ spl16_24
| ~ spl16_25
| ~ spl16_379 ),
inference(forward_subsumption_resolution,[],[f8600,f399]) ).
fof(f8605,plain,
( apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK8(sK1,sK4,sK5)),sK8(sK1,sK4,sK5)),sK7(sK1,sK4,sK5))
| ~ spl16_24
| ~ spl16_25
| ~ spl16_66
| ~ spl16_379 ),
inference(forward_subsumption_resolution,[],[f8604,f998]) ).
fof(f8607,definition,
( spl16_380
<=> apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK8(sK1,sK4,sK5)),sK8(sK1,sK4,sK5)),sK7(sK1,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl16_380])],[avatar_definition]) ).
fof(f8609,plain,
( apply(sK0,sK10(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK3,sK12(compose_function(sK0,compose_function(sK2,sK1,sK4,sK5,sK3),sK4,sK3,sK4),sK4,sK8(sK1,sK4,sK5)),sK8(sK1,sK4,sK5)),sK7(sK1,sK4,sK5))
| ~ spl16_380 ),
inference(avatar_component_clause,[],[f8607]) ).
fof(f8610,plain,
( spl16_380
| ~ spl16_24
| ~ spl16_25
| ~ spl16_66
| ~ spl16_379 ),
inference(avatar_split_clause,[],[f8605,f8597,f996,f398,f387,f8607]) ).
fof(f8613,plain,
( sK8(sK1,sK4,sK5) = sK7(sK1,sK4,sK5)
| ~ member(sK7(sK1,sK4,sK5),sK4)
| ~ member(sK8(sK1,sK4,sK5),sK4)
| ~ spl16_253
| ~ spl16_380 ),
inference(resolution,[],[f8609,f5152]) ).
fof(f8627,plain,
( ~ member(sK7(sK1,sK4,sK5),sK4)
| ~ member(sK8(sK1,sK4,sK5),sK4)
| spl16_68
| ~ spl16_253
| ~ spl16_380 ),
inference(forward_subsumption_resolution,[],[f8613,f1057]) ).
fof(f8628,plain,
( ~ member(sK8(sK1,sK4,sK5),sK4)
| ~ spl16_67
| spl16_68
| ~ spl16_253
| ~ spl16_380 ),
inference(forward_subsumption_resolution,[],[f8627,f1012]) ).
fof(f8629,plain,
( $false
| ~ spl16_66
| ~ spl16_67
| spl16_68
| ~ spl16_253
| ~ spl16_380 ),
inference(forward_subsumption_resolution,[],[f8628,f998]) ).
fof(f8630,plain,
( ~ spl16_66
| ~ spl16_67
| spl16_68
| ~ spl16_253
| ~ spl16_380 ),
inference(avatar_contradiction_clause,[],[f8629]) ).
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,[],[f103]) ).
cnf(s4,plain,
spl16_4,
inference(sat_conversion,[],[f113]) ).
cnf(s5,plain,
( ~ spl16_2
| spl16_5 ),
inference(sat_conversion,[],[f117]) ).
cnf(s7,plain,
spl16_7,
inference(sat_conversion,[],[f130]) ).
cnf(s9,plain,
spl16_9,
inference(sat_conversion,[],[f148]) ).
cnf(s10,plain,
( ~ spl16_9
| spl16_10 ),
inference(sat_conversion,[],[f155]) ).
cnf(s14,plain,
( ~ spl16_7
| spl16_14 ),
inference(sat_conversion,[],[f186]) ).
cnf(s17,plain,
( ~ spl16_3
| spl16_17 ),
inference(sat_conversion,[],[f200]) ).
cnf(s18,plain,
( ~ spl16_4
| spl16_18 ),
inference(sat_conversion,[],[f224]) ).
cnf(s19,plain,
( ~ spl16_3
| spl16_19 ),
inference(sat_conversion,[],[f248]) ).
cnf(s20,plain,
( ~ spl16_9
| spl16_20 ),
inference(sat_conversion,[],[f268]) ).
cnf(s21,plain,
( ~ spl16_4
| spl16_21 ),
inference(sat_conversion,[],[f334]) ).
cnf(s22,plain,
( ~ spl16_17
| ~ spl16_19
| spl16_22 ),
inference(sat_conversion,[],[f354]) ).
cnf(s23,plain,
( ~ spl16_17
| ~ spl16_19
| spl16_23 ),
inference(sat_conversion,[],[f365]) ).
cnf(s24,plain,
( ~ spl16_18
| ~ spl16_21
| spl16_24 ),
inference(sat_conversion,[],[f389]) ).
cnf(s25,plain,
( ~ spl16_18
| ~ spl16_21
| spl16_25 ),
inference(sat_conversion,[],[f400]) ).
cnf(s27,plain,
( ~ spl16_14
| spl16_27 ),
inference(sat_conversion,[],[f440]) ).
cnf(s60,plain,
( spl16_1
| ~ spl16_61
| ~ spl16_62 ),
inference(sat_conversion,[],[f960]) ).
cnf(s62,plain,
( spl16_62
| spl16_64 ),
inference(sat_conversion,[],[f980]) ).
cnf(s63,plain,
( spl16_62
| spl16_65 ),
inference(sat_conversion,[],[f994]) ).
cnf(s64,plain,
( spl16_62
| spl16_66 ),
inference(sat_conversion,[],[f999]) ).
cnf(s65,plain,
( spl16_62
| spl16_67 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s66,plain,
( spl16_62
| ~ spl16_68 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s69,plain,
( spl16_62
| spl16_71 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s80,plain,
( ~ spl16_10
| spl16_82 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s96,plain,
( ~ spl16_22
| spl16_99 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s115,plain,
( ~ spl16_5
| spl16_118 ),
inference(sat_conversion,[],[f1849]) ).
cnf(s245,plain,
( ~ spl16_24
| ~ spl16_25
| ~ spl16_27
| spl16_253 ),
inference(sat_conversion,[],[f5153]) ).
cnf(s263,plain,
( spl16_61
| ~ spl16_81 ),
inference(sat_conversion,[],[f5684]) ).
cnf(s271,plain,
( ~ spl16_23
| spl16_81
| ~ spl16_99 ),
inference(sat_conversion,[],[f5817]) ).
cnf(s354,plain,
( ~ spl16_82
| spl16_344 ),
inference(sat_conversion,[],[f7633]) ).
cnf(s355,plain,
( ~ spl16_20
| ~ spl16_118
| ~ spl16_344
| spl16_345 ),
inference(sat_conversion,[],[f7680]) ).
cnf(s356,plain,
( ~ spl16_20
| ~ spl16_344
| ~ spl16_345
| spl16_346 ),
inference(sat_conversion,[],[f7699]) ).
cnf(s357,plain,
( ~ spl16_346
| spl16_347 ),
inference(sat_conversion,[],[f7731]) ).
cnf(s358,plain,
( ~ spl16_347
| spl16_348 ),
inference(sat_conversion,[],[f7763]) ).
cnf(s359,plain,
( ~ spl16_348
| spl16_349 ),
inference(sat_conversion,[],[f7775]) ).
cnf(s360,plain,
( ~ spl16_349
| spl16_350 ),
inference(sat_conversion,[],[f7788]) ).
cnf(s369,plain,
( ~ spl16_64
| ~ spl16_66
| ~ spl16_71
| ~ spl16_350
| spl16_359 ),
inference(sat_conversion,[],[f8063]) ).
cnf(s372,plain,
( ~ spl16_65
| ~ spl16_67
| ~ spl16_359
| spl16_362 ),
inference(sat_conversion,[],[f8123]) ).
cnf(s389,plain,
( ~ spl16_24
| ~ spl16_25
| ~ spl16_67
| ~ spl16_362
| spl16_378 ),
inference(sat_conversion,[],[f8570]) ).
cnf(s390,plain,
( ~ spl16_24
| ~ spl16_67
| ~ spl16_378
| spl16_379 ),
inference(sat_conversion,[],[f8599]) ).
cnf(s391,plain,
( ~ spl16_24
| ~ spl16_25
| ~ spl16_66
| ~ spl16_379
| spl16_380 ),
inference(sat_conversion,[],[f8610]) ).
cnf(s392,plain,
( ~ spl16_66
| ~ spl16_67
| spl16_68
| ~ spl16_253
| ~ spl16_380 ),
inference(sat_conversion,[],[f8630]) ).
cnf(s393,plain,
spl16_20,
inference(rat,[],[s20,s9]) ).
cnf(s395,plain,
spl16_10,
inference(rat,[],[s10,s9]) ).
cnf(s409,plain,
spl16_82,
inference(rat,[],[s80,s395]) ).
cnf(s416,plain,
spl16_344,
inference(rat,[],[s354,s409]) ).
cnf(s418,plain,
spl16_14,
inference(rat,[],[s14,s7]) ).
cnf(s432,plain,
spl16_27,
inference(rat,[],[s27,s418]) ).
cnf(s483,plain,
spl16_21,
inference(rat,[],[s21,s4]) ).
cnf(s484,plain,
spl16_18,
inference(rat,[],[s18,s4]) ).
cnf(s489,plain,
spl16_25,
inference(rat,[],[s25,s483,s484]) ).
cnf(s490,plain,
spl16_24,
inference(rat,[],[s24,s483,s484]) ).
cnf(s496,plain,
spl16_253,
inference(rat,[],[s245,s489,s432,s490]) ).
cnf(s498,plain,
spl16_19,
inference(rat,[],[s19,s3]) ).
cnf(s499,plain,
spl16_17,
inference(rat,[],[s17,s3]) ).
cnf(s504,plain,
spl16_23,
inference(rat,[],[s23,s498,s499]) ).
cnf(s505,plain,
spl16_22,
inference(rat,[],[s22,s498,s499]) ).
cnf(s513,plain,
spl16_99,
inference(rat,[],[s96,s505]) ).
cnf(s515,plain,
spl16_81,
inference(rat,[],[s271,s504,s513]) ).
cnf(s516,plain,
spl16_61,
inference(rat,[],[s263,s515]) ).
cnf(s530,plain,
spl16_5,
inference(rat,[],[s5,s2]) ).
cnf(s531,plain,
spl16_118,
inference(rat,[],[s115,s530]) ).
cnf(s532,plain,
spl16_345,
inference(rat,[],[s355,s416,s393,s531]) ).
cnf(s534,plain,
spl16_346,
inference(rat,[],[s356,s416,s393,s532]) ).
cnf(s536,plain,
spl16_347,
inference(rat,[],[s357,s534]) ).
cnf(s538,plain,
spl16_348,
inference(rat,[],[s358,s536]) ).
cnf(s540,plain,
spl16_349,
inference(rat,[],[s359,s538]) ).
cnf(s542,plain,
spl16_350,
inference(rat,[],[s360,s540]) ).
cnf(s556,plain,
~ spl16_62,
inference(rat,[],[s60,s516,s1]) ).
cnf(s558,plain,
spl16_71,
inference(rat,[],[s69,s556]) ).
cnf(s559,plain,
~ spl16_68,
inference(rat,[],[s66,s556]) ).
cnf(s560,plain,
spl16_67,
inference(rat,[],[s65,s556]) ).
cnf(s561,plain,
spl16_66,
inference(rat,[],[s64,s556]) ).
cnf(s562,plain,
spl16_65,
inference(rat,[],[s63,s556]) ).
cnf(s563,plain,
spl16_64,
inference(rat,[],[s62,s556]) ).
cnf(s574,plain,
~ spl16_380,
inference(rat,[],[s392,s560,s496,s559,s561]) ).
cnf(s580,plain,
~ spl16_379,
inference(rat,[],[s391,s574,s490,s489,s561]) ).
cnf(s583,plain,
spl16_359,
inference(rat,[],[s369,s561,s542,s558,s563]) ).
cnf(s595,plain,
~ spl16_378,
inference(rat,[],[s390,s560,s490,s580]) ).
cnf(s599,plain,
spl16_362,
inference(rat,[],[s372,s562,s560,s583]) ).
cnf(s607,plain,
$false,
inference(rat,[],[s389,s560,s490,s489,s595,s599]) ).
fof(f8631,plain,
$false,
inference(avatar_sat_refutation,[],[s607]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SET740+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.31 % Computer : n012.cluster.edu
% 0.05/0.31 % Model : x86_64 x86_64
% 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.31 % Memory : 8046.5625MB
% 0.05/0.31 % OS : Linux 6.8.0-71-generic
% 0.05/0.31 % CPULimit : 300
% 0.05/0.31 % WCLimit : 300
% 0.05/0.31 % DateTime : Mon Sep 28 02:40:04 UTC 2026
% 0.05/0.31 % CPUTime :
% 0.05/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.33 Running first-order theorem proving
% 0.07/0.33 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.05/1.88 % (2959019)Detected formulas, will run a generic FOF schedule.
% 8.05/1.88 % (2959027)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=1244116211:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.05/1.88 % (2959030)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3612822323:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.05/1.88 % (2959026)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=241509852:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.05/1.88 % (2959025)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=2504106555:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.05/1.88 % (2959031)dis-21_1_sil=8000:lcm=predicate:random_seed=1145742982: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)
% 8.05/1.88 % (2959029)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4077469563:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.05/1.88 % (2959028)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2719753775:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.05/1.88 % (2959031)Instruction limit reached!
% 8.05/1.88 % (2959031)------------------------------
% 8.05/1.88 % (2959031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.05/1.88 % (2959031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.88 % (2959031)CaDiCaL version: 2.1.3
% 8.05/1.88 % (2959031)Termination reason: Instruction limit
% 8.05/1.88 % (2959031)Termination phase: Saturation
% 8.05/1.88 % (2959031)Time elapsed: 0.028 s
% 8.05/1.88 % (2959031)Peak memory usage: 89 MB
% 8.05/1.88 % (2959031)Instructions burned: 132 (million)
% 8.05/1.88 % (2959028)Instruction limit reached!
% 8.05/1.88 % (2959028)------------------------------
% 8.05/1.88 % (2959028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.05/1.88 % (2959028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.88 % (2959028)CaDiCaL version: 2.1.3
% 8.05/1.88 % (2959028)Termination reason: Instruction limit
% 8.05/1.88 % (2959028)Termination phase: Saturation
% 8.05/1.88 % (2959028)Time elapsed: 0.032 s
% 8.05/1.88 % (2959028)Peak memory usage: 89 MB
% 8.05/1.88 % (2959028)Instructions burned: 110 (million)
% 8.05/1.88 % (2959029)Instruction limit reached!
% 8.05/1.88 % (2959029)------------------------------
% 8.05/1.88 % (2959029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.05/1.88 % (2959029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.88 % (2959029)CaDiCaL version: 2.1.3
% 8.05/1.88 % (2959029)Termination reason: Instruction limit
% 8.05/1.88 % (2959029)Termination phase: Saturation
% 8.05/1.88 % (2959029)Time elapsed: 0.038 s
% 8.05/1.88 % (2959029)Peak memory usage: 89 MB
% 8.05/1.88 % (2959029)Instructions burned: 120 (million)
% 8.05/1.88 % (2959030)Instruction limit reached!
% 8.05/1.88 % (2959030)------------------------------
% 8.05/1.88 % (2959030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.05/1.88 % (2959030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.88 % (2959030)CaDiCaL version: 2.1.3
% 8.05/1.88 % (2959030)Termination reason: Instruction limit
% 8.05/1.88 % (2959030)Termination phase: Saturation
% 8.05/1.88 % (2959030)Time elapsed: 0.053 s
% 8.05/1.88 % (2959030)Peak memory usage: 89 MB
% 8.05/1.88 % (2959030)Instructions burned: 140 (million)
% 8.05/1.88 % (2959039)lrs+10_1_sil=8000:sp=occurrence:random_seed=2012116692:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.05/1.88 % (2959040)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2164817653:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 8.05/1.88 % (2959040)Refutation not found, incomplete strategy
% 8.05/1.88 % (2959040)------------------------------
% 8.05/1.88 % (2959040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.05/1.88 % (2959040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.88 % (2959040)CaDiCaL version: 2.1.3
% 8.05/1.88 % (2959040)Termination reason: Refutation not found, incomplete strategy
% 10.51/2.05 % (2959040)Time elapsed: 0.001 s
% 10.51/2.05 % (2959040)Peak memory usage: 88 MB
% 10.51/2.05 % (2959040)Instructions burned: 2 (million)
% 10.51/2.05 % (2959041)lrs+1011_1_sil=32000:sp=occurrence:random_seed=942684083:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 10.51/2.05 % (2959042)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=3114414780:s2a=on:i=248:s2at=1.23:gtg=position_2998 on theBenchmark for (2998ds/248Mi)
% 10.51/2.05 % (2959039)Instruction limit reached!
% 10.51/2.05 % (2959039)------------------------------
% 10.51/2.05 % (2959039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959039)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959039)Termination reason: Instruction limit
% 10.51/2.05 % (2959039)Termination phase: Saturation
% 10.51/2.05 % (2959039)Time elapsed: 0.088 s
% 10.51/2.05 % (2959039)Peak memory usage: 93 MB
% 10.51/2.05 % (2959039)Instructions burned: 287 (million)
% 10.51/2.05 % (2959042)Instruction limit reached!
% 10.51/2.05 % (2959042)------------------------------
% 10.51/2.05 % (2959042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959042)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959042)Termination reason: Instruction limit
% 10.51/2.05 % (2959042)Termination phase: Saturation
% 10.51/2.05 % (2959042)Time elapsed: 0.070 s
% 10.51/2.05 % (2959042)Peak memory usage: 92 MB
% 10.51/2.05 % (2959042)Instructions burned: 248 (million)
% 10.51/2.05 % (2959041)Instruction limit reached!
% 10.51/2.05 % (2959041)------------------------------
% 10.51/2.05 % (2959041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959041)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959041)Termination reason: Instruction limit
% 10.51/2.05 % (2959041)Termination phase: Saturation
% 10.51/2.05 % (2959041)Time elapsed: 0.123 s
% 10.51/2.05 % (2959041)Peak memory usage: 93 MB
% 10.51/2.05 % (2959041)Instructions burned: 327 (million)
% 10.51/2.05 % (2959040)------------------------------
% 10.51/2.05 % (2959040)------------------------------
% 10.51/2.05 % (2959047)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=479037773:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 10.51/2.05 % (2959048)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2905222148:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 10.51/2.05 % (2959050)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1784300046:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 10.51/2.05 % (2959049)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1151673087:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 10.51/2.05 % (2959047)Instruction limit reached!
% 10.51/2.05 % (2959047)------------------------------
% 10.51/2.05 % (2959047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959047)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959047)Termination reason: Instruction limit
% 10.51/2.05 % (2959047)Termination phase: Saturation
% 10.51/2.05 % (2959047)Time elapsed: 0.087 s
% 10.51/2.05 % (2959047)Peak memory usage: 89 MB
% 10.51/2.05 % (2959047)Instructions burned: 298 (million)
% 10.51/2.05 % (2959050)Instruction limit reached!
% 10.51/2.05 % (2959050)------------------------------
% 10.51/2.05 % (2959050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959050)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959050)Termination reason: Instruction limit
% 10.51/2.05 % (2959050)Termination phase: Saturation
% 10.51/2.05 % (2959050)Time elapsed: 0.038 s
% 10.51/2.05 % (2959050)Peak memory usage: 89 MB
% 10.51/2.05 % (2959050)Instructions burned: 130 (million)
% 10.51/2.05 % (2959049)Instruction limit reached!
% 10.51/2.05 % (2959049)------------------------------
% 10.51/2.05 % (2959049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959049)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959049)Termination reason: Instruction limit
% 10.51/2.05 % (2959049)Termination phase: Saturation
% 10.51/2.05 % (2959049)Time elapsed: 0.041 s
% 10.51/2.05 % (2959049)Peak memory usage: 89 MB
% 10.51/2.05 % (2959049)Instructions burned: 113 (million)
% 10.51/2.05 % (2959055)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3657652832:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 10.51/2.05 % (2959056)lrs+10_1_sil=8000:sp=occurrence:random_seed=330150608:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 10.51/2.05 % (2959057)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1860471816:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi)
% 10.51/2.05 % (2959055)Instruction limit reached!
% 10.51/2.05 % (2959055)------------------------------
% 10.51/2.05 % (2959055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959055)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959055)Termination reason: Instruction limit
% 10.51/2.05 % (2959055)Termination phase: Saturation
% 10.51/2.05 % (2959055)Time elapsed: 0.038 s
% 10.51/2.05 % (2959055)Peak memory usage: 89 MB
% 10.51/2.05 % (2959055)Instructions burned: 116 (million)
% 10.51/2.05 % (2959057)Instruction limit reached!
% 10.51/2.05 % (2959057)------------------------------
% 10.51/2.05 % (2959057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959057)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959057)Termination reason: Instruction limit
% 10.51/2.05 % (2959057)Termination phase: Saturation
% 10.51/2.05 % (2959057)Time elapsed: 0.132 s
% 10.51/2.05 % (2959057)Peak memory usage: 91 MB
% 10.51/2.05 % (2959057)Instructions burned: 439 (million)
% 10.51/2.05 % (2959061)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2050625456:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 10.51/2.05 % (2959056)Instruction limit reached!
% 10.51/2.05 % (2959056)------------------------------
% 10.51/2.05 % (2959056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959056)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959056)Termination reason: Instruction limit
% 10.51/2.05 % (2959056)Termination phase: Saturation
% 10.51/2.05 % (2959056)Time elapsed: 0.277 s
% 10.51/2.05 % (2959056)Peak memory usage: 101 MB
% 10.51/2.05 % (2959056)Instructions burned: 910 (million)
% 10.51/2.05 % (2959062)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1431753993:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi)
% 10.51/2.05 % (2959062)Refutation not found, incomplete strategy
% 10.51/2.05 % (2959062)------------------------------
% 10.51/2.05 % (2959062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959062)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959062)Termination reason: Refutation not found, incomplete strategy
% 10.51/2.05 % (2959062)Time elapsed: 0.001 s
% 10.51/2.05 % (2959062)Peak memory usage: 88 MB
% 10.51/2.05 % (2959062)Instructions burned: 2 (million)
% 10.51/2.05 % (2959065)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1996564498:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi)
% 10.51/2.05 % (2959062)------------------------------
% 10.51/2.05 % (2959062)------------------------------
% 10.51/2.05 % (2959067)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3765784505:st=3:i=13193:sd=3:ss=axioms_2988 on theBenchmark for (2988ds/13193Mi)
% 10.51/2.05 % (2959065)Instruction limit reached!
% 10.51/2.05 % (2959065)------------------------------
% 10.51/2.05 % (2959065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959065)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959065)Termination reason: Instruction limit
% 10.51/2.05 % (2959065)Termination phase: Saturation
% 10.51/2.05 % (2959065)Time elapsed: 0.186 s
% 10.51/2.05 % (2959065)Peak memory usage: 97 MB
% 10.51/2.05 % (2959065)Instructions burned: 593 (million)
% 10.51/2.05 % (2959027)First to succeed.
% 10.51/2.05 % (2959027)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2959019"
% 10.51/2.05 % (2959048)Instruction limit reached!
% 10.51/2.05 % (2959048)------------------------------
% 10.51/2.05 % (2959048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959048)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959048)Termination reason: Instruction limit
% 10.51/2.05 % (2959048)Termination phase: Saturation
% 10.51/2.05 % (2959048)Time elapsed: 0.869 s
% 10.51/2.05 % (2959048)Peak memory usage: 140 MB
% 10.51/2.05 % (2959048)Instructions burned: 2353 (million)
% 10.51/2.05 % (2959069)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=747743237:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/125Mi)
% 10.51/2.05 % (2959069)Instruction limit reached!
% 10.51/2.05 % (2959069)------------------------------
% 10.51/2.05 % (2959069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.05 % (2959069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.05 % (2959069)CaDiCaL version: 2.1.3
% 10.51/2.05 % (2959069)Termination reason: Instruction limit
% 10.51/2.05 % (2959069)Termination phase: Saturation
% 10.51/2.05 % (2959069)Time elapsed: 0.048 s
% 10.51/2.05 % (2959069)Peak memory usage: 90 MB
% 10.51/2.05 % (2959069)Instructions burned: 125 (million)
% 10.51/2.05 % (2959070)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1889521769:i=134:gtgl=5:slsql=off:gtg=exists_sym_2986 on theBenchmark for (2986ds/134Mi)
% 10.51/2.05 % (2959027)Refutation found. Thanks to Tanya!
% 10.51/2.05 % SZS status Theorem for theBenchmark
% 10.51/2.05 % SZS output start Proof for theBenchmark
% See solution above
% 10.88/2.15 % (2959027)------------------------------
% 10.88/2.15 % (2959027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.88/2.15 % (2959027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.88/2.15 % (2959027)CaDiCaL version: 2.1.3
% 10.88/2.15 % (2959027)Termination reason: Refutation
% 10.88/2.15 % (2959027)Time elapsed: 1.223 s
% 10.88/2.15 % (2959027)Peak memory usage: 149 MB
% 10.88/2.15 % (2959027)Instructions burned: 3293 (million)
% 10.88/2.15 % (2959027)------------------------------
% 10.88/2.15 % (2959027)------------------------------
% 10.88/2.15 % (2959019)Success in time 1.518 s
% 10.88/2.15 % Vampire exiting
%------------------------------------------------------------------------------