%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : COM123+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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:40:20 AM UTC 2026
% Result : Theorem 5.55s 1.81s
% Output : Refutation 5.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 12
% Syntax : Number of formulae : 96 ( 26 unt; 3 def)
% Number of atoms : 293 ( 141 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 285 ( 88 ~; 117 |; 68 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 9 con; 0-3 aty)
% Number of variables : 283 ( 225 !; 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/Axioms/COM001+0.ax','EQ-abs') ).
fof(f4,axiom,
! [X0,X1,X2,X3] : vvar(X0) != vabs(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax','DIFF-var-abs') ).
fof(f6,axiom,
! [X0,X1,X2,X3,X4] : vabs(X0,X1,X2) != vapp(X3,X4),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax','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/Axioms/COM001+0.ax',isFreeVar1) ).
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/Axioms/COM001+0.ax','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/Axioms/COM001+0.ax','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/Axioms/COM001+0.ax','T-inv') ).
fof(f57,axiom,
! [X0,X1,X2,X3] :
( ( ~ visFreeVar(X0,veabs)
& vtcheck(X2,veabs,X3) )
=> vtcheck(vbind(X0,X1,X2),veabs,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Weak-FreeVar-abs-IH') ).
fof(f58,conjecture,
! [X0,X1,X2,X3,X4,X5] :
( ( X0 != X3
& ~ visFreeVar(X0,vabs(X3,X4,veabs))
& vtcheck(X2,vabs(X3,X4,veabs),X5) )
=> vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Weak-FreeVar-abs-1') ).
fof(f59,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5] :
( ( X0 != X3
& ~ visFreeVar(X0,vabs(X3,X4,veabs))
& vtcheck(X2,vabs(X3,X4,veabs),X5) )
=> vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
fof(f66,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,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(f69,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,[],[f68]) ).
fof(f77,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(f78,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,[],[f77]) ).
fof(f98,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(f99,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,[],[f98]) ).
fof(f139,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(f142,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,[],[f66]) ).
fof(f143,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,[],[f142]) ).
fof(f148,plain,
! [X0,X1,X2,X3] :
( vtcheck(vbind(X0,X1,X2),veabs,X3)
| visFreeVar(X0,veabs)
| ~ vtcheck(X2,veabs,X3) ),
inference(ennf_transformation,[],[f57]) ).
fof(f149,plain,
! [X0,X1,X2,X3] :
( vtcheck(vbind(X0,X1,X2),veabs,X3)
| visFreeVar(X0,veabs)
| ~ vtcheck(X2,veabs,X3) ),
inference(flattening,[],[f148]) ).
fof(f150,plain,
? [X0,X1,X2,X3,X4,X5] :
( ~ vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5)
& X0 != X3
& ~ visFreeVar(X0,vabs(X3,X4,veabs))
& vtcheck(X2,vabs(X3,X4,veabs),X5) ),
inference(ennf_transformation,[],[f59]) ).
fof(f151,plain,
? [X0,X1,X2,X3,X4,X5] :
( ~ vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5)
& X0 != X3
& ~ visFreeVar(X0,vabs(X3,X4,veabs))
& vtcheck(X2,vabs(X3,X4,veabs),X5) ),
inference(flattening,[],[f150]) ).
fof(f167,definition,
! [X0,X1,X2] :
( ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ sP12(X0,X1,X2) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f168,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) )
| sP12(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(definition_folding,[],[f143,f167]) ).
fof(f210,plain,
! [X0,X1,X2] :
( ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ sP12(X0,X1,X2) ),
inference(nnf_transformation,[],[f167]) ).
fof(f211,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( vapp(X3,X4) = X0
& vtcheck(X2,X3,varrow(X5,X1))
& vtcheck(X2,X4,X5) )
| ~ sP12(X0,X1,X2) ),
inference(rectify,[],[f210]) ).
fof(f212,plain,
! [X0,X1,X2] :
( ( vapp(sK79(X0,X1,X2),sK80(X0,X1,X2)) = X0
& vtcheck(X2,sK79(X0,X1,X2),varrow(sK81(X0,X1,X2),X1))
& vtcheck(X2,sK80(X0,X1,X2),sK81(X0,X1,X2)) )
| ~ sP12(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK79,sK80,sK81]),skolemize(X3,sK79(X0,X1,X2)),skolemize(X4,sK80(X0,X1,X2)),skolemize(X5,sK81(X0,X1,X2))],[f211]) ).
fof(f213,plain,
! [X0,X1,X2] :
( ( vvar(sK82(X0,X1,X2)) = X0
& vsomeType(X1) = vlookup(sK82(X0,X1,X2),X2) )
| ( vabs(sK83(X0,X1,X2),sK85(X0,X1,X2),sK84(X0,X1,X2)) = X0
& varrow(sK85(X0,X1,X2),sK86(X0,X1,X2)) = X1
& vtcheck(vbind(sK83(X0,X1,X2),sK85(X0,X1,X2),X2),sK84(X0,X1,X2),sK86(X0,X1,X2)) )
| sP12(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK82,sK83,sK84,sK85,sK86]),skolemize(X3,sK82(X0,X1,X2)),skolemize(X4,sK83(X0,X1,X2)),skolemize(X5,sK84(X0,X1,X2)),skolemize(X6,sK85(X0,X1,X2)),skolemize(X7,sK86(X0,X1,X2))],[f168]) ).
fof(f214,plain,
( ~ vtcheck(vbind(sK87,sK88,sK89),vabs(sK90,sK91,veabs),sK92)
& sK87 != sK90
& ~ visFreeVar(sK87,vabs(sK90,sK91,veabs))
& vtcheck(sK89,vabs(sK90,sK91,veabs),sK92) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87,sK88,sK89,sK90,sK91,sK92]),skolemize(X0,sK87),skolemize(X1,sK88),skolemize(X2,sK89),skolemize(X3,sK90),skolemize(X4,sK91),skolemize(X5,sK92)],[f151]) ).
fof(f218,plain,
! [X2,X3,X0,X1,X4,X5] :
( vabs(X0,X1,X2) != vabs(X3,X4,X5)
| X2 = X5 ),
inference(cnf_transformation,[],[f69]) ).
fof(f219,plain,
! [X2,X3,X0,X1,X4,X5] :
( vabs(X0,X1,X2) != vabs(X3,X4,X5)
| X1 = X4 ),
inference(cnf_transformation,[],[f69]) ).
fof(f220,plain,
! [X2,X3,X0,X1,X4,X5] :
( vabs(X0,X1,X2) != vabs(X3,X4,X5)
| X0 = X3 ),
inference(cnf_transformation,[],[f69]) ).
fof(f224,plain,
! [X2,X3,X0,X1] : vvar(X0) != vabs(X1,X2,X3),
inference(cnf_transformation,[],[f4]) ).
fof(f226,plain,
! [X2,X3,X0,X1,X4] : vabs(X0,X1,X2) != vapp(X3,X4),
inference(cnf_transformation,[],[f6]) ).
fof(f234,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,[],[f78]) ).
fof(f266,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,[],[f99]) ).
fof(f352,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,[],[f139]) ).
fof(f356,plain,
! [X2,X0,X1] :
( ~ sP12(X0,X1,X2)
| vapp(sK79(X0,X1,X2),sK80(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f212]) ).
fof(f360,plain,
! [X2,X0,X1] :
( vtcheck(vbind(sK83(X0,X1,X2),sK85(X0,X1,X2),X2),sK84(X0,X1,X2),sK86(X0,X1,X2))
| vvar(sK82(X0,X1,X2)) = X0
| sP12(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(cnf_transformation,[],[f213]) ).
fof(f361,plain,
! [X2,X0,X1] :
( ~ vtcheck(X2,X0,X1)
| varrow(sK85(X0,X1,X2),sK86(X0,X1,X2)) = X1
| sP12(X0,X1,X2)
| vvar(sK82(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f213]) ).
fof(f362,plain,
! [X2,X0,X1] :
( ~ vtcheck(X2,X0,X1)
| vabs(sK83(X0,X1,X2),sK85(X0,X1,X2),sK84(X0,X1,X2)) = X0
| sP12(X0,X1,X2)
| vvar(sK82(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f213]) ).
fof(f365,plain,
! [X2,X3,X0,X1] :
( vtcheck(vbind(X0,X1,X2),veabs,X3)
| visFreeVar(X0,veabs)
| ~ vtcheck(X2,veabs,X3) ),
inference(cnf_transformation,[],[f149]) ).
fof(f366,plain,
vtcheck(sK89,vabs(sK90,sK91,veabs),sK92),
inference(cnf_transformation,[],[f214]) ).
fof(f367,plain,
~ visFreeVar(sK87,vabs(sK90,sK91,veabs)),
inference(cnf_transformation,[],[f214]) ).
fof(f368,plain,
sK87 != sK90,
inference(cnf_transformation,[],[f214]) ).
fof(f369,plain,
~ vtcheck(vbind(sK87,sK88,sK89),vabs(sK90,sK91,veabs),sK92),
inference(cnf_transformation,[],[f214]) ).
fof(f384,plain,
! [X2,X3,X0,X4,X5] :
( visFreeVar(X4,X2)
| X3 = X4
| ~ visFreeVar(X4,X5)
| vabs(X3,X0,X5) != X2 ),
inference(equality_resolution,[],[f234]) ).
fof(f385,plain,
! [X3,X0,X4,X5] :
( visFreeVar(X4,vabs(X3,X0,X5))
| X3 = X4
| ~ visFreeVar(X4,X5) ),
inference(equality_resolution,[],[f384]) ).
fof(f481,definition,
sF93 = vbind(sK87,sK88,sK89),
introduced(definition,[new_symbols(definition,[sF93])],[function_definition]) ).
fof(f482,plain,
vbind(sK87,sK88,sK89) = sF93,
inference(reorient_equations,[],[f481]) ).
fof(f483,definition,
sF94 = vabs(sK90,sK91,veabs),
introduced(definition,[new_symbols(definition,[sF94])],[function_definition]) ).
fof(f484,plain,
vabs(sK90,sK91,veabs) = sF94,
inference(reorient_equations,[],[f483]) ).
fof(f485,plain,
~ vtcheck(sF93,sF94,sK92),
inference(definition_folding,[],[f369,f484,f482]) ).
fof(f486,plain,
~ visFreeVar(sK87,sF94),
inference(definition_folding,[],[f367,f484]) ).
fof(f487,plain,
vtcheck(sK89,sF94,sK92),
inference(definition_folding,[],[f366,f484]) ).
fof(f492,plain,
! [X0] : vvar(X0) != sF94,
inference(superposition,[],[f224,f484]) ).
fof(f496,plain,
! [X0,X1] : vapp(X0,X1) != sF94,
inference(superposition,[],[f226,f484]) ).
fof(f542,plain,
! [X2,X0,X1] :
( vabs(X0,X1,X2) != sF94
| veabs = X2 ),
inference(superposition,[],[f218,f484]) ).
fof(f545,plain,
! [X2,X0,X1] :
( vabs(X0,X1,X2) != sF94
| sK91 = X1 ),
inference(superposition,[],[f219,f484]) ).
fof(f548,plain,
! [X2,X0,X1] :
( vabs(X0,X1,X2) != sF94
| sK90 = X0 ),
inference(superposition,[],[f220,f484]) ).
fof(f578,plain,
! [X0] :
( ~ visFreeVar(X0,veabs)
| sK90 = X0
| visFreeVar(X0,sF94) ),
inference(superposition,[],[f385,f484]) ).
fof(f932,plain,
! [X2,X3,X0,X1,X4,X5] :
( vtcheck(vbind(X0,X2,vbind(X1,X3,X4)),veabs,X5)
| X0 = X1
| visFreeVar(X1,veabs)
| ~ vtcheck(vbind(X0,X2,X4),veabs,X5) ),
inference(resolution,[],[f266,f365]) ).
fof(f994,plain,
( sK92 = varrow(sK85(sF94,sK92,sK89),sK86(sF94,sK92,sK89))
| sP12(sF94,sK92,sK89)
| sF94 = vvar(sK82(sF94,sK92,sK89)) ),
inference(resolution,[],[f361,f487]) ).
fof(f996,plain,
( sP12(sF94,sK92,sK89)
| sK92 = varrow(sK85(sF94,sK92,sK89),sK86(sF94,sK92,sK89)) ),
inference(forward_subsumption_resolution,[],[f994,f492]) ).
fof(f998,plain,
( sK92 = varrow(sK85(sF94,sK92,sK89),sK86(sF94,sK92,sK89))
| sF94 = vapp(sK79(sF94,sK92,sK89),sK80(sF94,sK92,sK89)) ),
inference(resolution,[],[f996,f356]) ).
fof(f999,plain,
sK92 = varrow(sK85(sF94,sK92,sK89),sK86(sF94,sK92,sK89)),
inference(forward_subsumption_resolution,[],[f998,f496]) ).
fof(f1018,plain,
( sF94 = vabs(sK83(sF94,sK92,sK89),sK85(sF94,sK92,sK89),sK84(sF94,sK92,sK89))
| sP12(sF94,sK92,sK89)
| sF94 = vvar(sK82(sF94,sK92,sK89)) ),
inference(resolution,[],[f362,f487]) ).
fof(f1021,plain,
( sP12(sF94,sK92,sK89)
| sF94 = vabs(sK83(sF94,sK92,sK89),sK85(sF94,sK92,sK89),sK84(sF94,sK92,sK89)) ),
inference(forward_subsumption_resolution,[],[f1018,f492]) ).
fof(f1210,plain,
( sF94 = vabs(sK83(sF94,sK92,sK89),sK85(sF94,sK92,sK89),sK84(sF94,sK92,sK89))
| sF94 = vapp(sK79(sF94,sK92,sK89),sK80(sF94,sK92,sK89)) ),
inference(resolution,[],[f1021,f356]) ).
fof(f1211,plain,
sF94 = vabs(sK83(sF94,sK92,sK89),sK85(sF94,sK92,sK89),sK84(sF94,sK92,sK89)),
inference(forward_subsumption_resolution,[],[f1210,f496]) ).
fof(f1229,plain,
( sF94 != sF94
| veabs = sK84(sF94,sK92,sK89) ),
inference(superposition,[],[f542,f1211]) ).
fof(f1230,plain,
( sF94 != sF94
| sK91 = sK85(sF94,sK92,sK89) ),
inference(superposition,[],[f545,f1211]) ).
fof(f1231,plain,
( sF94 != sF94
| sK90 = sK83(sF94,sK92,sK89) ),
inference(superposition,[],[f548,f1211]) ).
fof(f1237,plain,
sK90 = sK83(sF94,sK92,sK89),
inference(trivial_inequality_removal,[],[f1231]) ).
fof(f1238,plain,
sK91 = sK85(sF94,sK92,sK89),
inference(trivial_inequality_removal,[],[f1230]) ).
fof(f1239,plain,
veabs = sK84(sF94,sK92,sK89),
inference(trivial_inequality_removal,[],[f1229]) ).
fof(f1258,plain,
( vtcheck(vbind(sK90,sK85(sF94,sK92,sK89),sK89),sK84(sF94,sK92,sK89),sK86(sF94,sK92,sK89))
| sF94 = vvar(sK82(sF94,sK92,sK89))
| sP12(sF94,sK92,sK89)
| ~ vtcheck(sK89,sF94,sK92) ),
inference(superposition,[],[f360,f1237]) ).
fof(f1259,plain,
( vtcheck(vbind(sK90,sK85(sF94,sK92,sK89),sK89),sK84(sF94,sK92,sK89),sK86(sF94,sK92,sK89))
| sP12(sF94,sK92,sK89)
| ~ vtcheck(sK89,sF94,sK92) ),
inference(forward_subsumption_resolution,[],[f1258,f492]) ).
fof(f1262,plain,
( vtcheck(vbind(sK90,sK85(sF94,sK92,sK89),sK89),sK84(sF94,sK92,sK89),sK86(sF94,sK92,sK89))
| sP12(sF94,sK92,sK89) ),
inference(forward_subsumption_resolution,[],[f1259,f487]) ).
fof(f1265,plain,
( vtcheck(vbind(sK90,sK85(sF94,sK92,sK89),sK89),veabs,sK86(sF94,sK92,sK89))
| sP12(sF94,sK92,sK89) ),
inference(forward_demodulation,[],[f1262,f1239]) ).
fof(f1267,plain,
( vtcheck(vbind(sK90,sK91,sK89),veabs,sK86(sF94,sK92,sK89))
| sP12(sF94,sK92,sK89) ),
inference(forward_demodulation,[],[f1265,f1238]) ).
fof(f1271,plain,
sK92 = varrow(sK91,sK86(sF94,sK92,sK89)),
inference(superposition,[],[f999,f1238]) ).
fof(f1427,plain,
! [X2,X0,X1] :
( ~ vtcheck(vbind(X1,sK91,X0),X2,sK86(sF94,sK92,sK89))
| vtcheck(X0,vabs(X1,sK91,X2),sK92) ),
inference(superposition,[],[f352,f1271]) ).
fof(f2614,plain,
! [X2,X0,X1] :
( ~ vtcheck(vbind(X0,X1,sK89),veabs,X2)
| sK87 = X0
| visFreeVar(sK87,veabs)
| vtcheck(vbind(X0,X1,sF93),veabs,X2) ),
inference(superposition,[],[f932,f482]) ).
fof(f20093,plain,
( sK87 = sK90
| visFreeVar(sK87,veabs)
| vtcheck(vbind(sK90,sK91,sF93),veabs,sK86(sF94,sK92,sK89))
| sP12(sF94,sK92,sK89) ),
inference(resolution,[],[f2614,f1267]) ).
fof(f20097,plain,
( vtcheck(vbind(sK90,sK91,sF93),veabs,sK86(sF94,sK92,sK89))
| visFreeVar(sK87,veabs)
| sP12(sF94,sK92,sK89) ),
inference(forward_subsumption_resolution,[],[f20093,f368]) ).
fof(f20100,plain,
( visFreeVar(sK87,veabs)
| sP12(sF94,sK92,sK89)
| vtcheck(sF93,vabs(sK90,sK91,veabs),sK92) ),
inference(resolution,[],[f20097,f1427]) ).
fof(f20112,plain,
( vtcheck(sF93,sF94,sK92)
| visFreeVar(sK87,veabs)
| sP12(sF94,sK92,sK89) ),
inference(forward_demodulation,[],[f20100,f484]) ).
fof(f20114,plain,
( sP12(sF94,sK92,sK89)
| visFreeVar(sK87,veabs) ),
inference(forward_subsumption_resolution,[],[f20112,f485]) ).
fof(f20157,plain,
( visFreeVar(sK87,veabs)
| sF94 = vapp(sK79(sF94,sK92,sK89),sK80(sF94,sK92,sK89)) ),
inference(resolution,[],[f20114,f356]) ).
fof(f20158,plain,
visFreeVar(sK87,veabs),
inference(forward_subsumption_resolution,[],[f20157,f496]) ).
fof(f20200,plain,
( sK87 = sK90
| visFreeVar(sK87,sF94) ),
inference(resolution,[],[f20158,f578]) ).
fof(f20206,plain,
visFreeVar(sK87,sF94),
inference(forward_subsumption_resolution,[],[f20200,f368]) ).
fof(f20207,plain,
$false,
inference(forward_subsumption_resolution,[],[f20206,f486]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : COM123+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 21:54:49 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.12 Running first-order model finding
% 0.08/0.12 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.20/0.87 % (3823279)Will run a generic schedule for satisfiability detection.
% 4.20/0.87 % (3823285)% WARNING: option uhcvi not known.
% 4.20/0.87 % (3823285)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=18851186:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.20/0.87 % (3823284)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1222709089_2999 on theBenchmark for (2999ds/0Mi)
% 4.20/0.87 % (3823290)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1650500203:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.20/0.87 % (3823286)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4016023857:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.20/0.87 % (3823287)dis+10_1_sil=32000:sp=arity:random_seed=1716900450:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.20/0.87 % (3823288)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=492981238:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.20/0.87 % (3823289)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=651554675:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.20/0.87 % TRYING [1]
% 4.20/0.87 % TRYING [2]
% 4.20/0.87 % TRYING [3]
% 4.20/0.87 % (3823287)Instruction limit reached!
% 4.20/0.87 % (3823287)------------------------------
% 4.20/0.87 % (3823287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.20/0.87 % (3823287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/0.87 % (3823287)CaDiCaL version: 2.1.3
% 4.20/0.87 % (3823287)Termination reason: Instruction limit
% 4.20/0.87 % (3823287)Termination phase: Saturation
% 4.20/0.87 % (3823287)Time elapsed: 0.034 s
% 4.20/0.87 % (3823287)Peak memory usage: 13 MB
% 4.20/0.87 % (3823287)Instructions burned: 106 (million)
% 4.20/0.87 % (3823288)Instruction limit reached!
% 4.20/0.87 % (3823288)------------------------------
% 4.20/0.87 % (3823288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.20/0.87 % (3823288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/0.87 % (3823288)CaDiCaL version: 2.1.3
% 4.20/0.87 % (3823288)Termination reason: Instruction limit
% 4.20/0.87 % (3823288)Termination phase: Saturation
% 4.20/0.87 % (3823288)Time elapsed: 0.034 s
% 4.20/0.87 % (3823288)Peak memory usage: 13 MB
% 4.20/0.87 % (3823288)Instructions burned: 117 (million)
% 4.20/0.87 % (3823289)Instruction limit reached!
% 4.20/0.87 % (3823289)------------------------------
% 4.20/0.87 % (3823289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.20/0.87 % (3823289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/0.87 % (3823289)CaDiCaL version: 2.1.3
% 4.20/0.87 % (3823289)Termination reason: Instruction limit
% 4.20/0.87 % (3823289)Termination phase: Saturation
% 4.20/0.87 % (3823289)Time elapsed: 0.041 s
% 4.20/0.87 % (3823289)Peak memory usage: 13 MB
% 4.20/0.87 % (3823289)Instructions burned: 132 (million)
% 4.20/0.87 % (3823299)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=68227449:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.20/0.87 % (3823298)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4210234722:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.20/0.87 % (3823290)Instruction limit reached!
% 4.20/0.87 % (3823290)------------------------------
% 4.20/0.87 % (3823290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.20/0.87 % (3823290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/0.87 % (3823290)CaDiCaL version: 2.1.3
% 4.20/0.87 % (3823290)Termination reason: Instruction limit
% 4.20/0.87 % (3823290)Termination phase: Saturation
% 4.20/0.87 % (3823290)Time elapsed: 0.046 s
% 4.20/0.87 % (3823290)Peak memory usage: 14 MB
% 4.20/0.87 % (3823290)Instructions burned: 159 (million)
% 4.20/0.87 % (3823300)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3331355118:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.20/0.87 % TRYING [1]
% 4.20/0.87 % TRYING [2]
% 4.20/0.87 % (3823303)ott-21_1_sil=16000:fs=off:random_seed=574383692:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.20/0.87 % TRYING [3]
% 4.20/0.87 % (3823299)Instruction limit reached!
% 4.20/0.87 % (3823299)------------------------------
% 4.20/0.87 % (3823299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.20/0.87 % (3823299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823299)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823299)Termination reason: Instruction limit
% 5.55/1.81 % (3823299)Termination phase: Saturation
% 5.55/1.81 % (3823299)Time elapsed: 0.040 s
% 5.55/1.81 % (3823299)Peak memory usage: 13 MB
% 5.55/1.81 % (3823299)Instructions burned: 132 (million)
% 5.55/1.81 % (3823306)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1754352255:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.55/1.81 % (3823303)Instruction limit reached!
% 5.55/1.81 % (3823303)------------------------------
% 5.55/1.81 % (3823303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823303)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823303)Termination reason: Instruction limit
% 5.55/1.81 % (3823303)Termination phase: Saturation
% 5.55/1.81 % (3823303)Time elapsed: 0.054 s
% 5.55/1.81 % (3823303)Peak memory usage: 13 MB
% 5.55/1.81 % (3823303)Instructions burned: 181 (million)
% 5.55/1.81 % (3823308)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2975421236:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.55/1.81 % TRYING [1]
% 5.55/1.81 % TRYING [2]
% 5.55/1.81 % TRYING [4]
% 5.55/1.81 % TRYING [3]
% 5.55/1.81 % (3823298)Instruction limit reached!
% 5.55/1.81 % (3823298)------------------------------
% 5.55/1.81 % (3823298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823298)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823298)Termination reason: Instruction limit
% 5.55/1.81 % (3823298)Termination phase: Finite model building SAT solving
% 5.55/1.81 % (3823298)Time elapsed: 0.144 s
% 5.55/1.81 % (3823298)Peak memory usage: 42 MB
% 5.55/1.81 % (3823298)Instructions burned: 715 (million)
% 5.55/1.81 % (3823310)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3569957140:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 5.55/1.81 % (3823306)Instruction limit reached!
% 5.55/1.81 % (3823306)------------------------------
% 5.55/1.81 % (3823306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823306)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823306)Termination reason: Instruction limit
% 5.55/1.81 % (3823306)Termination phase: Saturation
% 5.55/1.81 % (3823306)Time elapsed: 0.151 s
% 5.55/1.81 % (3823306)Peak memory usage: 15 MB
% 5.55/1.81 % (3823306)Instructions burned: 481 (million)
% 5.55/1.81 % (3823300)Instruction limit reached!
% 5.55/1.81 % (3823300)------------------------------
% 5.55/1.81 % (3823300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823300)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823300)Termination reason: Instruction limit
% 5.55/1.81 % (3823300)Termination phase: Saturation
% 5.55/1.81 % (3823300)Time elapsed: 0.198 s
% 5.55/1.81 % (3823300)Peak memory usage: 18 MB
% 5.55/1.81 % (3823300)Instructions burned: 686 (million)
% 5.55/1.81 % (3823312)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2454075024:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 5.55/1.81 % (3823313)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1316192214:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 5.55/1.81 % (3823308)Instruction limit reached!
% 5.55/1.81 % (3823308)------------------------------
% 5.55/1.81 % (3823308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823308)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823308)Termination reason: Instruction limit
% 5.55/1.81 % (3823308)Termination phase: Finite model building SAT solving
% 5.55/1.81 % (3823308)Time elapsed: 0.182 s
% 5.55/1.81 % (3823308)Peak memory usage: 35 MB
% 5.55/1.81 % (3823308)Instructions burned: 869 (million)
% 5.55/1.81 % (3823316)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2533533804:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 5.55/1.81 % (3823313)Instruction limit reached!
% 5.55/1.81 % (3823313)------------------------------
% 5.55/1.81 % (3823313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823313)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823313)Termination reason: Instruction limit
% 5.55/1.81 % (3823313)Termination phase: Saturation
% 5.55/1.81 % (3823313)Time elapsed: 0.196 s
% 5.55/1.81 % (3823313)Peak memory usage: 20 MB
% 5.55/1.81 % (3823313)Instructions burned: 695 (million)
% 5.55/1.81 % (3823318)fmb+10_1_sil=64000:random_seed=671098667:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 5.55/1.81 % TRYING [1]
% 5.55/1.81 % TRYING [2]
% 5.55/1.81 % (3823312)Instruction limit reached!
% 5.55/1.81 % (3823312)------------------------------
% 5.55/1.81 % (3823312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823312)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823312)Termination reason: Instruction limit
% 5.55/1.81 % (3823312)Termination phase: Finite model building constraint generation
% 5.55/1.81 % (3823312)Time elapsed: 0.234 s
% 5.55/1.81 % (3823312)Peak memory usage: 106 MB
% 5.55/1.81 % (3823312)Instructions burned: 894 (million)
% 5.55/1.81 % TRYING [3]
% 5.55/1.81 % (3823320)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1247636517:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 5.55/1.81 % (3823320)Cannot represent all propositional literals internally
% 5.55/1.81 % (3823320)Refutation not found, incomplete strategy
% 5.55/1.81 % (3823320)------------------------------
% 5.55/1.81 % (3823320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823320)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823320)Termination reason: Refutation not found, incomplete strategy
% 5.55/1.81 % (3823320)Time elapsed: 0.009 s
% 5.55/1.81 % (3823320)Peak memory usage: 11 MB
% 5.55/1.81 % (3823320)Instructions burned: 33 (million)
% 5.55/1.81 % (3823320)------------------------------
% 5.55/1.81 % (3823320)------------------------------
% 5.55/1.81 % (3823322)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3789303568:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 5.55/1.81 % (3823310)Instruction limit reached!
% 5.55/1.81 % (3823310)------------------------------
% 5.55/1.81 % (3823310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823310)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823310)Termination reason: Instruction limit
% 5.55/1.81 % (3823310)Termination phase: Saturation
% 5.55/1.81 % (3823310)Time elapsed: 0.336 s
% 5.55/1.81 % (3823310)Peak memory usage: 20 MB
% 5.55/1.81 % (3823310)Instructions burned: 1181 (million)
% 5.55/1.81 % TRYING [8]
% 5.55/1.81 % (3823324)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4019177495:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 5.55/1.81 % (3823316)Instruction limit reached!
% 5.55/1.81 % (3823316)------------------------------
% 5.55/1.81 % (3823316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823316)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823316)Termination reason: Instruction limit
% 5.55/1.81 % (3823316)Termination phase: Saturation
% 5.55/1.81 % (3823316)Time elapsed: 0.258 s
% 5.55/1.81 % (3823316)Peak memory usage: 19 MB
% 5.55/1.81 % (3823316)Instructions burned: 880 (million)
% 5.55/1.81 % (3823326)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=825679641:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 5.55/1.81 % (3823322)Instruction limit reached!
% 5.55/1.81 % (3823322)------------------------------
% 5.55/1.81 % (3823322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823322)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823322)Termination reason: Instruction limit
% 5.55/1.81 % (3823322)Termination phase: Finite model building constraint generation
% 5.55/1.81 % (3823322)Time elapsed: 0.169 s
% 5.55/1.81 % (3823322)Peak memory usage: 58 MB
% 5.55/1.81 % (3823322)Instructions burned: 926 (million)
% 5.55/1.81 % (3823328)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1891016963:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 5.55/1.81 % (3823328)Cannot represent all propositional literals internally
% 5.55/1.81 % (3823328)Refutation not found, incomplete strategy
% 5.55/1.81 % (3823328)------------------------------
% 5.55/1.81 % (3823328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823328)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823328)Termination reason: Refutation not found, incomplete strategy
% 5.55/1.81 % (3823328)Time elapsed: 0.010 s
% 5.55/1.81 % (3823328)Peak memory usage: 11 MB
% 5.55/1.81 % (3823328)Instructions burned: 37 (million)
% 5.55/1.81 % (3823328)------------------------------
% 5.55/1.81 % (3823328)------------------------------
% 5.55/1.81 % (3823330)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1740890591:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 5.55/1.81 % TRYING [4]
% 5.55/1.81 % (3823330)Cannot represent all propositional literals internally
% 5.55/1.81 % (3823330)Refutation not found, incomplete strategy
% 5.55/1.81 % (3823330)------------------------------
% 5.55/1.81 % (3823330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823330)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823330)Termination reason: Refutation not found, incomplete strategy
% 5.55/1.81 % (3823330)Time elapsed: 0.069 s
% 5.55/1.81 % (3823330)Peak memory usage: 13 MB
% 5.55/1.81 % (3823330)Instructions burned: 267 (million)
% 5.55/1.81 % (3823330)------------------------------
% 5.55/1.81 % (3823330)------------------------------
% 5.55/1.81 % (3823332)ott-2_1_sil=16000:newcnf=on:random_seed=1549938214:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi)
% 5.55/1.81 % (3823326)Instruction limit reached!
% 5.55/1.81 % (3823326)------------------------------
% 5.55/1.81 % (3823326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823326)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823326)Termination reason: Instruction limit
% 5.55/1.81 % (3823326)Termination phase: Saturation
% 5.55/1.81 % (3823326)Time elapsed: 0.405 s
% 5.55/1.81 % (3823326)Peak memory usage: 25 MB
% 5.55/1.81 % (3823326)Instructions burned: 1472 (million)
% 5.55/1.81 % (3823334)ott+10_1_sil=32000:tgt=ground:random_seed=3639891943:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi)
% 5.55/1.81 % (3823332)Instruction limit reached!
% 5.55/1.81 % (3823332)------------------------------
% 5.55/1.81 % (3823332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823332)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823332)Termination reason: Instruction limit
% 5.55/1.81 % (3823332)Termination phase: Saturation
% 5.55/1.81 % (3823332)Time elapsed: 0.273 s
% 5.55/1.81 % (3823332)Peak memory usage: 19 MB
% 5.55/1.81 % (3823332)Instructions burned: 871 (million)
% 5.55/1.81 % (3823336)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=587480430:i=54282_2988 on theBenchmark for (2988ds/54282Mi)
% 5.55/1.81 % TRYING [1]
% 5.55/1.81 % TRYING [2]
% 5.55/1.81 % TRYING [3]
% 5.55/1.81 % TRYING [5]
% 5.55/1.81 % TRYING [4]
% 5.55/1.81 % (3823334) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3823279-3823334"...
% 5.55/1.81 % (3823334)...printing done.
% 5.55/1.81 % (3823334)Refutation found. Thanks to Tanya!
% 5.55/1.81 % SZS status Theorem for theBenchmark
% 5.55/1.81 % SZS output start Proof for theBenchmark
% See solution above
% 5.55/1.81 % (3823334)------------------------------
% 5.55/1.81 % (3823334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.81 % (3823334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.81 % (3823334)CaDiCaL version: 2.1.3
% 5.55/1.81 % (3823334)Termination reason: Refutation
% 5.55/1.81 % (3823334)Time elapsed: 0.635 s
% 5.55/1.81 % (3823334)Peak memory usage: 28 MB
% 5.55/1.81 % (3823334)Instructions burned: 2016 (million)
% 5.55/1.81 % (3823279)Success in time 1.687 s
% 5.55/1.81 % Vampire exiting
%------------------------------------------------------------------------------