%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO340+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:54:26 AM UTC 2026
% Result : Theorem 40.22s 7.40s
% Output : Refutation 40.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 3
% Syntax : Number of formulae : 61 ( 32 unt; 0 def)
% Number of atoms : 357 ( 192 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 495 ( 199 ~; 253 |; 40 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-7 aty)
% Number of variables : 115 ( 106 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
( X0 != vd1386
& vf(vd1385,vd1386) = vf(vd1385,X0)
& vf(vd1384,vd1386) = vf(vd1384,X0)
& rS(vd1386,X0,vd1391)
& rpoint(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','neg(neg(403))') ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
( X0 != vd1386
& vf(vd1385,vd1386) = vf(vd1385,X0)
& vf(vd1384,vd1386) = vf(vd1384,X0)
& rS(vd1386,X0,vd1391)
& rpoint(X0) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
( vd1391 = vd1392
& ron(vd1385,vd1391)
& ron(vd1384,vd1391)
& rline(vd1392)
& vd1385 != vd1386
& vd1384 != vd1386
& vd1384 != vd1385
& ? [X0] :
( vd1386 = X0
& rpoint(X0) )
& ? [X1] :
( vd1385 = X1
& rpoint(X1) )
& ? [X2] :
( vd1384 = X2
& rpoint(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))') ).
fof(f4,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X1,X3)
& ron(X0,X3)
& rline(X4)
& X1 != X2
& X0 != X2
& X0 != X1
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ! [X8] :
( ( X8 != X2
& vf(X1,X2) = vf(X1,X8)
& vf(X0,X2) = vf(X0,X8)
& rS(X2,X8,X3)
& rpoint(X8) )
=> ! [X9] :
( X9 = vskolem1416(X8,X0,X1,X2,X3,X4)
=> ! [X10] : X10 != vskolem1419(X9,X8,X0,X1,X2,X3,X4) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(404), 0), 0)') ).
fof(f126,plain,
? [X0] :
( X0 != vd1386
& vf(vd1385,vd1386) = vf(vd1385,X0)
& vf(vd1384,vd1386) = vf(vd1384,X0)
& rS(vd1386,X0,vd1391)
& rpoint(X0) ),
inference(flattening,[],[f2]) ).
fof(f131,plain,
! [X0,X1,X2,X3,X4] :
( ! [X8] :
( ! [X9] :
( ! [X10] : X10 != vskolem1419(X9,X8,X0,X1,X2,X3,X4)
| vskolem1416(X8,X0,X1,X2,X3,X4) != X9 )
| X2 = X8
| vf(X1,X2) != vf(X1,X8)
| vf(X0,X2) != vf(X0,X8)
| ~ rS(X2,X8,X3)
| ~ rpoint(X8) )
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f132,plain,
! [X0,X1,X2,X3,X4] :
( ! [X8] :
( ! [X9] :
( ! [X10] : X10 != vskolem1419(X9,X8,X0,X1,X2,X3,X4)
| vskolem1416(X8,X0,X1,X2,X3,X4) != X9 )
| X2 = X8
| vf(X1,X2) != vf(X1,X8)
| vf(X0,X2) != vf(X0,X8)
| ~ rS(X2,X8,X3)
| ~ rpoint(X8) )
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f131]) ).
fof(f359,plain,
rpoint(sK0),
inference(cnf_transformation,[],[f126]) ).
fof(f360,plain,
rS(vd1386,sK0,vd1391),
inference(cnf_transformation,[],[f126]) ).
fof(f361,plain,
vf(vd1384,vd1386) = vf(vd1384,sK0),
inference(cnf_transformation,[],[f126]) ).
fof(f362,plain,
vf(vd1385,vd1386) = vf(vd1385,sK0),
inference(cnf_transformation,[],[f126]) ).
fof(f363,plain,
vd1386 != sK0,
inference(cnf_transformation,[],[f126]) ).
fof(f364,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f3]) ).
fof(f365,plain,
vd1386 = sK3,
inference(cnf_transformation,[],[f3]) ).
fof(f366,plain,
rpoint(sK2),
inference(cnf_transformation,[],[f3]) ).
fof(f367,plain,
vd1385 = sK2,
inference(cnf_transformation,[],[f3]) ).
fof(f368,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f3]) ).
fof(f369,plain,
vd1384 = sK1,
inference(cnf_transformation,[],[f3]) ).
fof(f370,plain,
vd1385 != vd1384,
inference(cnf_transformation,[],[f3]) ).
fof(f371,plain,
vd1386 != vd1384,
inference(cnf_transformation,[],[f3]) ).
fof(f372,plain,
vd1386 != vd1385,
inference(cnf_transformation,[],[f3]) ).
fof(f373,plain,
rline(vd1392),
inference(cnf_transformation,[],[f3]) ).
fof(f374,plain,
ron(vd1384,vd1391),
inference(cnf_transformation,[],[f3]) ).
fof(f375,plain,
ron(vd1385,vd1391),
inference(cnf_transformation,[],[f3]) ).
fof(f376,plain,
vd1391 = vd1392,
inference(cnf_transformation,[],[f3]) ).
fof(f377,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| X0 = X1
| X0 = X2
| X1 = X2
| ~ rline(X4)
| ~ ron(X0,X3)
| ~ ron(X1,X3)
| X3 != X4
| ~ rpoint(X8)
| ~ rS(X2,X8,X3)
| vf(X0,X2) != vf(X0,X8)
| vf(X1,X2) != vf(X1,X8)
| X2 = X8
| vskolem1416(X8,X0,X1,X2,X3,X4) != X9
| vskolem1419(X9,X8,X0,X1,X2,X3,X4) != X10 ),
inference(cnf_transformation,[],[f132]) ).
fof(f645,plain,
sK0 != sK3,
inference(definition_unfolding,[],[f363,f365]) ).
fof(f646,plain,
vf(sK2,sK3) = vf(sK2,sK0),
inference(definition_unfolding,[],[f362,f367,f365,f367]) ).
fof(f647,plain,
vf(sK1,sK3) = vf(sK1,sK0),
inference(definition_unfolding,[],[f361,f369,f365,f369]) ).
fof(f648,plain,
rS(sK3,sK0,vd1392),
inference(definition_unfolding,[],[f360,f365,f376]) ).
fof(f649,plain,
ron(sK2,vd1392),
inference(definition_unfolding,[],[f375,f367,f376]) ).
fof(f650,plain,
ron(sK1,vd1392),
inference(definition_unfolding,[],[f374,f369,f376]) ).
fof(f651,plain,
sK2 != sK3,
inference(definition_unfolding,[],[f372,f365,f367]) ).
fof(f652,plain,
sK1 != sK3,
inference(definition_unfolding,[],[f371,f365,f369]) ).
fof(f653,plain,
sK1 != sK2,
inference(definition_unfolding,[],[f370,f367,f369]) ).
fof(f663,plain,
! [X2,X3,X10,X1,X8,X6,X9,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| X1 = X7
| X2 = X7
| X1 = X2
| ~ rline(X4)
| ~ ron(X7,X3)
| ~ ron(X1,X3)
| X3 != X4
| ~ rpoint(X8)
| ~ rS(X2,X8,X3)
| vf(X7,X2) != vf(X7,X8)
| vf(X1,X2) != vf(X1,X8)
| X2 = X8
| vskolem1416(X8,X7,X1,X2,X3,X4) != X9
| vskolem1419(X9,X8,X7,X1,X2,X3,X4) != X10 ),
inference(equality_resolution,[],[f377]) ).
fof(f664,plain,
! [X2,X3,X10,X8,X6,X9,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| X2 != X5
| X6 = X7
| X2 = X7
| X2 = X6
| ~ rline(X4)
| ~ ron(X7,X3)
| ~ ron(X6,X3)
| X3 != X4
| ~ rpoint(X8)
| ~ rS(X2,X8,X3)
| vf(X7,X2) != vf(X7,X8)
| vf(X6,X2) != vf(X6,X8)
| X2 = X8
| vskolem1416(X8,X7,X6,X2,X3,X4) != X9
| vskolem1419(X9,X8,X7,X6,X2,X3,X4) != X10 ),
inference(equality_resolution,[],[f663]) ).
fof(f665,plain,
! [X3,X10,X8,X6,X9,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| X6 = X7
| X5 = X7
| X5 = X6
| ~ rline(X4)
| ~ ron(X7,X3)
| ~ ron(X6,X3)
| X3 != X4
| ~ rpoint(X8)
| ~ rS(X5,X8,X3)
| vf(X7,X8) != vf(X7,X5)
| vf(X6,X8) != vf(X6,X5)
| X5 = X8
| vskolem1416(X8,X7,X6,X5,X3,X4) != X9
| vskolem1419(X9,X8,X7,X6,X5,X3,X4) != X10 ),
inference(equality_resolution,[],[f664]) ).
fof(f666,plain,
! [X10,X8,X6,X9,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| X6 = X7
| X5 = X7
| X5 = X6
| ~ rline(X4)
| ~ ron(X7,X4)
| ~ ron(X6,X4)
| ~ rpoint(X8)
| ~ rS(X5,X8,X4)
| vf(X7,X8) != vf(X7,X5)
| vf(X6,X8) != vf(X6,X5)
| X5 = X8
| vskolem1416(X8,X7,X6,X5,X4,X4) != X9
| vskolem1419(X9,X8,X7,X6,X5,X4,X4) != X10 ),
inference(equality_resolution,[],[f665]) ).
fof(f667,plain,
! [X10,X8,X6,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| X6 = X7
| X5 = X7
| X5 = X6
| ~ rline(X4)
| ~ ron(X7,X4)
| ~ ron(X6,X4)
| ~ rpoint(X8)
| ~ rS(X5,X8,X4)
| vf(X7,X8) != vf(X7,X5)
| vf(X6,X8) != vf(X6,X5)
| X5 = X8
| vskolem1419(vskolem1416(X8,X7,X6,X5,X4,X4),X8,X7,X6,X5,X4,X4) != X10 ),
inference(equality_resolution,[],[f666]) ).
fof(f668,plain,
! [X8,X6,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| X6 = X7
| X5 = X7
| X5 = X6
| ~ rline(X4)
| ~ ron(X7,X4)
| ~ ron(X6,X4)
| ~ rpoint(X8)
| ~ rS(X5,X8,X4)
| vf(X7,X8) != vf(X7,X5)
| vf(X6,X8) != vf(X6,X5)
| X5 = X8 ),
inference(equality_resolution,[],[f667]) ).
fof(f1900,plain,
~ ron(sK2,vd1392),
inference(consistent_polarity_flipping,[],[f649]) ).
fof(f1901,plain,
~ ron(sK1,vd1392),
inference(consistent_polarity_flipping,[],[f650]) ).
fof(f1902,plain,
~ rline(vd1392),
inference(consistent_polarity_flipping,[],[f373]) ).
fof(f1903,plain,
! [X8,X6,X7,X4,X5] :
( ~ rS(X5,X8,X4)
| ~ rpoint(X6)
| ~ rpoint(X5)
| X6 = X7
| X5 = X7
| X5 = X6
| rline(X4)
| ron(X7,X4)
| ron(X6,X4)
| ~ rpoint(X8)
| ~ rpoint(X7)
| vf(X7,X8) != vf(X7,X5)
| vf(X6,X8) != vf(X6,X5)
| X5 = X8 ),
inference(consistent_polarity_flipping,[],[f668]) ).
fof(f4030,plain,
! [X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(sK3)
| X0 = X1
| sK3 = X1
| sK3 = X0
| rline(vd1392)
| ron(X1,vd1392)
| ron(X0,vd1392)
| ~ rpoint(sK0)
| ~ rpoint(X1)
| vf(X1,sK0) != vf(X1,sK3)
| vf(X0,sK0) != vf(X0,sK3)
| sK0 = sK3 ),
inference(resolution,[],[f1903,f648]) ).
fof(f4059,plain,
! [X0,X1] :
( ~ rpoint(X0)
| X0 = X1
| sK3 = X1
| sK3 = X0
| rline(vd1392)
| ron(X1,vd1392)
| ron(X0,vd1392)
| ~ rpoint(sK0)
| ~ rpoint(X1)
| vf(X1,sK0) != vf(X1,sK3)
| vf(X0,sK0) != vf(X0,sK3)
| sK0 = sK3 ),
inference(forward_subsumption_resolution,[],[f4030,f364]) ).
fof(f4069,plain,
! [X0,X1] :
( ~ rpoint(X0)
| X0 = X1
| sK3 = X1
| sK3 = X0
| ron(X1,vd1392)
| ron(X0,vd1392)
| ~ rpoint(sK0)
| ~ rpoint(X1)
| vf(X1,sK0) != vf(X1,sK3)
| vf(X0,sK0) != vf(X0,sK3)
| sK0 = sK3 ),
inference(forward_subsumption_resolution,[],[f4059,f1902]) ).
fof(f4079,plain,
! [X0,X1] :
( ~ rpoint(X0)
| X0 = X1
| sK3 = X1
| sK3 = X0
| ron(X1,vd1392)
| ron(X0,vd1392)
| ~ rpoint(X1)
| vf(X1,sK0) != vf(X1,sK3)
| vf(X0,sK0) != vf(X0,sK3)
| sK0 = sK3 ),
inference(forward_subsumption_resolution,[],[f4069,f359]) ).
fof(f4129,plain,
! [X0,X1] :
( vf(X0,sK0) != vf(X0,sK3)
| X0 = X1
| sK3 = X1
| sK3 = X0
| ron(X1,vd1392)
| ron(X0,vd1392)
| ~ rpoint(X1)
| vf(X1,sK0) != vf(X1,sK3)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f4079,f645]) ).
fof(f7360,plain,
! [X0] :
( vf(sK2,sK3) != vf(sK2,sK3)
| sK2 = X0
| sK3 = X0
| sK2 = sK3
| ron(X0,vd1392)
| ron(sK2,vd1392)
| ~ rpoint(X0)
| vf(X0,sK0) != vf(X0,sK3)
| ~ rpoint(sK2) ),
inference(superposition,[],[f4129,f646]) ).
fof(f7367,plain,
! [X0] :
( sK2 = X0
| sK3 = X0
| sK2 = sK3
| ron(X0,vd1392)
| ron(sK2,vd1392)
| ~ rpoint(X0)
| vf(X0,sK0) != vf(X0,sK3)
| ~ rpoint(sK2) ),
inference(trivial_inequality_removal,[],[f7360]) ).
fof(f7451,plain,
! [X0] :
( sK2 = X0
| sK3 = X0
| ron(X0,vd1392)
| ron(sK2,vd1392)
| ~ rpoint(X0)
| vf(X0,sK0) != vf(X0,sK3)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f7367,f651]) ).
fof(f7471,plain,
! [X0] :
( sK2 = X0
| sK3 = X0
| ron(X0,vd1392)
| ~ rpoint(X0)
| vf(X0,sK0) != vf(X0,sK3)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f7451,f1900]) ).
fof(f7475,plain,
! [X0] :
( vf(X0,sK0) != vf(X0,sK3)
| sK3 = X0
| ron(X0,vd1392)
| ~ rpoint(X0)
| sK2 = X0 ),
inference(forward_subsumption_resolution,[],[f7471,f366]) ).
fof(f76114,plain,
( vf(sK1,sK3) != vf(sK1,sK3)
| sK1 = sK3
| ron(sK1,vd1392)
| ~ rpoint(sK1)
| sK1 = sK2 ),
inference(superposition,[],[f7475,f647]) ).
fof(f76121,plain,
( sK1 = sK3
| ron(sK1,vd1392)
| ~ rpoint(sK1)
| sK1 = sK2 ),
inference(trivial_inequality_removal,[],[f76114]) ).
fof(f76123,plain,
( ron(sK1,vd1392)
| ~ rpoint(sK1)
| sK1 = sK2 ),
inference(forward_subsumption_resolution,[],[f76121,f652]) ).
fof(f76125,plain,
( ~ rpoint(sK1)
| sK1 = sK2 ),
inference(forward_subsumption_resolution,[],[f76123,f1901]) ).
fof(f76127,plain,
sK1 = sK2,
inference(forward_subsumption_resolution,[],[f76125,f368]) ).
fof(f76129,plain,
$false,
inference(forward_subsumption_resolution,[],[f76127,f653]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO340+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.16/0.44 % Computer : n016.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sun Sep 27 08:13:32 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.21/0.49 Running first-order model finding
% 0.21/0.50 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
% 5.56/1.30 % (2310842)Will run a generic schedule for satisfiability detection.
% 5.56/1.30 % (2310852)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1197859677:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.56/1.30 % (2310847)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=714566998_2999 on theBenchmark for (2999ds/0Mi)
% 5.56/1.30 % (2310848)% WARNING: option uhcvi not known.
% 5.56/1.30 % (2310850)dis+10_1_sil=32000:sp=arity:random_seed=785630076:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.56/1.30 % (2310848)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3054930849:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.56/1.30 % (2310849)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3131610130:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.56/1.30 % (2310851)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3740870731:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.56/1.30 % (2310853)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=13975450:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.56/1.30 % (2310852)Instruction limit reached!
% 5.56/1.30 % (2310852)------------------------------
% 5.56/1.30 % (2310852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.30 % (2310852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.30 % (2310852)CaDiCaL version: 2.1.3
% 5.56/1.30 % (2310852)Termination reason: Instruction limit
% 5.56/1.30 % (2310852)Termination phase: Saturation
% 5.56/1.30 % (2310852)Time elapsed: 0.051 s
% 5.56/1.30 % (2310852)Peak memory usage: 13 MB
% 5.56/1.30 % (2310852)Instructions burned: 131 (million)
% 5.56/1.30 % (2310861)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2783426005:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.56/1.30 % Detected minimum model sizes of [3]
% 5.56/1.30 % Detected maximum model sizes of [max]
% 5.56/1.30 % (2310847)Cannot represent all propositional literals internally
% 5.56/1.30 % (2310847)Refutation not found, incomplete strategy
% 5.56/1.30 % (2310847)------------------------------
% 5.56/1.30 % (2310847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.30 % (2310847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.30 % (2310847)CaDiCaL version: 2.1.3
% 5.56/1.30 % (2310847)Termination reason: Refutation not found, incomplete strategy
% 5.56/1.30 % (2310847)Time elapsed: 0.083 s
% 5.56/1.30 % (2310847)Peak memory usage: 12 MB
% 5.56/1.30 % (2310847)Instructions burned: 94 (million)
% 5.56/1.30 % (2310847)------------------------------
% 5.56/1.30 % (2310847)------------------------------
% 5.56/1.30 % Detected minimum model sizes of [3]
% 5.56/1.30 % Detected maximum model sizes of [max]
% 5.56/1.30 % (2310861)Cannot represent all propositional literals internally
% 5.56/1.30 % (2310861)Refutation not found, incomplete strategy
% 5.56/1.30 % (2310861)------------------------------
% 5.56/1.30 % (2310861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.30 % (2310861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.30 % (2310861)CaDiCaL version: 2.1.3
% 5.56/1.30 % (2310861)Termination reason: Refutation not found, incomplete strategy
% 5.56/1.30 % (2310861)Time elapsed: 0.032 s
% 5.56/1.30 % (2310861)Peak memory usage: 12 MB
% 5.56/1.30 % (2310861)Instructions burned: 66 (million)
% 5.56/1.30 % (2310861)------------------------------
% 5.56/1.30 % (2310861)------------------------------
% 5.56/1.30 % (2310850)Instruction limit reached!
% 5.56/1.30 % (2310850)------------------------------
% 5.56/1.30 % (2310850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.30 % (2310850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.30 % (2310850)CaDiCaL version: 2.1.3
% 5.56/1.30 % (2310850)Termination reason: Instruction limit
% 5.56/1.30 % (2310850)Termination phase: Saturation
% 5.56/1.30 % (2310850)Time elapsed: 0.096 s
% 5.56/1.30 % (2310850)Peak memory usage: 13 MB
% 5.56/1.30 % (2310850)Instructions burned: 105 (million)
% 5.56/1.30 % (2310863)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2201011426:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.56/1.30 % (2310851)Instruction limit reached!
% 5.56/1.30 % (2310851)------------------------------
% 5.56/1.30 % (2310851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.30 % (2310851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.74 % (2310851)CaDiCaL version: 2.1.3
% 7.57/1.74 % (2310851)Termination reason: Instruction limit
% 7.57/1.74 % (2310851)Termination phase: Saturation
% 7.57/1.74 % (2310851)Time elapsed: 0.101 s
% 7.57/1.74 % (2310851)Peak memory usage: 13 MB
% 7.57/1.74 % (2310851)Instructions burned: 116 (million)
% 7.57/1.74 % (2310864)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=2002256041:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.57/1.74 % (2310867)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2448011361:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.57/1.74 % (2310865)ott-21_1_sil=16000:fs=off:random_seed=1952798020:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.57/1.74 % (2310853)Instruction limit reached!
% 7.57/1.74 % (2310853)------------------------------
% 7.57/1.74 % (2310853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.57/1.74 % (2310853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.74 % (2310853)CaDiCaL version: 2.1.3
% 7.57/1.74 % (2310853)Termination reason: Instruction limit
% 7.57/1.74 % (2310853)Termination phase: Saturation
% 7.57/1.74 % (2310853)Time elapsed: 0.150 s
% 7.57/1.74 % (2310853)Peak memory usage: 14 MB
% 7.57/1.74 % (2310853)Instructions burned: 159 (million)
% 7.57/1.74 % (2310871)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2618725394:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.57/1.74 % (2310863)Instruction limit reached!
% 7.57/1.74 % (2310863)------------------------------
% 7.57/1.74 % (2310863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.57/1.74 % (2310863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.74 % (2310863)CaDiCaL version: 2.1.3
% 7.57/1.74 % (2310863)Termination reason: Instruction limit
% 7.57/1.74 % (2310863)Termination phase: Saturation
% 7.57/1.74 % (2310863)Time elapsed: 0.104 s
% 7.57/1.74 % (2310863)Peak memory usage: 12 MB
% 7.57/1.74 % (2310863)Instructions burned: 131 (million)
% 7.57/1.74 % (2310873)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1912009588:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 7.57/1.74 % Detected minimum model sizes of [3]
% 7.57/1.74 % Detected maximum model sizes of [max]
% 7.57/1.74 % (2310871)Cannot represent all propositional literals internally
% 7.57/1.74 % (2310871)Refutation not found, incomplete strategy
% 7.57/1.74 % (2310871)------------------------------
% 7.57/1.74 % (2310871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.57/1.74 % (2310871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.74 % (2310871)CaDiCaL version: 2.1.3
% 7.57/1.74 % (2310871)Termination reason: Refutation not found, incomplete strategy
% 7.57/1.74 % (2310871)Time elapsed: 0.063 s
% 7.57/1.74 % (2310871)Peak memory usage: 12 MB
% 7.57/1.74 % (2310871)Instructions burned: 76 (million)
% 7.57/1.74 % (2310871)------------------------------
% 7.57/1.74 % (2310871)------------------------------
% 7.57/1.74 % (2310865)Instruction limit reached!
% 7.57/1.74 % (2310865)------------------------------
% 7.57/1.74 % (2310865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.57/1.74 % (2310865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.74 % (2310865)CaDiCaL version: 2.1.3
% 7.57/1.74 % (2310865)Termination reason: Instruction limit
% 7.57/1.74 % (2310865)Termination phase: Saturation
% 7.57/1.74 % (2310865)Time elapsed: 0.161 s
% 7.57/1.74 % (2310865)Peak memory usage: 14 MB
% 7.57/1.74 % (2310865)Instructions burned: 180 (million)
% 7.57/1.74 % (2310875)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2406979292:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 7.57/1.74 % (2310876)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=1379099332:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 7.57/1.74 % (2310875)Cannot represent all propositional literals internally
% 7.57/1.74 % (2310875)Refutation not found, incomplete strategy
% 7.57/1.74 % (2310875)------------------------------
% 7.57/1.74 % (2310875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.57/1.74 % (2310875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/4.36 % (2310875)CaDiCaL version: 2.1.3
% 27.00/4.36 % (2310875)Termination reason: Refutation not found, incomplete strategy
% 27.00/4.36 % (2310875)Time elapsed: 0.065 s
% 27.00/4.36 % (2310875)Peak memory usage: 12 MB
% 27.00/4.36 % (2310875)Instructions burned: 75 (million)
% 27.00/4.36 % (2310875)------------------------------
% 27.00/4.36 % (2310875)------------------------------
% 27.00/4.36 % (2310879)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2559462841:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 27.00/4.36 % (2310867)Instruction limit reached!
% 27.00/4.36 % (2310867)------------------------------
% 27.00/4.36 % (2310867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.00/4.36 % (2310867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/4.36 % (2310867)CaDiCaL version: 2.1.3
% 27.00/4.36 % (2310867)Termination reason: Instruction limit
% 27.00/4.36 % (2310867)Termination phase: Saturation
% 27.00/4.36 % (2310867)Time elapsed: 0.306 s
% 27.00/4.36 % (2310867)Peak memory usage: 15 MB
% 27.00/4.36 % (2310867)Instructions burned: 478 (million)
% 27.00/4.36 % (2310881)fmb+10_1_sil=64000:random_seed=3339789481:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 27.00/4.36 % Detected minimum model sizes of [3]
% 27.00/4.36 % Detected maximum model sizes of [max]
% 27.00/4.36 % (2310881)Cannot represent all propositional literals internally
% 27.00/4.36 % (2310881)Refutation not found, incomplete strategy
% 27.00/4.36 % (2310881)------------------------------
% 27.00/4.36 % (2310881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.00/4.36 % (2310881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/4.36 % (2310881)CaDiCaL version: 2.1.3
% 27.00/4.36 % (2310881)Termination reason: Refutation not found, incomplete strategy
% 27.00/4.36 % (2310881)Time elapsed: 0.029 s
% 27.00/4.36 % (2310881)Peak memory usage: 12 MB
% 27.00/4.36 % (2310881)Instructions burned: 63 (million)
% 27.00/4.36 % (2310881)------------------------------
% 27.00/4.36 % (2310881)------------------------------
% 27.00/4.36 % (2310883)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3228676824:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 27.00/4.36 % Detected minimum model sizes of [3]
% 27.00/4.36 % Detected maximum model sizes of [max]
% 27.00/4.36 % (2310883)Cannot represent all propositional literals internally
% 27.00/4.36 % (2310883)Refutation not found, incomplete strategy
% 27.00/4.36 % (2310883)------------------------------
% 27.00/4.36 % (2310883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.00/4.36 % (2310883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/4.36 % (2310883)CaDiCaL version: 2.1.3
% 27.00/4.36 % (2310883)Termination reason: Refutation not found, incomplete strategy
% 27.00/4.36 % (2310883)Time elapsed: 0.032 s
% 27.00/4.36 % (2310883)Peak memory usage: 12 MB
% 27.00/4.36 % (2310883)Instructions burned: 76 (million)
% 27.00/4.36 % (2310883)------------------------------
% 27.00/4.36 % (2310883)------------------------------
% 27.00/4.36 % (2310885)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1223600567:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 27.00/4.36 % Detected minimum model sizes of [3]
% 27.00/4.36 % Detected maximum model sizes of [max]
% 27.00/4.36 % (2310885)Cannot represent all propositional literals internally
% 27.00/4.36 % (2310885)Refutation not found, incomplete strategy
% 27.00/4.36 % (2310885)------------------------------
% 27.00/4.36 % (2310885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.00/4.36 % (2310885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/4.36 % (2310885)CaDiCaL version: 2.1.3
% 27.00/4.36 % (2310885)Termination reason: Refutation not found, incomplete strategy
% 27.00/4.36 % (2310885)Time elapsed: 0.047 s
% 27.00/4.36 % (2310885)Peak memory usage: 12 MB
% 27.00/4.36 % (2310885)Instructions burned: 76 (million)
% 27.00/4.36 % (2310885)------------------------------
% 27.00/4.36 % (2310885)------------------------------
% 27.00/4.36 % (2310887)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3948478109:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 27.00/4.36 % (2310864)Instruction limit reached!
% 27.00/4.36 % (2310864)------------------------------
% 27.00/4.36 % (2310864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.00/4.36 % (2310864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/4.36 % (2310864)CaDiCaL version: 2.1.3
% 27.00/4.36 % (2310864)Termination reason: Instruction limit
% 33.33/5.27 % (2310864)Termination phase: Saturation
% 33.33/5.27 % (2310864)Time elapsed: 0.634 s
% 33.33/5.27 % (2310864)Peak memory usage: 21 MB
% 33.33/5.27 % (2310864)Instructions burned: 685 (million)
% 33.33/5.27 % (2310890)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2812044854:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 33.33/5.27 % (2310876)Instruction limit reached!
% 33.33/5.27 % (2310876)------------------------------
% 33.33/5.27 % (2310876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.33/5.27 % (2310876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.33/5.27 % (2310876)CaDiCaL version: 2.1.3
% 33.33/5.27 % (2310876)Termination reason: Instruction limit
% 33.33/5.27 % (2310876)Termination phase: Saturation
% 33.33/5.27 % (2310876)Time elapsed: 0.659 s
% 33.33/5.27 % (2310876)Peak memory usage: 21 MB
% 33.33/5.27 % (2310876)Instructions burned: 693 (million)
% 33.33/5.27 % (2310894)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2954333694:i=6324_2989 on theBenchmark for (2989ds/6324Mi)
% 33.33/5.27 % (2310879)Instruction limit reached!
% 33.33/5.27 % (2310879)------------------------------
% 33.33/5.27 % (2310879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.33/5.27 % (2310879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.33/5.27 % (2310879)CaDiCaL version: 2.1.3
% 33.33/5.27 % (2310879)Termination reason: Instruction limit
% 33.33/5.27 % (2310879)Termination phase: Saturation
% 33.33/5.27 % (2310879)Time elapsed: 0.662 s
% 33.33/5.27 % (2310879)Peak memory usage: 20 MB
% 33.33/5.27 % (2310879)Instructions burned: 880 (million)
% 33.33/5.27 % (2310897)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2341308073:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi)
% 33.33/5.27 % (2310873)Instruction limit reached!
% 33.33/5.27 % (2310873)------------------------------
% 33.33/5.27 % (2310873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.33/5.27 % (2310873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.33/5.27 % (2310873)CaDiCaL version: 2.1.3
% 33.33/5.27 % (2310873)Termination reason: Instruction limit
% 33.33/5.27 % (2310873)Termination phase: Saturation
% 33.33/5.27 % (2310873)Time elapsed: 0.890 s
% 33.33/5.27 % (2310873)Peak memory usage: 19 MB
% 33.33/5.27 % (2310873)Instructions burned: 1179 (million)
% 33.33/5.27 % Detected minimum model sizes of [3]
% 33.33/5.27 % Detected maximum model sizes of [max]
% 33.33/5.27 % (2310897)Cannot represent all propositional literals internally
% 33.33/5.27 % (2310897)Refutation not found, incomplete strategy
% 33.33/5.27 % (2310897)------------------------------
% 33.33/5.27 % (2310897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.33/5.27 % (2310897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.33/5.27 % (2310897)CaDiCaL version: 2.1.3
% 33.33/5.27 % (2310897)Termination reason: Refutation not found, incomplete strategy
% 33.33/5.27 % (2310897)Time elapsed: 0.040 s
% 33.33/5.27 % (2310897)Peak memory usage: 12 MB
% 33.33/5.27 % (2310897)Instructions burned: 77 (million)
% 33.33/5.27 % (2310897)------------------------------
% 33.33/5.27 % (2310897)------------------------------
% 33.33/5.27 % Detected minimum model sizes of [3]
% 33.33/5.27 % Detected maximum model sizes of [max]
% 33.33/5.27 % (2310894)Cannot represent all propositional literals internally
% 33.33/5.27 % (2310894)Refutation not found, incomplete strategy
% 33.33/5.27 % (2310894)------------------------------
% 33.33/5.27 % (2310894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.33/5.27 % (2310894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.33/5.27 % (2310894)CaDiCaL version: 2.1.3
% 33.33/5.27 % (2310894)Termination reason: Refutation not found, incomplete strategy
% 33.33/5.27 % (2310894)Time elapsed: 0.099 s
% 33.33/5.27 % (2310894)Peak memory usage: 12 MB
% 33.33/5.27 % (2310894)Instructions burned: 93 (million)
% 33.33/5.27 % (2310899)ott-2_1_sil=16000:newcnf=on:random_seed=3220713021:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 33.33/5.27 % (2310894)------------------------------
% 33.33/5.27 % (2310894)------------------------------
% 33.33/5.27 % (2310900)ott+10_1_sil=32000:tgt=ground:random_seed=3238351478:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 33.33/5.27 % (2310902)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2437468639:i=54282_2988 on theBenchmark for (2988ds/54282Mi)
% 40.22/7.40 % Detected minimum model sizes of [3]
% 40.22/7.40 % Detected maximum model sizes of [max]
% 40.22/7.40 % (2310902)Cannot represent all propositional literals internally
% 40.22/7.40 % (2310902)Refutation not found, incomplete strategy
% 40.22/7.40 % (2310902)------------------------------
% 40.22/7.40 % (2310902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310902)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310902)Termination reason: Refutation not found, incomplete strategy
% 40.22/7.40 % (2310902)Time elapsed: 0.052 s
% 40.22/7.40 % (2310902)Peak memory usage: 12 MB
% 40.22/7.40 % (2310902)Instructions burned: 94 (million)
% 40.22/7.40 % (2310902)------------------------------
% 40.22/7.40 % (2310902)------------------------------
% 40.22/7.40 % (2310906)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2992259217:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi)
% 40.22/7.40 % (2310899)Instruction limit reached!
% 40.22/7.40 % (2310899)------------------------------
% 40.22/7.40 % (2310899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310899)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310899)Termination reason: Instruction limit
% 40.22/7.40 % (2310899)Termination phase: Saturation
% 40.22/7.40 % (2310899)Time elapsed: 0.701 s
% 40.22/7.40 % (2310899)Peak memory usage: 16 MB
% 40.22/7.40 % (2310899)Instructions burned: 869 (million)
% 40.22/7.40 % (2310911)dis+21_1_sil=32000:sas=cadical:random_seed=2067197756:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi)
% 40.22/7.40 % (2310890)Instruction limit reached!
% 40.22/7.40 % (2310890)------------------------------
% 40.22/7.40 % (2310890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310890)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310890)Termination reason: Instruction limit
% 40.22/7.40 % (2310890)Termination phase: Saturation
% 40.22/7.40 % (2310890)Time elapsed: 1.184 s
% 40.22/7.40 % (2310890)Peak memory usage: 16 MB
% 40.22/7.40 % (2310890)Instructions burned: 1473 (million)
% 40.22/7.40 % (2310917)ott+11_1_sil=16000:gs=on:random_seed=363741022:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi)
% 40.22/7.40 % (2310887)Instruction limit reached!
% 40.22/7.40 % (2310887)------------------------------
% 40.22/7.40 % (2310887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310887)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310887)Termination reason: Instruction limit
% 40.22/7.40 % (2310887)Termination phase: Saturation
% 40.22/7.40 % (2310887)Time elapsed: 2.050 s
% 40.22/7.40 % (2310887)Peak memory usage: 34 MB
% 40.22/7.40 % (2310887)Instructions burned: 5133 (million)
% 40.22/7.40 % (2310921)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=319989986:fmbsr=1.6:i=67534_2972 on theBenchmark for (2972ds/67534Mi)
% 40.22/7.40 % Detected minimum model sizes of [3]
% 40.22/7.40 % Detected maximum model sizes of [max]
% 40.22/7.40 % (2310921)Cannot represent all propositional literals internally
% 40.22/7.40 % (2310921)Refutation not found, incomplete strategy
% 40.22/7.40 % (2310921)------------------------------
% 40.22/7.40 % (2310921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310921)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310921)Termination reason: Refutation not found, incomplete strategy
% 40.22/7.40 % (2310921)Time elapsed: 0.046 s
% 40.22/7.40 % (2310921)Peak memory usage: 12 MB
% 40.22/7.40 % (2310921)Instructions burned: 82 (million)
% 40.22/7.40 % (2310921)------------------------------
% 40.22/7.40 % (2310921)------------------------------
% 40.22/7.40 % (2310923)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3317861659:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi)
% 40.22/7.40 % (2310917)Instruction limit reached!
% 40.22/7.40 % (2310917)------------------------------
% 40.22/7.40 % (2310917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310917)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310917)Termination reason: Instruction limit
% 40.22/7.40 % (2310917)Termination phase: Saturation
% 40.22/7.40 % (2310917)Time elapsed: 1.787 s
% 40.22/7.40 % (2310917)Peak memory usage: 17 MB
% 40.22/7.40 % (2310917)Instructions burned: 2251 (million)
% 40.22/7.40 % (2310927)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3062589523:i=29340_2961 on theBenchmark for (2961ds/29340Mi)
% 40.22/7.40 % (2310906)Instruction limit reached!
% 40.22/7.40 % (2310906)------------------------------
% 40.22/7.40 % (2310906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310906)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310906)Termination reason: Instruction limit
% 40.22/7.40 % (2310906)Termination phase: Saturation
% 40.22/7.40 % (2310906)Time elapsed: 2.980 s
% 40.22/7.40 % (2310906)Peak memory usage: 31 MB
% 40.22/7.40 % (2310906)Instructions burned: 3513 (million)
% 40.22/7.40 % (2310931)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4146119897:i=5211_2956 on theBenchmark for (2956ds/5211Mi)
% 40.22/7.40 % (2310923)Instruction limit reached!
% 40.22/7.40 % (2310923)------------------------------
% 40.22/7.40 % (2310923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310923)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310923)Termination reason: Instruction limit
% 40.22/7.40 % (2310923)Termination phase: Saturation
% 40.22/7.40 % (2310923)Time elapsed: 1.726 s
% 40.22/7.40 % (2310923)Peak memory usage: 27 MB
% 40.22/7.40 % (2310923)Instructions burned: 4591 (million)
% 40.22/7.40 % (2310933)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3490938978:i=5497:nm=2_2954 on theBenchmark for (2954ds/5497Mi)
% 40.22/7.40 % Detected minimum model sizes of [3]
% 40.22/7.40 % Detected maximum model sizes of [max]
% 40.22/7.40 % (2310933)Cannot represent all propositional literals internally
% 40.22/7.40 % (2310933)Refutation not found, incomplete strategy
% 40.22/7.40 % (2310933)------------------------------
% 40.22/7.40 % (2310933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310933)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310933)Termination reason: Refutation not found, incomplete strategy
% 40.22/7.40 % (2310933)Time elapsed: 0.046 s
% 40.22/7.40 % (2310933)Peak memory usage: 12 MB
% 40.22/7.40 % (2310933)Instructions burned: 74 (million)
% 40.22/7.40 % (2310933)------------------------------
% 40.22/7.40 % (2310933)------------------------------
% 40.22/7.40 % (2310935)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=521256977:fmbsr=2:i=46332_2953 on theBenchmark for (2953ds/46332Mi)
% 40.22/7.40 % Detected minimum model sizes of [3]
% 40.22/7.40 % Detected maximum model sizes of [max]
% 40.22/7.40 % (2310935)Cannot represent all propositional literals internally
% 40.22/7.40 % (2310935)Refutation not found, incomplete strategy
% 40.22/7.40 % (2310935)------------------------------
% 40.22/7.40 % (2310935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310935)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310935)Termination reason: Refutation not found, incomplete strategy
% 40.22/7.40 % (2310935)Time elapsed: 0.033 s
% 40.22/7.40 % (2310935)Peak memory usage: 12 MB
% 40.22/7.40 % (2310935)Instructions burned: 82 (million)
% 40.22/7.40 % (2310935)------------------------------
% 40.22/7.40 % (2310935)------------------------------
% 40.22/7.40 % (2310937)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4246086390:i=14071_2952 on theBenchmark for (2952ds/14071Mi)
% 40.22/7.40 % Detected minimum model sizes of [3]
% 40.22/7.40 % Detected maximum model sizes of [max]
% 40.22/7.40 % (2310937)Cannot represent all propositional literals internally
% 40.22/7.40 % (2310937)Refutation not found, incomplete strategy
% 40.22/7.40 % (2310937)------------------------------
% 40.22/7.40 % (2310937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310937)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310937)Termination reason: Refutation not found, incomplete strategy
% 40.22/7.40 % (2310937)Time elapsed: 0.040 s
% 40.22/7.40 % (2310937)Peak memory usage: 12 MB
% 40.22/7.40 % (2310937)Instructions burned: 76 (million)
% 40.22/7.40 % (2310937)------------------------------
% 40.22/7.40 % (2310937)------------------------------
% 40.22/7.40 % (2310939)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3908755078:i=22565:add=on:rawr=on_2952 on theBenchmark for (2952ds/22565Mi)
% 40.22/7.40 % (2310911)Instruction limit reached!
% 40.22/7.40 % (2310911)------------------------------
% 40.22/7.40 % (2310911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310911)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310911)Termination reason: Instruction limit
% 40.22/7.40 % (2310911)Termination phase: Saturation
% 40.22/7.40 % (2310911)Time elapsed: 3.195 s
% 40.22/7.40 % (2310911)Peak memory usage: 34 MB
% 40.22/7.40 % (2310911)Instructions burned: 3774 (million)
% 40.22/7.40 % (2310945)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3368703687:i=8173:av=off_2948 on theBenchmark for (2948ds/8173Mi)
% 40.22/7.40 % (2310900)Instruction limit reached!
% 40.22/7.40 % (2310900)------------------------------
% 40.22/7.40 % (2310900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310900)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310900)Termination reason: Instruction limit
% 40.22/7.40 % (2310900)Termination phase: Saturation
% 40.22/7.40 % (2310900)Time elapsed: 4.407 s
% 40.22/7.40 % (2310900)Peak memory usage: 61 MB
% 40.22/7.40 % (2310900)Instructions burned: 5114 (million)
% 40.22/7.40 % (2310947)dis+10_16:1_sil=16000:random_seed=3268946992:i=9155:fsr=off_2943 on theBenchmark for (2943ds/9155Mi)
% 40.22/7.40 % (2310848) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2310842-2310848"...
% 40.22/7.40 % (2310848)...printing done.
% 40.22/7.40 % (2310848)Refutation found. Thanks to Tanya!
% 40.22/7.40 % SZS status Theorem for theBenchmark
% 40.22/7.40 % SZS output start Proof for theBenchmark
% See solution above
% 40.22/7.40 % (2310848)------------------------------
% 40.22/7.40 % (2310848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/7.40 % (2310848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/7.40 % (2310848)CaDiCaL version: 2.1.3
% 40.22/7.40 % (2310848)Termination reason: Refutation
% 40.22/7.40 % (2310848)Time elapsed: 6.823 s
% 40.22/7.40 % (2310848)Peak memory usage: 44 MB
% 40.22/7.40 % (2310848)Instructions burned: 7779 (million)
% 40.22/7.40 % (2310842)Success in time 6.895 s
% 40.22/7.40 % Vampire exiting
%------------------------------------------------------------------------------