%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET745+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:41:48 PM UTC 2026
% Result : Theorem 10.78s 2.94s
% Output : Refutation 14.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 15
% Syntax : Number of formulae : 227 ( 17 unt; 12 def)
% Number of atoms : 1126 ( 78 equ)
% Maximal formula atoms : 30 ( 4 avg)
% Number of connectives : 1510 ( 611 ~; 707 |; 150 &)
% ( 25 <=>; 15 =>; 0 <=; 2 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 11 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-3 aty)
% Number of variables : 402 ( 0 sgn 346 !; 56 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1,X2] :
( member(X0,union(X1,X2))
<=> ( member(X0,X1)
| member(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union) ).
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(f29,conjecture,
! [X0,X1,X2,X3,X4,X5] :
( ( maps(X0,X3,X5)
& maps(X1,X4,X5)
& ! [X6,X7] :
( ( member(X6,union(X3,X4))
& member(X7,X5) )
=> ( apply(X2,X6,X7)
<=> ( ( member(X6,X3)
& apply(X0,X6,X7) )
| ( member(X6,X4)
& apply(X1,X6,X7) ) ) ) ) )
=> ( maps(X2,union(X3,X4),X5)
<=> ! [X6,X8,X9] :
( ( member(X6,X3)
& member(X6,X4)
& member(X8,X5)
& member(X9,X5)
& apply(X0,X6,X8)
& apply(X1,X6,X9) )
=> X8 = X9 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thII36) ).
fof(f30,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5] :
( ( maps(X0,X3,X5)
& maps(X1,X4,X5)
& ! [X6,X7] :
( ( member(X6,union(X3,X4))
& member(X7,X5) )
=> ( apply(X2,X6,X7)
<=> ( ( member(X6,X3)
& apply(X0,X6,X7) )
| ( member(X6,X4)
& apply(X1,X6,X7) ) ) ) ) )
=> ( maps(X2,union(X3,X4),X5)
<=> ! [X6,X8,X9] :
( ( member(X6,X3)
& member(X6,X4)
& member(X8,X5)
& member(X9,X5)
& apply(X0,X6,X8)
& apply(X1,X6,X9) )
=> X8 = X9 ) ) ),
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,X3,X4,X5] :
( ( maps(X0,X3,X5)
& maps(X1,X4,X5)
& ! [X6,X7] :
( ( member(X6,union(X3,X4))
& member(X7,X5) )
=> ( apply(X2,X6,X7)
<=> ( ( member(X6,X3)
& apply(X0,X6,X7) )
| ( member(X6,X4)
& apply(X1,X6,X7) ) ) ) ) )
=> ( maps(X2,union(X3,X4),X5)
<=> ! [X8,X9,X10] :
( ( member(X8,X3)
& member(X8,X4)
& member(X9,X5)
& member(X10,X5)
& apply(X0,X8,X9)
& apply(X1,X8,X10) )
=> X9 = X10 ) ) ),
inference(rectify,[],[f30]) ).
fof(f35,plain,
! [X0,X1,X2] :
( maps(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) ) ) ),
inference(ennf_transformation,[],[f31]) ).
fof(f36,plain,
! [X0,X1,X2] :
( maps(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) ) ) ),
inference(flattening,[],[f35]) ).
fof(f41,plain,
? [X0,X1,X2,X3,X4,X5] :
( ( maps(X2,union(X3,X4),X5)
<~> ! [X8,X9,X10] :
( X9 = X10
| ~ member(X8,X3)
| ~ member(X8,X4)
| ~ member(X9,X5)
| ~ member(X10,X5)
| ~ apply(X0,X8,X9)
| ~ apply(X1,X8,X10) ) )
& maps(X0,X3,X5)
& maps(X1,X4,X5)
& ! [X6,X7] :
( ( apply(X2,X6,X7)
<=> ( ( member(X6,X3)
& apply(X0,X6,X7) )
| ( member(X6,X4)
& apply(X1,X6,X7) ) ) )
| ~ member(X6,union(X3,X4))
| ~ member(X7,X5) ) ),
inference(ennf_transformation,[],[f32]) ).
fof(f42,plain,
? [X0,X1,X2,X3,X4,X5] :
( ( maps(X2,union(X3,X4),X5)
<~> ! [X8,X9,X10] :
( X9 = X10
| ~ member(X8,X3)
| ~ member(X8,X4)
| ~ member(X9,X5)
| ~ member(X10,X5)
| ~ apply(X0,X8,X9)
| ~ apply(X1,X8,X10) ) )
& maps(X0,X3,X5)
& maps(X1,X4,X5)
& ! [X6,X7] :
( ( apply(X2,X6,X7)
<=> ( ( member(X6,X3)
& apply(X0,X6,X7) )
| ( member(X6,X4)
& apply(X1,X6,X7) ) ) )
| ~ member(X6,union(X3,X4))
| ~ member(X7,X5) ) ),
inference(flattening,[],[f41]) ).
fof(f43,definition,
! [X0,X1,X2] :
( sP0(X0,X1,X2)
<=> ! [X5,X6,X7] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X5,X1)
| ~ member(X6,X2)
| ~ member(X7,X2) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f44,plain,
! [X0,X1,X2] :
( maps(X0,X1,X2)
<=> ( ! [X3] :
( ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) )
| ~ member(X3,X1) )
& sP0(X0,X1,X2) ) ),
inference(definition_folding,[],[f36,f43]) ).
fof(f51,plain,
! [X0,X1,X2] :
( ( member(X0,union(X1,X2))
| ( ~ member(X0,X1)
& ~ member(X0,X2) ) )
& ( member(X0,X1)
| member(X0,X2)
| ~ member(X0,union(X1,X2)) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f52,plain,
! [X0,X1,X2] :
( ( member(X0,union(X1,X2))
| ( ~ member(X0,X1)
& ~ member(X0,X2) ) )
& ( member(X0,X1)
| member(X0,X2)
| ~ member(X0,union(X1,X2)) ) ),
inference(flattening,[],[f51]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ? [X5,X6,X7] :
( X6 != X7
& apply(X0,X5,X6)
& apply(X0,X5,X7)
& member(X5,X1)
& member(X6,X2)
& member(X7,X2) ) )
& ( ! [X5,X6,X7] :
( X6 = X7
| ~ apply(X0,X5,X6)
| ~ apply(X0,X5,X7)
| ~ member(X5,X1)
| ~ member(X6,X2)
| ~ member(X7,X2) )
| ~ sP0(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f43]) ).
fof(f65,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ? [X3,X4,X5] :
( X4 != X5
& apply(X0,X3,X4)
& apply(X0,X3,X5)
& member(X3,X1)
& member(X4,X2)
& member(X5,X2) ) )
& ( ! [X6,X7,X8] :
( X7 = X8
| ~ apply(X0,X6,X7)
| ~ apply(X0,X6,X8)
| ~ member(X6,X1)
| ~ member(X7,X2)
| ~ member(X8,X2) )
| ~ sP0(X0,X1,X2) ) ),
inference(rectify,[],[f64]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ( sK5(X0,X1,X2) != sK6(X0,X1,X2)
& apply(X0,sK4(X0,X1,X2),sK5(X0,X1,X2))
& apply(X0,sK4(X0,X1,X2),sK6(X0,X1,X2))
& member(sK4(X0,X1,X2),X1)
& member(sK5(X0,X1,X2),X2)
& member(sK6(X0,X1,X2),X2) ) )
& ( ! [X6,X7,X8] :
( X7 = X8
| ~ apply(X0,X6,X7)
| ~ apply(X0,X6,X8)
| ~ member(X6,X1)
| ~ member(X7,X2)
| ~ member(X8,X2) )
| ~ sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X3,sK4(X0,X1,X2)),skolemize(X4,sK5(X0,X1,X2)),skolemize(X5,sK6(X0,X1,X2))],[f65]) ).
fof(f67,plain,
! [X0,X1,X2] :
( ( maps(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ member(X4,X2)
| ~ apply(X0,X3,X4) )
& member(X3,X1) )
| ~ sP0(X0,X1,X2) )
& ( ( ! [X3] :
( ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) )
| ~ member(X3,X1) )
& sP0(X0,X1,X2) )
| ~ maps(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f68,plain,
! [X0,X1,X2] :
( ( maps(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ member(X4,X2)
| ~ apply(X0,X3,X4) )
& member(X3,X1) )
| ~ sP0(X0,X1,X2) )
& ( ( ! [X3] :
( ? [X4] :
( member(X4,X2)
& apply(X0,X3,X4) )
| ~ member(X3,X1) )
& sP0(X0,X1,X2) )
| ~ maps(X0,X1,X2) ) ),
inference(flattening,[],[f67]) ).
fof(f69,plain,
! [X0,X1,X2] :
( ( maps(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ member(X4,X2)
| ~ apply(X0,X3,X4) )
& member(X3,X1) )
| ~ sP0(X0,X1,X2) )
& ( ( ! [X5] :
( ? [X6] :
( member(X6,X2)
& apply(X0,X5,X6) )
| ~ member(X5,X1) )
& sP0(X0,X1,X2) )
| ~ maps(X0,X1,X2) ) ),
inference(rectify,[],[f68]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ( maps(X0,X1,X2)
| ( ! [X4] :
( ~ member(X4,X2)
| ~ apply(X0,sK7(X0,X1,X2),X4) )
& member(sK7(X0,X1,X2),X1) )
| ~ sP0(X0,X1,X2) )
& ( ( ! [X5] :
( ( member(sK8(X0,X2,X5),X2)
& apply(X0,X5,sK8(X0,X2,X5)) )
| ~ member(X5,X1) )
& sP0(X0,X1,X2) )
| ~ maps(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X3,sK7(X0,X1,X2)),skolemize(X6,sK8(X0,X2,X5))],[f69]) ).
fof(f89,plain,
? [X0,X1,X2,X3,X4,X5] :
( ( ? [X8,X9,X10] :
( X9 != X10
& member(X8,X3)
& member(X8,X4)
& member(X9,X5)
& member(X10,X5)
& apply(X0,X8,X9)
& apply(X1,X8,X10) )
| ~ maps(X2,union(X3,X4),X5) )
& ( ! [X8,X9,X10] :
( X9 = X10
| ~ member(X8,X3)
| ~ member(X8,X4)
| ~ member(X9,X5)
| ~ member(X10,X5)
| ~ apply(X0,X8,X9)
| ~ apply(X1,X8,X10) )
| maps(X2,union(X3,X4),X5) )
& maps(X0,X3,X5)
& maps(X1,X4,X5)
& ! [X6,X7] :
( ( ( apply(X2,X6,X7)
| ( ( ~ member(X6,X3)
| ~ apply(X0,X6,X7) )
& ( ~ member(X6,X4)
| ~ apply(X1,X6,X7) ) ) )
& ( ( member(X6,X3)
& apply(X0,X6,X7) )
| ( member(X6,X4)
& apply(X1,X6,X7) )
| ~ apply(X2,X6,X7) ) )
| ~ member(X6,union(X3,X4))
| ~ member(X7,X5) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f90,plain,
? [X0,X1,X2,X3,X4,X5] :
( ( ? [X8,X9,X10] :
( X9 != X10
& member(X8,X3)
& member(X8,X4)
& member(X9,X5)
& member(X10,X5)
& apply(X0,X8,X9)
& apply(X1,X8,X10) )
| ~ maps(X2,union(X3,X4),X5) )
& ( ! [X8,X9,X10] :
( X9 = X10
| ~ member(X8,X3)
| ~ member(X8,X4)
| ~ member(X9,X5)
| ~ member(X10,X5)
| ~ apply(X0,X8,X9)
| ~ apply(X1,X8,X10) )
| maps(X2,union(X3,X4),X5) )
& maps(X0,X3,X5)
& maps(X1,X4,X5)
& ! [X6,X7] :
( ( ( apply(X2,X6,X7)
| ( ( ~ member(X6,X3)
| ~ apply(X0,X6,X7) )
& ( ~ member(X6,X4)
| ~ apply(X1,X6,X7) ) ) )
& ( ( member(X6,X3)
& apply(X0,X6,X7) )
| ( member(X6,X4)
& apply(X1,X6,X7) )
| ~ apply(X2,X6,X7) ) )
| ~ member(X6,union(X3,X4))
| ~ member(X7,X5) ) ),
inference(flattening,[],[f89]) ).
fof(f91,plain,
? [X0,X1,X2,X3,X4,X5] :
( ( ? [X6,X7,X8] :
( X7 != X8
& member(X6,X3)
& member(X6,X4)
& member(X7,X5)
& member(X8,X5)
& apply(X0,X6,X7)
& apply(X1,X6,X8) )
| ~ maps(X2,union(X3,X4),X5) )
& ( ! [X9,X10,X11] :
( X10 = X11
| ~ member(X9,X3)
| ~ member(X9,X4)
| ~ member(X10,X5)
| ~ member(X11,X5)
| ~ apply(X0,X9,X10)
| ~ apply(X1,X9,X11) )
| maps(X2,union(X3,X4),X5) )
& maps(X0,X3,X5)
& maps(X1,X4,X5)
& ! [X12,X13] :
( ( ( apply(X2,X12,X13)
| ( ( ~ member(X12,X3)
| ~ apply(X0,X12,X13) )
& ( ~ member(X12,X4)
| ~ apply(X1,X12,X13) ) ) )
& ( ( member(X12,X3)
& apply(X0,X12,X13) )
| ( member(X12,X4)
& apply(X1,X12,X13) )
| ~ apply(X2,X12,X13) ) )
| ~ member(X12,union(X3,X4))
| ~ member(X13,X5) ) ),
inference(rectify,[],[f90]) ).
fof(f92,plain,
( ( ( sK21 != sK22
& member(sK20,sK17)
& member(sK20,sK18)
& member(sK21,sK19)
& member(sK22,sK19)
& apply(sK14,sK20,sK21)
& apply(sK15,sK20,sK22) )
| ~ maps(sK16,union(sK17,sK18),sK19) )
& ( ! [X9,X10,X11] :
( X10 = X11
| ~ member(X9,sK17)
| ~ member(X9,sK18)
| ~ member(X10,sK19)
| ~ member(X11,sK19)
| ~ apply(sK14,X9,X10)
| ~ apply(sK15,X9,X11) )
| maps(sK16,union(sK17,sK18),sK19) )
& maps(sK14,sK17,sK19)
& maps(sK15,sK18,sK19)
& ! [X12,X13] :
( ( ( apply(sK16,X12,X13)
| ( ( ~ member(X12,sK17)
| ~ apply(sK14,X12,X13) )
& ( ~ member(X12,sK18)
| ~ apply(sK15,X12,X13) ) ) )
& ( ( member(X12,sK17)
& apply(sK14,X12,X13) )
| ( member(X12,sK18)
& apply(sK15,X12,X13) )
| ~ apply(sK16,X12,X13) ) )
| ~ member(X12,union(sK17,sK18))
| ~ member(X13,sK19) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22]),skolemize(X0,sK14),skolemize(X1,sK15),skolemize(X2,sK16),skolemize(X3,sK17),skolemize(X4,sK18),skolemize(X5,sK19),skolemize(X6,sK20),skolemize(X7,sK21),skolemize(X8,sK22)],[f91]) ).
fof(f101,plain,
! [X2,X0,X1] :
( ~ member(X0,union(X1,X2))
| member(X0,X2)
| member(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f102,plain,
! [X2,X0,X1] :
( member(X0,union(X1,X2))
| ~ member(X0,X2) ),
inference(cnf_transformation,[],[f52]) ).
fof(f103,plain,
! [X2,X0,X1] :
( member(X0,union(X1,X2))
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f119,plain,
! [X2,X0,X1,X8,X6,X7] :
( ~ sP0(X0,X1,X2)
| ~ apply(X0,X6,X7)
| ~ apply(X0,X6,X8)
| ~ member(X6,X1)
| ~ member(X7,X2)
| ~ member(X8,X2)
| X7 = X8 ),
inference(cnf_transformation,[],[f66]) ).
fof(f120,plain,
! [X2,X0,X1] :
( member(sK6(X0,X1,X2),X2)
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f66]) ).
fof(f121,plain,
! [X2,X0,X1] :
( member(sK5(X0,X1,X2),X2)
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f66]) ).
fof(f122,plain,
! [X2,X0,X1] :
( member(sK4(X0,X1,X2),X1)
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f66]) ).
fof(f123,plain,
! [X2,X0,X1] :
( apply(X0,sK4(X0,X1,X2),sK6(X0,X1,X2))
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f66]) ).
fof(f124,plain,
! [X2,X0,X1] :
( apply(X0,sK4(X0,X1,X2),sK5(X0,X1,X2))
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f66]) ).
fof(f125,plain,
! [X2,X0,X1] :
( sK5(X0,X1,X2) != sK6(X0,X1,X2)
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f66]) ).
fof(f126,plain,
! [X2,X0,X1] :
( ~ maps(X0,X1,X2)
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f70]) ).
fof(f127,plain,
! [X2,X0,X1,X5] :
( ~ maps(X0,X1,X2)
| ~ member(X5,X1)
| apply(X0,X5,sK8(X0,X2,X5)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f128,plain,
! [X2,X0,X1,X5] :
( ~ maps(X0,X1,X2)
| ~ member(X5,X1)
| member(sK8(X0,X2,X5),X2) ),
inference(cnf_transformation,[],[f70]) ).
fof(f129,plain,
! [X2,X0,X1] :
( member(sK7(X0,X1,X2),X1)
| maps(X0,X1,X2)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f70]) ).
fof(f130,plain,
! [X2,X0,X1,X4] :
( ~ apply(X0,sK7(X0,X1,X2),X4)
| ~ member(X4,X2)
| maps(X0,X1,X2)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f70]) ).
fof(f151,plain,
! [X12,X13] :
( apply(sK14,X12,X13)
| apply(sK15,X12,X13)
| ~ apply(sK16,X12,X13)
| ~ member(X12,union(sK17,sK18))
| ~ member(X13,sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f152,plain,
! [X12,X13] :
( apply(sK14,X12,X13)
| member(X12,sK18)
| ~ apply(sK16,X12,X13)
| ~ member(X12,union(sK17,sK18))
| ~ member(X13,sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f153,plain,
! [X12,X13] :
( member(X12,sK17)
| apply(sK15,X12,X13)
| ~ apply(sK16,X12,X13)
| ~ member(X12,union(sK17,sK18))
| ~ member(X13,sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f155,plain,
! [X12,X13] :
( apply(sK16,X12,X13)
| ~ member(X12,sK18)
| ~ apply(sK15,X12,X13)
| ~ member(X12,union(sK17,sK18))
| ~ member(X13,sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f156,plain,
! [X12,X13] :
( apply(sK16,X12,X13)
| ~ member(X12,sK17)
| ~ apply(sK14,X12,X13)
| ~ member(X12,union(sK17,sK18))
| ~ member(X13,sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f157,plain,
maps(sK15,sK18,sK19),
inference(cnf_transformation,[],[f92]) ).
fof(f158,plain,
maps(sK14,sK17,sK19),
inference(cnf_transformation,[],[f92]) ).
fof(f159,plain,
! [X10,X11,X9] :
( X10 = X11
| ~ member(X9,sK17)
| ~ member(X9,sK18)
| ~ member(X10,sK19)
| ~ member(X11,sK19)
| ~ apply(sK14,X9,X10)
| ~ apply(sK15,X9,X11)
| maps(sK16,union(sK17,sK18),sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f160,plain,
( apply(sK15,sK20,sK22)
| ~ maps(sK16,union(sK17,sK18),sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f161,plain,
( apply(sK14,sK20,sK21)
| ~ maps(sK16,union(sK17,sK18),sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f162,plain,
( member(sK22,sK19)
| ~ maps(sK16,union(sK17,sK18),sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f163,plain,
( member(sK21,sK19)
| ~ maps(sK16,union(sK17,sK18),sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f164,plain,
( member(sK20,sK18)
| ~ maps(sK16,union(sK17,sK18),sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f165,plain,
( member(sK20,sK17)
| ~ maps(sK16,union(sK17,sK18),sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f166,plain,
( sK21 != sK22
| ~ maps(sK16,union(sK17,sK18),sK19) ),
inference(cnf_transformation,[],[f92]) ).
fof(f170,definition,
sF23 = union(sK17,sK18),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f171,plain,
union(sK17,sK18) = sF23,
inference(reorient_equations,[],[f170]) ).
fof(f172,plain,
( sK21 != sK22
| ~ maps(sK16,sF23,sK19) ),
inference(definition_folding,[],[f166,f171]) ).
fof(f173,plain,
( member(sK20,sK17)
| ~ maps(sK16,sF23,sK19) ),
inference(definition_folding,[],[f165,f171]) ).
fof(f174,plain,
( member(sK20,sK18)
| ~ maps(sK16,sF23,sK19) ),
inference(definition_folding,[],[f164,f171]) ).
fof(f175,plain,
( member(sK21,sK19)
| ~ maps(sK16,sF23,sK19) ),
inference(definition_folding,[],[f163,f171]) ).
fof(f176,plain,
( member(sK22,sK19)
| ~ maps(sK16,sF23,sK19) ),
inference(definition_folding,[],[f162,f171]) ).
fof(f177,plain,
( apply(sK14,sK20,sK21)
| ~ maps(sK16,sF23,sK19) ),
inference(definition_folding,[],[f161,f171]) ).
fof(f178,plain,
( apply(sK15,sK20,sK22)
| ~ maps(sK16,sF23,sK19) ),
inference(definition_folding,[],[f160,f171]) ).
fof(f179,plain,
! [X10,X11,X9] :
( X10 = X11
| ~ member(X9,sK17)
| ~ member(X9,sK18)
| ~ member(X10,sK19)
| ~ member(X11,sK19)
| ~ apply(sK14,X9,X10)
| ~ apply(sK15,X9,X11)
| maps(sK16,sF23,sK19) ),
inference(definition_folding,[],[f159,f171]) ).
fof(f180,plain,
! [X12,X13] :
( ~ apply(sK14,X12,X13)
| ~ member(X12,sK17)
| apply(sK16,X12,X13)
| ~ member(X12,sF23)
| ~ member(X13,sK19) ),
inference(definition_folding,[],[f156,f171]) ).
fof(f181,plain,
! [X12,X13] :
( ~ apply(sK15,X12,X13)
| ~ member(X12,sK18)
| apply(sK16,X12,X13)
| ~ member(X12,sF23)
| ~ member(X13,sK19) ),
inference(definition_folding,[],[f155,f171]) ).
fof(f183,plain,
! [X12,X13] :
( ~ apply(sK16,X12,X13)
| apply(sK15,X12,X13)
| member(X12,sK17)
| ~ member(X12,sF23)
| ~ member(X13,sK19) ),
inference(definition_folding,[],[f153,f171]) ).
fof(f184,plain,
! [X12,X13] :
( ~ apply(sK16,X12,X13)
| member(X12,sK18)
| apply(sK14,X12,X13)
| ~ member(X12,sF23)
| ~ member(X13,sK19) ),
inference(definition_folding,[],[f152,f171]) ).
fof(f185,plain,
! [X12,X13] :
( ~ apply(sK16,X12,X13)
| apply(sK15,X12,X13)
| apply(sK14,X12,X13)
| ~ member(X12,sF23)
| ~ member(X13,sK19) ),
inference(definition_folding,[],[f151,f171]) ).
fof(f187,definition,
( spl24_1
<=> maps(sK16,sF23,sK19) ),
introduced(definition,[new_symbols(definition,[spl24_1])],[avatar_definition]) ).
fof(f188,plain,
( ~ maps(sK16,sF23,sK19)
| spl24_1 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f189,plain,
( maps(sK16,sF23,sK19)
| ~ spl24_1 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f191,definition,
( spl24_2
<=> ! [X9,X11,X10] :
( X10 = X11
| ~ apply(sK15,X9,X11)
| ~ member(X11,sK19)
| ~ member(X10,sK19)
| ~ member(X9,sK17)
| ~ apply(sK14,X9,X10)
| ~ member(X9,sK18) ) ),
introduced(definition,[new_symbols(definition,[spl24_2])],[avatar_definition]) ).
fof(f192,plain,
( ! [X10,X11,X9] :
( ~ apply(sK15,X9,X11)
| X10 = X11
| ~ member(X11,sK19)
| ~ member(X10,sK19)
| ~ member(X9,sK17)
| ~ apply(sK14,X9,X10)
| ~ member(X9,sK18) )
| ~ spl24_2 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f193,plain,
( spl24_1
| spl24_2 ),
inference(avatar_split_clause,[],[f179,f191,f187]) ).
fof(f195,definition,
( spl24_3
<=> apply(sK15,sK20,sK22) ),
introduced(definition,[new_symbols(definition,[spl24_3])],[avatar_definition]) ).
fof(f197,plain,
( apply(sK15,sK20,sK22)
| ~ spl24_3 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f198,plain,
( ~ spl24_1
| spl24_3 ),
inference(avatar_split_clause,[],[f178,f195,f187]) ).
fof(f200,definition,
( spl24_4
<=> apply(sK14,sK20,sK21) ),
introduced(definition,[new_symbols(definition,[spl24_4])],[avatar_definition]) ).
fof(f202,plain,
( apply(sK14,sK20,sK21)
| ~ spl24_4 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f203,plain,
( ~ spl24_1
| spl24_4 ),
inference(avatar_split_clause,[],[f177,f200,f187]) ).
fof(f205,definition,
( spl24_5
<=> member(sK22,sK19) ),
introduced(definition,[new_symbols(definition,[spl24_5])],[avatar_definition]) ).
fof(f207,plain,
( member(sK22,sK19)
| ~ spl24_5 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,plain,
( ~ spl24_1
| spl24_5 ),
inference(avatar_split_clause,[],[f176,f205,f187]) ).
fof(f210,definition,
( spl24_6
<=> member(sK21,sK19) ),
introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition]) ).
fof(f212,plain,
( member(sK21,sK19)
| ~ spl24_6 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f213,plain,
( ~ spl24_1
| spl24_6 ),
inference(avatar_split_clause,[],[f175,f210,f187]) ).
fof(f215,definition,
( spl24_7
<=> member(sK20,sK18) ),
introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition]) ).
fof(f217,plain,
( member(sK20,sK18)
| ~ spl24_7 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f218,plain,
( ~ spl24_1
| spl24_7 ),
inference(avatar_split_clause,[],[f174,f215,f187]) ).
fof(f220,definition,
( spl24_8
<=> member(sK20,sK17) ),
introduced(definition,[new_symbols(definition,[spl24_8])],[avatar_definition]) ).
fof(f222,plain,
( member(sK20,sK17)
| ~ spl24_8 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,plain,
( ~ spl24_1
| spl24_8 ),
inference(avatar_split_clause,[],[f173,f220,f187]) ).
fof(f225,definition,
( spl24_9
<=> sK21 = sK22 ),
introduced(definition,[new_symbols(definition,[spl24_9])],[avatar_definition]) ).
fof(f227,plain,
( sK21 != sK22
| spl24_9 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,plain,
( ~ spl24_1
| ~ spl24_9 ),
inference(avatar_split_clause,[],[f172,f225,f187]) ).
fof(f229,plain,
! [X0] :
( ~ member(X0,sK17)
| member(X0,sF23) ),
inference(superposition,[],[f103,f171]) ).
fof(f230,plain,
! [X0] :
( ~ member(X0,sK18)
| member(X0,sF23) ),
inference(superposition,[],[f102,f171]) ).
fof(f231,plain,
sP0(sK15,sK18,sK19),
inference(resolution,[],[f157,f126]) ).
fof(f232,plain,
sP0(sK14,sK17,sK19),
inference(resolution,[],[f158,f126]) ).
fof(f233,plain,
! [X0] :
( apply(sK15,X0,sK8(sK15,sK19,X0))
| ~ member(X0,sK18) ),
inference(resolution,[],[f127,f157]) ).
fof(f234,plain,
! [X0] :
( apply(sK14,X0,sK8(sK14,sK19,X0))
| ~ member(X0,sK17) ),
inference(resolution,[],[f127,f158]) ).
fof(f235,plain,
! [X2,X0,X1] :
( ~ apply(sK15,X0,X2)
| ~ apply(sK15,X0,X1)
| ~ member(X0,sK18)
| ~ member(X1,sK19)
| ~ member(X2,sK19)
| X1 = X2 ),
inference(resolution,[],[f119,f231]) ).
fof(f236,plain,
! [X2,X0,X1] :
( ~ apply(sK14,X0,X2)
| ~ apply(sK14,X0,X1)
| ~ member(X0,sK17)
| ~ member(X1,sK19)
| ~ member(X2,sK19)
| X1 = X2 ),
inference(resolution,[],[f119,f232]) ).
fof(f239,plain,
! [X0] :
( ~ member(X0,sF23)
| member(X0,sK18)
| member(X0,sK17) ),
inference(superposition,[],[f101,f171]) ).
fof(f240,plain,
! [X0,X1] :
( ~ member(X0,sK18)
| ~ apply(sK15,X0,X1)
| ~ member(X0,sK18)
| ~ member(X1,sK19)
| ~ member(sK8(sK15,sK19,X0),sK19)
| sK8(sK15,sK19,X0) = X1 ),
inference(resolution,[],[f233,f235]) ).
fof(f241,plain,
! [X0] :
( ~ member(X0,sK18)
| ~ member(X0,sK18)
| apply(sK16,X0,sK8(sK15,sK19,X0))
| ~ member(X0,sF23)
| ~ member(sK8(sK15,sK19,X0),sK19) ),
inference(resolution,[],[f233,f181]) ).
fof(f245,plain,
! [X0] :
( ~ member(X0,sK18)
| apply(sK16,X0,sK8(sK15,sK19,X0))
| ~ member(X0,sF23)
| ~ member(sK8(sK15,sK19,X0),sK19) ),
inference(duplicate_literal_removal,[],[f241]) ).
fof(f246,plain,
! [X0,X1] :
( ~ member(sK8(sK15,sK19,X0),sK19)
| ~ apply(sK15,X0,X1)
| ~ member(X1,sK19)
| ~ member(X0,sK18)
| sK8(sK15,sK19,X0) = X1 ),
inference(duplicate_literal_removal,[],[f240]) ).
fof(f247,plain,
! [X0] :
( apply(sK16,X0,sK8(sK15,sK19,X0))
| ~ member(X0,sK18)
| ~ member(sK8(sK15,sK19,X0),sK19) ),
inference(forward_subsumption_resolution,[],[f245,f230]) ).
fof(f249,plain,
! [X0] :
( ~ member(X0,sK17)
| ~ member(X0,sK17)
| apply(sK16,X0,sK8(sK14,sK19,X0))
| ~ member(X0,sF23)
| ~ member(sK8(sK14,sK19,X0),sK19) ),
inference(resolution,[],[f234,f180]) ).
fof(f251,plain,
! [X0] :
( ~ member(X0,sK17)
| apply(sK16,X0,sK8(sK14,sK19,X0))
| ~ member(X0,sF23)
| ~ member(sK8(sK14,sK19,X0),sK19) ),
inference(duplicate_literal_removal,[],[f249]) ).
fof(f253,plain,
! [X0] :
( apply(sK16,X0,sK8(sK14,sK19,X0))
| ~ member(X0,sK17)
| ~ member(sK8(sK14,sK19,X0),sK19) ),
inference(forward_subsumption_resolution,[],[f251,f229]) ).
fof(f268,plain,
! [X0] :
( member(sK8(sK15,sK19,X0),sK19)
| ~ member(X0,sK18) ),
inference(resolution,[],[f128,f157]) ).
fof(f269,plain,
! [X0] :
( member(sK8(sK14,sK19,X0),sK19)
| ~ member(X0,sK17) ),
inference(resolution,[],[f128,f158]) ).
fof(f293,plain,
! [X0,X1] :
( ~ member(sK7(sK16,X0,X1),sK17)
| ~ member(sK8(sK14,sK19,sK7(sK16,X0,X1)),sK19)
| ~ member(sK8(sK14,sK19,sK7(sK16,X0,X1)),X1)
| maps(sK16,X0,X1)
| ~ sP0(sK16,X0,X1) ),
inference(resolution,[],[f253,f130]) ).
fof(f298,plain,
! [X0,X1] :
( ~ member(sK8(sK14,sK19,sK7(sK16,X0,X1)),X1)
| ~ member(sK7(sK16,X0,X1),sK17)
| maps(sK16,X0,X1)
| ~ sP0(sK16,X0,X1) ),
inference(forward_subsumption_resolution,[],[f293,f269]) ).
fof(f307,plain,
! [X0,X1] :
( ~ member(sK7(sK16,X0,X1),sK18)
| ~ member(sK8(sK15,sK19,sK7(sK16,X0,X1)),sK19)
| ~ member(sK8(sK15,sK19,sK7(sK16,X0,X1)),X1)
| maps(sK16,X0,X1)
| ~ sP0(sK16,X0,X1) ),
inference(resolution,[],[f247,f130]) ).
fof(f312,plain,
! [X0,X1] :
( ~ member(sK8(sK15,sK19,sK7(sK16,X0,X1)),X1)
| ~ member(sK7(sK16,X0,X1),sK18)
| maps(sK16,X0,X1)
| ~ sP0(sK16,X0,X1) ),
inference(forward_subsumption_resolution,[],[f307,f268]) ).
fof(f322,plain,
! [X0] :
( ~ member(sK7(sK16,X0,sK19),sK18)
| ~ member(sK7(sK16,X0,sK19),sK18)
| maps(sK16,X0,sK19)
| ~ sP0(sK16,X0,sK19) ),
inference(resolution,[],[f268,f312]) ).
fof(f325,plain,
! [X0] :
( ~ member(sK7(sK16,X0,sK19),sK18)
| maps(sK16,X0,sK19)
| ~ sP0(sK16,X0,sK19) ),
inference(duplicate_literal_removal,[],[f322]) ).
fof(f327,plain,
! [X0] :
( ~ member(sK7(sK16,X0,sK19),sK17)
| ~ member(sK7(sK16,X0,sK19),sK17)
| maps(sK16,X0,sK19)
| ~ sP0(sK16,X0,sK19) ),
inference(resolution,[],[f269,f298]) ).
fof(f330,plain,
! [X0] :
( ~ member(sK7(sK16,X0,sK19),sK17)
| maps(sK16,X0,sK19)
| ~ sP0(sK16,X0,sK19) ),
inference(duplicate_literal_removal,[],[f327]) ).
fof(f334,plain,
! [X0,X1] :
( member(sK7(X0,sF23,X1),sK18)
| ~ sP0(X0,sF23,X1)
| maps(X0,sF23,X1)
| member(sK7(X0,sF23,X1),sK17) ),
inference(resolution,[],[f129,f239]) ).
fof(f366,plain,
! [X0,X1] :
( ~ apply(sK15,X0,X1)
| ~ member(X1,sK19)
| ~ member(X0,sK18)
| sK8(sK15,sK19,X0) = X1
| ~ member(X0,sK18) ),
inference(resolution,[],[f246,f268]) ).
fof(f367,plain,
! [X0,X1] :
( ~ apply(sK15,X0,X1)
| ~ member(X1,sK19)
| ~ member(X0,sK18)
| sK8(sK15,sK19,X0) = X1 ),
inference(duplicate_literal_removal,[],[f366]) ).
fof(f378,plain,
! [X0,X1] :
( apply(sK15,sK4(sK16,X0,X1),sK6(sK16,X0,X1))
| sP0(sK16,X0,X1)
| apply(sK14,sK4(sK16,X0,X1),sK6(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19) ),
inference(resolution,[],[f123,f185]) ).
fof(f379,plain,
! [X0,X1] :
( apply(sK15,sK4(sK16,X0,X1),sK6(sK16,X0,X1))
| sP0(sK16,X0,X1)
| member(sK4(sK16,X0,X1),sK17)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19) ),
inference(resolution,[],[f123,f183]) ).
fof(f380,plain,
! [X0,X1] :
( apply(sK14,sK4(sK16,X0,X1),sK6(sK16,X0,X1))
| member(sK4(sK16,X0,X1),sK18)
| sP0(sK16,X0,X1)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19) ),
inference(resolution,[],[f123,f184]) ).
fof(f398,plain,
! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| member(sK4(sK16,X0,X1),sK17)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| ~ apply(sK15,sK4(sK16,X0,X1),X2)
| ~ member(sK4(sK16,X0,X1),sK18)
| ~ member(X2,sK19)
| ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = X2 ),
inference(resolution,[],[f379,f235]) ).
fof(f403,plain,
! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| member(sK4(sK16,X0,X1),sK17)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| ~ apply(sK15,sK4(sK16,X0,X1),X2)
| ~ member(sK4(sK16,X0,X1),sK18)
| ~ member(X2,sK19)
| sK6(sK16,X0,X1) = X2 ),
inference(duplicate_literal_removal,[],[f398]) ).
fof(f405,plain,
! [X2,X0,X1] :
( ~ apply(sK15,sK4(sK16,X0,X1),X2)
| member(sK4(sK16,X0,X1),sK17)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| sP0(sK16,X0,X1)
| ~ member(X2,sK19)
| sK6(sK16,X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f403,f239]) ).
fof(f415,plain,
! [X0,X1] :
( apply(sK15,sK4(sK16,X0,X1),sK5(sK16,X0,X1))
| sP0(sK16,X0,X1)
| apply(sK14,sK4(sK16,X0,X1),sK5(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK5(sK16,X0,X1),sK19) ),
inference(resolution,[],[f124,f185]) ).
fof(f416,plain,
! [X0,X1] :
( apply(sK15,sK4(sK16,X0,X1),sK5(sK16,X0,X1))
| sP0(sK16,X0,X1)
| member(sK4(sK16,X0,X1),sK17)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK5(sK16,X0,X1),sK19) ),
inference(resolution,[],[f124,f183]) ).
fof(f417,plain,
! [X0,X1] :
( apply(sK14,sK4(sK16,X0,X1),sK5(sK16,X0,X1))
| member(sK4(sK16,X0,X1),sK18)
| sP0(sK16,X0,X1)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK5(sK16,X0,X1),sK19) ),
inference(resolution,[],[f124,f184]) ).
fof(f463,plain,
( ! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| apply(sK14,sK4(sK16,X0,X1),sK6(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = X2
| ~ member(sK6(sK16,X0,X1),sK19)
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| ~ apply(sK14,sK4(sK16,X0,X1),X2)
| ~ member(sK4(sK16,X0,X1),sK18) )
| ~ spl24_2 ),
inference(resolution,[],[f378,f192]) ).
fof(f464,plain,
( ! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| apply(sK14,sK4(sK16,X0,X1),sK6(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = X2
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| ~ apply(sK14,sK4(sK16,X0,X1),X2)
| ~ member(sK4(sK16,X0,X1),sK18) )
| ~ spl24_2 ),
inference(duplicate_literal_removal,[],[f463]) ).
fof(f468,plain,
( ! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| apply(sK14,sK4(sK16,X0,X1),sK6(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = X2
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| ~ apply(sK14,sK4(sK16,X0,X1),X2) )
| ~ spl24_2 ),
inference(forward_subsumption_resolution,[],[f464,f380]) ).
fof(f471,plain,
( ! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = X2
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| ~ apply(sK14,sK4(sK16,X0,X1),X2) )
| ~ spl24_2 ),
inference(forward_subsumption_resolution,[],[f468,f236]) ).
fof(f472,plain,
( ! [X2,X0,X1] :
( ~ apply(sK14,sK4(sK16,X0,X1),X2)
| ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = X2
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| sP0(sK16,X0,X1) )
| ~ spl24_2 ),
inference(forward_subsumption_resolution,[],[f471,f229]) ).
fof(f473,plain,
( ! [X0,X1] :
( ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = sK8(sK14,sK19,sK4(sK16,X0,X1))
| ~ member(sK8(sK14,sK19,sK4(sK16,X0,X1)),sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| sP0(sK16,X0,X1)
| ~ member(sK4(sK16,X0,X1),sK17) )
| ~ spl24_2 ),
inference(resolution,[],[f472,f234]) ).
fof(f478,plain,
( ! [X0,X1] :
( ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = sK8(sK14,sK19,sK4(sK16,X0,X1))
| ~ member(sK8(sK14,sK19,sK4(sK16,X0,X1)),sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| sP0(sK16,X0,X1) )
| ~ spl24_2 ),
inference(duplicate_literal_removal,[],[f473]) ).
fof(f480,plain,
( ! [X0,X1] :
( ~ member(sK6(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = sK8(sK14,sK19,sK4(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sK17)
| sP0(sK16,X0,X1) )
| ~ spl24_2 ),
inference(forward_subsumption_resolution,[],[f478,f269]) ).
fof(f488,definition,
( spl24_16
<=> sP0(sK16,sF23,sK19) ),
introduced(definition,[new_symbols(definition,[spl24_16])],[avatar_definition]) ).
fof(f489,plain,
( ~ sP0(sK16,sF23,sK19)
| spl24_16 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f490,plain,
( sP0(sK16,sF23,sK19)
| ~ spl24_16 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f519,plain,
( ! [X0] :
( sK6(sK16,X0,sK19) = sK8(sK14,sK19,sK4(sK16,X0,sK19))
| ~ member(sK4(sK16,X0,sK19),sK17)
| sP0(sK16,X0,sK19)
| sP0(sK16,X0,sK19) )
| ~ spl24_2 ),
inference(resolution,[],[f480,f120]) ).
fof(f520,plain,
( ! [X0] :
( ~ member(sK4(sK16,X0,sK19),sK17)
| sK6(sK16,X0,sK19) = sK8(sK14,sK19,sK4(sK16,X0,sK19))
| sP0(sK16,X0,sK19) )
| ~ spl24_2 ),
inference(duplicate_literal_removal,[],[f519]) ).
fof(f806,plain,
( ! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| apply(sK14,sK4(sK16,X0,X1),sK5(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK5(sK16,X0,X1),sK19)
| sK5(sK16,X0,X1) = X2
| ~ member(sK5(sK16,X0,X1),sK19)
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| ~ apply(sK14,sK4(sK16,X0,X1),X2)
| ~ member(sK4(sK16,X0,X1),sK18) )
| ~ spl24_2 ),
inference(resolution,[],[f415,f192]) ).
fof(f807,plain,
( ! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| apply(sK14,sK4(sK16,X0,X1),sK5(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK5(sK16,X0,X1),sK19)
| sK5(sK16,X0,X1) = X2
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| ~ apply(sK14,sK4(sK16,X0,X1),X2)
| ~ member(sK4(sK16,X0,X1),sK18) )
| ~ spl24_2 ),
inference(duplicate_literal_removal,[],[f806]) ).
fof(f812,plain,
( ! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| apply(sK14,sK4(sK16,X0,X1),sK5(sK16,X0,X1))
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK5(sK16,X0,X1),sK19)
| sK5(sK16,X0,X1) = X2
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| ~ apply(sK14,sK4(sK16,X0,X1),X2) )
| ~ spl24_2 ),
inference(forward_subsumption_resolution,[],[f807,f417]) ).
fof(f816,plain,
( ! [X2,X0,X1] :
( sP0(sK16,X0,X1)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK5(sK16,X0,X1),sK19)
| sK5(sK16,X0,X1) = X2
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| ~ apply(sK14,sK4(sK16,X0,X1),X2) )
| ~ spl24_2 ),
inference(forward_subsumption_resolution,[],[f812,f236]) ).
fof(f818,plain,
( ! [X2,X0,X1] :
( ~ apply(sK14,sK4(sK16,X0,X1),X2)
| ~ member(sK5(sK16,X0,X1),sK19)
| sK5(sK16,X0,X1) = X2
| ~ member(X2,sK19)
| ~ member(sK4(sK16,X0,X1),sK17)
| sP0(sK16,X0,X1) )
| ~ spl24_2 ),
inference(forward_subsumption_resolution,[],[f816,f229]) ).
fof(f911,plain,
! [X0,X1] :
( member(sK4(sK16,X0,X1),sK17)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| sP0(sK16,X0,X1)
| ~ member(sK5(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = sK5(sK16,X0,X1)
| sP0(sK16,X0,X1)
| member(sK4(sK16,X0,X1),sK17)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK5(sK16,X0,X1),sK19) ),
inference(resolution,[],[f405,f416]) ).
fof(f912,plain,
! [X0,X1] :
( member(sK4(sK16,X0,X1),sK17)
| ~ member(sK4(sK16,X0,X1),sF23)
| ~ member(sK6(sK16,X0,X1),sK19)
| sP0(sK16,X0,X1)
| ~ member(sK5(sK16,X0,X1),sK19)
| sK6(sK16,X0,X1) = sK5(sK16,X0,X1) ),
inference(duplicate_literal_removal,[],[f911]) ).
fof(f918,plain,
! [X0,X1] :
( ~ member(sK6(sK16,X0,X1),sK19)
| ~ member(sK4(sK16,X0,X1),sF23)
| member(sK4(sK16,X0,X1),sK17)
| sP0(sK16,X0,X1)
| ~ member(sK5(sK16,X0,X1),sK19) ),
inference(forward_subsumption_resolution,[],[f912,f125]) ).
fof(f923,plain,
! [X0] :
( ~ member(sK4(sK16,X0,sK19),sF23)
| member(sK4(sK16,X0,sK19),sK17)
| sP0(sK16,X0,sK19)
| ~ member(sK5(sK16,X0,sK19),sK19)
| sP0(sK16,X0,sK19) ),
inference(resolution,[],[f918,f120]) ).
fof(f924,plain,
! [X0] :
( ~ member(sK4(sK16,X0,sK19),sF23)
| member(sK4(sK16,X0,sK19),sK17)
| sP0(sK16,X0,sK19)
| ~ member(sK5(sK16,X0,sK19),sK19) ),
inference(duplicate_literal_removal,[],[f923]) ).
fof(f925,plain,
! [X0] :
( ~ member(sK4(sK16,X0,sK19),sF23)
| member(sK4(sK16,X0,sK19),sK17)
| sP0(sK16,X0,sK19) ),
inference(forward_subsumption_resolution,[],[f924,f121]) ).
fof(f926,plain,
( member(sK4(sK16,sF23,sK19),sK17)
| sP0(sK16,sF23,sK19)
| sP0(sK16,sF23,sK19) ),
inference(resolution,[],[f925,f122]) ).
fof(f931,plain,
( member(sK4(sK16,sF23,sK19),sK17)
| sP0(sK16,sF23,sK19) ),
inference(duplicate_literal_removal,[],[f926]) ).
fof(f997,plain,
( ~ sP0(sK16,sF23,sK19)
| maps(sK16,sF23,sK19)
| member(sK7(sK16,sF23,sK19),sK17)
| maps(sK16,sF23,sK19)
| ~ sP0(sK16,sF23,sK19) ),
inference(resolution,[],[f334,f325]) ).
fof(f1005,plain,
( ~ sP0(sK16,sF23,sK19)
| maps(sK16,sF23,sK19)
| member(sK7(sK16,sF23,sK19),sK17) ),
inference(duplicate_literal_removal,[],[f997]) ).
fof(f1019,plain,
( maps(sK16,sF23,sK19)
| member(sK7(sK16,sF23,sK19),sK17)
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1005,f490]) ).
fof(f1020,plain,
( member(sK7(sK16,sF23,sK19),sK17)
| spl24_1
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1019,f188]) ).
fof(f1021,plain,
( maps(sK16,sF23,sK19)
| ~ sP0(sK16,sF23,sK19)
| spl24_1
| ~ spl24_16 ),
inference(resolution,[],[f1020,f330]) ).
fof(f1025,plain,
( ~ sP0(sK16,sF23,sK19)
| spl24_1
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1021,f188]) ).
fof(f1026,plain,
( $false
| spl24_1
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1025,f490]) ).
fof(f1027,plain,
( spl24_1
| ~ spl24_16 ),
inference(avatar_contradiction_clause,[],[f1026]) ).
fof(f1037,plain,
( member(sK4(sK16,sF23,sK19),sK17)
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f931,f489]) ).
fof(f1053,plain,
( sK6(sK16,sF23,sK19) = sK8(sK14,sK19,sK4(sK16,sF23,sK19))
| sP0(sK16,sF23,sK19)
| ~ spl24_2
| spl24_16 ),
inference(resolution,[],[f1037,f520]) ).
fof(f1056,plain,
( sK6(sK16,sF23,sK19) = sK8(sK14,sK19,sK4(sK16,sF23,sK19))
| ~ spl24_2
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f1053,f489]) ).
fof(f1064,plain,
( apply(sK14,sK4(sK16,sF23,sK19),sK6(sK16,sF23,sK19))
| ~ member(sK4(sK16,sF23,sK19),sK17)
| ~ spl24_2
| spl24_16 ),
inference(superposition,[],[f234,f1056]) ).
fof(f1065,plain,
( apply(sK14,sK4(sK16,sF23,sK19),sK6(sK16,sF23,sK19))
| ~ spl24_2
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f1064,f1037]) ).
fof(f1091,plain,
( ~ member(sK5(sK16,sF23,sK19),sK19)
| sK6(sK16,sF23,sK19) = sK5(sK16,sF23,sK19)
| ~ member(sK6(sK16,sF23,sK19),sK19)
| ~ member(sK4(sK16,sF23,sK19),sK17)
| sP0(sK16,sF23,sK19)
| ~ spl24_2
| spl24_16 ),
inference(resolution,[],[f1065,f818]) ).
fof(f1102,plain,
( sK6(sK16,sF23,sK19) = sK5(sK16,sF23,sK19)
| ~ member(sK6(sK16,sF23,sK19),sK19)
| ~ member(sK4(sK16,sF23,sK19),sK17)
| sP0(sK16,sF23,sK19)
| ~ spl24_2
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f1091,f121]) ).
fof(f1106,plain,
( ~ member(sK6(sK16,sF23,sK19),sK19)
| ~ member(sK4(sK16,sF23,sK19),sK17)
| sP0(sK16,sF23,sK19)
| ~ spl24_2
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f1102,f125]) ).
fof(f1109,plain,
( ~ member(sK4(sK16,sF23,sK19),sK17)
| sP0(sK16,sF23,sK19)
| ~ spl24_2
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f1106,f120]) ).
fof(f1112,plain,
( sP0(sK16,sF23,sK19)
| ~ spl24_2
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f1109,f1037]) ).
fof(f1114,plain,
( $false
| ~ spl24_2
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f1112,f489]) ).
fof(f1115,plain,
( ~ spl24_2
| spl24_16 ),
inference(avatar_contradiction_clause,[],[f1114]) ).
fof(f1126,plain,
( member(sK20,sF23)
| ~ spl24_7 ),
inference(resolution,[],[f217,f230]) ).
fof(f1134,plain,
( ~ member(sK22,sK19)
| ~ member(sK20,sK18)
| sK22 = sK8(sK15,sK19,sK20)
| ~ spl24_3 ),
inference(resolution,[],[f197,f367]) ).
fof(f1141,plain,
( ~ member(sK20,sK18)
| sK22 = sK8(sK15,sK19,sK20)
| ~ spl24_3
| ~ spl24_5 ),
inference(forward_subsumption_resolution,[],[f1134,f207]) ).
fof(f1146,plain,
( sK22 = sK8(sK15,sK19,sK20)
| ~ spl24_3
| ~ spl24_5
| ~ spl24_7 ),
inference(forward_subsumption_resolution,[],[f1141,f217]) ).
fof(f1165,plain,
( ~ member(sK20,sK17)
| apply(sK16,sK20,sK21)
| ~ member(sK20,sF23)
| ~ member(sK21,sK19)
| ~ spl24_4 ),
inference(resolution,[],[f202,f180]) ).
fof(f1166,plain,
( apply(sK16,sK20,sK21)
| ~ member(sK20,sF23)
| ~ member(sK21,sK19)
| ~ spl24_4
| ~ spl24_8 ),
inference(forward_subsumption_resolution,[],[f1165,f222]) ).
fof(f1171,plain,
( apply(sK16,sK20,sK21)
| ~ member(sK21,sK19)
| ~ spl24_4
| ~ spl24_7
| ~ spl24_8 ),
inference(forward_subsumption_resolution,[],[f1166,f1126]) ).
fof(f1176,plain,
( apply(sK16,sK20,sK21)
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8 ),
inference(forward_subsumption_resolution,[],[f1171,f212]) ).
fof(f1188,plain,
( ! [X2,X0,X1] :
( ~ apply(sK16,X0,X2)
| ~ apply(sK16,X0,X1)
| ~ member(X0,sF23)
| ~ member(X1,sK19)
| ~ member(X2,sK19)
| X1 = X2 )
| ~ spl24_16 ),
inference(resolution,[],[f490,f119]) ).
fof(f1291,plain,
( sP0(sK16,sF23,sK19)
| ~ spl24_1 ),
inference(resolution,[],[f189,f126]) ).
fof(f1441,plain,
( ! [X0] :
( ~ apply(sK16,sK20,X0)
| ~ member(sK20,sF23)
| ~ member(X0,sK19)
| ~ member(sK21,sK19)
| sK21 = X0 )
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| ~ spl24_16 ),
inference(resolution,[],[f1188,f1176]) ).
fof(f1447,plain,
( ! [X0] :
( ~ apply(sK16,sK20,X0)
| ~ member(X0,sK19)
| ~ member(sK21,sK19)
| sK21 = X0 )
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1441,f1126]) ).
fof(f1452,plain,
( ! [X0] :
( ~ apply(sK16,sK20,X0)
| ~ member(X0,sK19)
| sK21 = X0 )
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1447,f212]) ).
fof(f1456,plain,
( ~ member(sK8(sK15,sK19,sK20),sK19)
| sK21 = sK8(sK15,sK19,sK20)
| ~ member(sK20,sK18)
| ~ member(sK8(sK15,sK19,sK20),sK19)
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| ~ spl24_16 ),
inference(resolution,[],[f1452,f247]) ).
fof(f1460,plain,
( ~ member(sK8(sK15,sK19,sK20),sK19)
| sK21 = sK8(sK15,sK19,sK20)
| ~ member(sK20,sK18)
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| ~ spl24_16 ),
inference(duplicate_literal_removal,[],[f1456]) ).
fof(f1463,plain,
( sK21 = sK8(sK15,sK19,sK20)
| ~ member(sK20,sK18)
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1460,f268]) ).
fof(f1466,plain,
( sK21 = sK8(sK15,sK19,sK20)
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1463,f217]) ).
fof(f1467,plain,
( sK21 = sK22
| ~ spl24_3
| ~ spl24_4
| ~ spl24_5
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| ~ spl24_16 ),
inference(forward_demodulation,[],[f1466,f1146]) ).
fof(f1468,plain,
( $false
| ~ spl24_3
| ~ spl24_4
| ~ spl24_5
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| spl24_9
| ~ spl24_16 ),
inference(forward_subsumption_resolution,[],[f1467,f227]) ).
fof(f1469,plain,
( ~ spl24_3
| ~ spl24_4
| ~ spl24_5
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| spl24_9
| ~ spl24_16 ),
inference(avatar_contradiction_clause,[],[f1468]) ).
fof(f1471,plain,
( $false
| ~ spl24_1
| spl24_16 ),
inference(forward_subsumption_resolution,[],[f1291,f489]) ).
fof(f1472,plain,
( ~ spl24_1
| spl24_16 ),
inference(avatar_contradiction_clause,[],[f1471]) ).
cnf(s1,plain,
( spl24_1
| spl24_2 ),
inference(sat_conversion,[],[f193]) ).
cnf(s2,plain,
( ~ spl24_1
| spl24_3 ),
inference(sat_conversion,[],[f198]) ).
cnf(s3,plain,
( ~ spl24_1
| spl24_4 ),
inference(sat_conversion,[],[f203]) ).
cnf(s4,plain,
( ~ spl24_1
| spl24_5 ),
inference(sat_conversion,[],[f208]) ).
cnf(s5,plain,
( ~ spl24_1
| spl24_6 ),
inference(sat_conversion,[],[f213]) ).
cnf(s6,plain,
( ~ spl24_1
| spl24_7 ),
inference(sat_conversion,[],[f218]) ).
cnf(s7,plain,
( ~ spl24_1
| spl24_8 ),
inference(sat_conversion,[],[f223]) ).
cnf(s8,plain,
( ~ spl24_1
| ~ spl24_9 ),
inference(sat_conversion,[],[f228]) ).
cnf(s25,plain,
( spl24_1
| ~ spl24_16 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s29,plain,
( ~ spl24_2
| spl24_16 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s53,plain,
( ~ spl24_3
| ~ spl24_4
| ~ spl24_5
| ~ spl24_6
| ~ spl24_7
| ~ spl24_8
| spl24_9
| ~ spl24_16 ),
inference(sat_conversion,[],[f1469]) ).
cnf(s54,plain,
( ~ spl24_1
| spl24_16 ),
inference(sat_conversion,[],[f1472]) ).
cnf(s58,plain,
spl24_1,
inference(rat,[],[s29,s1,s25]) ).
cnf(s59,plain,
spl24_16,
inference(rat,[],[s54,s58]) ).
cnf(s60,plain,
~ spl24_9,
inference(rat,[],[s8,s58]) ).
cnf(s61,plain,
spl24_8,
inference(rat,[],[s7,s58]) ).
cnf(s62,plain,
spl24_7,
inference(rat,[],[s6,s58]) ).
cnf(s63,plain,
spl24_6,
inference(rat,[],[s5,s58]) ).
cnf(s64,plain,
spl24_5,
inference(rat,[],[s4,s58]) ).
cnf(s65,plain,
spl24_4,
inference(rat,[],[s3,s58]) ).
cnf(s66,plain,
spl24_3,
inference(rat,[],[s2,s58]) ).
cnf(s67,plain,
$false,
inference(rat,[],[s53,s59,s60,s61,s62,s63,s64,s65,s66]) ).
fof(f1480,plain,
$false,
inference(avatar_sat_refutation,[],[s67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET745+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n014.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 02:41:16 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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
% 10.78/2.93 % (1385791)Detected formulas, will run a generic FOF schedule.
% 10.78/2.93 % (1385839)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2939950251:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.78/2.93 % (1385839)Instruction limit reached!
% 10.78/2.93 % (1385839)------------------------------
% 10.78/2.93 % (1385839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.93 % (1385839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.93 % (1385839)CaDiCaL version: 2.1.3
% 10.78/2.93 % (1385839)Termination reason: Instruction limit
% 10.78/2.93 % (1385839)Termination phase: Saturation
% 10.78/2.93 % (1385839)Time elapsed: 0.038 s
% 10.78/2.93 % (1385839)Peak memory usage: 88 MB
% 10.78/2.93 % (1385839)Instructions burned: 121 (million)
% 10.78/2.93 % (1385838)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3528423884:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.78/2.93 % (1385835)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=2905696747:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.78/2.93 % (1385837)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=2363266525:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.78/2.93 % (1385840)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1513694819:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.78/2.93 % (1385836)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=61830932:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.78/2.93 % (1385841)dis-21_1_sil=8000:lcm=predicate:random_seed=2185983574: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)
% 10.78/2.93 % (1385838)Instruction limit reached!
% 10.78/2.93 % (1385838)------------------------------
% 10.78/2.93 % (1385838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.93 % (1385838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.93 % (1385838)CaDiCaL version: 2.1.3
% 10.78/2.93 % (1385838)Termination reason: Instruction limit
% 10.78/2.93 % (1385838)Termination phase: Saturation
% 10.78/2.93 % (1385838)Time elapsed: 0.110 s
% 10.78/2.93 % (1385838)Peak memory usage: 89 MB
% 10.78/2.93 % (1385838)Instructions burned: 110 (million)
% 10.78/2.93 % (1385841)Instruction limit reached!
% 10.78/2.93 % (1385841)------------------------------
% 10.78/2.93 % (1385841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.93 % (1385841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.93 % (1385841)CaDiCaL version: 2.1.3
% 10.78/2.93 % (1385841)Termination reason: Instruction limit
% 10.78/2.93 % (1385841)Termination phase: Saturation
% 10.78/2.93 % (1385841)Time elapsed: 0.087 s
% 10.78/2.93 % (1385841)Peak memory usage: 89 MB
% 10.78/2.93 % (1385841)Instructions burned: 129 (million)
% 10.78/2.93 % (1385849)lrs+10_1_sil=8000:sp=occurrence:random_seed=1061729733:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.78/2.93 % (1385840)Instruction limit reached!
% 10.78/2.93 % (1385840)------------------------------
% 10.78/2.93 % (1385840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.93 % (1385840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.93 % (1385840)CaDiCaL version: 2.1.3
% 10.78/2.93 % (1385840)Termination reason: Instruction limit
% 10.78/2.93 % (1385840)Termination phase: Saturation
% 10.78/2.93 % (1385840)Time elapsed: 0.155 s
% 10.78/2.93 % (1385840)Peak memory usage: 89 MB
% 10.78/2.93 % (1385840)Instructions burned: 139 (million)
% 10.78/2.93 % (1385849)Instruction limit reached!
% 10.78/2.93 % (1385849)------------------------------
% 10.78/2.93 % (1385849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.93 % (1385849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.93 % (1385849)CaDiCaL version: 2.1.3
% 10.78/2.93 % (1385849)Termination reason: Instruction limit
% 10.78/2.93 % (1385849)Termination phase: Saturation
% 10.78/2.93 % (1385849)Time elapsed: 0.141 s
% 10.78/2.93 % (1385849)Peak memory usage: 92 MB
% 10.78/2.93 % (1385849)Instructions burned: 287 (million)
% 10.78/2.93 % (1385857)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1062692900:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.78/2.93 % (1385858)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1766355325:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 10.78/2.93 % (1385860)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2726229312:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 10.78/2.93 % (1385859)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=728742380:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 10.78/2.93 % (1385857)Instruction limit reached!
% 10.78/2.93 % (1385857)------------------------------
% 10.78/2.93 % (1385857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.93 % (1385857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.93 % (1385857)CaDiCaL version: 2.1.3
% 10.78/2.93 % (1385857)Termination reason: Instruction limit
% 10.78/2.93 % (1385857)Termination phase: Saturation
% 10.78/2.94 % (1385857)Time elapsed: 0.120 s
% 10.78/2.94 % (1385857)Peak memory usage: 89 MB
% 10.78/2.94 % (1385857)Instructions burned: 159 (million)
% 10.78/2.94 % (1385860)Instruction limit reached!
% 10.78/2.94 % (1385860)------------------------------
% 10.78/2.94 % (1385860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.94 % (1385860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.94 % (1385860)CaDiCaL version: 2.1.3
% 10.78/2.94 % (1385860)Termination reason: Instruction limit
% 10.78/2.94 % (1385860)Termination phase: Saturation
% 10.78/2.94 % (1385860)Time elapsed: 0.170 s
% 10.78/2.94 % (1385860)Peak memory usage: 89 MB
% 10.78/2.94 % (1385860)Instructions burned: 296 (million)
% 10.78/2.94 % (1385859)Instruction limit reached!
% 10.78/2.94 % (1385859)------------------------------
% 10.78/2.94 % (1385859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.94 % (1385859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.94 % (1385859)CaDiCaL version: 2.1.3
% 10.78/2.94 % (1385859)Termination reason: Instruction limit
% 10.78/2.94 % (1385859)Termination phase: Saturation
% 10.78/2.94 % (1385859)Time elapsed: 0.208 s
% 10.78/2.94 % (1385859)Peak memory usage: 90 MB
% 10.78/2.94 % (1385859)Instructions burned: 249 (million)
% 10.78/2.94 % (1385858)Instruction limit reached!
% 10.78/2.94 % (1385858)------------------------------
% 10.78/2.94 % (1385858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.94 % (1385858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.94 % (1385858)CaDiCaL version: 2.1.3
% 10.78/2.94 % (1385858)Termination reason: Instruction limit
% 10.78/2.94 % (1385858)Termination phase: Saturation
% 10.78/2.94 % (1385858)Time elapsed: 0.320 s
% 10.78/2.94 % (1385858)Peak memory usage: 90 MB
% 10.78/2.94 % (1385858)Instructions burned: 325 (million)
% 10.78/2.94 % (1385866)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1653509056:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 10.78/2.94 % (1385871)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2990347906:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 10.78/2.94 % (1385875)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1241654078:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 10.78/2.94 % (1385871)Instruction limit reached!
% 10.78/2.94 % (1385871)------------------------------
% 10.78/2.94 % (1385871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.94 % (1385871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.94 % (1385871)CaDiCaL version: 2.1.3
% 10.78/2.94 % (1385871)Termination reason: Instruction limit
% 10.78/2.94 % (1385871)Termination phase: Saturation
% 10.78/2.94 % (1385871)Time elapsed: 0.068 s
% 10.78/2.94 % (1385871)Peak memory usage: 89 MB
% 10.78/2.94 % (1385871)Instructions burned: 114 (million)
% 10.78/2.94 % (1385877)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4181181295:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 10.78/2.94 % (1385875)Instruction limit reached!
% 10.78/2.94 % (1385875)------------------------------
% 10.78/2.94 % (1385875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.94 % (1385875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.94 % (1385875)CaDiCaL version: 2.1.3
% 10.78/2.94 % (1385875)Termination reason: Instruction limit
% 10.78/2.94 % (1385875)Termination phase: Saturation
% 10.78/2.94 % (1385875)Time elapsed: 0.107 s
% 10.78/2.94 % (1385875)Peak memory usage: 89 MB
% 10.78/2.94 % (1385875)Instructions burned: 127 (million)
% 10.78/2.94 % (1385877)Instruction limit reached!
% 10.78/2.94 % (1385877)------------------------------
% 10.78/2.94 % (1385877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.94 % (1385877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.94 % (1385877)CaDiCaL version: 2.1.3
% 10.78/2.94 % (1385877)Termination reason: Instruction limit
% 10.78/2.94 % (1385877)Termination phase: Saturation
% 10.78/2.94 % (1385877)Time elapsed: 0.119 s
% 10.78/2.94 % (1385877)Peak memory usage: 89 MB
% 10.78/2.94 % (1385877)Instructions burned: 115 (million)
% 10.78/2.94 % (1385880)lrs+10_1_sil=8000:sp=occurrence:random_seed=3500945296:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 10.78/2.94 % (1385835)First to succeed.
% 10.78/2.94 % (1385835)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1385791"
% 10.78/2.94 % (1385882)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1338665469:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 10.78/2.94 % (1385883)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4193997937:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 10.78/2.94 % (1385880)Instruction limit reached!
% 10.78/2.94 % (1385880)------------------------------
% 10.78/2.94 % (1385880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.94 % (1385880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.94 % (1385880)CaDiCaL version: 2.1.3
% 10.78/2.94 % (1385880)Termination reason: Instruction limit
% 10.78/2.94 % (1385880)Termination phase: Saturation
% 10.78/2.94 % (1385880)Time elapsed: 0.400 s
% 10.78/2.94 % (1385880)Peak memory usage: 97 MB
% 10.78/2.94 % (1385880)Instructions burned: 909 (million)
% 10.78/2.94 % (1385837)Also succeeded, but the first one will report.
% 10.78/2.94 % (1385835)Refutation found. Thanks to Tanya!
% 10.78/2.94 % SZS status Theorem for theBenchmark
% 10.78/2.94 % SZS output start Proof for theBenchmark
% See solution above
% 14.36/3.23 % (1385835)------------------------------
% 14.36/3.23 % (1385835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.36/3.23 % (1385835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.36/3.23 % (1385835)CaDiCaL version: 2.1.3
% 14.36/3.23 % (1385835)Termination reason: Refutation
% 14.36/3.23 % (1385835)Time elapsed: 1.247 s
% 14.36/3.23 % (1385835)Peak memory usage: 131 MB
% 14.36/3.23 % (1385835)Instructions burned: 1169 (million)
% 14.36/3.23 % (1385835)------------------------------
% 14.36/3.23 % (1385835)------------------------------
% 14.36/3.23 % (1385791)Success in time 1.921 s
% 14.36/3.23 % Vampire exiting
%------------------------------------------------------------------------------