%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV677+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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 12:59:39 PM UTC 2026
% Result : Theorem 57.95s 15.58s
% Output : Refutation 57.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 65 ( 29 unt; 3 def)
% Number of atoms : 147 ( 54 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 123 ( 41 ~; 55 |; 19 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 4 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 30 ( 0 sgn 23 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f277,axiom,
! [X0] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X0)
=> ( ( X0 = cCoq_2eInit_2eDatatypes_2eO
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU0 )
| ? [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
& ( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
=> ( X0 = cCoq_2eInit_2eDatatypes_2eS___24a1(X1)
& ( ( X1 = cCoq_2eInit_2eDatatypes_2eO
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU1 )
| ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& X1 = cCoq_2eInit_2eDatatypes_2eS___24a1(X2)
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cCoq_2eSets_2eEnsembles_2eFull__set___24a1(cTopology_2eTopologicalSpaces_2epoint__set___24a1(cX)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_UrysohnsLemma.Urysohns_Lemma_construction.Un') ).
fof(f1363,axiom,
cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(cX),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_X') ).
fof(f1885,axiom,
! [X0] :
( cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(X0)
=> cTopology_2eTopologicalSpaces_2eopen___24a2(X0,cCoq_2eSets_2eEnsembles_2eFull__set___24a1(cTopology_2eTopologicalSpaces_2epoint__set___24a1(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Topology.TopologicalSpaces.open_full') ).
fof(f1898,axiom,
cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cU0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','U0_open') ).
fof(f1899,axiom,
cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cU1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','U1_open') ).
fof(f2373,axiom,
! [X0] : happ(cTopology_2eTopologicalSpaces_2epoint__set,X0) = cTopology_2eTopologicalSpaces_2epoint__set___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Topology.TopologicalSpaces.point_set_$a1') ).
fof(f2516,axiom,
! [X0] : happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) = cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_UrysohnsLemma.Urysohns_Lemma_construction.Un_$a1') ).
fof(f2619,axiom,
! [X0] : happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0) = cCoq_2eSets_2eEnsembles_2eFull__set___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Coq.Sets.Ensembles.Full_set_$a1') ).
fof(f3186,conjecture,
! [X0] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X0)
=> cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof(f3187,negated_conjecture,
~ ! [X0] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X0)
=> cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0)) ),
inference(negated_conjecture,[status(cth)],[f3186]) ).
fof(f3484,plain,
! [X0] :
( ( X0 = cCoq_2eInit_2eDatatypes_2eO
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU0 )
| ? [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
& ( ( X0 = cCoq_2eInit_2eDatatypes_2eS___24a1(X1)
& ( ( X1 = cCoq_2eInit_2eDatatypes_2eO
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU1 )
| ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& X1 = cCoq_2eInit_2eDatatypes_2eS___24a1(X2)
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cCoq_2eSets_2eEnsembles_2eFull__set___24a1(cTopology_2eTopologicalSpaces_2epoint__set___24a1(cX)) ) ) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1) ) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0) ),
inference(ennf_transformation,[],[f277]) ).
fof(f3485,plain,
! [X0] :
( ( X0 = cCoq_2eInit_2eDatatypes_2eO
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU0 )
| ? [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
& ( ( X0 = cCoq_2eInit_2eDatatypes_2eS___24a1(X1)
& ( ( X1 = cCoq_2eInit_2eDatatypes_2eO
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU1 )
| ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& X1 = cCoq_2eInit_2eDatatypes_2eS___24a1(X2)
& cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cCoq_2eSets_2eEnsembles_2eFull__set___24a1(cTopology_2eTopologicalSpaces_2epoint__set___24a1(cX)) ) ) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1) ) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0) ),
inference(flattening,[],[f3484]) ).
fof(f5062,plain,
! [X0] :
( cTopology_2eTopologicalSpaces_2eopen___24a2(X0,cCoq_2eSets_2eEnsembles_2eFull__set___24a1(cTopology_2eTopologicalSpaces_2epoint__set___24a1(X0)))
| ~ cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(X0) ),
inference(ennf_transformation,[],[f1885]) ).
fof(f5197,plain,
? [X0] :
( ~ cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0))
& cCoq_2eInit_2eDatatypes_2enat___24t(X0) ),
inference(ennf_transformation,[],[f3187]) ).
fof(f6958,plain,
! [X0] :
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sK385(X0))
| cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cCoq_2eSets_2eEnsembles_2eFull__set___24a1(cTopology_2eTopologicalSpaces_2epoint__set___24a1(cX))
| cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU1
| cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU0 ),
inference(cnf_transformation,[],[f3485]) ).
fof(f6970,plain,
! [X0] :
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0)
| cCoq_2eInit_2eDatatypes_2enat___24t(sK385(X0))
| cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = cU0 ),
inference(cnf_transformation,[],[f3485]) ).
fof(f10340,plain,
cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(cX),
inference(cnf_transformation,[],[f1363]) ).
fof(f11314,plain,
! [X0] :
( ~ cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(X0)
| cTopology_2eTopologicalSpaces_2eopen___24a2(X0,cCoq_2eSets_2eEnsembles_2eFull__set___24a1(cTopology_2eTopologicalSpaces_2epoint__set___24a1(X0))) ),
inference(cnf_transformation,[],[f5062]) ).
fof(f11364,plain,
cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cU0),
inference(cnf_transformation,[],[f1898]) ).
fof(f11365,plain,
cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cU1),
inference(cnf_transformation,[],[f1899]) ).
fof(f12047,plain,
! [X0] : cTopology_2eTopologicalSpaces_2epoint__set___24a1(X0) = happ(cTopology_2eTopologicalSpaces_2epoint__set,X0),
inference(cnf_transformation,[],[f2373]) ).
fof(f12223,plain,
! [X0] : cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(X0) = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0),
inference(cnf_transformation,[],[f2516]) ).
fof(f12360,plain,
! [X0] : cCoq_2eSets_2eEnsembles_2eFull__set___24a1(X0) = happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0),
inference(cnf_transformation,[],[f2619]) ).
fof(f13377,plain,
cCoq_2eInit_2eDatatypes_2enat___24t(sK1712),
inference(cnf_transformation,[],[f5197]) ).
fof(f13378,plain,
~ cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn___24a1(sK1712)),
inference(cnf_transformation,[],[f5197]) ).
fof(f14683,plain,
! [X0] :
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0)
| cCoq_2eInit_2eDatatypes_2enat___24t(sK385(X0))
| cU0 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) ),
inference(definition_unfolding,[],[f6970,f12223]) ).
fof(f14693,plain,
! [X0] :
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sK385(X0))
| happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) = happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,cX))
| cU1 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0)
| cU0 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) ),
inference(definition_unfolding,[],[f6958,f12223,f12360,f12047,f12223,f12223]) ).
fof(f16524,plain,
! [X0] :
( ~ cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(X0)
| cTopology_2eTopologicalSpaces_2eopen___24a2(X0,happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,X0))) ),
inference(definition_unfolding,[],[f11314,f12360,f12047]) ).
fof(f16849,plain,
~ cTopology_2eTopologicalSpaces_2eopen___24a2(cX,happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)),
inference(definition_unfolding,[],[f13378,f12223]) ).
fof(f18251,plain,
! [X0] :
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sK385(X0))
| cCoq_2eInit_2eDatatypes_2enat___24t(X0)
| cU0 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) ),
inference(consistent_polarity_flipping,[],[f14683]) ).
fof(f18263,plain,
! [X0] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X0)
| cCoq_2eInit_2eDatatypes_2enat___24t(sK385(X0))
| happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) = happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,cX))
| cU1 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0)
| cU0 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) ),
inference(consistent_polarity_flipping,[],[f14693]) ).
fof(f20648,plain,
~ cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(cX),
inference(consistent_polarity_flipping,[],[f10340]) ).
fof(f21593,plain,
! [X0] :
( ~ cTopology_2eTopologicalSpaces_2eopen___24a2(X0,happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,X0)))
| cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(X0) ),
inference(consistent_polarity_flipping,[],[f16524]) ).
fof(f21642,plain,
~ cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cU0),
inference(consistent_polarity_flipping,[],[f11364]) ).
fof(f21643,plain,
~ cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cU1),
inference(consistent_polarity_flipping,[],[f11365]) ).
fof(f22655,plain,
cTopology_2eTopologicalSpaces_2eopen___24a2(cX,happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)),
inference(consistent_polarity_flipping,[],[f16849]) ).
fof(f22656,plain,
~ cCoq_2eInit_2eDatatypes_2enat___24t(sK1712),
inference(consistent_polarity_flipping,[],[f13377]) ).
fof(f128526,definition,
( spl1713_10460
<=> cU0 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712) ),
introduced(definition,[new_symbols(definition,[spl1713_10460])],[avatar_definition]) ).
fof(f128527,plain,
( cU0 != happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)
| spl1713_10460 ),
inference(avatar_component_clause,[],[f128526]) ).
fof(f128528,plain,
( cU0 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)
| ~ spl1713_10460 ),
inference(avatar_component_clause,[],[f128526]) ).
fof(f143735,plain,
( cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cU0)
| ~ spl1713_10460 ),
inference(superposition,[],[f22655,f128528]) ).
fof(f143851,plain,
( $false
| ~ spl1713_10460 ),
inference(forward_subsumption_resolution,[],[f143735,f21642]) ).
fof(f143852,plain,
~ spl1713_10460,
inference(avatar_contradiction_clause,[],[f143851]) ).
fof(f188879,definition,
( spl1713_15120
<=> cU1 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712) ),
introduced(definition,[new_symbols(definition,[spl1713_15120])],[avatar_definition]) ).
fof(f188881,plain,
( cU1 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)
| ~ spl1713_15120 ),
inference(avatar_component_clause,[],[f188879]) ).
fof(f188910,definition,
( spl1713_15126
<=> happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,cX)) = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712) ),
introduced(definition,[new_symbols(definition,[spl1713_15126])],[avatar_definition]) ).
fof(f188912,plain,
( happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,cX)) = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)
| ~ spl1713_15126 ),
inference(avatar_component_clause,[],[f188910]) ).
fof(f198490,plain,
! [X0] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X0)
| happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) = happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,cX))
| cU1 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0)
| cU0 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,X0) ),
inference(forward_subsumption_resolution,[],[f18263,f18251]) ).
fof(f198592,plain,
( happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,cX)) = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)
| cU1 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)
| cU0 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712) ),
inference(resolution,[],[f198490,f22656]) ).
fof(f198593,plain,
( happ(cCoq_2eSets_2eEnsembles_2eFull__set,happ(cTopology_2eTopologicalSpaces_2epoint__set,cX)) = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)
| cU1 = happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712)
| spl1713_10460 ),
inference(forward_subsumption_resolution,[],[f198592,f128527]) ).
fof(f228650,plain,
( spl1713_15120
| spl1713_15126
| spl1713_10460 ),
inference(avatar_split_clause,[],[f198593,f128526,f188910,f188879]) ).
fof(f339697,plain,
( cTopology_2eTopologicalSpaces_2eopen___24a2(cX,cU1)
| ~ spl1713_15120 ),
inference(superposition,[],[f22655,f188881]) ).
fof(f339854,plain,
( $false
| ~ spl1713_15120 ),
inference(forward_subsumption_resolution,[],[f339697,f21643]) ).
fof(f339855,plain,
~ spl1713_15120,
inference(avatar_contradiction_clause,[],[f339854]) ).
fof(f346708,plain,
( ~ cTopology_2eTopologicalSpaces_2eopen___24a2(cX,happ(cUrysohnsLemma_2eUrysohns__Lemma__construction_2eUn,sK1712))
| cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(cX)
| ~ spl1713_15126 ),
inference(superposition,[],[f21593,f188912]) ).
fof(f347441,plain,
( cTopology_2eTopologicalSpaces_2eTopologicalSpace___24t(cX)
| ~ spl1713_15126 ),
inference(forward_subsumption_resolution,[],[f346708,f22655]) ).
fof(f347451,plain,
( $false
| ~ spl1713_15126 ),
inference(forward_subsumption_resolution,[],[f347441,f20648]) ).
fof(f347452,plain,
~ spl1713_15126,
inference(avatar_contradiction_clause,[],[f347451]) ).
cnf(s7927,plain,
~ spl1713_10460,
inference(sat_conversion,[],[f143852]) ).
cnf(s14583,plain,
( spl1713_10460
| spl1713_15120
| spl1713_15126 ),
inference(sat_conversion,[],[f228650]) ).
cnf(s23057,plain,
~ spl1713_15120,
inference(sat_conversion,[],[f339855]) ).
cnf(s24139,plain,
~ spl1713_15126,
inference(sat_conversion,[],[f347452]) ).
cnf(s24155,plain,
spl1713_10460,
inference(rat,[],[s14583,s24139,s23057]) ).
cnf(s24414,plain,
$false,
inference(rat,[],[s7927,s24155]) ).
fof(f347453,plain,
$false,
inference(avatar_sat_refutation,[],[s24414]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV677+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 28 06:53:18 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.43 Running first-order model finding
% 0.15/0.43 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
% 22.76/3.94 % (3812139)Will run a generic schedule for satisfiability detection.
% 22.76/3.94 % (3812148)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=115364316:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 22.76/3.94 % (3812145)% WARNING: option uhcvi not known.
% 22.76/3.94 % (3812145)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3655828441:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 22.76/3.94 % (3812146)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1267541270:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 22.76/3.94 % (3812147)dis+10_1_sil=32000:sp=arity:random_seed=628813097:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 22.76/3.94 % (3812144)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1306858258_2997 on theBenchmark for (2997ds/0Mi)
% 22.76/3.94 % (3812150)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1725257152:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 22.76/3.94 % (3812149)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3651108979:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 22.76/3.94 % (3812148)Instruction limit reached!
% 22.76/3.94 % (3812148)------------------------------
% 22.76/3.94 % (3812148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.76/3.94 % (3812148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.76/3.94 % (3812148)CaDiCaL version: 2.1.3
% 22.76/3.94 % (3812148)Termination reason: Instruction limit
% 22.76/3.94 % (3812148)Termination phase: NewCNF
% 22.76/3.94 % (3812148)Time elapsed: 0.064 s
% 22.76/3.94 % (3812148)Peak memory usage: 19 MB
% 22.76/3.94 % (3812148)Instructions burned: 117 (million)
% 22.76/3.94 % (3812158)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3498733050:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 22.76/3.94 % (3812147)Instruction limit reached!
% 22.76/3.94 % (3812147)------------------------------
% 22.76/3.94 % (3812147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.76/3.94 % (3812147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.76/3.94 % (3812147)CaDiCaL version: 2.1.3
% 22.76/3.94 % (3812147)Termination reason: Instruction limit
% 22.76/3.94 % (3812147)Termination phase: Preprocessing 3
% 22.76/3.94 % (3812147)Time elapsed: 0.107 s
% 22.76/3.94 % (3812147)Peak memory usage: 19 MB
% 22.76/3.94 % (3812147)Instructions burned: 103 (million)
% 22.76/3.94 % (3812149)Instruction limit reached!
% 22.76/3.94 % (3812149)------------------------------
% 22.76/3.94 % (3812149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.76/3.94 % (3812149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.76/3.94 % (3812149)CaDiCaL version: 2.1.3
% 22.76/3.94 % (3812149)Termination reason: Instruction limit
% 22.76/3.94 % (3812149)Termination phase: Clausification
% 22.76/3.94 % (3812149)Time elapsed: 0.136 s
% 22.76/3.94 % (3812149)Peak memory usage: 21 MB
% 22.76/3.94 % (3812149)Instructions burned: 131 (million)
% 22.76/3.94 % (3812160)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2174395440:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi)
% 22.76/3.94 % (3812150)Instruction limit reached!
% 22.76/3.94 % (3812150)------------------------------
% 22.76/3.94 % (3812150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.76/3.94 % (3812150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.76/3.94 % (3812150)CaDiCaL version: 2.1.3
% 22.76/3.94 % (3812150)Termination reason: Instruction limit
% 22.76/3.94 % (3812150)Termination phase: Property scanning
% 22.76/3.94 % (3812150)Time elapsed: 0.163 s
% 22.76/3.94 % (3812150)Peak memory usage: 22 MB
% 22.76/3.94 % (3812150)Instructions burned: 159 (million)
% 22.76/3.94 % (3812161)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=2583873900:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 22.76/3.94 % (3812163)ott-21_1_sil=16000:fs=off:random_seed=425390522:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 22.76/3.94 % (3812160)Instruction limit reached!
% 22.76/3.94 % (3812160)------------------------------
% 22.76/3.94 % (3812160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.76/3.94 % (3812160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.03/7.35 % (3812160)CaDiCaL version: 2.1.3
% 47.03/7.35 % (3812160)Termination reason: Instruction limit
% 47.03/7.35 % (3812160)Termination phase: Clausification
% 47.03/7.35 % (3812160)Time elapsed: 0.138 s
% 47.03/7.35 % (3812160)Peak memory usage: 21 MB
% 47.03/7.35 % (3812160)Instructions burned: 131 (million)
% 47.03/7.35 % (3812166)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2452858984:i=477:bd=all_2993 on theBenchmark for (2993ds/477Mi)
% 47.03/7.35 % (3812163)Instruction limit reached!
% 47.03/7.35 % (3812163)------------------------------
% 47.03/7.35 % (3812163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.03/7.35 % (3812163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.03/7.35 % (3812163)CaDiCaL version: 2.1.3
% 47.03/7.35 % (3812163)Termination reason: Instruction limit
% 47.03/7.35 % (3812163)Termination phase: Property scanning
% 47.03/7.35 % (3812163)Time elapsed: 0.180 s
% 47.03/7.35 % (3812163)Peak memory usage: 22 MB
% 47.03/7.35 % (3812163)Instructions burned: 180 (million)
% 47.03/7.35 % (3812158)Instruction limit reached!
% 47.03/7.35 % (3812158)------------------------------
% 47.03/7.35 % (3812158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.03/7.35 % (3812158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.03/7.35 % (3812158)CaDiCaL version: 2.1.3
% 47.03/7.35 % (3812158)Termination reason: Instruction limit
% 47.03/7.35 % (3812158)Termination phase: Finite model building preprocessing
% 47.03/7.35 % (3812158)Time elapsed: 0.347 s
% 47.03/7.35 % (3812158)Peak memory usage: 32 MB
% 47.03/7.35 % (3812158)Instructions burned: 715 (million)
% 47.03/7.35 % (3812168)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1022005056:fmbsr=1.3:i=865:ins=25_2992 on theBenchmark for (2992ds/865Mi)
% 47.03/7.35 % (3812169)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3606974679:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 47.03/7.35 % (3812161)Instruction limit reached!
% 47.03/7.35 % (3812161)------------------------------
% 47.03/7.35 % (3812161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.03/7.35 % (3812161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.03/7.35 % (3812161)CaDiCaL version: 2.1.3
% 47.03/7.35 % (3812161)Termination reason: Instruction limit
% 47.03/7.35 % (3812161)Termination phase: Saturation
% 47.03/7.35 % (3812161)Time elapsed: 0.570 s
% 47.03/7.35 % (3812161)Peak memory usage: 26 MB
% 47.03/7.35 % (3812161)Instructions burned: 684 (million)
% 47.03/7.35 % (3812166)Instruction limit reached!
% 47.03/7.35 % (3812166)------------------------------
% 47.03/7.35 % (3812166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.03/7.35 % (3812166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.03/7.35 % (3812166)CaDiCaL version: 2.1.3
% 47.03/7.35 % (3812166)Termination reason: Instruction limit
% 47.03/7.35 % (3812166)Termination phase: Saturation
% 47.03/7.35 % (3812166)Time elapsed: 0.442 s
% 47.03/7.35 % (3812166)Peak memory usage: 27 MB
% 47.03/7.35 % (3812166)Instructions burned: 477 (million)
% 47.03/7.35 % (3812172)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2851767477:i=889:ins=1_2989 on theBenchmark for (2989ds/889Mi)
% 47.03/7.35 % (3812173)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=1335631930:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2989 on theBenchmark for (2989ds/692Mi)
% 47.03/7.35 % (3812169)Instruction limit reached!
% 47.03/7.35 % (3812169)------------------------------
% 47.03/7.35 % (3812169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.03/7.35 % (3812169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.03/7.35 % (3812169)CaDiCaL version: 2.1.3
% 47.03/7.35 % (3812169)Termination reason: Instruction limit
% 47.03/7.35 % (3812169)Termination phase: Saturation
% 47.03/7.35 % (3812169)Time elapsed: 0.609 s
% 47.03/7.35 % (3812169)Peak memory usage: 40 MB
% 47.03/7.35 % (3812169)Instructions burned: 1179 (million)
% 47.03/7.35 % (3812176)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1118491856:i=879:kws=inv_precedence:fsr=off_2986 on theBenchmark for (2986ds/879Mi)
% 47.03/7.35 % (3812168)Instruction limit reached!
% 47.03/7.35 % (3812168)------------------------------
% 47.03/7.35 % (3812168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.03/7.35 % (3812168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/11.69 % (3812168)CaDiCaL version: 2.1.3
% 67.81/11.69 % (3812168)Termination reason: Instruction limit
% 67.81/11.69 % (3812168)Termination phase: Finite model building preprocessing
% 67.81/11.69 % (3812168)Time elapsed: 0.778 s
% 67.81/11.69 % (3812168)Peak memory usage: 30 MB
% 67.81/11.69 % (3812168)Instructions burned: 865 (million)
% 67.81/11.69 % (3812178)fmb+10_1_sil=64000:random_seed=3185421609:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 67.81/11.69 % (3812173)Instruction limit reached!
% 67.81/11.69 % (3812173)------------------------------
% 67.81/11.69 % (3812173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.81/11.69 % (3812173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/11.69 % (3812173)CaDiCaL version: 2.1.3
% 67.81/11.69 % (3812173)Termination reason: Instruction limit
% 67.81/11.69 % (3812173)Termination phase: Saturation
% 67.81/11.69 % (3812173)Time elapsed: 0.634 s
% 67.81/11.69 % (3812173)Peak memory usage: 30 MB
% 67.81/11.69 % (3812173)Instructions burned: 692 (million)
% 67.81/11.69 % (3812180)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=791600856:i=9515:nm=5_2982 on theBenchmark for (2982ds/9515Mi)
% 67.81/11.69 % (3812176)Instruction limit reached!
% 67.81/11.69 % (3812176)------------------------------
% 67.81/11.69 % (3812176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.81/11.69 % (3812176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/11.69 % (3812176)CaDiCaL version: 2.1.3
% 67.81/11.69 % (3812176)Termination reason: Instruction limit
% 67.81/11.69 % (3812176)Termination phase: Saturation
% 67.81/11.69 % (3812176)Time elapsed: 0.404 s
% 67.81/11.69 % (3812176)Peak memory usage: 33 MB
% 67.81/11.69 % (3812176)Instructions burned: 879 (million)
% 67.81/11.69 % (3812182)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1625330003:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 67.81/11.69 % (3812172)Instruction limit reached!
% 67.81/11.69 % (3812172)------------------------------
% 67.81/11.69 % (3812172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.81/11.69 % (3812172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/11.69 % (3812172)CaDiCaL version: 2.1.3
% 67.81/11.69 % (3812172)Termination reason: Instruction limit
% 67.81/11.69 % (3812172)Termination phase: Finite model building preprocessing
% 67.81/11.69 % (3812172)Time elapsed: 0.802 s
% 67.81/11.69 % (3812172)Peak memory usage: 30 MB
% 67.81/11.69 % (3812172)Instructions burned: 890 (million)
% 67.81/11.69 % (3812184)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=981458867:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 67.81/11.69 % (3812182)Instruction limit reached!
% 67.81/11.69 % (3812182)------------------------------
% 67.81/11.69 % (3812182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.81/11.69 % (3812182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/11.69 % (3812182)CaDiCaL version: 2.1.3
% 67.81/11.69 % (3812182)Termination reason: Instruction limit
% 67.81/11.69 % (3812182)Termination phase: Finite model building preprocessing
% 67.81/11.69 % (3812182)Time elapsed: 0.783 s
% 67.81/11.69 % (3812182)Peak memory usage: 30 MB
% 67.81/11.69 % (3812182)Instructions burned: 921 (million)
% 67.81/11.69 % (3812186)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1494618458:i=1472:ins=7:fdi=8:gsp=on_2973 on theBenchmark for (2973ds/1472Mi)
% 67.81/11.69 % (3812186)Instruction limit reached!
% 67.81/11.69 % (3812186)------------------------------
% 67.81/11.69 % (3812186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.81/11.69 % (3812186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/11.69 % (3812186)CaDiCaL version: 2.1.3
% 67.81/11.69 % (3812186)Termination reason: Instruction limit
% 67.81/11.69 % (3812186)Termination phase: Saturation
% 67.81/11.69 % (3812186)Time elapsed: 0.587 s
% 67.81/11.69 % (3812186)Peak memory usage: 28 MB
% 67.81/11.69 % (3812186)Instructions burned: 1473 (million)
% 67.81/11.69 % (3812188)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3445139299:i=6324_2967 on theBenchmark for (2967ds/6324Mi)
% 67.81/11.69 % (3812184)Instruction limit reached!
% 67.81/11.69 % (3812184)------------------------------
% 67.81/11.69 % (3812184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.81/11.69 % (3812184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/11.69 % (3812184)CaDiCaL version: 2.1.3
% 67.81/11.69 % (3812184)Termination reason: Instruction limit
% 57.95/15.58 % (3812184)Termination phase: Saturation
% 57.95/15.58 % (3812184)Time elapsed: 1.541 s
% 57.95/15.58 % (3812184)Peak memory usage: 110 MB
% 57.95/15.58 % (3812184)Instructions burned: 5133 (million)
% 57.95/15.58 % (3812190)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1476383372:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi)
% 57.95/15.58 % (3812190)Instruction limit reached!
% 57.95/15.58 % (3812190)------------------------------
% 57.95/15.58 % (3812190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812190)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812190)Termination reason: Instruction limit
% 57.95/15.58 % (3812190)Termination phase: Finite model building preprocessing
% 57.95/15.58 % (3812190)Time elapsed: 0.580 s
% 57.95/15.58 % (3812190)Peak memory usage: 50 MB
% 57.95/15.58 % (3812190)Instructions burned: 2175 (million)
% 57.95/15.58 % (3812192)ott-2_1_sil=16000:newcnf=on:random_seed=7517325:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2958 on theBenchmark for (2958ds/869Mi)
% 57.95/15.58 % TRYING [1]
% 57.95/15.58 % TRYING [2]
% 57.95/15.58 % TRYING [1]
% 57.95/15.58 % (3812192)Instruction limit reached!
% 57.95/15.58 % (3812192)------------------------------
% 57.95/15.58 % (3812192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812192)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812192)Termination reason: Instruction limit
% 57.95/15.58 % (3812192)Termination phase: Saturation
% 57.95/15.58 % (3812192)Time elapsed: 0.230 s
% 57.95/15.58 % (3812192)Peak memory usage: 29 MB
% 57.95/15.58 % (3812192)Instructions burned: 873 (million)
% 57.95/15.58 % (3812194)ott+10_1_sil=32000:tgt=ground:random_seed=3976346234:i=5114:av=off_2956 on theBenchmark for (2956ds/5114Mi)
% 57.95/15.58 % (3812180)Cannot represent all propositional literals internally
% 57.95/15.58 % (3812180)Refutation not found, incomplete strategy
% 57.95/15.58 % (3812180)------------------------------
% 57.95/15.58 % (3812180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812180)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812180)Termination reason: Refutation not found, incomplete strategy
% 57.95/15.58 % (3812180)Time elapsed: 2.788 s
% 57.95/15.58 % (3812180)Peak memory usage: 66 MB
% 57.95/15.58 % (3812180)Instructions burned: 4778 (million)
% 57.95/15.58 % (3812180)------------------------------
% 57.95/15.58 % (3812180)------------------------------
% 57.95/15.58 % (3812196)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1045611347:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 57.95/15.58 % (3812194)Instruction limit reached!
% 57.95/15.58 % (3812194)------------------------------
% 57.95/15.58 % (3812194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812194)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812194)Termination reason: Instruction limit
% 57.95/15.58 % (3812194)Termination phase: Saturation
% 57.95/15.58 % (3812194)Time elapsed: 1.536 s
% 57.95/15.58 % (3812194)Peak memory usage: 136 MB
% 57.95/15.58 % (3812194)Instructions burned: 5115 (million)
% 57.95/15.58 % (3812198)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1099724787:i=3512:aac=none_2940 on theBenchmark for (2940ds/3512Mi)
% 57.95/15.58 % (3812188)Cannot represent all propositional literals internally
% 57.95/15.58 % (3812188)Refutation not found, incomplete strategy
% 57.95/15.58 % (3812188)------------------------------
% 57.95/15.58 % (3812188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812188)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812188)Termination reason: Refutation not found, incomplete strategy
% 57.95/15.58 % (3812188)Time elapsed: 2.809 s
% 57.95/15.58 % (3812188)Peak memory usage: 75 MB
% 57.95/15.58 % (3812188)Instructions burned: 5350 (million)
% 57.95/15.58 % (3812188)------------------------------
% 57.95/15.58 % (3812188)------------------------------
% 57.95/15.58 % (3812200)dis+21_1_sil=32000:sas=cadical:random_seed=357300829:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 57.95/15.58 % (3812198)Instruction limit reached!
% 57.95/15.58 % (3812198)------------------------------
% 57.95/15.58 % (3812198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812198)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812198)Termination reason: Instruction limit
% 57.95/15.58 % (3812198)Termination phase: Saturation
% 57.95/15.58 % (3812198)Time elapsed: 0.993 s
% 57.95/15.58 % (3812198)Peak memory usage: 70 MB
% 57.95/15.58 % (3812198)Instructions burned: 3515 (million)
% 57.95/15.58 % (3812202)ott+11_1_sil=16000:gs=on:random_seed=2660078229:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2930 on theBenchmark for (2930ds/2251Mi)
% 57.95/15.58 % TRYING [1]
% 57.95/15.58 % TRYING [2]
% 57.95/15.58 % (3812202)Instruction limit reached!
% 57.95/15.58 % (3812202)------------------------------
% 57.95/15.58 % (3812202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812202)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812202)Termination reason: Instruction limit
% 57.95/15.58 % (3812202)Termination phase: Saturation
% 57.95/15.58 % (3812202)Time elapsed: 0.735 s
% 57.95/15.58 % (3812202)Peak memory usage: 58 MB
% 57.95/15.58 % (3812202)Instructions burned: 2251 (million)
% 57.95/15.58 % (3812204)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2337184453:fmbsr=1.6:i=67534_2923 on theBenchmark for (2923ds/67534Mi)
% 57.95/15.58 % TRYING [2]
% 57.95/15.58 % (3812200)Instruction limit reached!
% 57.95/15.58 % (3812200)------------------------------
% 57.95/15.58 % (3812200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812200)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812200)Termination reason: Instruction limit
% 57.95/15.58 % (3812200)Termination phase: Saturation
% 57.95/15.58 % (3812200)Time elapsed: 1.952 s
% 57.95/15.58 % (3812200)Peak memory usage: 95 MB
% 57.95/15.58 % (3812200)Instructions burned: 3775 (million)
% 57.95/15.58 % (3812206)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=531332611:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2918 on theBenchmark for (2918ds/4591Mi)
% 57.95/15.58 % (3812204)Cannot represent all propositional literals internally
% 57.95/15.58 % (3812204)Refutation not found, incomplete strategy
% 57.95/15.58 % (3812204)------------------------------
% 57.95/15.58 % (3812204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812204)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812204)Termination reason: Refutation not found, incomplete strategy
% 57.95/15.58 % (3812204)Time elapsed: 1.445 s
% 57.95/15.58 % (3812204)Peak memory usage: 66 MB
% 57.95/15.58 % (3812204)Instructions burned: 5356 (million)
% 57.95/15.58 % (3812204)------------------------------
% 57.95/15.58 % (3812204)------------------------------
% 57.95/15.58 % (3812208)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2230405497:i=29340_2908 on theBenchmark for (2908ds/29340Mi)
% 57.95/15.58 % (3812206)Instruction limit reached!
% 57.95/15.58 % (3812206)------------------------------
% 57.95/15.58 % (3812206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812206)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812206)Termination reason: Instruction limit
% 57.95/15.58 % (3812206)Termination phase: Saturation
% 57.95/15.58 % (3812206)Time elapsed: 1.581 s
% 57.95/15.58 % (3812206)Peak memory usage: 29 MB
% 57.95/15.58 % (3812206)Instructions burned: 4591 (million)
% 57.95/15.58 % (3812210)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1225087003:i=5211_2902 on theBenchmark for (2902ds/5211Mi)
% 57.95/15.58 % (3812178)Instruction limit reached!
% 57.95/15.58 % (3812178)------------------------------
% 57.95/15.58 % (3812178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812178)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812178)Termination reason: Instruction limit
% 57.95/15.58 % (3812178)Termination phase: Finite model building constraint generation
% 57.95/15.58 % (3812178)Time elapsed: 9.491 s
% 57.95/15.58 % (3812178)Peak memory usage: 1156 MB
% 57.95/15.58 % (3812178)Instructions burned: 22063 (million)
% 57.95/15.58 % (3812212)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1986286983:i=5497:nm=2_2887 on theBenchmark for (2887ds/5497Mi)
% 57.95/15.58 % (3812210)Instruction limit reached!
% 57.95/15.58 % (3812210)------------------------------
% 57.95/15.58 % (3812210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812210)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812210)Termination reason: Instruction limit
% 57.95/15.58 % (3812210)Termination phase: Saturation
% 57.95/15.58 % (3812210)Time elapsed: 1.611 s
% 57.95/15.58 % (3812210)Peak memory usage: 40 MB
% 57.95/15.58 % (3812210)Instructions burned: 5212 (million)
% 57.95/15.58 % (3812214)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=745062781:fmbsr=2:i=46332_2886 on theBenchmark for (2886ds/46332Mi)
% 57.95/15.58 % (3812214)Cannot represent all propositional literals internally
% 57.95/15.58 % (3812214)Refutation not found, incomplete strategy
% 57.95/15.58 % (3812214)------------------------------
% 57.95/15.58 % (3812214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812214)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812214)Termination reason: Refutation not found, incomplete strategy
% 57.95/15.58 % (3812214)Time elapsed: 1.490 s
% 57.95/15.58 % (3812214)Peak memory usage: 66 MB
% 57.95/15.58 % (3812214)Instructions burned: 5356 (million)
% 57.95/15.58 % (3812214)------------------------------
% 57.95/15.58 % (3812214)------------------------------
% 57.95/15.58 % (3812216)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=596986695:i=14071_2871 on theBenchmark for (2871ds/14071Mi)
% 57.95/15.58 % (3812212)Cannot represent all propositional literals internally
% 57.95/15.58 % (3812212)Refutation not found, incomplete strategy
% 57.95/15.58 % (3812212)------------------------------
% 57.95/15.58 % (3812212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812212)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812212)Termination reason: Refutation not found, incomplete strategy
% 57.95/15.58 % (3812212)Time elapsed: 2.335 s
% 57.95/15.58 % (3812212)Peak memory usage: 65 MB
% 57.95/15.58 % (3812212)Instructions burned: 4402 (million)
% 57.95/15.58 % (3812212)------------------------------
% 57.95/15.58 % (3812212)------------------------------
% 57.95/15.58 % (3812218)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2789779603:i=22565:add=on:rawr=on_2863 on theBenchmark for (2863ds/22565Mi)
% 57.95/15.58 % (3812216)Cannot represent all propositional literals internally
% 57.95/15.58 % (3812216)Refutation not found, incomplete strategy
% 57.95/15.58 % (3812216)------------------------------
% 57.95/15.58 % (3812216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812216)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812216)Termination reason: Refutation not found, incomplete strategy
% 57.95/15.58 % (3812216)Time elapsed: 1.422 s
% 57.95/15.58 % (3812216)Peak memory usage: 72 MB
% 57.95/15.58 % (3812216)Instructions burned: 5140 (million)
% 57.95/15.58 % (3812216)------------------------------
% 57.95/15.58 % (3812216)------------------------------
% 57.95/15.58 % (3812220)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=406141126:i=8173:av=off_2856 on theBenchmark for (2856ds/8173Mi)
% 57.95/15.58 % (3812145) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3812139-3812145"...
% 57.95/15.58 % (3812145)...printing done.
% 57.95/15.58 % (3812145)Refutation found. Thanks to Tanya!
% 57.95/15.58 % SZS status Theorem for theBenchmark
% 57.95/15.58 % SZS output start Proof for theBenchmark
% See solution above
% 57.95/15.58 % (3812145)------------------------------
% 57.95/15.58 % (3812145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.95/15.58 % (3812145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.95/15.58 % (3812145)CaDiCaL version: 2.1.3
% 57.95/15.58 % (3812145)Termination reason: Refutation
% 57.95/15.58 % (3812145)Time elapsed: 14.649 s
% 57.95/15.58 % (3812145)Peak memory usage: 231 MB
% 57.95/15.58 % (3812145)Instructions burned: 25168 (million)
% 57.95/15.58 % (3812139)Success in time 15.136 s
% 57.95/15.58 % Vampire exiting
%------------------------------------------------------------------------------