%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : COM134+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:22 AM UTC 2026
% Result : Theorem 156.69s 34.42s
% Output : Refutation 156.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 9
% Syntax : Number of formulae : 68 ( 20 unt; 0 def)
% Number of atoms : 204 ( 106 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 200 ( 64 ~; 80 |; 45 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 7 con; 0-3 aty)
% Number of variables : 233 ( 191 !; 42 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( vapp(X0,X1) = vapp(X2,X3)
=> ( X0 = X2
& X1 = X3 ) )
& ( ( X0 = X2
& X1 = X3 )
=> vapp(X0,X1) = vapp(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax','EQ-app') ).
fof(f5,axiom,
! [X0,X1,X2] : vvar(X0) != vapp(X1,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax','DIFF-var-app') ).
fof(f6,axiom,
! [X0,X1,X2,X3,X4] : vabs(X0,X1,X2) != vapp(X3,X4),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax','DIFF-abs-app') ).
fof(f31,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( X0 = X5
& X1 = X6
& X2 = vapp(X4,X7) )
=> ( X3 = vsubst(X0,X1,X2)
=> X3 = vapp(vsubst(X5,X6,X4),vsubst(X5,X6,X7)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax',subst2) ).
fof(f53,axiom,
! [X0,X1,X2,X3,X4] :
( ( vtcheck(X1,X2,varrow(X0,X4))
& vtcheck(X1,X3,X0) )
=> vtcheck(X1,vapp(X2,X3),X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax','T-app') ).
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/sandbox2/benchmark/Axioms/COM001+0.ax','T-inv') ).
fof(f58,axiom,
! [X0,X1,X2,X3,X4] :
( ( vtcheck(X1,X3,X0)
& vtcheck(vbind(X2,X0,X1),ve1,X4) )
=> vtcheck(X1,vsubst(X2,X3,ve1),X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-subst-IH-app1') ).
fof(f59,axiom,
! [X0,X1,X2,X3,X4] :
( ( vtcheck(X1,X3,X0)
& vtcheck(vbind(X2,X0,X1),ve2,X4) )
=> vtcheck(X1,vsubst(X2,X3,ve2),X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-subst-IH-app2') ).
fof(f60,conjecture,
! [X0,X1,X2,X3,X4] :
( ( vtcheck(X1,X3,X0)
& vtcheck(vbind(X2,X0,X1),vapp(ve1,ve2),X4) )
=> vtcheck(X1,vsubst(X2,X3,vapp(ve1,ve2)),X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-subst-app') ).
fof(f61,negated_conjecture,
~ ! [X0,X1,X2,X3,X4] :
( ( vtcheck(X1,X3,X0)
& vtcheck(vbind(X2,X0,X1),vapp(ve1,ve2),X4) )
=> vtcheck(X1,vsubst(X2,X3,vapp(ve1,ve2)),X4) ),
inference(negated_conjecture,[status(cth)],[f60]) ).
fof(f68,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(f72,plain,
! [X0,X1,X2,X3] :
( ( ( X0 = X2
& X1 = X3 )
| vapp(X0,X1) != vapp(X2,X3) )
& ( vapp(X0,X1) = vapp(X2,X3)
| X0 != X2
| X1 != X3 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( ( ( X0 = X2
& X1 = X3 )
| vapp(X0,X1) != vapp(X2,X3) )
& ( vapp(X0,X1) = vapp(X2,X3)
| X0 != X2
| X1 != X3 ) ),
inference(flattening,[],[f72]) ).
fof(f107,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( X3 = vapp(vsubst(X5,X6,X4),vsubst(X5,X6,X7))
| vsubst(X0,X1,X2) != X3
| X0 != X5
| X1 != X6
| vapp(X4,X7) != X2 ),
inference(ennf_transformation,[],[f31]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( X3 = vapp(vsubst(X5,X6,X4),vsubst(X5,X6,X7))
| vsubst(X0,X1,X2) != X3
| X0 != X5
| X1 != X6
| vapp(X4,X7) != X2 ),
inference(flattening,[],[f107]) ).
fof(f142,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X1,vapp(X2,X3),X4)
| ~ vtcheck(X1,X2,varrow(X0,X4))
| ~ vtcheck(X1,X3,X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f143,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X1,vapp(X2,X3),X4)
| ~ vtcheck(X1,X2,varrow(X0,X4))
| ~ vtcheck(X1,X3,X0) ),
inference(flattening,[],[f142]) ).
fof(f144,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,[],[f68]) ).
fof(f145,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,[],[f144]) ).
fof(f152,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X1,vsubst(X2,X3,ve1),X4)
| ~ vtcheck(X1,X3,X0)
| ~ vtcheck(vbind(X2,X0,X1),ve1,X4) ),
inference(ennf_transformation,[],[f58]) ).
fof(f153,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X1,vsubst(X2,X3,ve1),X4)
| ~ vtcheck(X1,X3,X0)
| ~ vtcheck(vbind(X2,X0,X1),ve1,X4) ),
inference(flattening,[],[f152]) ).
fof(f154,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X1,vsubst(X2,X3,ve2),X4)
| ~ vtcheck(X1,X3,X0)
| ~ vtcheck(vbind(X2,X0,X1),ve2,X4) ),
inference(ennf_transformation,[],[f59]) ).
fof(f155,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X1,vsubst(X2,X3,ve2),X4)
| ~ vtcheck(X1,X3,X0)
| ~ vtcheck(vbind(X2,X0,X1),ve2,X4) ),
inference(flattening,[],[f154]) ).
fof(f156,plain,
? [X0,X1,X2,X3,X4] :
( ~ vtcheck(X1,vsubst(X2,X3,vapp(ve1,ve2)),X4)
& vtcheck(X1,X3,X0)
& vtcheck(vbind(X2,X0,X1),vapp(ve1,ve2),X4) ),
inference(ennf_transformation,[],[f61]) ).
fof(f157,plain,
? [X0,X1,X2,X3,X4] :
( ~ vtcheck(X1,vsubst(X2,X3,vapp(ve1,ve2)),X4)
& vtcheck(X1,X3,X0)
& vtcheck(vbind(X2,X0,X1),vapp(ve1,ve2),X4) ),
inference(flattening,[],[f156]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ( vvar(sK66(X0,X1,X2)) = X0
& vsomeType(X1) = vlookup(sK66(X0,X1,X2),X2) )
| ( vabs(sK67(X0,X1,X2),sK69(X0,X1,X2),sK68(X0,X1,X2)) = X0
& varrow(sK69(X0,X1,X2),sK70(X0,X1,X2)) = X1
& vtcheck(vbind(sK67(X0,X1,X2),sK69(X0,X1,X2),X2),sK68(X0,X1,X2),sK70(X0,X1,X2)) )
| ( vapp(sK71(X0,X1,X2),sK72(X0,X1,X2)) = X0
& vtcheck(X2,sK71(X0,X1,X2),varrow(sK73(X0,X1,X2),X1))
& vtcheck(X2,sK72(X0,X1,X2),sK73(X0,X1,X2)) )
| ~ vtcheck(X2,X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66,sK67,sK68,sK69,sK70,sK71,sK72,sK73]),skolemize(X3,sK66(X0,X1,X2)),skolemize(X4,sK67(X0,X1,X2)),skolemize(X5,sK68(X0,X1,X2)),skolemize(X6,sK69(X0,X1,X2)),skolemize(X7,sK70(X0,X1,X2)),skolemize(X8,sK71(X0,X1,X2)),skolemize(X9,sK72(X0,X1,X2)),skolemize(X10,sK73(X0,X1,X2))],[f145]) ).
fof(f164,plain,
( ~ vtcheck(sK75,vsubst(sK76,sK77,vapp(ve1,ve2)),sK78)
& vtcheck(sK75,sK77,sK74)
& vtcheck(vbind(sK76,sK74,sK75),vapp(ve1,ve2),sK78) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK74,sK75,sK76,sK77,sK78]),skolemize(X0,sK74),skolemize(X1,sK75),skolemize(X2,sK76),skolemize(X3,sK77),skolemize(X4,sK78)],[f157]) ).
fof(f172,plain,
! [X2,X3,X0,X1] :
( vapp(X0,X1) != vapp(X2,X3)
| X1 = X3 ),
inference(cnf_transformation,[],[f73]) ).
fof(f173,plain,
! [X2,X3,X0,X1] :
( vapp(X0,X1) != vapp(X2,X3)
| X0 = X2 ),
inference(cnf_transformation,[],[f73]) ).
fof(f175,plain,
! [X2,X0,X1] : vvar(X0) != vapp(X1,X2),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
! [X2,X3,X0,X1,X4] : vabs(X0,X1,X2) != vapp(X3,X4),
inference(cnf_transformation,[],[f6]) ).
fof(f257,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( vapp(vsubst(X5,X6,X4),vsubst(X5,X6,X7)) = X3
| vsubst(X0,X1,X2) != X3
| X0 != X5
| X1 != X6
| vapp(X4,X7) != X2 ),
inference(cnf_transformation,[],[f108]) ).
fof(f31280,plain,
! [X2,X3,X0,X1,X4] :
( ~ vtcheck(X1,X2,varrow(X0,X4))
| vtcheck(X1,vapp(X2,X3),X4)
| ~ vtcheck(X1,X3,X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f31296,plain,
! [X2,X0,X1] :
( ~ vtcheck(X2,X0,X1)
| vabs(sK67(X0,X1,X2),sK69(X0,X1,X2),sK68(X0,X1,X2)) = X0
| vtcheck(X2,sK72(X0,X1,X2),sK73(X0,X1,X2))
| vvar(sK66(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f163]) ).
fof(f31297,plain,
! [X2,X0,X1] :
( ~ vtcheck(X2,X0,X1)
| vabs(sK67(X0,X1,X2),sK69(X0,X1,X2),sK68(X0,X1,X2)) = X0
| vtcheck(X2,sK71(X0,X1,X2),varrow(sK73(X0,X1,X2),X1))
| vvar(sK66(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f163]) ).
fof(f31298,plain,
! [X2,X0,X1] :
( ~ vtcheck(X2,X0,X1)
| vabs(sK67(X0,X1,X2),sK69(X0,X1,X2),sK68(X0,X1,X2)) = X0
| vapp(sK71(X0,X1,X2),sK72(X0,X1,X2)) = X0
| vvar(sK66(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f163]) ).
fof(f31302,plain,
! [X2,X3,X0,X1,X4] :
( ~ vtcheck(vbind(X2,X0,X1),ve1,X4)
| ~ vtcheck(X1,X3,X0)
| vtcheck(X1,vsubst(X2,X3,ve1),X4) ),
inference(cnf_transformation,[],[f153]) ).
fof(f31303,plain,
! [X2,X3,X0,X1,X4] :
( ~ vtcheck(vbind(X2,X0,X1),ve2,X4)
| ~ vtcheck(X1,X3,X0)
| vtcheck(X1,vsubst(X2,X3,ve2),X4) ),
inference(cnf_transformation,[],[f155]) ).
fof(f31304,plain,
vtcheck(vbind(sK76,sK74,sK75),vapp(ve1,ve2),sK78),
inference(cnf_transformation,[],[f164]) ).
fof(f31305,plain,
vtcheck(sK75,sK77,sK74),
inference(cnf_transformation,[],[f164]) ).
fof(f31306,plain,
~ vtcheck(sK75,vsubst(sK76,sK77,vapp(ve1,ve2)),sK78),
inference(cnf_transformation,[],[f164]) ).
fof(f31411,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( vsubst(X0,X1,X2) = vapp(vsubst(X5,X6,X4),vsubst(X5,X6,X7))
| X0 != X5
| X1 != X6
| vapp(X4,X7) != X2 ),
inference(equality_resolution,[],[f257]) ).
fof(f31412,plain,
! [X2,X1,X6,X7,X4,X5] :
( vapp(vsubst(X5,X6,X4),vsubst(X5,X6,X7)) = vsubst(X5,X1,X2)
| X1 != X6
| vapp(X4,X7) != X2 ),
inference(equality_resolution,[],[f31411]) ).
fof(f31413,plain,
! [X2,X6,X7,X4,X5] :
( vapp(vsubst(X5,X6,X4),vsubst(X5,X6,X7)) = vsubst(X5,X6,X2)
| vapp(X4,X7) != X2 ),
inference(equality_resolution,[],[f31412]) ).
fof(f31414,plain,
! [X6,X7,X4,X5] : vapp(vsubst(X5,X6,X4),vsubst(X5,X6,X7)) = vsubst(X5,X6,vapp(X4,X7)),
inference(equality_resolution,[],[f31413]) ).
fof(f85377,plain,
( vapp(ve1,ve2) = vabs(sK67(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK69(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK68(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)))
| vtcheck(vbind(sK76,sK74,sK75),sK72(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)))
| vapp(ve1,ve2) = vvar(sK66(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))) ),
inference(resolution,[],[f31296,f31304]) ).
fof(f85387,plain,
( vtcheck(vbind(sK76,sK74,sK75),sK72(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)))
| vapp(ve1,ve2) = vvar(sK66(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))) ),
inference(forward_subsumption_resolution,[],[f85377,f176]) ).
fof(f85409,plain,
vtcheck(vbind(sK76,sK74,sK75),sK72(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))),
inference(forward_subsumption_resolution,[],[f85387,f175]) ).
fof(f87799,plain,
( vapp(ve1,ve2) = vabs(sK67(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK69(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK68(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)))
| vapp(ve1,ve2) = vapp(sK71(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK72(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)))
| vapp(ve1,ve2) = vvar(sK66(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))) ),
inference(resolution,[],[f31298,f31304]) ).
fof(f87810,plain,
( vapp(ve1,ve2) = vapp(sK71(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK72(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)))
| vapp(ve1,ve2) = vvar(sK66(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))) ),
inference(forward_subsumption_resolution,[],[f87799,f176]) ).
fof(f87832,plain,
vapp(ve1,ve2) = vapp(sK71(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK72(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))),
inference(forward_subsumption_resolution,[],[f87810,f175]) ).
fof(f87851,plain,
! [X0,X1] :
( vapp(X0,X1) != vapp(ve1,ve2)
| sK72(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)) = X1 ),
inference(superposition,[],[f172,f87832]) ).
fof(f87853,plain,
! [X0,X1] :
( vapp(X0,X1) != vapp(ve1,ve2)
| sK71(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)) = X0 ),
inference(superposition,[],[f173,f87832]) ).
fof(f87861,plain,
ve2 = sK72(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),
inference(equality_resolution,[],[f87851]) ).
fof(f87863,plain,
vtcheck(vbind(sK76,sK74,sK75),ve2,sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))),
inference(superposition,[],[f85409,f87861]) ).
fof(f87874,plain,
! [X0] :
( ~ vtcheck(sK75,X0,sK74)
| vtcheck(sK75,vsubst(sK76,X0,ve2),sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))) ),
inference(resolution,[],[f87863,f31303]) ).
fof(f95030,plain,
ve1 = sK71(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),
inference(equality_resolution,[],[f87853]) ).
fof(f95038,plain,
vtcheck(sK75,vsubst(sK76,sK77,ve2),sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))),
inference(resolution,[],[f87874,f31305]) ).
fof(f95644,plain,
( vapp(ve1,ve2) = vabs(sK67(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK69(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK68(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)))
| vtcheck(vbind(sK76,sK74,sK75),sK71(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),varrow(sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK78))
| vapp(ve1,ve2) = vvar(sK66(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))) ),
inference(resolution,[],[f31297,f31304]) ).
fof(f95657,plain,
( vtcheck(vbind(sK76,sK74,sK75),sK71(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),varrow(sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK78))
| vapp(ve1,ve2) = vvar(sK66(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75))) ),
inference(forward_subsumption_resolution,[],[f95644,f176]) ).
fof(f95681,plain,
vtcheck(vbind(sK76,sK74,sK75),sK71(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),varrow(sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK78)),
inference(forward_subsumption_resolution,[],[f95657,f175]) ).
fof(f95690,plain,
vtcheck(vbind(sK76,sK74,sK75),ve1,varrow(sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK78)),
inference(forward_demodulation,[],[f95681,f95030]) ).
fof(f95691,plain,
! [X0] :
( ~ vtcheck(sK75,X0,sK74)
| vtcheck(sK75,vsubst(sK76,X0,ve1),varrow(sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK78)) ),
inference(resolution,[],[f95690,f31302]) ).
fof(f97874,plain,
vtcheck(sK75,vsubst(sK76,sK77,ve1),varrow(sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)),sK78)),
inference(resolution,[],[f95691,f31305]) ).
fof(f97876,plain,
! [X0] :
( ~ vtcheck(sK75,X0,sK73(vapp(ve1,ve2),sK78,vbind(sK76,sK74,sK75)))
| vtcheck(sK75,vapp(vsubst(sK76,sK77,ve1),X0),sK78) ),
inference(resolution,[],[f97874,f31280]) ).
fof(f97889,plain,
vtcheck(sK75,vapp(vsubst(sK76,sK77,ve1),vsubst(sK76,sK77,ve2)),sK78),
inference(resolution,[],[f97876,f95038]) ).
fof(f97890,plain,
vtcheck(sK75,vsubst(sK76,sK77,vapp(ve1,ve2)),sK78),
inference(forward_demodulation,[],[f97889,f31414]) ).
fof(f97891,plain,
$false,
inference(forward_subsumption_resolution,[],[f97890,f31306]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM134+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n013.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 21:54:51 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.26/1.55 % (1623684)Will run a generic schedule for satisfiability detection.
% 8.26/1.55 % (1623693)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3063843003:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.26/1.55 % (1623690)% WARNING: option uhcvi not known.
% 8.26/1.55 % (1623689)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1320785628_2999 on theBenchmark for (2999ds/0Mi)
% 8.26/1.55 % (1623692)dis+10_1_sil=32000:sp=arity:random_seed=250866981:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.26/1.55 % (1623690)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1336567670:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.26/1.55 % (1623691)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3336095498:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.26/1.55 % (1623695)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2791457420:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.26/1.55 % (1623694)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=717825428:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.26/1.55 % TRYING [1]
% 8.26/1.55 % TRYING [2]
% 8.26/1.55 % (1623693)Instruction limit reached!
% 8.26/1.55 % (1623693)------------------------------
% 8.26/1.55 % (1623693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.55 % (1623693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.55 % (1623693)CaDiCaL version: 2.1.3
% 8.26/1.55 % (1623693)Termination reason: Instruction limit
% 8.26/1.55 % (1623693)Termination phase: Saturation
% 8.26/1.55 % (1623693)Time elapsed: 0.034 s
% 8.26/1.55 % (1623693)Peak memory usage: 13 MB
% 8.26/1.55 % (1623693)Instructions burned: 116 (million)
% 8.26/1.55 % TRYING [3]
% 8.26/1.55 % (1623703)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3955629961:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.26/1.55 % TRYING [1]
% 8.26/1.55 % TRYING [2]
% 8.26/1.55 % TRYING [3]
% 8.26/1.55 % (1623692)Instruction limit reached!
% 8.26/1.55 % (1623692)------------------------------
% 8.26/1.55 % (1623692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.55 % (1623692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.55 % (1623692)CaDiCaL version: 2.1.3
% 8.26/1.55 % (1623692)Termination reason: Instruction limit
% 8.26/1.55 % (1623692)Termination phase: Saturation
% 8.26/1.55 % (1623692)Time elapsed: 0.063 s
% 8.26/1.55 % (1623692)Peak memory usage: 13 MB
% 8.26/1.55 % (1623692)Instructions burned: 104 (million)
% 8.26/1.55 % (1623694)Instruction limit reached!
% 8.26/1.55 % (1623694)------------------------------
% 8.26/1.55 % (1623694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.55 % (1623694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.55 % (1623694)CaDiCaL version: 2.1.3
% 8.26/1.55 % (1623694)Termination reason: Instruction limit
% 8.26/1.55 % (1623694)Termination phase: Saturation
% 8.26/1.55 % (1623694)Time elapsed: 0.081 s
% 8.26/1.55 % (1623694)Peak memory usage: 13 MB
% 8.26/1.55 % (1623705)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2495322983:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.26/1.55 % (1623694)Instructions burned: 132 (million)
% 8.26/1.55 % (1623695)Instruction limit reached!
% 8.26/1.55 % (1623695)------------------------------
% 8.26/1.55 % (1623695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.55 % (1623695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.55 % (1623695)CaDiCaL version: 2.1.3
% 8.26/1.55 % (1623695)Termination reason: Instruction limit
% 8.26/1.55 % (1623695)Termination phase: Saturation
% 8.26/1.55 % (1623695)Time elapsed: 0.100 s
% 8.26/1.55 % (1623695)Peak memory usage: 14 MB
% 8.26/1.55 % (1623695)Instructions burned: 160 (million)
% 8.26/1.55 % (1623707)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=3586278088:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.26/1.55 % (1623709)ott-21_1_sil=16000:fs=off:random_seed=757690013:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.26/1.55 % (1623705)Instruction limit reached!
% 8.26/1.55 % (1623705)------------------------------
% 8.26/1.55 % (1623705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.55 % (1623705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.08/5.11 % (1623705)CaDiCaL version: 2.1.3
% 34.08/5.11 % (1623705)Termination reason: Instruction limit
% 34.08/5.11 % (1623705)Termination phase: Saturation
% 34.08/5.11 % (1623705)Time elapsed: 0.076 s
% 34.08/5.11 % (1623705)Peak memory usage: 13 MB
% 34.08/5.11 % (1623705)Instructions burned: 132 (million)
% 34.08/5.11 % (1623711)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3531140566:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 34.08/5.11 % (1623703)Instruction limit reached!
% 34.08/5.11 % (1623703)------------------------------
% 34.08/5.11 % (1623703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.08/5.11 % (1623703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.08/5.11 % (1623703)CaDiCaL version: 2.1.3
% 34.08/5.11 % (1623703)Termination reason: Instruction limit
% 34.08/5.11 % (1623703)Termination phase: Finite model building constraint generation
% 34.08/5.11 % (1623703)Time elapsed: 0.142 s
% 34.08/5.11 % (1623703)Peak memory usage: 42 MB
% 34.08/5.11 % (1623703)Instructions burned: 716 (million)
% 34.08/5.11 % (1623713)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4198285181:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 34.08/5.11 % TRYING [1]
% 34.08/5.11 % TRYING [2]
% 34.08/5.11 % (1623709)Instruction limit reached!
% 34.08/5.11 % (1623709)------------------------------
% 34.08/5.11 % (1623709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.08/5.11 % (1623709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.08/5.11 % (1623709)CaDiCaL version: 2.1.3
% 34.08/5.11 % (1623709)Termination reason: Instruction limit
% 34.08/5.11 % (1623709)Termination phase: Saturation
% 34.08/5.11 % (1623709)Time elapsed: 0.096 s
% 34.08/5.11 % (1623709)Peak memory usage: 13 MB
% 34.08/5.11 % (1623709)Instructions burned: 181 (million)
% 34.08/5.11 % TRYING [3]
% 34.08/5.11 % (1623715)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2405838603:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 34.08/5.11 % TRYING [4]
% 34.08/5.11 % (1623713)Instruction limit reached!
% 34.08/5.11 % (1623713)------------------------------
% 34.08/5.11 % (1623713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.08/5.11 % (1623713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.08/5.11 % (1623713)CaDiCaL version: 2.1.3
% 34.08/5.11 % (1623713)Termination reason: Instruction limit
% 34.08/5.11 % (1623713)Termination phase: Finite model building SAT solving
% 34.08/5.11 % (1623713)Time elapsed: 0.180 s
% 34.08/5.11 % (1623713)Peak memory usage: 35 MB
% 34.08/5.11 % (1623713)Instructions burned: 870 (million)
% 34.08/5.11 % (1623717)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4124356175:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 34.08/5.11 % (1623711)Instruction limit reached!
% 34.08/5.11 % (1623711)------------------------------
% 34.08/5.11 % (1623711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.08/5.11 % (1623711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.08/5.11 % (1623711)CaDiCaL version: 2.1.3
% 34.08/5.11 % (1623711)Termination reason: Instruction limit
% 34.08/5.11 % (1623711)Termination phase: Saturation
% 34.08/5.11 % (1623711)Time elapsed: 0.276 s
% 34.08/5.11 % (1623711)Peak memory usage: 14 MB
% 34.08/5.11 % (1623711)Instructions burned: 478 (million)
% 34.08/5.11 % (1623719)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=1268934806:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 34.08/5.11 % (1623707)Instruction limit reached!
% 34.08/5.11 % (1623707)------------------------------
% 34.08/5.11 % (1623707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.08/5.11 % (1623707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.08/5.11 % (1623707)CaDiCaL version: 2.1.3
% 34.08/5.11 % (1623707)Termination reason: Instruction limit
% 34.08/5.11 % (1623707)Termination phase: Saturation
% 34.08/5.11 % (1623707)Time elapsed: 0.407 s
% 34.08/5.11 % (1623707)Peak memory usage: 18 MB
% 34.08/5.11 % (1623707)Instructions burned: 684 (million)
% 34.08/5.11 % (1623721)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1011319207:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 34.08/5.11 % (1623717)Instruction limit reached!
% 34.08/5.11 % (1623717)------------------------------
% 34.08/5.11 % (1623717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.77/10.12 % (1623717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.77/10.12 % (1623717)CaDiCaL version: 2.1.3
% 69.77/10.12 % (1623717)Termination reason: Instruction limit
% 69.77/10.12 % (1623717)Termination phase: Finite model building constraint generation
% 69.77/10.12 % (1623717)Time elapsed: 0.243 s
% 69.77/10.12 % (1623717)Peak memory usage: 111 MB
% 69.77/10.12 % (1623717)Instructions burned: 892 (million)
% 69.77/10.12 % (1623723)fmb+10_1_sil=64000:random_seed=1968807926:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 69.77/10.12 % TRYING [1]
% 69.77/10.12 % TRYING [2]
% 69.77/10.12 % TRYING [3]
% 69.77/10.12 % (1623719)Instruction limit reached!
% 69.77/10.12 % (1623719)------------------------------
% 69.77/10.12 % (1623719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.77/10.12 % (1623719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.77/10.12 % (1623719)CaDiCaL version: 2.1.3
% 69.77/10.12 % (1623719)Termination reason: Instruction limit
% 69.77/10.12 % (1623719)Termination phase: Saturation
% 69.77/10.12 % (1623719)Time elapsed: 0.452 s
% 69.77/10.12 % (1623719)Peak memory usage: 19 MB
% 69.77/10.12 % (1623719)Instructions burned: 692 (million)
% 69.77/10.12 % (1623715)Instruction limit reached!
% 69.77/10.12 % (1623715)------------------------------
% 69.77/10.12 % (1623715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.77/10.12 % (1623715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.77/10.12 % (1623715)CaDiCaL version: 2.1.3
% 69.77/10.12 % (1623715)Termination reason: Instruction limit
% 69.77/10.12 % (1623715)Termination phase: Saturation
% 69.77/10.12 % (1623715)Time elapsed: 0.694 s
% 69.77/10.12 % (1623715)Peak memory usage: 25 MB
% 69.77/10.12 % (1623715)Instructions burned: 1181 (million)
% 69.77/10.12 % (1623725)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=768494118:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 69.77/10.12 % (1623726)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3802745979:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 69.77/10.12 % (1623725)Cannot represent all propositional literals internally
% 69.77/10.12 % (1623725)Refutation not found, incomplete strategy
% 69.77/10.12 % (1623725)------------------------------
% 69.77/10.12 % (1623725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.77/10.12 % (1623725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.77/10.12 % (1623725)CaDiCaL version: 2.1.3
% 69.77/10.12 % (1623725)Termination reason: Refutation not found, incomplete strategy
% 69.77/10.12 % (1623725)Time elapsed: 0.018 s
% 69.77/10.12 % (1623725)Peak memory usage: 11 MB
% 69.77/10.12 % (1623725)Instructions burned: 34 (million)
% 69.77/10.12 % (1623725)------------------------------
% 69.77/10.12 % (1623725)------------------------------
% 69.77/10.12 % TRYING [4]
% 69.77/10.12 % TRYING [8]
% 69.77/10.12 % (1623729)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4287481659:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 69.77/10.12 % (1623721)Instruction limit reached!
% 69.77/10.12 % (1623721)------------------------------
% 69.77/10.12 % (1623721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.77/10.12 % (1623721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.77/10.12 % (1623721)CaDiCaL version: 2.1.3
% 69.77/10.12 % (1623721)Termination reason: Instruction limit
% 69.77/10.12 % (1623721)Termination phase: Saturation
% 69.77/10.12 % (1623721)Time elapsed: 0.490 s
% 69.77/10.12 % (1623721)Peak memory usage: 19 MB
% 69.77/10.12 % (1623721)Instructions burned: 880 (million)
% 69.77/10.12 % (1623731)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1804229432:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 69.77/10.12 % (1623726)Instruction limit reached!
% 69.77/10.12 % (1623726)------------------------------
% 69.77/10.12 % (1623726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.77/10.12 % (1623726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.77/10.12 % (1623726)CaDiCaL version: 2.1.3
% 69.77/10.12 % (1623726)Termination reason: Instruction limit
% 69.77/10.12 % (1623726)Termination phase: Finite model building constraint generation
% 69.77/10.12 % (1623726)Time elapsed: 0.314 s
% 69.77/10.12 % (1623726)Peak memory usage: 60 MB
% 69.77/10.12 % (1623726)Instructions burned: 923 (million)
% 69.77/10.12 % (1623733)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3083825988:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 175.03/24.97 % (1623733)Cannot represent all propositional literals internally
% 175.03/24.97 % (1623733)Refutation not found, incomplete strategy
% 175.03/24.97 % (1623733)------------------------------
% 175.03/24.97 % (1623733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.03/24.97 % (1623733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/24.97 % (1623733)CaDiCaL version: 2.1.3
% 175.03/24.97 % (1623733)Termination reason: Refutation not found, incomplete strategy
% 175.03/24.97 % (1623733)Time elapsed: 0.019 s
% 175.03/24.97 % (1623733)Peak memory usage: 11 MB
% 175.03/24.97 % (1623733)Instructions burned: 38 (million)
% 175.03/24.97 % (1623733)------------------------------
% 175.03/24.97 % (1623733)------------------------------
% 175.03/24.97 % (1623735)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1975636280:fmbsr=2.30978:i=2174_2986 on theBenchmark for (2986ds/2174Mi)
% 175.03/24.97 % (1623735)Cannot represent all propositional literals internally
% 175.03/24.97 % (1623735)Refutation not found, incomplete strategy
% 175.03/24.97 % (1623735)------------------------------
% 175.03/24.97 % (1623735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.03/24.97 % (1623735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/24.97 % (1623735)CaDiCaL version: 2.1.3
% 175.03/24.97 % (1623735)Termination reason: Refutation not found, incomplete strategy
% 175.03/24.97 % (1623735)Time elapsed: 0.133 s
% 175.03/24.97 % (1623735)Peak memory usage: 13 MB
% 175.03/24.97 % (1623735)Instructions burned: 270 (million)
% 175.03/24.97 % (1623735)------------------------------
% 175.03/24.97 % (1623735)------------------------------
% 175.03/24.97 % (1623737)ott-2_1_sil=16000:newcnf=on:random_seed=2785488292:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2984 on theBenchmark for (2984ds/869Mi)
% 175.03/24.97 % (1623731)Instruction limit reached!
% 175.03/24.97 % (1623731)------------------------------
% 175.03/24.97 % (1623731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.03/24.97 % (1623731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/24.97 % (1623731)CaDiCaL version: 2.1.3
% 175.03/24.97 % (1623731)Termination reason: Instruction limit
% 175.03/24.97 % (1623731)Termination phase: Saturation
% 175.03/24.97 % (1623731)Time elapsed: 0.742 s
% 175.03/24.97 % (1623731)Peak memory usage: 25 MB
% 175.03/24.97 % (1623731)Instructions burned: 1473 (million)
% 175.03/24.97 % (1623739)ott+10_1_sil=32000:tgt=ground:random_seed=1413193741:i=5114:av=off_2981 on theBenchmark for (2981ds/5114Mi)
% 175.03/24.97 % (1623737)Instruction limit reached!
% 175.03/24.97 % (1623737)------------------------------
% 175.03/24.97 % (1623737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.03/24.97 % (1623737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/24.97 % (1623737)CaDiCaL version: 2.1.3
% 175.03/24.97 % (1623737)Termination reason: Instruction limit
% 175.03/24.97 % (1623737)Termination phase: Saturation
% 175.03/24.97 % (1623737)Time elapsed: 0.506 s
% 175.03/24.97 % (1623737)Peak memory usage: 22 MB
% 175.03/24.97 % (1623737)Instructions burned: 870 (million)
% 175.03/24.97 % (1623741)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3841919108:i=54282_2979 on theBenchmark for (2979ds/54282Mi)
% 175.03/24.97 % TRYING [1]
% 175.03/24.97 % TRYING [2]
% 175.03/24.97 % TRYING [3]
% 175.03/24.97 % TRYING [5]
% 175.03/24.97 % TRYING [4]
% 175.03/24.97 % (1623729)Instruction limit reached!
% 175.03/24.97 % (1623729)------------------------------
% 175.03/24.97 % (1623729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.03/24.97 % (1623729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/24.97 % (1623729)CaDiCaL version: 2.1.3
% 175.03/24.97 % (1623729)Termination reason: Instruction limit
% 175.03/24.97 % (1623729)Termination phase: Saturation
% 175.03/24.97 % (1623729)Time elapsed: 2.503 s
% 175.03/24.97 % (1623729)Peak memory usage: 30 MB
% 175.03/24.97 % (1623729)Instructions burned: 5131 (million)
% 175.03/24.97 % (1623743)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4036705640:i=3512:aac=none_2964 on theBenchmark for (2964ds/3512Mi)
% 175.03/24.97 % TRYING [5]
% 175.03/24.97 % TRYING [5]
% 175.03/24.97 % (1623739)Instruction limit reached!
% 175.03/24.97 % (1623739)------------------------------
% 175.03/24.97 % (1623739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.03/24.97 % (1623739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/24.97 % (1623739)CaDiCaL version: 2.1.3
% 175.03/24.97 % (1623739)Termination reason: Instruction limit
% 175.03/24.97 % (1623739)Termination phase: Saturation
% 175.03/24.97 % (1623739)Time elapsed: 3.047 s
% 156.69/34.41 % (1623739)Peak memory usage: 53 MB
% 156.69/34.41 % (1623739)Instructions burned: 5114 (million)
% 156.69/34.41 % (1623745)dis+21_1_sil=32000:sas=cadical:random_seed=1658984602:i=3773:amm=off_2950 on theBenchmark for (2950ds/3773Mi)
% 156.69/34.41 % (1623723)Instruction limit reached!
% 156.69/34.41 % (1623723)------------------------------
% 156.69/34.41 % (1623723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623723)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623723)Termination reason: Instruction limit
% 156.69/34.41 % (1623723)Termination phase: Finite model building constraint generation
% 156.69/34.41 % (1623723)Time elapsed: 4.587 s
% 156.69/34.41 % (1623723)Peak memory usage: 382 MB
% 156.69/34.41 % (1623723)Instructions burned: 22068 (million)
% 156.69/34.41 % (1623747)ott+11_1_sil=16000:gs=on:random_seed=1974106569:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2946 on theBenchmark for (2946ds/2251Mi)
% 156.69/34.41 % (1623743)Instruction limit reached!
% 156.69/34.41 % (1623743)------------------------------
% 156.69/34.41 % (1623743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623743)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623743)Termination reason: Instruction limit
% 156.69/34.41 % (1623743)Termination phase: Saturation
% 156.69/34.41 % (1623743)Time elapsed: 1.902 s
% 156.69/34.41 % (1623743)Peak memory usage: 34 MB
% 156.69/34.41 % (1623743)Instructions burned: 3513 (million)
% 156.69/34.41 % (1623749)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1871610190:fmbsr=1.6:i=67534_2945 on theBenchmark for (2945ds/67534Mi)
% 156.69/34.41 % (1623747)Instruction limit reached!
% 156.69/34.41 % (1623747)------------------------------
% 156.69/34.41 % (1623747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623747)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623747)Termination reason: Instruction limit
% 156.69/34.41 % (1623747)Termination phase: Saturation
% 156.69/34.41 % (1623747)Time elapsed: 0.524 s
% 156.69/34.41 % (1623747)Peak memory usage: 16 MB
% 156.69/34.41 % (1623747)Instructions burned: 2253 (million)
% 156.69/34.41 % (1623751)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=358636201:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2941 on theBenchmark for (2941ds/4591Mi)
% 156.69/34.41 % TRYING [7]
% 156.69/34.41 % (1623751)Instruction limit reached!
% 156.69/34.41 % (1623751)------------------------------
% 156.69/34.41 % (1623751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623751)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623751)Termination reason: Instruction limit
% 156.69/34.41 % (1623751)Termination phase: Saturation
% 156.69/34.41 % (1623751)Time elapsed: 1.039 s
% 156.69/34.41 % (1623751)Peak memory usage: 38 MB
% 156.69/34.41 % (1623751)Instructions burned: 4596 (million)
% 156.69/34.41 % (1623753)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=115580197:i=29340_2930 on theBenchmark for (2930ds/29340Mi)
% 156.69/34.41 % (1623745)Instruction limit reached!
% 156.69/34.41 % (1623745)------------------------------
% 156.69/34.41 % (1623745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623745)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623745)Termination reason: Instruction limit
% 156.69/34.41 % (1623745)Termination phase: Saturation
% 156.69/34.41 % (1623745)Time elapsed: 2.089 s
% 156.69/34.41 % (1623745)Peak memory usage: 36 MB
% 156.69/34.41 % (1623745)Instructions burned: 3774 (million)
% 156.69/34.41 % (1623755)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3300590400:i=5211_2929 on theBenchmark for (2929ds/5211Mi)
% 156.69/34.41 % (1623755)Instruction limit reached!
% 156.69/34.41 % (1623755)------------------------------
% 156.69/34.41 % (1623755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623755)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623755)Termination reason: Instruction limit
% 156.69/34.41 % (1623755)Termination phase: Saturation
% 156.69/34.41 % (1623755)Time elapsed: 2.866 s
% 156.69/34.41 % (1623755)Peak memory usage: 58 MB
% 156.69/34.41 % (1623755)Instructions burned: 5212 (million)
% 156.69/34.41 % (1623757)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1344600912:i=5497:nm=2_2900 on theBenchmark for (2900ds/5497Mi)
% 156.69/34.41 % TRYING [17]
% 156.69/34.41 % (1623757)Instruction limit reached!
% 156.69/34.41 % (1623757)------------------------------
% 156.69/34.41 % (1623757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623757)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623757)Termination reason: Instruction limit
% 156.69/34.41 % (1623757)Termination phase: Finite model building constraint generation
% 156.69/34.41 % (1623757)Time elapsed: 1.936 s
% 156.69/34.41 % (1623757)Peak memory usage: 386 MB
% 156.69/34.41 % (1623757)Instructions burned: 5500 (million)
% 156.69/34.41 % (1623759)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=629005473:fmbsr=2:i=46332_2880 on theBenchmark for (2880ds/46332Mi)
% 156.69/34.41 % TRYING [15]
% 156.69/34.41 % TRYING [6]
% 156.69/34.41 % (1623753)Instruction limit reached!
% 156.69/34.41 % (1623753)------------------------------
% 156.69/34.41 % (1623753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623753)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623753)Termination reason: Instruction limit
% 156.69/34.41 % (1623753)Termination phase: Saturation
% 156.69/34.41 % (1623753)Time elapsed: 8.114 s
% 156.69/34.41 % (1623753)Peak memory usage: 247 MB
% 156.69/34.41 % (1623753)Instructions burned: 29342 (million)
% 156.69/34.41 % (1623761)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=627756494:i=14071_2849 on theBenchmark for (2849ds/14071Mi)
% 156.69/34.41 % TRYING [12]
% 156.69/34.41 % TRYING [6]
% 156.69/34.41 % (1623761)Instruction limit reached!
% 156.69/34.41 % (1623761)------------------------------
% 156.69/34.41 % (1623761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.41 % (1623761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.41 % (1623761)CaDiCaL version: 2.1.3
% 156.69/34.41 % (1623761)Termination reason: Instruction limit
% 156.69/34.41 % (1623761)Termination phase: Finite model building constraint generation
% 156.69/34.42 % (1623761)Time elapsed: 2.641 s
% 156.69/34.42 % (1623761)Peak memory usage: 737 MB
% 156.69/34.42 % (1623761)Instructions burned: 14073 (million)
% 156.69/34.42 % (1623763)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2049096675:i=22565:add=on:rawr=on_2822 on theBenchmark for (2822ds/22565Mi)
% 156.69/34.42 % (1623741)Instruction limit reached!
% 156.69/34.42 % (1623741)------------------------------
% 156.69/34.42 % (1623741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.42 % (1623741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.42 % (1623741)CaDiCaL version: 2.1.3
% 156.69/34.42 % (1623741)Termination reason: Instruction limit
% 156.69/34.42 % (1623741)Termination phase: Finite model building constraint generation
% 156.69/34.42 % (1623741)Time elapsed: 18.688 s
% 156.69/34.42 % (1623741)Peak memory usage: 1292 MB
% 156.69/34.42 % (1623741)Instructions burned: 54285 (million)
% 156.69/34.42 % (1623765)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3119242494:i=8173:av=off_2790 on theBenchmark for (2790ds/8173Mi)
% 156.69/34.42 % (1623763)Instruction limit reached!
% 156.69/34.42 % (1623763)------------------------------
% 156.69/34.42 % (1623763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.42 % (1623763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.42 % (1623763)CaDiCaL version: 2.1.3
% 156.69/34.42 % (1623763)Termination reason: Instruction limit
% 156.69/34.42 % (1623763)Termination phase: Saturation
% 156.69/34.42 % (1623763)Time elapsed: 4.400 s
% 156.69/34.42 % (1623763)Peak memory usage: 54 MB
% 156.69/34.42 % (1623763)Instructions burned: 22570 (million)
% 156.69/34.42 % (1623767)dis+10_16:1_sil=16000:random_seed=1623711756:i=9155:fsr=off_2778 on theBenchmark for (2778ds/9155Mi)
% 156.69/34.42 % (1623767)Instruction limit reached!
% 156.69/34.42 % (1623767)------------------------------
% 156.69/34.42 % (1623767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.42 % (1623767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.42 % (1623767)CaDiCaL version: 2.1.3
% 156.69/34.42 % (1623767)Termination reason: Instruction limit
% 156.69/34.42 % (1623767)Termination phase: Saturation
% 156.69/34.42 % (1623767)Time elapsed: 2.557 s
% 156.69/34.42 % (1623767)Peak memory usage: 47 MB
% 156.69/34.42 % (1623767)Instructions burned: 9158 (million)
% 156.69/34.42 % (1623769)ott-3_8_sil=64000:random_seed=22244238:i=20139:bs=on_2752 on theBenchmark for (2752ds/20139Mi)
% 156.69/34.42 % (1623765)Instruction limit reached!
% 156.69/34.42 % (1623765)------------------------------
% 156.69/34.42 % (1623765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.42 % (1623765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.42 % (1623765)CaDiCaL version: 2.1.3
% 156.69/34.42 % (1623765)Termination reason: Instruction limit
% 156.69/34.42 % (1623765)Termination phase: Saturation
% 156.69/34.42 % (1623765)Time elapsed: 4.465 s
% 156.69/34.42 % (1623765)Peak memory usage: 73 MB
% 156.69/34.42 % (1623765)Instructions burned: 8173 (million)
% 156.69/34.42 % (1623771)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1386514164:fmbsr=2:i=32576_2745 on theBenchmark for (2745ds/32576Mi)
% 156.69/34.42 % TRYING [9]
% 156.69/34.42 % (1623749)Instruction limit reached!
% 156.69/34.42 % (1623749)------------------------------
% 156.69/34.42 % (1623749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.42 % (1623749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.42 % (1623749)CaDiCaL version: 2.1.3
% 156.69/34.42 % (1623749)Termination reason: Instruction limit
% 156.69/34.42 % (1623749)Termination phase: Finite model building constraint generation
% 156.69/34.42 % (1623749)Time elapsed: 21.402 s
% 156.69/34.42 % (1623749)Peak memory usage: 2357 MB
% 156.69/34.42 % (1623749)Instructions burned: 67535 (million)
% 156.69/34.42 % (1623773)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2091889310:i=11404_2727 on theBenchmark for (2727ds/11404Mi)
% 156.69/34.42 % (1623759)Instruction limit reached!
% 156.69/34.42 % (1623759)------------------------------
% 156.69/34.42 % (1623759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.42 % (1623759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.42 % (1623759)CaDiCaL version: 2.1.3
% 156.69/34.42 % (1623759)Termination reason: Instruction limit
% 156.69/34.42 % (1623759)Termination phase: Finite model building constraint generation
% 156.69/34.42 % (1623759)Time elapsed: 15.440 s
% 156.69/34.42 % (1623759)Peak memory usage: 2133 MB
% 156.69/34.42 % (1623759)Instructions burned: 46333 (million)
% 156.69/34.42 % (1623775)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3005430106:i=14134_2723 on theBenchmark for (2723ds/14134Mi)
% 156.69/34.42 % (1623769)Instruction limit reached!
% 156.69/34.42 % (1623769)------------------------------
% 156.69/34.42 % (1623769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.42 % (1623769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.42 % (1623769)CaDiCaL version: 2.1.3
% 156.69/34.42 % (1623769)Termination reason: Instruction limit
% 156.69/34.42 % (1623769)Termination phase: Saturation
% 156.69/34.42 % (1623769)Time elapsed: 7.091 s
% 156.69/34.42 % (1623769)Peak memory usage: 149 MB
% 156.69/34.42 % (1623769)Instructions burned: 20140 (million)
% 156.69/34.42 % (1623778)dis+33_16_sil=32000:sac=on:random_seed=1355249579:i=15851:nm=0_2681 on theBenchmark for (2681ds/15851Mi)
% 156.69/34.42 % (1623778) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1623684-1623778"...
% 156.69/34.42 % (1623778)...printing done.
% 156.69/34.42 % (1623778)Refutation found. Thanks to Tanya!
% 156.69/34.42 % SZS status Theorem for theBenchmark
% 156.69/34.42 % SZS output start Proof for theBenchmark
% See solution above
% 156.69/34.42 % (1623778)------------------------------
% 156.69/34.42 % (1623778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.69/34.42 % (1623778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.69/34.42 % (1623778)CaDiCaL version: 2.1.3
% 156.69/34.42 % (1623778)Termination reason: Refutation
% 156.69/34.42 % (1623778)Time elapsed: 1.849 s
% 156.69/34.42 % (1623778)Peak memory usage: 50 MB
% 156.69/34.42 % (1623778)Instructions burned: 8031 (million)
% 156.69/34.42 % (1623684)Success in time 34.2 s
% 156.69/34.42 % Vampire exiting
%------------------------------------------------------------------------------