%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM136+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 09:39:38 AM UTC 2026
% Result : Theorem 4.69s 1.03s
% Output : Refutation 4.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 19
% Syntax : Number of formulae : 129 ( 18 unt; 9 def)
% Number of atoms : 393 ( 127 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 419 ( 155 ~; 179 |; 64 &)
% ( 8 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 9 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 7 con; 0-3 aty)
% Number of variables : 309 ( 0 sgn 251 !; 58 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( vabs(X0,X1,X2) = vabs(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) )
& ( ( X0 = X3
& X1 = X4
& X2 = X5 )
=> vabs(X0,X1,X2) = vabs(X3,X4,X5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','EQ-abs') ).
fof(f4,axiom,
! [X0,X1,X2,X3] : vvar(X0) != vabs(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-var-abs') ).
fof(f6,axiom,
! [X0,X1,X2,X3,X4] : vabs(X0,X1,X2) != vapp(X3,X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-abs-app') ).
fof(f11,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( X1 = X4
& X2 = vabs(X3,X0,X5) )
=> ( ( ( X3 != X4
& visFreeVar(X4,X5) )
=> visFreeVar(X1,X2) )
& ( visFreeVar(X1,X2)
=> ( X3 != X4
& visFreeVar(X4,X5) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',isFreeVar1) ).
fof(f26,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( X2 = X0
& vtcheck(vbind(X2,X3,vbind(X0,X1,X4)),X5,X6) )
=> vtcheck(vbind(X2,X3,X4),X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Context-Duplicate') ).
fof(f27,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( X2 != X0
& vtcheck(vbind(X2,X3,vbind(X0,X1,X4)),X5,X6) )
=> vtcheck(vbind(X0,X1,vbind(X2,X3,X4)),X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Context-Swap') ).
fof(f52,axiom,
! [X0,X1,X2,X3,X4] :
( vtcheck(vbind(X1,X3,X0),X2,X4)
=> vtcheck(X0,vabs(X1,X3,X2),varrow(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-abs') ).
fof(f54,axiom,
! [X0,X1,X2] :
( vtcheck(X2,X0,X1)
=> ( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X3,X4,X5,X6] :
( X0 = vabs(X3,X5,X4)
& X1 = varrow(X5,X6)
& vtcheck(vbind(X3,X5,X2),X4,X6) )
| ? [X7,X4,X8] :
( X0 = vapp(X7,X4)
& vtcheck(X2,X7,varrow(X8,X1))
& vtcheck(X2,X4,X8) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-inv') ).
fof(f56,axiom,
! [X0,X1,X2,X3] :
( ( ~ visFreeVar(X0,veabs)
& vtcheck(vbind(X0,X1,X2),veabs,X3) )
=> vtcheck(X2,veabs,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Strong-abs-IH') ).
fof(f57,conjecture,
! [X0,X1,X2,X3,X4,X5] :
( ( ~ visFreeVar(X0,vabs(X3,X4,veabs))
& vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5) )
=> vtcheck(X2,vabs(X3,X4,veabs),X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Strong-abs') ).
fof(f58,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5] :
( ( ~ visFreeVar(X0,vabs(X3,X4,veabs))
& vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5) )
=> vtcheck(X2,vabs(X3,X4,veabs),X5) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f59,plain,
! [X0,X1,X2] :
( vtcheck(X2,X0,X1)
=> ( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X4,X5,X6,X7] :
( vabs(X4,X6,X5) = X0
& varrow(X6,X7) = X1
& vtcheck(vbind(X4,X6,X2),X5,X7) )
| ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) ) ) ),
inference(rectify,[],[f54]) ).
fof(f68,plain,
! [X0,X1,X2,X3] :
( vtcheck(X2,veabs,X3)
| visFreeVar(X0,veabs)
| ~ vtcheck(vbind(X0,X1,X2),veabs,X3) ),
inference(ennf_transformation,[],[f56]) ).
fof(f69,plain,
! [X0,X1,X2,X3] :
( vtcheck(X2,veabs,X3)
| visFreeVar(X0,veabs)
| ~ vtcheck(vbind(X0,X1,X2),veabs,X3) ),
inference(flattening,[],[f68]) ).
fof(f70,plain,
? [X0,X1,X2,X3,X4,X5] :
( ~ vtcheck(X2,vabs(X3,X4,veabs),X5)
& ~ visFreeVar(X0,vabs(X3,X4,veabs))
& vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5) ),
inference(ennf_transformation,[],[f58]) ).
fof(f71,plain,
? [X0,X1,X2,X3,X4,X5] :
( ~ vtcheck(X2,vabs(X3,X4,veabs),X5)
& ~ visFreeVar(X0,vabs(X3,X4,veabs))
& vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5) ),
inference(flattening,[],[f70]) ).
fof(f72,plain,
! [X0,X1,X2] :
( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X4,X5,X6,X7] :
( vabs(X4,X6,X5) = X0
& varrow(X6,X7) = X1
& vtcheck(vbind(X4,X6,X2),X5,X7) )
| ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ vtcheck(X2,X0,X1) ),
inference(ennf_transformation,[],[f59]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X4,X5,X6,X7] :
( vabs(X4,X6,X5) = X0
& varrow(X6,X7) = X1
& vtcheck(vbind(X4,X6,X2),X5,X7) )
| ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ vtcheck(X2,X0,X1) ),
inference(flattening,[],[f72]) ).
fof(f76,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X0,vabs(X1,X3,X2),varrow(X3,X4))
| ~ vtcheck(vbind(X1,X3,X0),X2,X4) ),
inference(ennf_transformation,[],[f52]) ).
fof(f78,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( vtcheck(vbind(X0,X1,vbind(X2,X3,X4)),X5,X6)
| X0 = X2
| ~ vtcheck(vbind(X2,X3,vbind(X0,X1,X4)),X5,X6) ),
inference(ennf_transformation,[],[f27]) ).
fof(f79,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( vtcheck(vbind(X0,X1,vbind(X2,X3,X4)),X5,X6)
| X0 = X2
| ~ vtcheck(vbind(X2,X3,vbind(X0,X1,X4)),X5,X6) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( vtcheck(vbind(X2,X3,X4),X5,X6)
| X0 != X2
| ~ vtcheck(vbind(X2,X3,vbind(X0,X1,X4)),X5,X6) ),
inference(ennf_transformation,[],[f26]) ).
fof(f81,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( vtcheck(vbind(X2,X3,X4),X5,X6)
| X0 != X2
| ~ vtcheck(vbind(X2,X3,vbind(X0,X1,X4)),X5,X6) ),
inference(flattening,[],[f80]) ).
fof(f102,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( ( visFreeVar(X1,X2)
| X3 = X4
| ~ visFreeVar(X4,X5) )
& ( ( X3 != X4
& visFreeVar(X4,X5) )
| ~ visFreeVar(X1,X2) ) )
| X1 != X4
| vabs(X3,X0,X5) != X2 ),
inference(ennf_transformation,[],[f11]) ).
fof(f103,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( ( visFreeVar(X1,X2)
| X3 = X4
| ~ visFreeVar(X4,X5) )
& ( ( X3 != X4
& visFreeVar(X4,X5) )
| ~ visFreeVar(X1,X2) ) )
| X1 != X4
| vabs(X3,X0,X5) != X2 ),
inference(flattening,[],[f102]) ).
fof(f106,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( ( X0 = X3
& X1 = X4
& X2 = X5 )
| vabs(X0,X1,X2) != vabs(X3,X4,X5) )
& ( vabs(X0,X1,X2) = vabs(X3,X4,X5)
| X0 != X3
| X1 != X4
| X2 != X5 ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f107,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( ( X0 = X3
& X1 = X4
& X2 = X5 )
| vabs(X0,X1,X2) != vabs(X3,X4,X5) )
& ( vabs(X0,X1,X2) = vabs(X3,X4,X5)
| X0 != X3
| X1 != X4
| X2 != X5 ) ),
inference(flattening,[],[f106]) ).
fof(f149,definition,
! [X0,X1,X2] :
( ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ sP0(X0,X1,X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f150,plain,
! [X0,X1,X2] :
( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X4,X5,X6,X7] :
( vabs(X4,X6,X5) = X0
& varrow(X6,X7) = X1
& vtcheck(vbind(X4,X6,X2),X5,X7) )
| sP0(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(definition_folding,[],[f73,f149]) ).
fof(f164,plain,
( ~ vtcheck(sK13,vabs(sK14,sK15,veabs),sK16)
& ~ visFreeVar(sK11,vabs(sK14,sK15,veabs))
& vtcheck(vbind(sK11,sK12,sK13),vabs(sK14,sK15,veabs),sK16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13,sK14,sK15,sK16]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13),skolemize(X3,sK14),skolemize(X4,sK15),skolemize(X5,sK16)],[f71]) ).
fof(f165,plain,
! [X0,X1,X2] :
( ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ sP0(X0,X1,X2) ),
inference(nnf_transformation,[],[f149]) ).
fof(f166,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( vapp(X3,X4) = X0
& vtcheck(X2,X3,varrow(X5,X1))
& vtcheck(X2,X4,X5) )
| ~ sP0(X0,X1,X2) ),
inference(rectify,[],[f165]) ).
fof(f167,plain,
! [X0,X1,X2] :
( ( vapp(sK17(X0,X1,X2),sK18(X0,X1,X2)) = X0
& vtcheck(X2,sK17(X0,X1,X2),varrow(sK19(X0,X1,X2),X1))
& vtcheck(X2,sK18(X0,X1,X2),sK19(X0,X1,X2)) )
| ~ sP0(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X3,sK17(X0,X1,X2)),skolemize(X4,sK18(X0,X1,X2)),skolemize(X5,sK19(X0,X1,X2))],[f166]) ).
fof(f168,plain,
! [X0,X1,X2] :
( ( vvar(sK20(X0,X1,X2)) = X0
& vsomeType(X1) = vlookup(sK20(X0,X1,X2),X2) )
| ( vabs(sK21(X0,X1,X2),sK23(X0,X1,X2),sK22(X0,X1,X2)) = X0
& varrow(sK23(X0,X1,X2),sK24(X0,X1,X2)) = X1
& vtcheck(vbind(sK21(X0,X1,X2),sK23(X0,X1,X2),X2),sK22(X0,X1,X2),sK24(X0,X1,X2)) )
| sP0(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24]),skolemize(X3,sK20(X0,X1,X2)),skolemize(X4,sK21(X0,X1,X2)),skolemize(X5,sK22(X0,X1,X2)),skolemize(X6,sK23(X0,X1,X2)),skolemize(X7,sK24(X0,X1,X2))],[f150]) ).
fof(f205,plain,
! [X2,X3,X0,X1] :
( ~ vtcheck(vbind(X0,X1,X2),veabs,X3)
| visFreeVar(X0,veabs)
| vtcheck(X2,veabs,X3) ),
inference(cnf_transformation,[],[f69]) ).
fof(f206,plain,
vtcheck(vbind(sK11,sK12,sK13),vabs(sK14,sK15,veabs),sK16),
inference(cnf_transformation,[],[f164]) ).
fof(f207,plain,
~ visFreeVar(sK11,vabs(sK14,sK15,veabs)),
inference(cnf_transformation,[],[f164]) ).
fof(f208,plain,
~ vtcheck(sK13,vabs(sK14,sK15,veabs),sK16),
inference(cnf_transformation,[],[f164]) ).
fof(f211,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| vapp(sK17(X0,X1,X2),sK18(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f167]) ).
fof(f215,plain,
! [X2,X0,X1] :
( ~ vtcheck(X2,X0,X1)
| vtcheck(vbind(sK21(X0,X1,X2),sK23(X0,X1,X2),X2),sK22(X0,X1,X2),sK24(X0,X1,X2))
| sP0(X0,X1,X2)
| vvar(sK20(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f168]) ).
fof(f216,plain,
! [X2,X0,X1] :
( ~ vtcheck(X2,X0,X1)
| varrow(sK23(X0,X1,X2),sK24(X0,X1,X2)) = X1
| sP0(X0,X1,X2)
| vvar(sK20(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f168]) ).
fof(f217,plain,
! [X2,X0,X1] :
( ~ vtcheck(X2,X0,X1)
| vabs(sK21(X0,X1,X2),sK23(X0,X1,X2),sK22(X0,X1,X2)) = X0
| sP0(X0,X1,X2)
| vvar(sK20(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f168]) ).
fof(f219,plain,
! [X2,X3,X0,X1,X4] :
( vtcheck(X0,vabs(X1,X3,X2),varrow(X3,X4))
| ~ vtcheck(vbind(X1,X3,X0),X2,X4) ),
inference(cnf_transformation,[],[f76]) ).
fof(f221,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ vtcheck(vbind(X2,X3,vbind(X0,X1,X4)),X5,X6)
| X0 = X2
| vtcheck(vbind(X0,X1,vbind(X2,X3,X4)),X5,X6) ),
inference(cnf_transformation,[],[f79]) ).
fof(f222,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( vtcheck(vbind(X2,X3,X4),X5,X6)
| X0 != X2
| ~ vtcheck(vbind(X2,X3,vbind(X0,X1,X4)),X5,X6) ),
inference(cnf_transformation,[],[f81]) ).
fof(f289,plain,
! [X2,X3,X0,X1,X4,X5] :
( visFreeVar(X1,X2)
| X3 = X4
| ~ visFreeVar(X4,X5)
| X1 != X4
| vabs(X3,X0,X5) != X2 ),
inference(cnf_transformation,[],[f103]) ).
fof(f293,plain,
! [X2,X3,X0,X1,X4,X5] :
( vabs(X0,X1,X2) != vabs(X3,X4,X5)
| X2 = X5 ),
inference(cnf_transformation,[],[f107]) ).
fof(f294,plain,
! [X2,X3,X0,X1,X4,X5] :
( vabs(X0,X1,X2) != vabs(X3,X4,X5)
| X1 = X4 ),
inference(cnf_transformation,[],[f107]) ).
fof(f295,plain,
! [X2,X3,X0,X1,X4,X5] :
( vabs(X0,X1,X2) != vabs(X3,X4,X5)
| X0 = X3 ),
inference(cnf_transformation,[],[f107]) ).
fof(f297,plain,
! [X2,X3,X0,X1] : vvar(X0) != vabs(X1,X2,X3),
inference(cnf_transformation,[],[f4]) ).
fof(f300,plain,
! [X2,X3,X0,X1,X4] : vabs(X0,X1,X2) != vapp(X3,X4),
inference(cnf_transformation,[],[f6]) ).
fof(f370,plain,
! [X2,X3,X1,X6,X4,X5] :
( ~ vtcheck(vbind(X2,X3,vbind(X2,X1,X4)),X5,X6)
| vtcheck(vbind(X2,X3,X4),X5,X6) ),
inference(equality_resolution,[],[f222]) ).
fof(f417,plain,
! [X2,X3,X0,X4,X5] :
( visFreeVar(X4,X2)
| X3 = X4
| ~ visFreeVar(X4,X5)
| vabs(X3,X0,X5) != X2 ),
inference(equality_resolution,[],[f289]) ).
fof(f418,plain,
! [X3,X0,X4,X5] :
( ~ visFreeVar(X4,X5)
| X3 = X4
| visFreeVar(X4,vabs(X3,X0,X5)) ),
inference(equality_resolution,[],[f417]) ).
fof(f507,plain,
( vabs(sK14,sK15,veabs) = vabs(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK22(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| vabs(sK14,sK15,veabs) = vvar(sK20(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))) ),
inference(resolution,[],[f217,f206]) ).
fof(f510,plain,
( vabs(sK14,sK15,veabs) = vabs(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK22(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)) ),
inference(forward_subsumption_resolution,[],[f507,f297]) ).
fof(f512,definition,
( spl91_1
<=> sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)) ),
introduced(definition,[new_symbols(definition,[spl91_1])],[avatar_definition]) ).
fof(f513,plain,
( sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| ~ spl91_1 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f515,definition,
( spl91_2
<=> vabs(sK14,sK15,veabs) = vabs(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK22(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))) ),
introduced(definition,[new_symbols(definition,[spl91_2])],[avatar_definition]) ).
fof(f516,plain,
( vabs(sK14,sK15,veabs) = vabs(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK22(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_2 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f517,plain,
( spl91_1
| spl91_2 ),
inference(avatar_split_clause,[],[f510,f515,f512]) ).
fof(f522,plain,
( sK16 = varrow(sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| vabs(sK14,sK15,veabs) = vvar(sK20(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))) ),
inference(resolution,[],[f216,f206]) ).
fof(f525,plain,
( sK16 = varrow(sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)) ),
inference(forward_subsumption_resolution,[],[f522,f297]) ).
fof(f527,definition,
( spl91_3
<=> sK16 = varrow(sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))) ),
introduced(definition,[new_symbols(definition,[spl91_3])],[avatar_definition]) ).
fof(f528,plain,
( sK16 = varrow(sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_3 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f529,plain,
( spl91_1
| spl91_3 ),
inference(avatar_split_clause,[],[f525,f527,f512]) ).
fof(f551,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != vabs(sK14,sK15,veabs)
| sK22(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)) = X2 )
| ~ spl91_2 ),
inference(superposition,[],[f293,f516]) ).
fof(f553,plain,
( veabs = sK22(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| ~ spl91_2 ),
inference(equality_resolution,[],[f551]) ).
fof(f554,plain,
( vabs(sK14,sK15,veabs) = vabs(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),veabs)
| ~ spl91_2 ),
inference(superposition,[],[f516,f553]) ).
fof(f566,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != vabs(sK14,sK15,veabs)
| sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)) = X1 )
| ~ spl91_2 ),
inference(superposition,[],[f294,f554]) ).
fof(f568,plain,
( sK15 = sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| ~ spl91_2 ),
inference(equality_resolution,[],[f566]) ).
fof(f569,plain,
( vabs(sK14,sK15,veabs) = vabs(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK15,veabs)
| ~ spl91_2 ),
inference(superposition,[],[f554,f568]) ).
fof(f589,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != vabs(sK14,sK15,veabs)
| sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)) = X0 )
| ~ spl91_2 ),
inference(superposition,[],[f295,f569]) ).
fof(f591,plain,
( sK14 = sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| ~ spl91_2 ),
inference(equality_resolution,[],[f589]) ).
fof(f601,plain,
( vabs(sK14,sK15,veabs) = vapp(sK17(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK18(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_1 ),
inference(resolution,[],[f211,f513]) ).
fof(f603,plain,
( $false
| ~ spl91_1 ),
inference(forward_subsumption_resolution,[],[f601,f300]) ).
fof(f604,plain,
~ spl91_1,
inference(avatar_contradiction_clause,[],[f603]) ).
fof(f605,plain,
( sK16 = varrow(sK15,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_2
| ~ spl91_3 ),
inference(forward_demodulation,[],[f528,f568]) ).
fof(f606,plain,
( ! [X2,X0,X1] :
( ~ vtcheck(vbind(X1,sK15,X0),X2,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| vtcheck(X0,vabs(X1,sK15,X2),sK16) )
| ~ spl91_2
| ~ spl91_3 ),
inference(superposition,[],[f219,f605]) ).
fof(f607,plain,
( vtcheck(vbind(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),vbind(sK11,sK12,sK13)),sK22(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| vabs(sK14,sK15,veabs) = vvar(sK20(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))) ),
inference(resolution,[],[f215,f206]) ).
fof(f610,plain,
( vtcheck(vbind(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),vbind(sK11,sK12,sK13)),sK22(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)) ),
inference(forward_subsumption_resolution,[],[f607,f297]) ).
fof(f611,plain,
( vtcheck(vbind(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK23(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),vbind(sK11,sK12,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| ~ spl91_2 ),
inference(forward_demodulation,[],[f610,f553]) ).
fof(f612,plain,
( vtcheck(vbind(sK21(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)),sK15,vbind(sK11,sK12,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| ~ spl91_2 ),
inference(forward_demodulation,[],[f611,f568]) ).
fof(f613,plain,
( vtcheck(vbind(sK14,sK15,vbind(sK11,sK12,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| sP0(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))
| ~ spl91_2 ),
inference(forward_demodulation,[],[f612,f591]) ).
fof(f615,definition,
( spl91_8
<=> vtcheck(vbind(sK14,sK15,vbind(sK11,sK12,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))) ),
introduced(definition,[new_symbols(definition,[spl91_8])],[avatar_definition]) ).
fof(f616,plain,
( vtcheck(vbind(sK14,sK15,vbind(sK11,sK12,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_8 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f617,plain,
( spl91_1
| spl91_8
| ~ spl91_2 ),
inference(avatar_split_clause,[],[f613,f515,f615,f512]) ).
fof(f674,definition,
( spl91_22
<=> visFreeVar(sK11,veabs) ),
introduced(definition,[new_symbols(definition,[spl91_22])],[avatar_definition]) ).
fof(f675,plain,
( visFreeVar(sK11,veabs)
| ~ spl91_22 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f800,plain,
( sK11 = sK14
| vtcheck(vbind(sK11,sK12,vbind(sK14,sK15,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_8 ),
inference(resolution,[],[f221,f616]) ).
fof(f807,definition,
( spl91_37
<=> sK11 = sK14 ),
introduced(definition,[new_symbols(definition,[spl91_37])],[avatar_definition]) ).
fof(f808,plain,
( sK11 = sK14
| ~ spl91_37 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f815,definition,
( spl91_39
<=> vtcheck(vbind(sK11,sK12,vbind(sK14,sK15,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))) ),
introduced(definition,[new_symbols(definition,[spl91_39])],[avatar_definition]) ).
fof(f816,plain,
( vtcheck(vbind(sK11,sK12,vbind(sK14,sK15,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_39 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f817,plain,
( spl91_39
| spl91_37
| ~ spl91_8 ),
inference(avatar_split_clause,[],[f800,f615,f807,f815]) ).
fof(f832,plain,
( ! [X2,X0,X1] :
( ~ vtcheck(vbind(X0,sK15,X1),X2,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK14,sK12,sK13)))
| vtcheck(X1,vabs(X0,sK15,X2),sK16) )
| ~ spl91_2
| ~ spl91_3
| ~ spl91_37 ),
inference(superposition,[],[f606,f808]) ).
fof(f833,plain,
( vtcheck(vbind(sK14,sK15,vbind(sK14,sK12,sK13)),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK14,sK12,sK13)))
| ~ spl91_8
| ~ spl91_37 ),
inference(superposition,[],[f616,f808]) ).
fof(f874,plain,
( vtcheck(vbind(sK14,sK15,sK13),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK14,sK12,sK13)))
| ~ spl91_8
| ~ spl91_37 ),
inference(resolution,[],[f833,f370]) ).
fof(f886,plain,
( vtcheck(sK13,vabs(sK14,sK15,veabs),sK16)
| ~ spl91_2
| ~ spl91_3
| ~ spl91_8
| ~ spl91_37 ),
inference(resolution,[],[f874,f832]) ).
fof(f913,plain,
( $false
| ~ spl91_2
| ~ spl91_3
| ~ spl91_8
| ~ spl91_37 ),
inference(forward_subsumption_resolution,[],[f886,f208]) ).
fof(f914,plain,
( ~ spl91_2
| ~ spl91_3
| ~ spl91_8
| ~ spl91_37 ),
inference(avatar_contradiction_clause,[],[f913]) ).
fof(f917,plain,
( visFreeVar(sK11,veabs)
| vtcheck(vbind(sK14,sK15,sK13),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_39 ),
inference(resolution,[],[f816,f205]) ).
fof(f945,definition,
( spl91_50
<=> vtcheck(vbind(sK14,sK15,sK13),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13))) ),
introduced(definition,[new_symbols(definition,[spl91_50])],[avatar_definition]) ).
fof(f946,plain,
( vtcheck(vbind(sK14,sK15,sK13),veabs,sK24(vabs(sK14,sK15,veabs),sK16,vbind(sK11,sK12,sK13)))
| ~ spl91_50 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f947,plain,
( spl91_50
| spl91_22
| ~ spl91_39 ),
inference(avatar_split_clause,[],[f917,f815,f674,f945]) ).
fof(f952,plain,
( vtcheck(sK13,vabs(sK14,sK15,veabs),sK16)
| ~ spl91_2
| ~ spl91_3
| ~ spl91_50 ),
inference(resolution,[],[f946,f606]) ).
fof(f979,plain,
( $false
| ~ spl91_2
| ~ spl91_3
| ~ spl91_50 ),
inference(forward_subsumption_resolution,[],[f952,f208]) ).
fof(f980,plain,
( ~ spl91_2
| ~ spl91_3
| ~ spl91_50 ),
inference(avatar_contradiction_clause,[],[f979]) ).
fof(f983,plain,
( ! [X0,X1] :
( visFreeVar(sK11,vabs(X0,X1,veabs))
| sK11 = X0 )
| ~ spl91_22 ),
inference(resolution,[],[f675,f418]) ).
fof(f1039,plain,
( sK11 = sK14
| ~ spl91_22 ),
inference(resolution,[],[f983,f207]) ).
fof(f1047,plain,
( spl91_37
| ~ spl91_22 ),
inference(avatar_split_clause,[],[f1039,f674,f807]) ).
cnf(s1,plain,
( spl91_1
| spl91_2 ),
inference(sat_conversion,[],[f517]) ).
cnf(s2,plain,
( spl91_1
| spl91_3 ),
inference(sat_conversion,[],[f529]) ).
cnf(s6,plain,
~ spl91_1,
inference(sat_conversion,[],[f604]) ).
cnf(s7,plain,
( spl91_1
| ~ spl91_2
| spl91_8 ),
inference(sat_conversion,[],[f617]) ).
cnf(s29,plain,
( ~ spl91_8
| spl91_37
| spl91_39 ),
inference(sat_conversion,[],[f817]) ).
cnf(s34,plain,
( ~ spl91_2
| ~ spl91_3
| ~ spl91_8
| ~ spl91_37 ),
inference(sat_conversion,[],[f914]) ).
cnf(s40,plain,
( spl91_22
| ~ spl91_39
| spl91_50 ),
inference(sat_conversion,[],[f947]) ).
cnf(s47,plain,
( ~ spl91_2
| ~ spl91_3
| ~ spl91_50 ),
inference(sat_conversion,[],[f980]) ).
cnf(s59,plain,
( ~ spl91_22
| spl91_37 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s62,plain,
spl91_3,
inference(rat,[],[s2,s6]) ).
cnf(s63,plain,
spl91_2,
inference(rat,[],[s1,s6]) ).
cnf(s64,plain,
~ spl91_50,
inference(rat,[],[s47,s62,s63]) ).
cnf(s65,plain,
spl91_8,
inference(rat,[],[s7,s6,s63]) ).
cnf(s66,plain,
~ spl91_37,
inference(rat,[],[s34,s63,s62,s65]) ).
cnf(s67,plain,
~ spl91_22,
inference(rat,[],[s59,s66]) ).
cnf(s68,plain,
spl91_39,
inference(rat,[],[s29,s65,s66]) ).
cnf(s69,plain,
$false,
inference(rat,[],[s40,s64,s68,s67]) ).
fof(f1051,plain,
$false,
inference(avatar_sat_refutation,[],[s69]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : COM136+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 21:55:19 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.13 Running first-order theorem proving
% 0.09/0.13 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.69/1.03 % (3824832)Detected formulas, will run a generic FOF schedule.
% 4.69/1.03 % (3824903)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=113835466:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.69/1.03 % (3824909)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3925927081:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.69/1.03 % (3824906)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=52747718:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.69/1.03 % (3824910)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1503808255:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.69/1.03 % (3824907)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3992846401:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.69/1.03 % (3824911)dis-21_1_sil=8000:lcm=predicate:random_seed=2746831554: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)
% 4.69/1.03 % (3824905)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=1766778054:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.69/1.03 % (3824907)Refutation not found, incomplete strategy
% 4.69/1.03 % (3824907)------------------------------
% 4.69/1.03 % (3824907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3824907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3824907)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3824907)Termination reason: Refutation not found, incomplete strategy
% 4.69/1.03 % (3824907)Time elapsed: 0.001 s
% 4.69/1.03 % (3824907)Peak memory usage: 88 MB
% 4.69/1.03 % (3824907)Instructions burned: 2 (million)
% 4.69/1.03 % (3824911)Instruction limit reached!
% 4.69/1.03 % (3824911)------------------------------
% 4.69/1.03 % (3824911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3824911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3824911)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3824911)Termination reason: Instruction limit
% 4.69/1.03 % (3824911)Termination phase: Saturation
% 4.69/1.03 % (3824911)Time elapsed: 0.038 s
% 4.69/1.03 % (3824911)Peak memory usage: 89 MB
% 4.69/1.03 % (3824911)Instructions burned: 130 (million)
% 4.69/1.03 % (3824909)Instruction limit reached!
% 4.69/1.03 % (3824909)------------------------------
% 4.69/1.03 % (3824909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3824909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3824909)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3824909)Termination reason: Instruction limit
% 4.69/1.03 % (3824909)Termination phase: Saturation
% 4.69/1.03 % (3824909)Time elapsed: 0.038 s
% 4.69/1.03 % (3824909)Peak memory usage: 88 MB
% 4.69/1.03 % (3824909)Instructions burned: 120 (million)
% 4.69/1.03 % (3824910)Instruction limit reached!
% 4.69/1.03 % (3824910)------------------------------
% 4.69/1.03 % (3824910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3824910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3824910)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3824910)Termination reason: Instruction limit
% 4.69/1.03 % (3824910)Termination phase: Saturation
% 4.69/1.03 % (3824910)Time elapsed: 0.049 s
% 4.69/1.03 % (3824910)Peak memory usage: 90 MB
% 4.69/1.03 % (3824910)Instructions burned: 140 (million)
% 4.69/1.03 % (3824974)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3984240092:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 4.69/1.03 % (3824973)lrs+10_1_sil=8000:sp=occurrence:random_seed=948813715:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.69/1.03 % (3824907)------------------------------
% 4.69/1.03 % (3824907)------------------------------
% 4.69/1.03 % (3824977)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3391336279:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 4.69/1.03 % (3824974)Instruction limit reached!
% 4.69/1.03 % (3824974)------------------------------
% 4.69/1.03 % (3824974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3824974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3824974)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3824974)Termination reason: Instruction limit
% 4.69/1.03 % (3824974)Termination phase: Saturation
% 4.69/1.03 % (3824974)Time elapsed: 0.043 s
% 4.69/1.03 % (3824974)Peak memory usage: 90 MB
% 4.69/1.03 % (3824974)Instructions burned: 158 (million)
% 4.69/1.03 % (3824973)Instruction limit reached!
% 4.69/1.03 % (3824973)------------------------------
% 4.69/1.03 % (3824973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3824973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3824973)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3824973)Termination reason: Instruction limit
% 4.69/1.03 % (3824973)Termination phase: Saturation
% 4.69/1.03 % (3824973)Time elapsed: 0.094 s
% 4.69/1.03 % (3824973)Peak memory usage: 91 MB
% 4.69/1.03 % (3824973)Instructions burned: 286 (million)
% 4.69/1.03 % (3825012)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=3405387371:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 4.69/1.03 % (3824977)Instruction limit reached!
% 4.69/1.03 % (3824977)------------------------------
% 4.69/1.03 % (3824977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3824977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3824977)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3824977)Termination reason: Instruction limit
% 4.69/1.03 % (3824977)Termination phase: Saturation
% 4.69/1.03 % (3824977)Time elapsed: 0.109 s
% 4.69/1.03 % (3824977)Peak memory usage: 92 MB
% 4.69/1.03 % (3824977)Instructions burned: 330 (million)
% 4.69/1.03 % (3825013)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3681087981:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2997 on theBenchmark for (2997ds/294Mi)
% 4.69/1.03 % (3825013)Refutation not found, incomplete strategy
% 4.69/1.03 % (3825013)------------------------------
% 4.69/1.03 % (3825013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3825013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3825013)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3825013)Termination reason: Refutation not found, incomplete strategy
% 4.69/1.03 % (3825013)Time elapsed: 0.004 s
% 4.69/1.03 % (3825013)Peak memory usage: 88 MB
% 4.69/1.03 % (3825013)Instructions burned: 10 (million)
% 4.69/1.03 % (3825012)Instruction limit reached!
% 4.69/1.03 % (3825012)------------------------------
% 4.69/1.03 % (3825012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3825012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3825012)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3825012)Termination reason: Instruction limit
% 4.69/1.03 % (3825012)Termination phase: Saturation
% 4.69/1.03 % (3825012)Time elapsed: 0.083 s
% 4.69/1.03 % (3825012)Peak memory usage: 91 MB
% 4.69/1.03 % (3825012)Instructions burned: 251 (million)
% 4.69/1.03 % (3825014)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2032309518:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 4.69/1.03 % (3825021)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=582593579:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi)
% 4.69/1.03 % (3824905)First to succeed.
% 4.69/1.03 % (3824905)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3824832"
% 4.69/1.03 % (3825021)Instruction limit reached!
% 4.69/1.03 % (3825021)------------------------------
% 4.69/1.03 % (3825021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3825021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3825021)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3825021)Termination reason: Instruction limit
% 4.69/1.03 % (3825021)Termination phase: Saturation
% 4.69/1.03 % (3825021)Time elapsed: 0.038 s
% 4.69/1.03 % (3825021)Peak memory usage: 89 MB
% 4.69/1.03 % (3825021)Instructions burned: 114 (million)
% 4.69/1.03 % (3824903)Also succeeded, but the first one will report.
% 4.69/1.03 % (3825054)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3459301229:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 4.69/1.03 % (3825013)------------------------------
% 4.69/1.03 % (3825013)------------------------------
% 4.69/1.03 % (3825054)Instruction limit reached!
% 4.69/1.03 % (3825054)------------------------------
% 4.69/1.03 % (3825054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3825054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3825054)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3825054)Termination reason: Instruction limit
% 4.69/1.03 % (3825054)Termination phase: Saturation
% 4.69/1.03 % (3825054)Time elapsed: 0.035 s
% 4.69/1.03 % (3825054)Peak memory usage: 88 MB
% 4.69/1.03 % (3825054)Instructions burned: 129 (million)
% 4.69/1.03 % (3825068)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2924077986:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2995 on theBenchmark for (2995ds/114Mi)
% 4.69/1.03 % (3825068)Instruction limit reached!
% 4.69/1.03 % (3825068)------------------------------
% 4.69/1.03 % (3825068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3825068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3825068)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3825068)Termination reason: Instruction limit
% 4.69/1.03 % (3825068)Termination phase: Saturation
% 4.69/1.03 % (3825068)Time elapsed: 0.033 s
% 4.69/1.03 % (3825068)Peak memory usage: 89 MB
% 4.69/1.03 % (3825068)Instructions burned: 117 (million)
% 4.69/1.03 % (3825070)lrs+10_1_sil=8000:sp=occurrence:random_seed=3808701469:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 4.69/1.03 % (3825071)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=185967660:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi)
% 4.69/1.03 % (3825071)Refutation not found, incomplete strategy
% 4.69/1.03 % (3825071)------------------------------
% 4.69/1.03 % (3825071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.03 % (3825071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.03 % (3825071)CaDiCaL version: 2.1.3
% 4.69/1.03 % (3825071)Termination reason: Refutation not found, incomplete strategy
% 4.69/1.03 % (3825071)Time elapsed: 0.001 s
% 4.69/1.03 % (3825071)Peak memory usage: 88 MB
% 4.69/1.03 % (3825071)Instructions burned: 2 (million)
% 4.69/1.03 % (3824905)Refutation found. Thanks to Tanya!
% 4.69/1.03 % SZS status Theorem for theBenchmark
% 4.69/1.03 % SZS output start Proof for theBenchmark
% See solution above
% 4.93/1.13 % (3824905)------------------------------
% 4.93/1.13 % (3824905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.13 % (3824905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.13 % (3824905)CaDiCaL version: 2.1.3
% 4.93/1.13 % (3824905)Termination reason: Refutation
% 4.93/1.13 % (3824905)Time elapsed: 0.400 s
% 4.93/1.13 % (3824905)Peak memory usage: 131 MB
% 4.93/1.13 % (3824905)Instructions burned: 1075 (million)
% 4.93/1.13 % (3824905)------------------------------
% 4.93/1.13 % (3824905)------------------------------
% 4.93/1.13 % (3824832)Success in time 0.661 s
% 4.93/1.13 % Vampire exiting
%------------------------------------------------------------------------------