%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR181+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:46:26 AM UTC 2026
% Result : Theorem 29.28s 7.64s
% Output : Refutation 29.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 17
% Syntax : Number of formulae : 75 ( 38 unt; 0 def)
% Number of atoms : 225 ( 0 equ)
% Maximal formula atoms : 40 ( 3 avg)
% Number of connectives : 194 ( 44 ~; 37 |; 89 &)
% ( 21 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-7 aty)
% Number of functors : 13 ( 13 usr; 12 con; 0-1 aty)
% Number of variables : 167 ( 164 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',predefinitionsA12) ).
fof(f5,axiom,
! [X0,X1] :
( p__d__disjoint(X0,X1)
<=> ! [X2] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',predefinitionsA15) ).
fof(f6,axiom,
( ! [X0,X1,X2] :
( p__d__partition3(X0,X1,X2)
<=> ( p__d__exhaustiveDecomposition3(X0,X1,X2)
& p__d__disjointDecomposition3(X0,X1,X2) ) )
& ! [X0,X1,X2,X3] :
( p__d__partition4(X0,X1,X2,X3)
<=> ( p__d__exhaustiveDecomposition4(X0,X1,X2,X3)
& p__d__disjointDecomposition4(X0,X1,X2,X3) ) )
& ! [X0,X1,X2,X3,X4] :
( p__d__partition5(X0,X1,X2,X3,X4)
<=> ( p__d__exhaustiveDecomposition5(X0,X1,X2,X3,X4)
& p__d__disjointDecomposition5(X0,X1,X2,X3,X4) ) )
& ! [X0,X1,X2,X3,X4,X5] :
( p__d__partition6(X0,X1,X2,X3,X4,X5)
<=> ( p__d__exhaustiveDecomposition6(X0,X1,X2,X3,X4,X5)
& p__d__disjointDecomposition6(X0,X1,X2,X3,X4,X5) ) )
& ! [X0,X1,X2,X3,X4,X5,X6] :
( p__d__partition7(X0,X1,X2,X3,X4,X5,X6)
<=> ( p__d__exhaustiveDecomposition7(X0,X1,X2,X3,X4,X5,X6)
& p__d__disjointDecomposition7(X0,X1,X2,X3,X4,X5,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',predefinitionsA18) ).
fof(f8,axiom,
( ! [X0,X1,X2] :
( p__d__disjointDecomposition3(X0,X1,X2)
<=> p__d__disjoint(X1,X2) )
& ! [X0,X1,X2,X3] :
( p__d__disjointDecomposition4(X0,X1,X2,X3)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X2,X3) ) )
& ! [X0,X1,X2,X3,X4] :
( p__d__disjointDecomposition5(X0,X1,X2,X3,X4)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X3,X4) ) )
& ! [X0,X1,X2,X3,X4,X5] :
( p__d__disjointDecomposition6(X0,X1,X2,X3,X4,X5)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X1,X5)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X2,X5)
& p__d__disjoint(X3,X4)
& p__d__disjoint(X3,X5)
& p__d__disjoint(X4,X5) ) )
& ! [X0,X1,X2,X3,X4,X5,X6] :
( p__d__disjointDecomposition7(X0,X1,X2,X3,X4,X5,X6)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X1,X5)
& p__d__disjoint(X1,X6)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X2,X5)
& p__d__disjoint(X2,X6)
& p__d__disjoint(X3,X4)
& p__d__disjoint(X3,X5)
& p__d__disjoint(X3,X6)
& p__d__disjoint(X4,X5)
& p__d__disjoint(X4,X6)
& p__d__disjoint(X5,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',predefinitionsA24) ).
fof(f107,axiom,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA173) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA178) ).
fof(f233,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA324) ).
fof(f242,axiom,
p__d__subclass(c__Attribute,c__Abstract),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA333) ).
fof(f254,axiom,
p__d__subclass(c__InternalAttribute,c__Attribute),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA351) ).
fof(f1582,axiom,
p__d__subclass(c__BiologicalProcess,c__InternalChange),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA2309) ).
fof(f1617,axiom,
p__d__subclass(c__PathologicProcess,c__BiologicalProcess),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA2346) ).
fof(f1859,axiom,
p__d__subclass(c__InternalChange,c__Process),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA2644) ).
fof(f2662,axiom,
p__d__subclass(c__BiologicalAttribute,c__InternalAttribute),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA3659) ).
fof(f2691,axiom,
p__d__subclass(c__DiseaseOrSyndrome,c__BiologicalAttribute),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA3695) ).
fof(f7433,conjecture,
! [X0] :
( ~ p__d__subclass(X0,c__DiseaseOrSyndrome)
| ~ p__d__subclass(X0,c__PathologicProcess) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',negatedCommonSubclassEvent0219) ).
fof(f7434,negated_conjecture,
~ ! [X0] :
( ~ p__d__subclass(X0,c__DiseaseOrSyndrome)
| ~ p__d__subclass(X0,c__PathologicProcess) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7435,plain,
( ! [X0,X1,X2] :
( p__d__partition3(X0,X1,X2)
<=> ( p__d__exhaustiveDecomposition3(X0,X1,X2)
& p__d__disjointDecomposition3(X0,X1,X2) ) )
& ! [X3,X4,X5,X6] :
( p__d__partition4(X3,X4,X5,X6)
<=> ( p__d__exhaustiveDecomposition4(X3,X4,X5,X6)
& p__d__disjointDecomposition4(X3,X4,X5,X6) ) )
& ! [X7,X8,X9,X10,X11] :
( p__d__partition5(X7,X8,X9,X10,X11)
<=> ( p__d__exhaustiveDecomposition5(X7,X8,X9,X10,X11)
& p__d__disjointDecomposition5(X7,X8,X9,X10,X11) ) )
& ! [X12,X13,X14,X15,X16,X17] :
( p__d__partition6(X12,X13,X14,X15,X16,X17)
<=> ( p__d__exhaustiveDecomposition6(X12,X13,X14,X15,X16,X17)
& p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17) ) )
& ! [X18,X19,X20,X21,X22,X23,X24] :
( p__d__partition7(X18,X19,X20,X21,X22,X23,X24)
<=> ( p__d__exhaustiveDecomposition7(X18,X19,X20,X21,X22,X23,X24)
& p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24) ) ) ),
inference(rectify,[],[f6]) ).
fof(f7437,plain,
( ! [X0,X1,X2] :
( p__d__disjointDecomposition3(X0,X1,X2)
<=> p__d__disjoint(X1,X2) )
& ! [X3,X4,X5,X6] :
( p__d__disjointDecomposition4(X3,X4,X5,X6)
<=> ( p__d__disjoint(X4,X5)
& p__d__disjoint(X4,X6)
& p__d__disjoint(X5,X6) ) )
& ! [X7,X8,X9,X10,X11] :
( p__d__disjointDecomposition5(X7,X8,X9,X10,X11)
<=> ( p__d__disjoint(X8,X9)
& p__d__disjoint(X8,X10)
& p__d__disjoint(X8,X11)
& p__d__disjoint(X9,X10)
& p__d__disjoint(X9,X11)
& p__d__disjoint(X10,X11) ) )
& ! [X12,X13,X14,X15,X16,X17] :
( p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17)
<=> ( p__d__disjoint(X13,X14)
& p__d__disjoint(X13,X15)
& p__d__disjoint(X13,X16)
& p__d__disjoint(X13,X17)
& p__d__disjoint(X14,X15)
& p__d__disjoint(X14,X16)
& p__d__disjoint(X14,X17)
& p__d__disjoint(X15,X16)
& p__d__disjoint(X15,X17)
& p__d__disjoint(X16,X17) ) )
& ! [X18,X19,X20,X21,X22,X23,X24] :
( p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24)
<=> ( p__d__disjoint(X19,X20)
& p__d__disjoint(X19,X21)
& p__d__disjoint(X19,X22)
& p__d__disjoint(X19,X23)
& p__d__disjoint(X19,X24)
& p__d__disjoint(X20,X21)
& p__d__disjoint(X20,X22)
& p__d__disjoint(X20,X23)
& p__d__disjoint(X20,X24)
& p__d__disjoint(X21,X22)
& p__d__disjoint(X21,X23)
& p__d__disjoint(X21,X24)
& p__d__disjoint(X22,X23)
& p__d__disjoint(X22,X24)
& p__d__disjoint(X23,X24) ) ) ),
inference(rectify,[],[f8]) ).
fof(f7449,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7450,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7449]) ).
fof(f7453,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7454,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7453]) ).
fof(f7503,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f11600,plain,
? [X0] :
( p__d__subclass(X0,c__DiseaseOrSyndrome)
& p__d__subclass(X0,c__PathologicProcess) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f11602,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2)
| p__d__subclass(X0,X2) ),
inference(cnf_transformation,[],[f7450]) ).
fof(f11604,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__instance(X0,X1)
| p__d__instance(X0,X2) ),
inference(cnf_transformation,[],[f7454]) ).
fof(f11605,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X2,X1)
| ~ p__d__instance(X2,X0)
| ~ p__d__disjoint(X0,X1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f11608,plain,
! [X2,X0,X1] :
( p__d__disjointDecomposition3(X0,X1,X2)
| ~ p__d__partition3(X0,X1,X2) ),
inference(cnf_transformation,[],[f7435]) ).
fof(f11692,plain,
! [X2,X0,X1] :
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X0,X1,X2) ),
inference(cnf_transformation,[],[f7437]) ).
fof(f11880,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
inference(cnf_transformation,[],[f107]) ).
fof(f11883,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Entity)
| p__d__instance(sK34(X0),X0) ),
inference(cnf_transformation,[],[f7503]) ).
fof(f11886,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f12045,plain,
p__d__subclass(c__Process,c__Physical),
inference(cnf_transformation,[],[f233]) ).
fof(f12057,plain,
p__d__subclass(c__Attribute,c__Abstract),
inference(cnf_transformation,[],[f242]) ).
fof(f12069,plain,
p__d__subclass(c__InternalAttribute,c__Attribute),
inference(cnf_transformation,[],[f254]) ).
fof(f13647,plain,
p__d__subclass(c__BiologicalProcess,c__InternalChange),
inference(cnf_transformation,[],[f1582]) ).
fof(f13694,plain,
p__d__subclass(c__PathologicProcess,c__BiologicalProcess),
inference(cnf_transformation,[],[f1617]) ).
fof(f14072,plain,
p__d__subclass(c__InternalChange,c__Process),
inference(cnf_transformation,[],[f1859]) ).
fof(f15118,plain,
p__d__subclass(c__BiologicalAttribute,c__InternalAttribute),
inference(cnf_transformation,[],[f2662]) ).
fof(f15155,plain,
p__d__subclass(c__DiseaseOrSyndrome,c__BiologicalAttribute),
inference(cnf_transformation,[],[f2691]) ).
fof(f22366,plain,
p__d__subclass(sK1237,c__PathologicProcess),
inference(cnf_transformation,[],[f11600]) ).
fof(f22367,plain,
p__d__subclass(sK1237,c__DiseaseOrSyndrome),
inference(cnf_transformation,[],[f11600]) ).
fof(f22555,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1)
| p__d__disjoint(X0,X1) ),
inference(consistent_polarity_flipping,[],[f11605]) ).
fof(f22562,plain,
! [X2,X0,X1] :
( ~ p__d__disjointDecomposition3(X0,X1,X2)
| ~ p__d__partition3(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f11608]) ).
fof(f22576,plain,
! [X2,X0,X1] :
( ~ p__d__disjoint(X1,X2)
| p__d__disjointDecomposition3(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f11692]) ).
fof(f32574,plain,
! [X0] :
( ~ p__d__subclass(c__PathologicProcess,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f11602,f22366]) ).
fof(f32575,plain,
! [X0] :
( ~ p__d__subclass(c__DiseaseOrSyndrome,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f11602,f22367]) ).
fof(f60133,plain,
p__d__subclass(sK1237,c__BiologicalProcess),
inference(resolution,[],[f32574,f13694]) ).
fof(f60137,plain,
! [X0] :
( ~ p__d__subclass(c__BiologicalProcess,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f60133,f11602]) ).
fof(f60234,plain,
p__d__subclass(sK1237,c__BiologicalAttribute),
inference(resolution,[],[f32575,f15155]) ).
fof(f60281,plain,
! [X0] :
( ~ p__d__subclass(c__BiologicalAttribute,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f60234,f11602]) ).
fof(f60453,plain,
p__d__subclass(sK1237,c__InternalChange),
inference(resolution,[],[f60137,f13647]) ).
fof(f60459,plain,
! [X0] :
( ~ p__d__subclass(c__InternalChange,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f60453,f11602]) ).
fof(f60469,plain,
p__d__subclass(sK1237,c__InternalAttribute),
inference(resolution,[],[f60281,f15118]) ).
fof(f60473,plain,
! [X0] :
( ~ p__d__subclass(c__InternalAttribute,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f60469,f11602]) ).
fof(f60484,plain,
p__d__subclass(sK1237,c__Process),
inference(resolution,[],[f60459,f14072]) ).
fof(f60490,plain,
! [X0] :
( ~ p__d__subclass(c__Process,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f60484,f11602]) ).
fof(f60500,plain,
p__d__subclass(sK1237,c__Attribute),
inference(resolution,[],[f60473,f12069]) ).
fof(f60515,plain,
! [X0] :
( ~ p__d__subclass(c__Attribute,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f60500,f11602]) ).
fof(f60525,plain,
p__d__subclass(sK1237,c__Physical),
inference(resolution,[],[f60490,f12045]) ).
fof(f60527,plain,
! [X0] :
( ~ p__d__instance(X0,sK1237)
| p__d__instance(X0,c__Physical) ),
inference(resolution,[],[f60525,f11604]) ).
fof(f60529,plain,
! [X0] :
( ~ p__d__subclass(c__Physical,X0)
| p__d__subclass(sK1237,X0) ),
inference(resolution,[],[f60525,f11602]) ).
fof(f60540,plain,
p__d__subclass(sK1237,c__Abstract),
inference(resolution,[],[f60515,f12057]) ).
fof(f60542,plain,
! [X0] :
( ~ p__d__instance(X0,sK1237)
| p__d__instance(X0,c__Abstract) ),
inference(resolution,[],[f60540,f11604]) ).
fof(f60554,plain,
p__d__subclass(sK1237,c__Entity),
inference(resolution,[],[f60529,f11886]) ).
fof(f60556,plain,
p__d__instance(sK34(sK1237),sK1237),
inference(resolution,[],[f60554,f11883]) ).
fof(f63252,plain,
p__d__instance(sK34(sK1237),c__Physical),
inference(resolution,[],[f60556,f60527]) ).
fof(f63276,plain,
! [X0] :
( ~ p__d__instance(sK34(sK1237),X0)
| p__d__disjoint(c__Physical,X0) ),
inference(resolution,[],[f63252,f22555]) ).
fof(f63277,plain,
p__d__instance(sK34(sK1237),c__Abstract),
inference(resolution,[],[f60542,f60556]) ).
fof(f97153,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(resolution,[],[f63276,f63277]) ).
fof(f97214,plain,
! [X0] : p__d__disjointDecomposition3(X0,c__Physical,c__Abstract),
inference(resolution,[],[f97153,f22576]) ).
fof(f97374,plain,
! [X0] : ~ p__d__partition3(X0,c__Physical,c__Abstract),
inference(resolution,[],[f97214,f22562]) ).
fof(f98545,plain,
$false,
inference(backward_subsumption_resolution,[],[f11880,f97374]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR181+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n015.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 23:44:33 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 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
% 9.06/2.00 % (3152447)Will run a generic schedule for satisfiability detection.
% 9.06/2.00 % (3152456)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1861692265:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 9.06/2.00 % (3152453)% WARNING: option uhcvi not known.
% 9.06/2.00 % (3152453)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2637773507:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 9.06/2.00 % (3152452)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2523317929_2998 on theBenchmark for (2998ds/0Mi)
% 9.06/2.00 % (3152454)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3674285330:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 9.06/2.00 % (3152455)dis+10_1_sil=32000:sp=arity:random_seed=1904699117:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 9.06/2.00 % (3152458)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=655665281:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 9.06/2.00 % (3152457)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1134341998:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 9.06/2.00 % (3152456)Instruction limit reached!
% 9.06/2.00 % (3152456)------------------------------
% 9.06/2.00 % (3152456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/2.00 % (3152456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.00 % (3152456)CaDiCaL version: 2.1.3
% 9.06/2.00 % (3152456)Termination reason: Instruction limit
% 9.06/2.00 % (3152456)Termination phase: NewCNF
% 9.06/2.00 % (3152456)Time elapsed: 0.040 s
% 9.06/2.00 % (3152456)Peak memory usage: 23 MB
% 9.06/2.00 % (3152456)Instructions burned: 118 (million)
% 9.06/2.00 % (3152466)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=21642678:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 9.06/2.00 % (3152455)Instruction limit reached!
% 9.06/2.00 % (3152455)------------------------------
% 9.06/2.00 % (3152455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/2.00 % (3152455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.00 % (3152455)CaDiCaL version: 2.1.3
% 9.06/2.00 % (3152455)Termination reason: Instruction limit
% 9.06/2.00 % (3152455)Termination phase: Clausification
% 9.06/2.00 % (3152455)Time elapsed: 0.066 s
% 9.06/2.00 % (3152455)Peak memory usage: 23 MB
% 9.06/2.00 % (3152455)Instructions burned: 103 (million)
% 9.06/2.00 % (3152457)Instruction limit reached!
% 9.06/2.00 % (3152457)------------------------------
% 9.06/2.00 % (3152457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/2.00 % (3152457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.00 % (3152457)CaDiCaL version: 2.1.3
% 9.06/2.00 % (3152457)Termination reason: Instruction limit
% 9.06/2.00 % (3152457)Termination phase: Property scanning
% 9.06/2.00 % (3152457)Time elapsed: 0.086 s
% 9.06/2.00 % (3152457)Peak memory usage: 24 MB
% 9.06/2.00 % (3152457)Instructions burned: 132 (million)
% 9.06/2.00 % (3152468)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3921135348:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 9.06/2.00 % (3152458)Instruction limit reached!
% 9.06/2.00 % (3152458)------------------------------
% 9.06/2.00 % (3152458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/2.00 % (3152458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.00 % (3152458)CaDiCaL version: 2.1.3
% 9.06/2.00 % (3152458)Termination reason: Instruction limit
% 9.06/2.00 % (3152458)Termination phase: Property scanning
% 9.06/2.00 % (3152458)Time elapsed: 0.097 s
% 9.06/2.00 % (3152458)Peak memory usage: 24 MB
% 9.06/2.00 % (3152458)Instructions burned: 161 (million)
% 9.06/2.00 % (3152470)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=4057223780:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 9.06/2.00 % (3152471)ott-21_1_sil=16000:fs=off:random_seed=371329569:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 9.06/2.00 % (3152468)Instruction limit reached!
% 9.06/2.00 % (3152468)------------------------------
% 9.06/2.00 % (3152468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.06/2.00 % (3152468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.25/5.03 % (3152468)CaDiCaL version: 2.1.3
% 31.25/5.03 % (3152468)Termination reason: Instruction limit
% 31.25/5.03 % (3152468)Termination phase: Property scanning
% 31.25/5.03 % (3152468)Time elapsed: 0.082 s
% 31.25/5.03 % (3152468)Peak memory usage: 24 MB
% 31.25/5.03 % (3152468)Instructions burned: 132 (million)
% 31.25/5.03 % (3152474)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2030548724:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 31.25/5.03 % (3152471)Instruction limit reached!
% 31.25/5.03 % (3152471)------------------------------
% 31.25/5.03 % (3152471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.25/5.03 % (3152471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.25/5.03 % (3152471)CaDiCaL version: 2.1.3
% 31.25/5.03 % (3152471)Termination reason: Instruction limit
% 31.25/5.03 % (3152471)Termination phase: Property scanning
% 31.25/5.03 % (3152471)Time elapsed: 0.103 s
% 31.25/5.03 % (3152471)Peak memory usage: 25 MB
% 31.25/5.03 % (3152471)Instructions burned: 181 (million)
% 31.25/5.03 % (3152466)Instruction limit reached!
% 31.25/5.03 % (3152466)------------------------------
% 31.25/5.03 % (3152466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.25/5.03 % (3152466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.25/5.03 % (3152466)CaDiCaL version: 2.1.3
% 31.25/5.03 % (3152466)Termination reason: Instruction limit
% 31.25/5.03 % (3152466)Termination phase: Finite model building preprocessing
% 31.25/5.03 % (3152466)Time elapsed: 0.197 s
% 31.25/5.03 % (3152466)Peak memory usage: 37 MB
% 31.25/5.03 % (3152466)Instructions burned: 718 (million)
% 31.25/5.03 % (3152476)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1035187129:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 31.25/5.03 % (3152478)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1511321770:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 31.25/5.03 % (3152474)Instruction limit reached!
% 31.25/5.03 % (3152474)------------------------------
% 31.25/5.03 % (3152474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.25/5.03 % (3152474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.25/5.03 % (3152474)CaDiCaL version: 2.1.3
% 31.25/5.03 % (3152474)Termination reason: Instruction limit
% 31.25/5.03 % (3152474)Termination phase: Saturation
% 31.25/5.03 % (3152474)Time elapsed: 0.255 s
% 31.25/5.03 % (3152474)Peak memory usage: 30 MB
% 31.25/5.03 % (3152474)Instructions burned: 479 (million)
% 31.25/5.03 % (3152480)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2224174767:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 31.25/5.03 % (3152470)Instruction limit reached!
% 31.25/5.03 % (3152470)------------------------------
% 31.25/5.03 % (3152470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.25/5.03 % (3152470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.25/5.03 % (3152470)CaDiCaL version: 2.1.3
% 31.25/5.03 % (3152470)Termination reason: Instruction limit
% 31.25/5.03 % (3152470)Termination phase: Saturation
% 31.25/5.03 % (3152470)Time elapsed: 0.363 s
% 31.25/5.03 % (3152470)Peak memory usage: 31 MB
% 31.25/5.03 % (3152470)Instructions burned: 685 (million)
% 31.25/5.03 % (3152482)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=2804926610:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 31.25/5.03 % (3152478)Instruction limit reached!
% 31.25/5.03 % (3152478)------------------------------
% 31.25/5.03 % (3152478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.25/5.03 % (3152478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.25/5.03 % (3152478)CaDiCaL version: 2.1.3
% 31.25/5.03 % (3152478)Termination reason: Instruction limit
% 31.25/5.03 % (3152478)Termination phase: Saturation
% 31.25/5.03 % (3152478)Time elapsed: 0.325 s
% 31.25/5.03 % (3152478)Peak memory usage: 34 MB
% 31.25/5.03 % (3152478)Instructions burned: 1180 (million)
% 31.25/5.03 % (3152484)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3341729581:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 31.25/5.03 % TRYING [1]
% 31.25/5.03 % (3152476)Instruction limit reached!
% 31.25/5.03 % (3152476)------------------------------
% 31.25/5.03 % (3152476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.25/5.03 % (3152476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152476)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152476)Termination reason: Instruction limit
% 29.28/7.64 % (3152476)Termination phase: Finite model building preprocessing
% 29.28/7.64 % (3152476)Time elapsed: 0.417 s
% 29.28/7.64 % (3152476)Peak memory usage: 42 MB
% 29.28/7.64 % (3152476)Instructions burned: 866 (million)
% 29.28/7.64 % TRYING [2]
% 29.28/7.64 % (3152486)fmb+10_1_sil=64000:random_seed=527272632:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 29.28/7.64 % (3152484)Instruction limit reached!
% 29.28/7.64 % (3152484)------------------------------
% 29.28/7.64 % (3152484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152484)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152484)Termination reason: Instruction limit
% 29.28/7.64 % (3152484)Termination phase: Saturation
% 29.28/7.64 % (3152484)Time elapsed: 0.223 s
% 29.28/7.64 % (3152484)Peak memory usage: 38 MB
% 29.28/7.64 % (3152484)Instructions burned: 881 (million)
% 29.28/7.64 % (3152488)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=78603845:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 29.28/7.64 % TRYING [3]
% 29.28/7.64 % (3152482)Instruction limit reached!
% 29.28/7.64 % (3152482)------------------------------
% 29.28/7.64 % (3152482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152482)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152482)Termination reason: Instruction limit
% 29.28/7.64 % (3152482)Termination phase: Saturation
% 29.28/7.64 % (3152482)Time elapsed: 0.374 s
% 29.28/7.64 % (3152482)Peak memory usage: 35 MB
% 29.28/7.64 % (3152482)Instructions burned: 693 (million)
% 29.28/7.64 % (3152490)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2184797382:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 29.28/7.64 % (3152480)Instruction limit reached!
% 29.28/7.64 % (3152480)------------------------------
% 29.28/7.64 % (3152480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152480)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152480)Termination reason: Instruction limit
% 29.28/7.64 % (3152480)Termination phase: Finite model building preprocessing
% 29.28/7.64 % (3152480)Time elapsed: 0.434 s
% 29.28/7.64 % (3152480)Peak memory usage: 40 MB
% 29.28/7.64 % (3152480)Instructions burned: 889 (million)
% 29.28/7.64 % (3152492)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2590830400:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 29.28/7.64 % (3152488)Cannot represent all propositional literals internally
% 29.28/7.64 % (3152488)Refutation not found, incomplete strategy
% 29.28/7.64 % (3152488)------------------------------
% 29.28/7.64 % (3152488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152488)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152488)Termination reason: Refutation not found, incomplete strategy
% 29.28/7.64 % (3152488)Time elapsed: 0.310 s
% 29.28/7.64 % (3152488)Peak memory usage: 44 MB
% 29.28/7.64 % (3152488)Instructions burned: 1161 (million)
% 29.28/7.64 % (3152488)------------------------------
% 29.28/7.64 % (3152488)------------------------------
% 29.28/7.64 % (3152494)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3068887047:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 29.28/7.64 % TRYING [1]
% 29.28/7.64 % TRYING [2]
% 29.28/7.64 % (3152490)Instruction limit reached!
% 29.28/7.64 % (3152490)------------------------------
% 29.28/7.64 % (3152490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152490)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152490)Termination reason: Instruction limit
% 29.28/7.64 % (3152490)Termination phase: Finite model building preprocessing
% 29.28/7.64 % (3152490)Time elapsed: 0.450 s
% 29.28/7.64 % (3152490)Peak memory usage: 41 MB
% 29.28/7.64 % (3152490)Instructions burned: 920 (million)
% 29.28/7.64 % (3152496)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=364922562:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 29.28/7.64 % (3152494)Instruction limit reached!
% 29.28/7.64 % (3152494)------------------------------
% 29.28/7.64 % (3152494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152494)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152494)Termination reason: Instruction limit
% 29.28/7.64 % (3152494)Termination phase: Saturation
% 29.28/7.64 % (3152494)Time elapsed: 0.408 s
% 29.28/7.64 % (3152494)Peak memory usage: 38 MB
% 29.28/7.64 % (3152494)Instructions burned: 1473 (million)
% 29.28/7.64 % TRYING [4]
% 29.28/7.64 % (3152498)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3485163587:fmbsr=2.30978:i=2174_2982 on theBenchmark for (2982ds/2174Mi)
% 29.28/7.64 % (3152496)Cannot represent all propositional literals internally
% 29.28/7.64 % (3152496)Refutation not found, incomplete strategy
% 29.28/7.64 % (3152496)------------------------------
% 29.28/7.64 % (3152496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152496)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152496)Termination reason: Refutation not found, incomplete strategy
% 29.28/7.64 % (3152496)Time elapsed: 0.594 s
% 29.28/7.64 % (3152496)Peak memory usage: 44 MB
% 29.28/7.64 % (3152496)Instructions burned: 1216 (million)
% 29.28/7.64 % (3152496)------------------------------
% 29.28/7.64 % (3152496)------------------------------
% 29.28/7.64 % (3152500)ott-2_1_sil=16000:newcnf=on:random_seed=3745933244:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi)
% 29.28/7.64 % (3152498)Instruction limit reached!
% 29.28/7.64 % (3152498)------------------------------
% 29.28/7.64 % (3152498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152498)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152498)Termination reason: Instruction limit
% 29.28/7.64 % (3152498)Termination phase: Finite model building preprocessing
% 29.28/7.64 % (3152498)Time elapsed: 0.571 s
% 29.28/7.64 % (3152498)Peak memory usage: 67 MB
% 29.28/7.64 % (3152498)Instructions burned: 2175 (million)
% 29.28/7.64 % (3152502)ott+10_1_sil=32000:tgt=ground:random_seed=1189229572:i=5114:av=off_2976 on theBenchmark for (2976ds/5114Mi)
% 29.28/7.64 % TRYING [3]
% 29.28/7.64 % (3152500)Instruction limit reached!
% 29.28/7.64 % (3152500)------------------------------
% 29.28/7.64 % (3152500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152500)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152500)Termination reason: Instruction limit
% 29.28/7.64 % (3152500)Termination phase: Saturation
% 29.28/7.64 % (3152500)Time elapsed: 0.446 s
% 29.28/7.64 % (3152500)Peak memory usage: 35 MB
% 29.28/7.64 % (3152500)Instructions burned: 869 (million)
% 29.28/7.64 % (3152504)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1493855327:i=54282_2973 on theBenchmark for (2973ds/54282Mi)
% 29.28/7.64 % TRYING [1]
% 29.28/7.64 % TRYING [2]
% 29.28/7.64 % TRYING [3]
% 29.28/7.64 % (3152492)Instruction limit reached!
% 29.28/7.64 % (3152492)------------------------------
% 29.28/7.64 % (3152492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152492)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152492)Termination reason: Instruction limit
% 29.28/7.64 % (3152492)Termination phase: Saturation
% 29.28/7.64 % (3152492)Time elapsed: 2.600 s
% 29.28/7.64 % (3152492)Peak memory usage: 61 MB
% 29.28/7.64 % (3152492)Instructions burned: 5132 (million)
% 29.28/7.64 % (3152506)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3268567666:i=3512:aac=none_2962 on theBenchmark for (2962ds/3512Mi)
% 29.28/7.64 % (3152502)Instruction limit reached!
% 29.28/7.64 % (3152502)------------------------------
% 29.28/7.64 % (3152502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152502)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152502)Termination reason: Instruction limit
% 29.28/7.64 % (3152502)Termination phase: Saturation
% 29.28/7.64 % (3152502)Time elapsed: 1.424 s
% 29.28/7.64 % (3152502)Peak memory usage: 74 MB
% 29.28/7.64 % (3152502)Instructions burned: 5116 (million)
% 29.28/7.64 % (3152508)dis+21_1_sil=32000:sas=cadical:random_seed=1707099665:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi)
% 29.28/7.64 % TRYING [4]
% 29.28/7.64 % (3152508)Instruction limit reached!
% 29.28/7.64 % (3152508)------------------------------
% 29.28/7.64 % (3152508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152508)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152508)Termination reason: Instruction limit
% 29.28/7.64 % (3152508)Termination phase: Saturation
% 29.28/7.64 % (3152508)Time elapsed: 0.985 s
% 29.28/7.64 % (3152508)Peak memory usage: 56 MB
% 29.28/7.64 % (3152508)Instructions burned: 3774 (million)
% 29.28/7.64 % (3152510)ott+11_1_sil=16000:gs=on:random_seed=470110206:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2952 on theBenchmark for (2952ds/2251Mi)
% 29.28/7.64 % (3152506)Instruction limit reached!
% 29.28/7.64 % (3152506)------------------------------
% 29.28/7.64 % (3152506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152506)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152506)Termination reason: Instruction limit
% 29.28/7.64 % (3152506)Termination phase: Saturation
% 29.28/7.64 % (3152506)Time elapsed: 1.731 s
% 29.28/7.64 % (3152506)Peak memory usage: 54 MB
% 29.28/7.64 % (3152506)Instructions burned: 3515 (million)
% 29.28/7.64 % (3152510)Instruction limit reached!
% 29.28/7.64 % (3152510)------------------------------
% 29.28/7.64 % (3152510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152510)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152510)Termination reason: Instruction limit
% 29.28/7.64 % (3152510)Termination phase: Saturation
% 29.28/7.64 % (3152510)Time elapsed: 0.702 s
% 29.28/7.64 % (3152510)Peak memory usage: 100 MB
% 29.28/7.64 % (3152510)Instructions burned: 2252 (million)
% 29.28/7.64 % (3152512)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2221907471:fmbsr=1.6:i=67534_2945 on theBenchmark for (2945ds/67534Mi)
% 29.28/7.64 % (3152514)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1200621166:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2944 on theBenchmark for (2944ds/4591Mi)
% 29.28/7.64 % TRYING [4]
% 29.28/7.64 % TRYING [5]
% 29.28/7.64 % (3152514)Instruction limit reached!
% 29.28/7.64 % (3152514)------------------------------
% 29.28/7.64 % (3152514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.64 % (3152514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.64 % (3152514)CaDiCaL version: 2.1.3
% 29.28/7.64 % (3152514)Termination reason: Instruction limit
% 29.28/7.64 % (3152514)Termination phase: Saturation
% 29.28/7.64 % (3152514)Time elapsed: 1.029 s
% 29.28/7.64 % (3152514)Peak memory usage: 49 MB
% 29.28/7.64 % (3152514)Instructions burned: 4595 (million)
% 29.28/7.64 % (3152517)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1232794945:i=29340_2934 on theBenchmark for (2934ds/29340Mi)
% 29.28/7.64 % (3152453) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3152447-3152453"...
% 29.28/7.64 % (3152453)...printing done.
% 29.28/7.64 % (3152453)Refutation found. Thanks to Tanya!
% 29.28/7.64 % SZS status Theorem for theBenchmark
% 29.28/7.64 % SZS output start Proof for theBenchmark
% See solution above
% 29.28/7.65 % (3152453)------------------------------
% 29.28/7.65 % (3152453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.28/7.65 % (3152453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.28/7.65 % (3152453)CaDiCaL version: 2.1.3
% 29.28/7.65 % (3152453)Termination reason: Refutation
% 29.28/7.65 % (3152453)Time elapsed: 7.098 s
% 29.28/7.65 % (3152453)Peak memory usage: 64 MB
% 29.28/7.65 % (3152453)Instructions burned: 14509 (million)
% 29.28/7.65 % (3152447)Success in time 7.393 s
% 29.28/7.65 % Vampire exiting
%------------------------------------------------------------------------------